feat(registry): flux-verified name normalization + batch hardening - #32
Open
willemneal wants to merge 1 commit into
Open
feat(registry): flux-verified name normalization + batch hardening#32willemneal wants to merge 1 commit into
willemneal wants to merge 1 commit into
Conversation
Add the Flux refinement checker as a verification gate over the registry contract: 437/437 functions checked (including scerr/contracttrait macro-generated code). Normalized is now a flux-refined struct — the len <= MAX_NAME_LENGTH invariant lives on the type, so every slice/index of the 64-byte buffer is machine-checked. normalize() walks bytes instead of chars() (behavior-identical for the crates.io charset: every multi-byte UTF-8 byte fails is_ascii_alphanumeric exactly like its char did), dropping the unsafe as_bytes_mut and the deferred chars_to_change buffer. Two real hardenings out of the checker run: - NormalizedName::hash() sized its scratch buffer at 100 bytes for a 64-byte-max name: 65..=100-byte unnormalized names (only reachable via unsafe new_unchecked misuse) hashed silently, >100 sliced out of bounds. Now a 64-byte buffer behind an explicit assert. - process_batch's 'cursor + limit' could overflow u32 and trap on a caller-supplied limit near u32::MAX; now saturating_add (clamps to 'process to the end'), with #[opts(check_overflow = "strict")] discharging the remaining arithmetic. Batch iteration switches to index loops (soroban Vec iteration ICEs flux, projections.rs:720) — behaviorally identical. Gates: cargo flux green; clippy pedantic green; workspace tests green (44 registry tests); just build green. New just flux recipe. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01M52tZC7sppbbo1HDBpj9KK
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds the Flux refinement checker as a verification gate over the registry contract — 437/437 functions checked, including
scerr/contracttraitmacro-generated code.Refined type
Normalizednow carries its invariant in the type:#[refined_by(n: int)] #[invariant(n <= MAX_NAME_LENGTH)]— every slice/index of the 64-byte buffer is machine-checked.normalize()walks bytes instead ofchars()(behavior-identical for the crates.io charset: any byte of a multi-byte UTF-8 char failsis_ascii_alphanumericexactly like itscharcounterpart), which also drops theunsafe as_bytes_mutand the deferredchars_to_changebuffer.Real hardenings from the checker
NormalizedName::hash()used a 100-byte scratch buffer for a 64-byte-max name — 65..=100-byte unnormalized names (reachable only viaunsafe new_uncheckedmisuse) hashed silently; >100 sliced out of bounds. Now a right-sized 64-byte buffer behind an explicit assert.process_batch:cursor + limitcould overflow u32 and trap on a caller-suppliedlimitnearu32::MAX. Nowsaturating_add(clamps to "process to the end"), with#[opts(check_overflow = \"strict\")]discharging the remaining arithmetic.Notes
soroban_sdk_tools::scerr's generatedfrom_seqarithmetic can't be annotated; slice/index bounds are always checked regardless.Veciteration ICEs flux) — behaviorally identical.Gates
just fluxgreen (437 checked, ~290 ms) · clippy pedantic green · workspace tests green (44 registry tests) ·just buildgreen.🤖 Generated with Claude Code
https://claude.ai/code/session_01M52tZC7sppbbo1HDBpj9KK