Repository navigation
docs(core): eight more DSM core rows that cited removed code, re-verified - #1079
Merged
Merged
Conversation
…fied §6.44 listed nine MR-DSM rows citing items removed inside files that still exist. MR-DSM-0092 is #1078's. The other eight are re-verified against the specification and main. - Met: - 0034: `route_seats` writes leader first, then each later seat in route order, each copy carrying the chain so far. - 0083: the same; a write cut short after the leader is carried to finality by the next party. - Mutation: the writer carrying a no-response slot in place of the leader's link turns the root-registration and carried-release tests red. - Still Partial, with corrected citations: - 0002, 0004, 0005, 0014 and 0199: the receipt's state rules, the tip the receiver holds, adoption before a credit and the canonical apply are the checks now. The candidate, guard, Π and index structure remain absent. - 0068: both read paths re-hash; no test serves `fetch_verified` bytes that do not re-hash. - §6.48 records it, with a verification-matrix row and intent-manifest rows for 0034 and 0083. DSM core totals: 78 Met, 108 Partial, 39 Missing, 0 Violated.
…ting-removed-items # Conflicts: # specs/requirements/CONFORMANCE_GAPS.md
Pinned at 51741a7 against CI's code map of that commit (run 36775030983); its tree fingerprint equals this tree's. The rows are MR-DSM-0034 (route_seats::continue_write, from_leader, write_recorded) and MR-DSM-0083 (route_seats::continue_recorded_writes, from_leader, write_recorded). Their evidence passed in that run's Pin evidence log. MR-STOR-0116's two rows, stale on main since #1081, are repinned on main by #1080 and arrive with it.
…ting-removed-items # Conflicts: # specs/requirements/CONFORMANCE_GAPS.md
cryptskii
marked this pull request as ready for review
September 30, 2026 21:29
cryptskii
added a commit
that referenced
this pull request
Sep 30, 2026
Code-class only: rows whose closures reach recipient_dispatch.rs, storage_routes.rs and core_sdk.rs, including #1079's six route_seats rows for MR-DSM-0034 and 0083. Taken from CI's code map of 9db43e0, whose tree fingerprint equals this tree's; their 56 evidence tests ran and passed at that commit. make requirement-map-intent against that map reads 1,111 rows, 0 failing, and 598 pins, 0 failing.
cryptskii
added a commit
that referenced
this pull request
Sep 30, 2026
* fix(online): a receipt binds only when its state rules hold The online receiver bound a sender's receipt to its transfer on the child tip alone. It checked the signatures and that the child tip is the operation's successor, but never that the receipt's writes fold from its parent root to its child root. The BLE receiver checks this, and so does every producer before it signs. MR-DSM-0092's online order has it as "recompute hashes and roots". Probe (2026-09-30, on main after #1073, run on isolated node databases): a sender whose receipt claimed a child root one bit off what its writes produce was credited by the receiver. Binding now runs the one production verifier, verify_receipt_state, against the Device Tree root and genesis this device pinned for the sender: - holds: the pair binds, as before; - fails: the receipt is refused. It never binds, nothing is credited, and nothing negative is recorded; the sync reports it; - the sender's root is not pinned yet: the pair waits, staged and unbound, and binds on a later copy. Tests: - a_signed_receipt_whose_state_writes_fail_binds_nothing: three forgeries re-signed by the sender's real per-step EK, every signature valid. A child root the writes do not fold to, a write whose path is not its leaf's, and a write the operation does not imply are each refused, and the honest receipt still binds and credits once. - a_receipt_waits_while_its_senders_device_tree_root_is_not_pinned. Mutation controls: a failing state check that binds anyway, and an unpinned root that binds, each turned its test red. * test(online): the new tests' assertion messages are fixed text CodeQL flagged rust/cleartext-logging (alerts #733, #734) on the two assertion messages in a_signed_receipt_whose_state_writes_fail_binds_nothing and a_receipt_waits_while_its_senders_device_tree_root_is_not_pinned. They formatted `out.unbound`, whose reason text carries the sender's Base32 id, and a count of it still counted as tainted: the taint starts at load_cert_chain_head_pubkey, read while the receipt is recognized. Both messages are now fixed text. The assertions (`matches!` on `[Unbound::Refused(_)]` and `[Unbound::Pending(_)]`) are unchanged, and both tests pass. * chore(pins): repin the 64 rows #1078's change moves Code-class only: rows whose closures reach recipient_dispatch.rs, storage_routes.rs and core_sdk.rs, including #1079's six route_seats rows for MR-DSM-0034 and 0083. Taken from CI's code map of 9db43e0, whose tree fingerprint equals this tree's; their 56 evidence tests ran and passed at that commit. make requirement-map-intent against that map reads 1,111 rows, 0 failing, and 598 pins, 0 failing.
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.
§6.44 listed nine MR-DSM rows citing items removed inside files that
still exist. MR-DSM-0092 is #1078's. The other eight are re-verified
against the specification and main.
route_seatswrites leader first, then each later seat inroute order, each copy carrying the chain so far.
finality by the next party.
leader's link turns the root-registration and carried-release tests
red.
the receiver holds, adoption before a credit and the canonical apply
are the checks now. The candidate, guard, Π and index structure
remain absent.
fetch_verifiedbytesthat do not re-hash.
rows for 0034 and 0083. DSM core totals: 78 Met, 108 Partial, 39
Missing, 0 Violated.
Checks run
ci/conformance_evidence.pypasses.write_recordedmissing from the matrix row.Merge order. This goes after #1078 and #1075. §6.48 is provisional: it takes its final number when this branch is brought up to date, and its reference to §6.47 (#1078's section) resolves once #1078 is in. Its six manifest rows get pins from CI's code map at that point.