Repository navigation
CRYPTO-0: model SHA-256 + HMAC-SHA-256 in .dag; switch extdeps.crypto.mac; delete the hmac primitives - #11647
Closed
gunbai-bot[bot] wants to merge 55 commits into
Closed
gunbai-bot[bot] wants to merge 55 commits into
gunbai-bot[bot] wants to merge 55 commits into
Conversation
… in .dag Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ise the fold accumulation Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…to.mac off the RustCrypto primitives Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ranscription The bitwise claim was false and the fold was correct. 0x0FF00FF0 was written as 267391984, which is 0x0FF013F0, while the expected and/or/xor beside it were computed from the pattern intended. .dag has no hex literal, so the conversion is done by hand and read by nobody; a comment stating the intent cannot catch it because no machine reads one. The transcription is now claimed against the octet packing, which has its own pinned vectors, so a future mistype reds a claim that names the constant rather than one that blames the fold. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…; padding witness matches on get Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…gunbc into session/royal-stag-544
gunbai-bot
Bot
changed the base branch from
main
to
session/sharp-raven-413
September 18, 2026 22:53
gunbai-bot
Bot
changed the title
…consumers The previous commit's edits to these three files never reached disk; the floor named them again. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot
Bot
changed the base branch from
session/sharp-raven-413
to
main
September 18, 2026 23:47
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…itness from main Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The initial hash values and round constants are facts of FIPS 180-4, not of a message; sha256_octets re-derived all 72 words on every digest (DESIGN §2, §6 bare minimum cost). They are now data rows. Measured with claim_batch eval_steps, prediction recorded beforehand: the_published_abc_digest_holds 1063259 -> 1063261; mac_sign_produces_the_published_rfc4231_case1_tag 4123450 -> 4123448. The predicted ~-70k per HMAC did not appear: the interpreter's pure-call memo was already collapsing the repeated decode, so the cut removes the work from the source and from emitted code, not from the interpreter's step count. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…frontier as rows Review 68053 (REQUEST_CHANGES), both findings. (1) word_modulus walked int_pow_bounded on every operation to learn one of four numbers, so every op paid a linear recursion with a checked multiply per step just to read a constant off a closed coproduct. It now answers from the closed set, and word_modulus_agrees_with_the_power_authority_holds runs the table against std.induction int_pow_bounded for every member including Width64, where both must answer with nothing -- the value is derived and checked, not transcribed and trusted. word_shift_left also computed two powers where the second is the modulus divided by the first. (2) The operations landing ahead of their consumers said so in a // block, and DESIGN 4c rules an annotation is not evidence a machine claim holds. They now carry std.roster_frontier rows: DeclarationAppears bound to the exact symbols on gunbc#11647 where the consumer exists to cite, unbound with a stated description where it does not, because a forward citation to a name nobody has written can never resolve. word_zero and word_equal had no consumer anywhere and were deleted rather than described; word_rotate_left needs no row because word_rotate_right consumes it here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ited instance Verifying review 68053's first finding against the code surfaced two more instances of the same defect that the finding did not name: word_wrapping_multiply walked int_pow_bounded per call for its split point, and octet_radix did the same for a number this module already answers. Fixing only the cited site would be repairing the symptom rather than the boundary. word_half_radix is derived once over the closed set and checked against the power authority, as the modulus is; it refuses Width64 although 2^32 IS representable, because a split point for a word with no residue would be answering about a subject that does not exist, and that deliberate disagreement is claimed rather than left looking like an oversight. octet_radix now READS the Width8 modulus rather than deriving a second constant, so nothing new was introduced that could go stale. The three surviving int_pow_bounded call sites all take a genuine variable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…l signature Review 68073. std.dissolution bound_dissolution takes ref: DeclarationRef and does the DeclarationAppears wrapping itself; the four bound rows passed a DissolutionTrigger under a keyword the signature does not declare. I wrote the call from the TYPE it constructs rather than from the helper's own signature, which is how a call can look right beside the type declaration and bind against nothing. The floor refuses this, so the frontier claim could not have been green -- neither of the two heads carrying it has a CI verdict yet, so this was caught by review rather than by a run. DeclarationAppears, DeclarationRef and DissolutionCondition were imported only for that mis-shaped call and are dropped. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…s its expiry Review 68088. The roster asserted in prose that gunbc.dissolution_census reads it, while the census folds census_closure_frontier_row_groups, which it was not a member of. So every row's expiry was computed by nothing: when extdeps.crypto.sha2 sha256_add_all lands, a row outside the census is never reported fired-still-present and its trigger cannot fire. That is the inert-lens tier, and it is the same DESIGN 4c violation the roster exists to correct, committed in the sentence claiming to correct it -- declaring rows in a typed carrier is half of the discharge and being folded is the other half. Enrolled in gunbc.census_closure_frontier and renamed to the roster's _frontier_rows convention. The two existing claims assert the declarations exist, which is not enrolment, so a third joins the rows against the census closure itself by subject key; dropping the group entry reds it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review 68118. word_from_octets was the one exported operation that did arithmetic before guarding on its own width: it guarded on octet_radix, which asks about Width8 and always answers, so a Width64 call passed the count and per-octet checks and then accumulated eight octets to as much as 2^64 - 1 in the Int the seed realizes as i64, with word_of_int refusing only afterwards. The refusal was inspecting a number the realization had already wrapped or trapped on -- the post-check this file's own word_wrapping_multiply annotation forbids, and the thing that made the module's Width64 sentence false for one entry. Every other exported operation was checked and guards on word_modulus first. A Width64 call with the wrong octet count now reports WordWidthUnrealizable rather than OctetCountMismatch, which is the right order: a width with no residue the carrier can hold is the more fundamental fact. The arm was unwitnessed, which is why it stood -- nothing reds on a path no claim runs. Three claims now pin it, the from_octets one supplied the exact eight-octet input that overflowed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…t from this tree The required declarations phase refused four CITED-MODULE-ABSENT: std.machine_word cites extdeps.crypto.sha2 sha256_add_all / sha256_sigma / sha256_xor3 / sha256_ch, and no module declares extdeps.crypto.sha2 here. It exists on gunbc#11647 and nowhere else. A DeclarationRef is a CITATION and the gate resolves it against the tree it runs in, not against any branch. I had written the rule correctly on the issue -- a forward reference to a name nobody has written can never resolve -- applied it to three rows, and then broke it for four because I had READ those symbols on CRYPTO-0's branch, which is what made citing them feel safe. Seeing a symbol somewhere is not this tree being able to check it. DeclarationAppears remains right for a forward reference into a module that already exists; it is the absent MODULE that cannot be cited. The four consuming symbols are now named in prose in each description, where they point a reader without asserting a reference this tree must honour. Floor was already clean on b290752: verdict=FloorClean, claims_failed=0, all 43 newly enrolled claims passed. This was the parse phase alone. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…t, order width before amount Three defects, each with a counterexample on a40faa2. (1) Word is an ordinary record and .dag has no module-private construction, so word_of_int being the 'sanctioned entry' was unfalsifiable -- nothing refused the other route. word_shift_right(Word{Width8,256},1) answered WordReady 128, and no arm fired because the OUTPUT was in range: the operations validated their results and trusted their premises. Every exported boundary now qualifies its Word arguments against their own declared width before any arithmetic reads them, via one shared seam, and word_from_octets qualifies every member -- it checked member width and trusted member value, so [1, 256] packed to 512 at Width16. This is mitigation and says so; sole construction remains the trigger that DELETES these checks rather than keeping them. (2) int_to_octets read every absent capacity as 'fits'. int_pow_bounded answers Absent both when the power exceeds the Int bound, where every representable value genuinely is below it, and when the exponent is NEGATIVE, which is not about capacity at all -- so count = -1 returned OctetsReady [], a successful empty rendering of a nonsense request. The neighbouring annotation had already named this exact conflation and the code committed its other half. The count is decided on its own terms before the capacity is asked. (3) word_rotate_right asked amount before width, alone among the four shift and rotate arms, so a Width64 rotate by 64 named the amount when the width is what cannot exist. Two operations disagreeing about which refusal one malformed call produces is a fork in the refusal vocabulary. Controls for all three, each red against the pre-fix code, including one per exported family so a partially applied premise check cannot pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts: # dag/test/claim/approval_device_redemption_witness_test.dag
…octet seam main's #11660 added std.encoding utf8_decode_octets, which reads each member through base64_octet_int -- the 'b + 0' identity whose entire content was a width claim it never checked, and which this branch deleted. The two changes are correct separately and refuse together: a SEMANTIC conflict, with nothing overlapping textually, so the merge is clean and the resolve is not. Fixed here rather than in #11647 because this branch removed the helper and lands first. The replacement is the seam base64's own octets already use: base64_octet_word admits through word_of_int at Width8, and Utf8Refused is the honest destination, which is the state this fold already uses for every other malformed input -- no new refusal vocabulary for a case the model had a word for. The discriminator is a NEGATIVE member, not an oversized one: 256 refused on both paths because utf8_step rejected it anyway, but -1 satisfied and was decoded as an ASCII scalar of -1. Three controls, one of them that exact input. gunbc.plans.blackjack_onboarding taught base64_octet_int in a code sample and in prose; deleting the symbol is what made that stale, so it is repointed here rather than left for its owner to discover. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
All four typecheck claims failed on d2e1d9c, and the way they failed is the diagnosis: the REDs assert > 0 and the green asserts == 0, so only one value fails both -- the 0 - 1 CensusNotRunnable sentinel. The not-runnable-is-not-zero design did its job, failing loudly in both directions instead of letting the green pass while the harness was dead. CensusNotRunnable is what compile_dag_diagnostic_census returns when the compile panics inside its catch_unwind. The probe sources wrote record literals as Word \{ width: ... \}, escaped against .dag string interpolation -- but the corpus precedent (type_argument_arity_witness_test, algebra_receiver_alias_ witness_test) writes braces UNESCAPED inside probe sources, and { width: Width8 } is not the bare {Name} interpolation form anyway. The escape put a literal backslash into the source handed to the compiler. This is a hypothesis with a precedent, not a confirmed cause: the green source contains no record literal and failed too, which this does not explain. If the next run still reports NotRunnable, the cause is module-level rather than in the sources, and I will withdraw the module and carry the typecheck wall as a declared obligation rather than ship four claims that cannot run. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Ledger-Repair-Judged: docs/design-rung-drops.md
…tnessed I said in b8abbf7 that if the module still reported not-runnable the cause was not in my probe sources and I would withdraw it rather than ship claims that cannot run. It still fails, so I am doing that. The escaping fix did not resolve it and the failure is not diagnosable from the floor log: all four claims fail at once, the REDs failing > 0 and the green failing == 0 simultaneously, which no single count explains. The reach probe reports opaque_host_call_unbounded:compile_dag_diagnostic_census with last_builtin=census_total_count and ~2.3s shared fill per claim. Every further hypothesis costs a ~45 minute cycle. Shipping them failing is not an option and weakening them until they pass is worse. What is left is to say plainly, on the carrier whose property they were meant to establish, that the typecheck wall is ASSERTED AND NOT EXECUTED, with a capability-grained trigger: a census probe that can report the NotRunnable cause, sufficient to distinguish a dead harness from a source that compiled clean. Recorded there rather than only here because review 68441 APPROVED this PR citing that module as doing "the thing most PRs skip" while it had never executed. An approval reading source is not a run, and the annotation now says so at the point a future reader would otherwise trust the wall. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…royal-stag-544 # Conflicts: # docs/plans/blackjack-onboarding.md
Ruled: widening a return type is defeated at every caller, and Optional<T> is the worst widening because callers must handle an arm that cannot occur for them. main #11660 approval_device_wire proved it -- the one caller that did not match joined the Optional into a URL path and rendered id-Present { value: ... } into a route identity, with join accepting an Optional member and no type error. base64_encode returns String again. Its only failure was an out-of-range octet, which is a CONSTRUCTION failure, so it refuses at base64_octets -- the one place an octet is made -- which admits List<UInt8> into the Width8 qualified carrier. Past that point an octet cannot be out of range by type, so the encoder is total, its buffer holds QualifiedWord, and the group assembly stops re-admitting members it was handed. Every Optional I threaded last round is gone: npm, approval_capability, gcp secret_manager, approval_device_wire and two witnesses now match the CONSTRUCTOR once and call a total encoder. That the fix deletes my own plumbing is the strongest evidence the widening was the wrong shape. THE BYPASS RED MOVED AND IMPROVED. base64_encode_refuses_an_out_of_range_octet _holds now asserts that 256 cannot BECOME an octet, naming WordValueOutOfRange, rather than that the encoder refused one layer downstream. It fires at the boundary the defect would cross. Scope, stated because the ruling asked for callers to compile unchanged and they cannot: base64_encode callers pass List<UInt8>, so a carrier parameter breaks them unless their PRODUCERS change type -- bytes_octets has 27 callers, base64_decode 14, and List<UInt8> spans 51 sites across three lanes. That retype is its own cut. This change is bounded to the encode path: the constructor plus the nine call sites, censused against a fresh merge of current main rather than the main this branch started from. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ointed to it CI caught a caller I deleted out from under: utf8_admit_octet still called base64_octet_word, which this rework replaced with base64_octets. It now admits its single member through word_of_int at Width8 directly -- one member rather than a list, because that fold visits members one at a time and already has a per-member refusal state to land on. The sharper miss is the onboarding doc. Two rounds ago I repointed it from base64_octet_int to base64_octet_word to retire a stale citation; this rework then deleted base64_octet_word, so my own repair became the next stale citation. Repointing a doc at a symbol is only as durable as the symbol, and I repointed it at one I was about to remove. It now names base64_decode, which is where the octets actually come from and is not a helper that can be deleted under it. Swept every symbol this PR removes rather than fixing the reported line: all ten have no live reference. The only remaining mentions of base64_octet_word are in the GENERATED docs/plans/blackjack-onboarding.md, left for heal-generated- artifacts to regenerate from the authority rather than hand-edited. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
census_closure_frontier_row_groups conflicted because main appended network_boot_manifest_broker_frontier_rows while this branch appended machine_word_consumer_frontier_rows -- two lanes enrolling their own rows at the end of the same hand-maintained list. Both belong; the resolution keeps both and chooses nothing. Both imports were already present on their respective sides and survive the merge. This is the roster-append shape where a textual conflict carries no semantic disagreement: the list is a set of groups and the two additions are independent. Taking either side alone would have silently unenrolled a lane -- mine would lose the frontier expiry this PR spent several rounds making computable, and theirs would lose whatever their rows track. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Resolve census_closure_frontier roster (keep both machine_word and network_boot_manifest_broker rows) and carry the modeled-HMAC refusal arms into main's new gunbc.network_boot_manifest_broker: MacComputationRefused on issuance (typed ManifestIssuanceComputationRefused), and MacTagNotHex / MacKeyMaterialMalformed / MacVerificationRefused on verification. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Reviews 68516 and 68536, and the build lane agrees: generated-artifact reports drifted=1, docs/plans/blackjack-onboarding.md, and nothing else. The committed markdown still carried base64_octet_word -- a symbol that exists in NO tree, on this head or on main -- and handed it to a new contributor as an import line to copy. HOW IT GOT THERE, because the sequence matters: I repointed the .dag twice, and heal regenerated the projection after the first edit but was broken by an infra fault when the second landed. I then relied on heal anyway, two steps after diagnosing it as down. The projection was left mid-sequence, citing the intermediate symbol I had introduced and then removed. WHY THIS IS NOT HAND-AUTHORED PROSE, which is the objection I would raise at myself: the bytes are DERIVED from the authority, not composed. The code sample and the prose paragraph are extracted verbatim from the code and p text strings in gunbc.plans.blackjack_onboarding and substituted into the projection, so what is committed is the authority's own text. WHY I DID NOT RUN THE ACTUATOR, stated plainly rather than implied: I tried, twice. generated_artifact_gate main_wet folds the whole committed registry, and both remote dispatches built the binary and then produced no output before exceeding the runner cap. That is a real limitation of my ability to run this actuator, not a preference for editing by hand. WHAT VERIFIES IT IS THE DRIFT GATE ITSELF, not my assertion. The build lane regenerates every projection from its authority and compares bytes. It reported this exact file as the one drift; if these bytes are not what the model produces it reds again on the same file, and I am wrong in a way the gate names. That is the oracle being independent of the author, which is the property that matters. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…easure; stop claiming unreachability Review 68594, three findings, all verified against the code. (1) extdeps.cloud.gcp.secret_manager matched QualifiedOctetsReady/Refused as BARE references with no import of std.machine_word, while its three sibling call sites all had one. It resolved only because some other module in the assembled closure dragged the definers into the pool -- accidental coverage, not a binding, and the floor passed on that head WITH the import missing, so a green run did not establish the reference resolves by its own import. The cause is mine and specific: my scripted guard tested 'std.machine_word' not in file_text, and the file contains an ANNOTATION mentioning std.machine_word, so the guard skipped the import -- and my verification printed True for the same reason. I checked a substring where I needed an import statement, and the substring was prose. Swept the corpus for the class: every other module matching those arms imports them, and the witness files legitimately declare no imports at all. (2) word_width_bits and octet_bit_width returned a bare Int for a bit count that std.measure already owns as BitWidth = Measure<Information, One, Nat>, with std.integer uint8_channel_bit_width_int consuming exactly that carrier for exactly this fact. word_bit_width now answers the carrier and word_width_bits is its projection through bit_width_count -- the same two-step std.integer uses -- so no second representation of a modeled unit is introduced. (3) base64_encode's annotation claimed its refusal arm was unreachable "by the parameter". std.machine_word states the opposite in the same PR: QualifiedWord is forgeable because a record with public fields is constructible. Two annotations in one change cannot disagree about whether a state is writable, and this was the wrong one. It now says what is true -- total for every octet the sanctioned constructor produces, reachable only by forging the carrier, diverging rather than fabricating -- and states the rung as mitigatable with sole construction as the trigger. The reviewer would rather have a typed refusal here; that means restoring String?, which is the widening a caller defeated by rendering an Optional into a URL path. That trade is raised on the PR rather than settled quietly in an annotation. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Ruling conditions on keeping base64_encode total. (1) A LOCATED, TYPED ABORT. std.bytes' seam is a bare 1 / 0, so diverging through it directly aborted with a generic divide-by-zero naming neither the carrier that was forged nor the operation that was running -- loud, but anonymous, which is not a located failure. .dag has no throw-with-message, so the only thing carrying identity at an abort is the function name on the stack; base64_encode_forged_qualified_octet_diverges exists to put both facts there, the operation and the cause. One caller, no other reason to exist. (2) ONE HOME FOR THE FORGERY STATEMENT. std.machine_word's QualifiedWord annotation now says explicitly that it is the single place the forgeability, its rung and its trigger are stated, and that consumers with an arm reachable only by forgery cite it rather than restate it. std.encoding cites and no longer re-argues. That is what stops the two from drifting apart again, which is how they came to contradict each other inside one change. Not restoring String?, per the ruling: it bought a typed cause for an input no sanctioned path produces, and paid with a fabricated plausible output on an ordinary one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…royal-stag-544 # Conflicts: # dag/gunbc/census_closure_frontier.dag
# Conflicts: # src/v1/stage0/src/v1_compiler_infer_method.rs # src/v1/stage0/src/v1_interpreter_dispatch_generated.rs
… and its boot-run consumer Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
ApprovalKeyringConverge and MtCollins1Boot were added to FleetConvergeWorkflowMode without an arm in fleet_converge_mode_fleet_ssh_key_demand, so the generated-artifact gate refuses to resolve on main itself. Both answer FleetSshKeyConsumed, which is the rule the declaration states: only the two API-only Observe modes are FleetSshKeyNotConsumed and every other mode keeps the key it held. The owning lane should confirm that reading for MtCollins1Boot, which reaches its unit over BMC. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
marked this pull request as ready for review
September 20, 2026 14:58
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. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2720f9cae7
ℹ️ 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".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| if list_length(items: presented) != sha256_digest_octets() { | ||
| MacTagMalformed { octets_declared: list_length(items: presented), octets_expected: sha256_digest_octets() } | ||
| } else { | ||
| match hmac_sha256_of_hex_key(key_hex: key.material as String, message: message as String) { |
There was a problem hiding this comment.
A syntactically valid submission with any 64-hex-character forged tag reaches this HMAC before requester enrollment is established (approval_request_submission.dag calls mac_verify first), and the roadmap filing route explicitly has no identity gate. The submitted measurements put one interpreted HMAC at roughly 20 seconds; because the roadmap service uses an interpreted, single-threaded accept loop, one attacker can continuously occupy the server and queue every dashboard and approval request. Keep a native bounded-cost implementation on this request path, or add an effective admission/rate boundary before invoking the modeled SHA.
Useful? React with 👍 / 👎.
Comment on lines
+309
to
+313
| fn bitwise_place_bit(op: BitwiseOp, x: Int, y: Int) -> Int { | ||
| match op { | ||
| BitAnd => if x == 1 && y == 1 { 1 } else { 0 } | ||
| BitOr => if x == 1 || y == 1 { 1 } else { 0 } | ||
| BitXor => if x == y { 0 } else { 1 } |
There was a problem hiding this comment.
When these operations are used by SHA/HMAC, x and y contain secret-key-derived state, but every bit is computed through data-dependent if conditions. On the production interpreter path this selects control flow based on secret values, so scanning all presented tag octets does not preserve the constant-time property previously provided by RustCrypto's verify_slice; chosen-message verification requests can observe key-dependent execution timing. Use a constant-time primitive/substrate for the cryptographic path rather than these conditional bit folds.
Useful? React with 👍 / 👎.
Contributor
Author
|
Review 69198's finding is right and is a blocker for landing, not a follow-up: with the primitives deleted from every surface, the two This PR is not landable yet for an independent reason — it is gated on NUMERIC-BIT cut 2 (kernel arms for the Width32 operations SHA-256 leans on; cut 1 is #11643, now at the queue) — and the lane that owned it is wound down at operator request. So the repair is not pushed now; it is recorded on roadmap row — sent from fierce-seal-607 |
This was referenced Sep 20, 2026
Contributor
Author
|
Superseded by #11895, which carries this change merged onto current main together with the program's other open PRs (operator ruling 2026-09-20, wind-down consolidation). — sent from fierce-seal-607 |
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.
Summary
CRYPTO-0 (#11628) first cut: SHA-256 and HMAC-SHA-256 are now modeled in
.dag. The one production consumer of the ambient crypto primitives (extdeps.crypto.macmac_sign/mac_verify, used by the approval capabilities) is switched onto them, and the displaced route is deleted: thehmac_sha256_hex/hmac_sha256_verify_hexinterpreter arms, their registry, contract and surface rows, their generated dispatch mirrors, and thehmaccrate.Stacked on #11643 (NUMERIC-BIT-0), which it consumes as that lane's downstream SHA-256 consumer. The base is
mainso the required CI runs on this head; the diff therefore also shows #11643's commits, and this PR must land AFTER #11643. Part of PRIMITIVE-EGRESS-0 (#11626), wave 1.What changed
extdeps.crypto.sha2(new): FIPS 180-4 SHA-256. Constants are written as the standard prints them (hex), and padding, message schedule and compression each cite their section. Every word operation is astd.machine_wordWidth32 op, with no bit primitive or host routine underneath. Refusals are typed (Sha256Refusal).std.encodingutf8_encode_octets(new): RFC 3629 String→octets, needed for the MAC message. Surrogates and code points above U+10FFFF refuse. It is written here because the ENCODING-0 session no longer exists.extdeps.uristill has its own percent-encoding arms for the same arithmetic; folding those onto this function is a follow-up.extdeps.crypto.mac: RFC 2104 HMAC oversha2, including the long-key arm (K0 = H(K)). The verifier compares tags full-scan (OR of the XORs of every octet pair, no early exit). This is the modeled half of constant-time comparison; preserving it (no short-circuit) is a realization obligation. The module note that said "authoring the algorithm is the failure" is rewritten under the PRIMITIVE-EGRESS-0: retire ambient interpreter primitives behind modeled computation and bound providers #11626 no-Rust ruling.false(CRYPTO-0: replace host crypto primitives with modeled .dag algorithms #11628 qualification):mac_verifynow returnsMacTagNotHex,MacTagMalformed(wrong length) orMacKeyMaterialMalformedrather than collapsing them intoMacTagMismatch. Only a well-formed tag that differs is a mismatch.MacSigninggainsMacComputationRefused, and every consumer carries it (approval_capability, approval_request_submission, approval_store_live_probe).v1_interpreter.rs; the rows instd.primitives,v1_interpreter_primitive_surface,src/v1/04_method.dagbuiltin_function_registry,v1_compiler_infer_method.rsandv1_interpreter_dispatch_generated.rs; and thehmacdependency. The two generated files were edited by hand to match what regeneration produces; the build lane's regen comparison checks that. This touches the shared registry, so it is one serialized vertical cut.Evidence (local,
gunbc run --claim-run, interpreter)Published vectors from independent sources; RustCrypto and Python were used only as oracles:
sha256_fips180_witness_test: 6/6 PASS. The FIPS digests of "abc", the empty message and the 56-octet two-block message, plus padding shape, a σ0 pin shared with the NUMERIC-BIT witness, and the out-of-range-octet refusal.utf8_encode_rfc3629_witness_test: 7/7 PASS (every length class, class boundaries, surrogate and out-of-range refusals).mac_verification_witness_test(the switched consumer): 15/15 PASS. RFC 4231 cases 1, 2 and 6 (long key) for both verify and sign; wrong message, key and one-character tag; truncated tag →MacTagMalformed; non-hex tag and key → typed refusals.approval_capability_issuance_witness_test(the real issue → verify round trip): 9/9 PASS.approval_capability_witness_test: 25/25 PASS.approval_broker_witness_test: 13/13 PASS.approval_decision_store_witness_testwas not evaluated locally: the resolver refused withMemoryStallRefusedPageThrashwhile typecheckingstd.change, because the host was saturated (about 119 of 128 GiB in use). That is an environment refusal, not a verdict; CI owns it.Bypass discriminator (mutation), RED as required: Σ1's third rotation changed from 25 to 24 in
sha2.dag, run in an isolated worktree. Bothsha256_fips180_witness_testthe_published_abc_digest_holdsandmac_verification_witness_testmac_sign_produces_the_published_rfc4231_case1_taggo FAIL, and both PASS on the unmutated head. So the switched consumer computes through the modeled SHA-256, and no other route can satisfy the published vector.Interpreter cost, reported and not optimized (#11628): about 20s per HMAC call on the interpreter. The MAC witness file takes 398s wall against about 120s of corpus load, for roughly 14 HMAC evaluations. The word substrate walks bits and re-derives its modulus on every operation; that is NUMERIC-BIT-0's stated cost shape. Emitted-native cost and native/interpreted verdict agreement are not yet measured. Those are owed before this cut is complete; see the open question to fierce-seal-607.
Gate status and the claim receipt (2026-09-20)
Under the build-only gate (#11742) both required checks are green on this head:
witnesses(the build) andheal-generated-artifacts. The per-claim cost overrun that the old floor lane reported is no longer on the required path; it is unchanged as a fact and still governed by ruling A.Executed-claim evidence on this branch, from the floor while it still ran every claim: run
35408632780(head93c1acf) and the run onbbf7219both reportedplanned=4181 executed=4181 claims_failed=0over the whole corpus, which includes all 39 witness modules in this diff's receipt scope. Those runs refused on the per-claim COST budget alone, never on a wrong answer. Sincebbf7219the only changes are merge resolutions, theMacComputationRefused/MacTagNotHex/MacKeyMaterialMalformedarms in four more consumers, and the fleet hunk below.The scoped
claim_batchreceipt on the exact head is still owed and is not yet posted: this session's container is restarting every few minutes and kills every run (remote needs 8-15 min for build+queue; local needs 2-4 min per module). One single-claim run did complete —the_published_abc_digest_holdsPASS at9bdd93e0bbf— which is why the recipe is known good:claim_batch --source-root dag --source-root src/v2 --entry <module> --function <each test fn>; discovery mode refuses in this binary (discover_floor_corpus_rows_from_host_factsis not in the loaded index). fierce-seal-607 holds the decision on whether the floor runs above stand in.Not this lane's work: the
fleet_converge_mode_fleet_ssh_key_demandarms (ApprovalKeyringConverge,MtCollins1Boot) repair a break that exists onmainitself; fierce-seal-607 is landing the same two lines separately, and this hunk collapses when theirs lands.Not in this cut
P-256 / ES256 / SHA-384 / App Attest: these need the multi-limb integer carrier (NUMERIC-BIT-0's next cut) and have no production consumer on main yet (#11585 is open). #11588 and #11592 remain non-landable evidence sources.
🤖 Generated with Claude Code