Skip to content

fix: defined panic instead of UB when admin was never set; flux gate - #19

Open
willemneal wants to merge 4 commits into
mainfrom
feat/flux-verification
Open

fix: defined panic instead of UB when admin was never set; flux gate#19
willemneal wants to merge 4 commits into
mainfrom
feat/flux-verification

Conversation

@willemneal

@willemneal willemneal commented Aug 17, 2026

Copy link
Copy Markdown
Member

Out of the Flux verification sweep (see nidohq/soroban-flux):

  1. Safety invariant documented: Administratable::admin()'s default impl reads the admin with unwrap_unchecked — sound because every consuming contract calls set_admin from its constructor (whose first call skips the auth check for exactly this purpose), so the entry exists before any read. That requirement is now stated as a trait-level Safety invariant doc plus a SAFETY: comment on the unsafe block, since the trait is public API and future consumers must uphold it. (An earlier revision swapped in .expect(...); reverted per review — the constructor wiring makes the unchecked read sound.)

  2. Flux gate: [package.metadata.flux] enabled = true — metadata only, no dependency, inert for normal builds and crates.io. cargo flux -p admin-sep checks 19/19 functions (including #[contracttrait]-generated code) under flux 283ad73 / nightly-2026-02-05.

Gates: workspace tests green, clippy -D warnings green, flux green, fmt green.

🤖 Generated with Claude Code

https://claude.ai/code/session_01M52tZC7sppbbo1HDBpj9KK

willemneal and others added 3 commits August 5, 2026 11:57
The repo has a v0.1.0 git tag and GitHub release, but admin-sep@0.1.0
was never published to crates.io. release-plz refuses to proceed on
that mismatch. Bumping to 0.2.0 (correct anyway after the breaking
soroban-sdk v27 update) lets release-plz treat it as a first release.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Administratable::admin() used unsafe unwrap_unchecked on the storage
read — if no admin was ever set (constructor never called set_admin),
that is undefined behavior in wasm and could hand back a garbage
Address for require_admin to authorize against. Replace with
.expect("admin-sep: admin not set"): a defined, loud panic.

Also enable Flux refinement checking (metadata-only, no dependency —
inert for normal builds and crates.io): cargo flux -p admin-sep checks
19/19 functions including the contracttrait-generated code.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01M52tZC7sppbbo1HDBpj9KK
#[contracttrait]
pub trait Administratable {
fn admin(env: &Env) -> soroban_sdk::Address {
unsafe { admin_from_storage(env).unwrap_unchecked() }

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

set_admin is called in a contracts constructor so this is safe.

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed — with set_admin wired into every consuming contract's constructor (and its first call skipping the auth check for exactly that purpose), the entry always exists before a read, so the unchecked unwrap is sound in intended use. Reverted to unwrap_unchecked and moved the requirement into a trait-level Safety invariant doc + SAFETY: comment instead, so the obligation is stated where future consumers (the trait is public API) can see what they must uphold. Gates re-run: tests, clippy, cargo flux (19/19) all green.

…iant

Per review: set_admin runs in every consuming contract's constructor, so
the storage entry exists before any admin() read — the unsafe read is
sound in intended use. Keep it, and encode the requirement as a
trait-level safety invariant + SAFETY comment instead of a runtime check,
so future consumers know what they must uphold.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01M52tZC7sppbbo1HDBpj9KK
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant