[coderdan]

Closes #524. Stacked on #530.

What

packages/aead-frame/src/storage/proofs.rs adds 23 Kani harnesses about the storage reader, the code that parses bytes that may be corrupt or tampered with. Each property holds for every input within its bound.

Harness	Proves	Bound
the_header_is_refused_exactly_as_its_rules_say	body is refused as NotABlob exactly when rule 1 says, and as UnsupportedVersion exactly when rule 2 says; otherwise it returns the rest of the input itself	≤ 6 bytes
a_count_is_never_more_than_the_bytes_left	Cursor::count returns exactly the u32 at the cursor when it fits in the bytes left after it, and refuses otherwise	≤ 8 bytes, any position
reading_a_scalar_stays_in_bounds	Cursor::scalar never panics; it reads exactly buf[pos..new_pos], at least one byte, or refuses and leaves the cursor where it was; it accepts a plainly valid scalar (a null, a whole u8)	≤ 6 bytes, any position
reading_an_object_key_stays_in_bounds	Cursor::key never panics, and reads exactly the key the u32 length at the cursor and valid UTF-8 allow	≤ 6 bytes, any position
a_four_byte_object_key_is_read_exactly_when_it_is_utf8	a four-byte key is read exactly when its bytes are UTF-8, by an RFC 3629 checker written apart from the standard library	any 4 bytes
reading_a_map_key_admits_only_its_kinds	Cursor::map_key never panics, accepts only a tag STORAGE.md allows (written out, not the reader's list), read exactly at the cursor, and accepts a whole u8 key	≤ 6 bytes, any position
reading_a_wide_scalar_takes_exactly_its_width	i64, u64, f64, i128 and u128 are read whole exactly when the input holds them, and refused otherwise; the integers also as map keys, and f64 never	every length ≤ 17 bytes
the_depth_bound_is_128	MAX_DEPTH is 128; node past 128 refuses without reading a byte; at 128 a null still reads	concrete depths
a_some_passes_its_value_down_a_level, an_array_passes_its_elements_down_a_level, a_map_passes_its_values_down_a_level	each container holding a null at 128 is refused (the some and the array read at 127). An object is not provable in Kani: its repeat check's HashSet asks the OS for random bytes, which Kani can't model; the corpus's depth rows pin it	concrete
integer_keys_equal_by_value_from_* (10)	for every pair of integer widths and every value, two map keys have the same Identity exactly when their values are equal, where the value is worked out from the bytes without the leaf codec	every value
text_and_bytes_keys_equal_by_their_bytes	two text keys, or two bytes keys, are one key exactly when their bytes are equal	≤ 2 bytes each
keys_of_different_kinds_are_never_one_key	text, bytes and integer keys never share an Identity, even with the same bytes	≤ 2 bytes

cargo kani -p vitaminc-aead-frame --features serde -j 2 --output-format terse verifies all 23 in 607 s on an M-series Mac.

What isn't proved, and why

The issue's third harness, validate on any short body, did not solve in a usable time:

• With the real recursion, it ran over 20 minutes even for 3-byte bodies. Each level of nesting inlines another copy of node per recursive call site (array, object, map value, some), each with the leaf codec and the object's HashSet.
• A Kani function contract on node (#[kani::recursion], -Z function-contracts) removes the copies, but still didn't finish in 15 minutes for 4-byte bodies.

So, following protected's locked/proofs.rs, which documents a whole-path harness it couldn't solve, the proofs cover the pieces a body is read with. Whole bodies stay with the property tests (any_bytes_are_read_alike, a_corrupted_blob_is_read_alike), the Go fuzz target, and the Rust fuzzing follow-up. The module doc records this.

Production code only gains #[cfg(kani)] mod proofs;. The reader is unchanged.

CI

There's a new workflow, .github/workflows/kani-storage.yml ("📐 Kani (storage reader)"):

• It runs only when packages/aead-frame/src/**, the leaf codec (packages/aead/src/**), vitaminc-protected (packages/protected/src/**), those crates' manifests, the root Cargo.toml or Cargo.lock change.
• It runs -j 2 with timeout-minutes: 60.
• kani.yml (protected) is unchanged, so neither crate's change runs the other's proofs.

Also

• packages/aead-frame/Cargo.toml declares cfg(kani) for check-cfg in [lints.rust]; protected does the same in its build.rs.
• .cargo/mutants.toml excludes the proofs file, as for protected.
• .cargo-crap.toml excludes src/**/proofs.rs: Kani harnesses are built only under cfg(kani), so coverage always reads them as 0% and the pessimistic CRAP score flagged three of them. This also covers protected's locked/proofs.rs, which had passed only because its functions are simple. (61f5537)
• The README's Tests section lists each property and its bound.

Notes for review

• Concrete tags, lengths and depths. Several harnesses loop over these rather than leaving them symbolic. With a symbolic tag, CBMC encodes every path of the leaf codec: date, timestamp, and decimal with 128-bit arithmetic. With a symbolic length, UTF-8 validation runs over every length at once. Either way, a harness that now takes a minute or three ran past 15 or 20 minutes. Each harness's doc says what it fixes and why.
• Local runs. Kani 0.67.0 is the version CI pins. Locally the mise cargo-kani shim has no version set, so I ran the installed binary directly.
• Reviewed at high effort. The findings are addressed in 7e36f01 and 0d30e6b.

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-25T17:22:32.060677Z	f527d68	PR opened
🔒 Security Review	✅ Completed 2026-10-25T17:24:03.094033Z	f527d68	PR opened

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[github-actions]

🧬 Mutation testing (cargo-mutants, --in-diff)

No mutants were generated for the changed lines.

[coderdan]

Code review (high effort): 10 findings, most serious first. Each is inline.

The harnesses are correct for what they assert. The findings are places where they prove less than their docs, the README or the workflow comment say, plus CI trigger and runtime costs. I'll fix them on this branch before pushing.

[github-actions]

✅ No CRAP threshold violations

1496 function(s) analyzed · threshold 30

[freshtonic]

Comment only. I reviewed against #524. The header, count and integer-identity harnesses are correct, and the value oracle handles sign extension and the u128 > i128::MAX case. Dropping the whole-body validate harness is reasonable, given the solver times you found. I am not approving yet, because some harnesses claim properties that they do not prove (the first two items below). For a PR whose purpose is the proofs, I think we must fix that before merge.

Trigger paths. 09a2ab3 adds packages/aead-frame/src/**, which covers serde.rs and lib.rs. packages/protected/** is still not in the trigger, and --features serde compiles it into the code under proof (Protected, Zeroizing). Add packages/protected/src/** and packages/protected/Cargo.toml.

Some harnesses pass for an implementation that refuses everything.

• reading_an_object_key_stays_in_bounds, reading_a_map_key_admits_only_its_kinds and reading_a_scalar_stays_in_bounds assert only inside if let Ok. A key() or map_key() that always returned Err would pass all three. Add a check that a valid key or scalar is accepted.
• The key harness does not check that the key length equals the u32 at pos.
• The map-key harness asserts KEYS.contains(..), which is the check that map_key makes. Compare against a tag list taken from STORAGE.md. Also, assert that f64 is refused as a key in the wide-scalar harness.

Depth. Only the some call site is shown to pass depth + 1. If the array, object or map site passed depth, recursion would have no bound and every harness would still pass. Concrete checks, each with a container at depth 128 that holds a null and is refused, would close this cheaply. Also, the_depth_bound_is_128 never asserts MAX_DEPTH == 128, so a change to frame::MAX_DEPTH would leave a proof whose name is wrong.

Smaller items

• With a 6-byte bound and a 4-byte length, text has at most 2 payload bytes. So rule 6 (UTF-8) is not checked on 3- and 4-byte sequences. Say so in the doc, or give one harness a larger concrete length.
• About 60 lines of kani-storage.yml copy kani.yml, including the KANI_VERSION pin and the cache key. So a Kani version bump needs edits in two files, and the two workflows share one cache.
• cfg(kani) is declared in [lints.rust], but protected uses build.rs. Both are fine, but the PR description says it follows protected.
• Use HEADER.len() in place of the bare 4 in the header harness.

[coderdan]

Thanks, James. These are fixed in b29eb3e and d57c5db:

• Trigger paths: kani-storage.yml now also runs on packages/protected/src/** and packages/protected/Cargo.toml.
• Harnesses that passed for a reader that refuses everything:
  • The scalar and map-key harnesses now also require a plainly valid input (a null, or a whole u8) to be accepted.
  • The object-key harness now requires exactly the key that the u32 length at pos and valid UTF-8 allow, so it also checks the key's length.
• Key tags: the map-key harness checks the tag against the tags STORAGE.md's table allows, written out, not KEYS. The wide-scalar harness requires f64 to be refused as a key.
• Depth:
  • MAX_DEPTH == 128 is asserted.
  • New harnesses show that a some, an array and a map at 128 holding a null are refused, so each passes its children down a level. The some and the array also read at 127.
  • A map's read at 127 is left to depth_128_maps: once the value reads, the map checks its keys for a repeat, and that ran past ten minutes.
  • An object can't be proved in Kani. Its repeat check uses a HashSet, whose hasher asks the OS for random bytes (CCRandomGenerateBytes locally), and Kani can't model that. The corpus's depth_128_objects and depth_129_objects rows pin its depth, and the module doc says so.
• UTF-8: a new harness checks a four-byte key, any four bytes, against an RFC 3629 checker written separately from the standard library's. It is read exactly when the bytes are UTF-8.
• HEADER.len(): now used in place of the bare 4.
• cfg(kani): you're right, protected declares it in build.rs and this crate in [lints.rust]. I've corrected the PR description.
• Duplicated workflows: in the cleanup PR on top of fix(aead-frame)!: wipe the copies the zeroize audit found, and record the ones it accepts #532, as a shared setup step with one KANI_VERSION pin.

All 23 harnesses verify locally in 607 s, two at a time.

[coderdan]

The cleanup PR mentioned above is #540, on top of #532. It covers the shared reserve, the storage tag names, the Go writer's single list of model types and the reader tidy-ups, the append-only check for every corpus version, and one shared Kani setup.