Repository navigation
test(aead-frame): land the storage corpus coverage and Kani proofs on main - #557
Merged
Merged
Conversation
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
Contributor
🧬 Mutation testing (cargo-mutants,
|
Contributor
✅ No CRAP threshold violations1496 function(s) analyzed · threshold 30 |
… keys in the storage corpus
…ad a denying struct in Go where it reads
…ts own reason, against the specification's exact text
…tag, and Options of null-written types reading null as None
Appends a vector with an integer, a text and a bytes key of the same byte, a refused map key starting with a byte that is no tag, and reads rows for Option<UnitStruct> and Option<Option<u8>> reading null as None. The corpus type language gains {"unit_struct": name}. Go skips a deny-unknown row only when its own type denies unknown keys, not when the word appears in a nested type. Raised in review on #530.
Claude-Session: https://claude.ai/code/session_01EnoQSYdggmUYkqNyahDchE
… check what a clause's row reads as Rule 8's 'text and bytes never equal each other or an integer' and a read at exactly depth 128 now need a vector that shows them. A map key starting with a refused tag or a byte that is no tag needs a refused row. The reading paragraph of Map keys is pinned with its clauses. The Option clauses and the missing-Option-field clause check that the row reads as None, not just its shape, and the unit-struct case is its own clause. The reference reader's Broken variants take small enums rather than bools, and a row's type is parsed once. Raised in review on #530. Claude-Session: https://claude.ai/code/session_01EnoQSYdggmUYkqNyahDchE
…ay in bounds and keys compare as specified
…epth bound from both sides, wide scalars and same-kind keys
…t it compiles from, two harnesses at a time
… transport changes serde.rs defines the storage profile's SOME and MAP tags and builds body()'s errors, both of which the harnesses check, so kani-storage.yml now triggers on all of packages/aead-frame/src. The mutants exclusion's comment names both Kani workflows. Raised in review on #531. Claude-Session: https://claude.ai/code/session_01EnoQSYdggmUYkqNyahDchE
…ses everything, and prove each container's depth Raised in review on #531: - The scalar, object-key and map-key harnesses now also require a plainly valid input to be accepted, so a reader that refused everything would fail them. The key harness requires exactly the key the u32 length and UTF-8 allow. - A four-byte key is checked against RFC 3629's table, written apart from the standard library, to cover three- and four-byte sequences. - The map-key harness checks the key's tag against the tags STORAGE.md allows, written out, rather than the reader's own list. The wide-scalar harness requires a float to be refused as a key. - MAX_DEPTH is asserted to be 128. A some, an array and a map at 128 holding a null are refused, so each passes its children down a level. An object's hash set asks the OS for random bytes, which Kani cannot model, so the corpus pins its depth. - The header harness uses HEADER.len() rather than a bare 4. Claude-Session: https://claude.ai/code/session_01EnoQSYdggmUYkqNyahDchE
The serde feature compiles Protected and Zeroizing into the code under proof. Raised in review on #531. Claude-Session: https://claude.ai/code/session_01EnoQSYdggmUYkqNyahDchE
coderdan
force-pushed
the
feat/storage-corpus-coverage
branch
from
October 27, 2026 02:24
f1b2abc to
95a8a71
Compare
cipherstash-bot
left a comment
cipherstash-bot
left a comment
There was a problem hiding this comment.
Recommendation: 🟢 merge as it is (3 of 6 review job(s) failed)
Nothing must change before merging. This PR adds tests, Kani proofs and CI; the only shipped-code change is #[cfg(kani)] mod proofs;. Two optional test-strength items can wait for a follow-up. No Rust, cargo or Go tools were run in review; the findings come from reading the code.
How this review was made
| Agent | Model | Review type | Result |
|---|---|---|---|
| claude | claude-opus-5-5 | test-gap | 1 found, 1 posted |
| claude | claude-opus-5-5 | rust | 0 found, 0 posted |
| claude | claude-opus-5-5 | golang | 1 found, 1 posted |
| codex | gpt-5.6-terra | test-gap | failed |
| codex | gpt-5.6-terra | rust | failed |
| codex | gpt-5.6-terra | golang | failed |
Synthesis: claude-sonnet-5-5 merged the findings, removed duplicates and dropped findings it could not confirm in the code. 0 posted finding(s) were raised by two or more models.
Plain language: claude-sonnet-5-5 read every comment as a new reader would. No comment had a problem that stopped the reader acting, so none was rewritten.
Stack: position 1 of 3 (#532, #534, *️⃣ #557). *️⃣ marks this pull request.
Context loaded: the description, 2 linked issue(s) and 3 discussion entries.
… hand-made blobs, since the coverage test trusts that answer
…o a row of that type refused for another reason is still checked
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
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.
This brings #530 and #531 to main. Both were reviewed and merged, but each merged into its stacked base after that base had already merged, so their commits never reached main:
feat/aead-frame-storage-profileat 03:08:55, and that branch reached main through Feat/aead frame storage profile #544.feat/vcffi-storage-profile) 15 seconds later, at 03:09:10.feat/storage-corpus-coverage) at 03:09:36.This branch is
feat/storage-corpus-coverageas it stood after #531 merged. It has no new changes. It merges into main without conflicts.What it adds
tests/storage_coverage.rs, which fails when the storage corpus has no row for some part of version 1, and nine new corpus rows. Closes Check that the storage corpus covers every rule of version 1 #522.packages/aead-frame/src/storage/proofs.rs, and the "📐 Kani (storage reader)" workflow that runs them. Closes Prove the storage reader never panics on bounded input with Kani #524.See #530 and #531 for the full descriptions and review.
#532 is stacked on this PR, and #534 on #532. Merge this first.