The approval app's crypto in .dag: bitwise, bignat, SHA-256, P-256 (blocked on MachineWidth reflection)

[gunbai-bot]

The approval app's crypto, authored in .dag and intended to run compiled. Draft: blocked on compile-time reflection of MachineWidth<N>, dispatched as its own lane.

What this carries

Eight files, nothing else:

• std.bitwise — bitwise operations over bounded naturals, emulated arithmetically. Conjunction from a derived nibble table; xor and or follow from it.
• std.bignat — multi-limb unsigned naturals, 24-bit limbs (a limb product is below 2^48, and 24 bits is exactly three octets), Montgomery CIOS, Fermat inverse.
• extdeps.crypto.sha2 — SHA-256, FIPS 180-4.
• extdeps.crypto.nist_p256 — P-256 (SP 800-186) and ECDSA verify (FIPS 186-5 §6.4.2), Jacobian arithmetic with Shamir's trick.
• std.bounded_nat — the declared operation family for bounded naturals, over a supplied width: a three-arm width admission, a sole-constructed carrier whose range admission is its only mint, checked arithmetic with typed outcomes, and add_mod / mul_mod as the named wrapping arm. It is what std.operator_realization's refusal points at. The UInt32 / UInt8 bindings are not here: they need the width reified from the declaration.
• Three witness modules: the FIPS 180-2 SHA-256 vectors and the bitwise identities; RFC 6979 §A.2.5 and Wycheproof P-256 vectors.

Evidence so far

• sha256_fips_witness_test: 7/7 interpreted. The round constants and initial hash values were checked against a derivation from the primes, not transcribed on trust.
• P-256: the RFC 6979 'sample' verify answers correctly, 226,455 ms interpreted. The 12-witness file HAS NEVER COMPLETED A RUN -- three attempts now, the third on 2026-09-20 through a verified-provenance binary, all killed by container restarts (the third died after 53 bytes of output, at host slice pressure of 80 of 88 GiB across 41 containers). I am not retrying it further, and the reason is structural rather than bad luck: at the measured interpreted verify cost the suite needs roughly 30-45 minutes uninterrupted, which is longer than this container's restart interval under load. That cost is not a separate mystery -- it IS the Milestone-1 feasibility finding already reported, since the gate was 'a few seconds' per verify. What would run them: the same driver on a host that stays up for the length of the run, or a CI lane, neither of which exists for witnesses today.
• SHA-256 of 1 KiB: 2,724 ms interpreted, digest correct.
• bounded_nat_witness_test: 8 of 8 pass, executed 2026-09-20. Run as gunbc run over a driver that tags each failing witness by name, against a gunbc I built from this exact tree (8b7792a) into a per-session target dir. Positive arm: exit 0, empty output, 109s. Negative control, because exit 0 with empty output is also what a broken driver returns: inverting one witness with ! gives exit 1 and prints a_value_inside_the_width_mints_and_one_outside_it_does_not. So RED is reachable and the green is readable.
• Instrument provenance matters here and is not incidental. An earlier run of the same driver through the SHARED /cargo-target/release/gunbc failed in std.keyed_row / std.keyed_roster — files this branch does not touch. That binary is not the seed: it carries another lane's unlanded kinding check (verified by a string the seed does not contain; my build has 0 occurrences, it has 1). The failure was a fact about the instrument, not the corpus, and it is reported to that lane. Per-session target dirs are why the result above is trustworthy.
• Still not run by any required lane — not because CI runs no claims (it does again, since Add the fleet lane the hosted gate cannot carry: fold, drift gate, repair #11791), but because this witness is not in the floor's prefix roster. See below.
• Not re-verified against current main. Local .dag execution is currently unusable in my container: a module importing only std.process takes 19 minutes to run on this main, against about 110 seconds for the same shape earlier the same day. That is a discriminating control — it contains none of this PR's code — and it holds with a gunbc rebuilt from this exact tree, so it is neither these modules nor a stale binary. The figures above are therefore from the pre-merge tree; and CI does not check them either, for the reason stated above.

Why it is blocked

Emitting this closure to native Rust is refused at 18 sites: arithmetic on std.integer's bounded naturals has no host realization (UInt32, UInt8). The approved repair is one bounded-natural operation family in std.integer, derived once over N, with checked arithmetic and explicitly-named wrapping. That needs the N of MachineWidth<N> readable in a body, which the operator ruled on 2026-09-20 as compile-time static reflection. That compiler work is a separate lane; this PR waits for it, then converts every infix site here.

Two failure modes found on the way landed separately in #11702.

🤖 Generated with Claude Code

What this PR is, and what it is not

In scope: the six .dag crypto modules and std.bounded_nat. None of them names a width, and each stands on its own.

Explicitly OUT of scope: the 18 infix conversion sites, and the interpreted-vs-native equal-answer witnesses. Their trigger is the compile-time reification of the N in MachineWidth<N> (operator ruling, 2026-09-20), which is a separate lane. So if you are wondering why the operation family has no callers yet: its binding layer is a declared frontier with a named trigger, not an oversight. std.bounded_nat takes its width as a supplied value until that lands.

Re-running the witnesses, since nothing else will

CORRECTED 2026-09-20 — I was wrong about this, in the pessimistic direction. I checked v2.workflow.required_floor required_gate_prefixes, found no match for these modules, and concluded CI never runs them. That reads ONE selector and concludes about the whole lane. The floor job ALSO selects by changed enclosing declaration, and it reaches them: floor run 35505867616 on d3de6681685 planned 35 of this PR's witnesses as planned_as_changed_witness and executed 27 of them.

module	planned	passed	note
bounded_nat_witness_test	10	10	standing=admitted, 0–2 ms each
bignat_montgomery_witness_test	6	6
sha256_fips_witness_test	7	7
p256_dag_ecdsa_witness_test	12	4	8 did not reach a verdict — see below

So a green check on this PR does mean 27 of these witnesses ran, in a required lane. That is stronger evidence than this body previously claimed. To reproduce locally:

CARGO_TARGET_DIR=/cargo-target/<your-session-id> cargo build --release -p v1-compiler --bin gunbc
/cargo-target/<your-session-id>/release/gunbc run \
  --source-root dag --source-root src/v2 --source-root .scratch \
  --entry .scratch/scratch_bn_driver.dag --function main

The driver ANDs the eight test fns and prints the name of each one that fails, so exit 0 with empty output is a pass and exit 1 names the failure. Build with a PER-SESSION target dir: the shared /cargo-target/release/gunbc is whatever another session built last, and may not be the seed.

Review response: the host-width rule was over-prohibiting, and is fixed

The reviewer asked whether host-width safeguards reject valid operands. For the wrapping product they did, and that is now fixed in 95004fb. Answering the concrete case from the code:

1. Before: bounded_nat_product_admitted was 2N <= 62, shared by both multiplications, so UInt32 refused with ProductExceedsHostInt in bounded_nat_mul and bounded_nat_mul_mod. Only the checked arm needed that: detecting overflow requires the whole product to exist; reduction mod 2^N needs only the low N bits.
2. Was any consumer affected? No, and that is a boundary rather than a gap. extdeps.crypto.sha2 is additive — its only * are raw Int byte-packing (word * 256, 8 * (i - 1)) — and extdeps.crypto.nist_p256 routes all field multiplication through std.bignat Montgomery arithmetic (52 references; zero uses of UInt32 or std.bounded_nat). So nothing in this PR needed the refused operation.
3. Fixed anyway, because an unreached over-prohibition still costs the next consumer. Splitting one operand at h = N / 2 computes the low N bits without forming the product. UInt32 wrapping multiplication now succeeds; UInt32 checked multiplication still refuses, correctly.

The new ceiling is stated, not rounded. The split admits N <= 41 — not every width the carrier admits — and 42..62 still refuse as a property of the naive host realization, with a next-rung trigger naming the capability (bignat routing or a recursive split). The pre-existing bounded_nat_width_ceiling_trigger is a different ceiling (magnitudes exceeding the host Int, i.e. UInt64/UInt128), where bignat genuinely is required; it is unchanged and still correct.

Evidence: 10/10 witnesses pass (exit 0), and each new witness was re-run inverted to show its red is reachable (exit 1, naming both). Both new vectors have 64-bit full products, so neither answer is reachable by forming the product on this host — the split is doing the work. The ceiling is asserted at its 41/42 edge so a later widening is reported rather than absorbed.

Review round 2: what is closed, and what is explicitly NOT

The boundary was wrong and is fixed (42/43, not 41/42). The split's admission compared its bit demand against bounded_nat_host_bit_ceiling() = 62 — the widest carrier this family admits — when the relevant limit is the host's positive capacity, 63. Two unrelated limits behind one constant: the same defect this branch had just removed one level up. Width 42's worst intermediate is 9223367638806167553 against an i64 max of 9223372036854775807; 43 is the first that genuinely does not fit.

The witness had canonized that off-by-one — it asserted a refusal at width 42 for 3 × 5, product 15. It now asserts the admitted edge with near-maximal operands, (2^42 − 1)² mod 2^42 = 1, an answer unobtainable by forming the true 84-bit product.

Checked multiplication consumes std.checked_arithmetic rather than re-deriving it: that module already owns "PRE-CHECK, NEVER POST-CHECK" and the division-based bound test. Only the bound is local here (the carrier's 2^N − 1, not the host range).

The refusal arm was renamed from ProductExceedsHostInt, which stated a falsehood — at width 43, 3 × 5 is 15 and nothing exceeds anything — to WrappingProductUnavailableAtWidth, with a trigger naming both sufficient routes (recursive splitting or std.bignat).

std.bignat: fabrication closed, invariant admission NOT closed

BigNat and MontgomeryModulus are now sole_constructor. Every overflow argument in that module rests on each limb lying in [0, 2^24), yet as plain records any caller could write BigNat { limbs: [-5, 99999999] } and the arithmetic would compute on it.

This is a partial close and must not be read as a full one. sole_constructor restricts who may construct, not what may be constructed. montgomery_modulus still derives its fields from unchecked arguments, so an even modulus, zero modulus, or negative width remains constructible inside the module. The next-rung trigger names the capability (a refusing admission establishing each invariant) and is deferred because making it refusing turns p256_field/p256_order into refusable data rows, cascading through every consumer of the field arithmetic — and the P-256 suite has never executed, so that restructuring cannot yet be read for breakage.

Paired witness: 5 small-modulus claims exercise the real producers (Montgomery round trip, a multiplication that must reduce — 20 × 30 = 600 = 6 × 97 + 18 — additive wrap, zero). 5/5 pass: the first executed evidence std.bignat has ever had. Control: setting bignat_base to 2^24 − 1 turns three of the five red by name; the other two do not depend on the base under that perturbation and are not credited with discrimination they lack.

Review round 3 (69054): the failure mode closed at its own site — one half of it

std.bitwise is new in this PR, and it was landing fresh population of a class already filed on main: word32_xor was a + b - 2 * word32_and(...), whose sum reaches 2^33 − 2 while typed UInt32. The failure-mode row cites that line verbatim, DESIGN §4b puts the class below the ladder, and no drop was declared. The finding was correct.

Fixed by removing the oversized intermediate, not by declaring it. Exclusive or is nibble-wise through a derived table (as word32_and already was); disjunction is xor + and, which are disjoint bit sets, so their sum is the disjunction and is bounded by it; addition decides the carry before forming the sum. Verified at the edges and over 60,000 random pairs against the reference operations — zero mismatches, largest xor intermediate 4294960992, inside 2^32. SHA-256 still 7/7, bounded_nat 10/10.

This closes ONE of two classes and must not be read as both. The invalid state bounded_natural_arithmetic_evaluated_as_unbounded_int names — "a value typed UInt32 that is not a 32-bit unsigned natural" — is now unreachable in std.bitwise. But std.operator_realization refuses infix arithmetic on a structural operand regardless of magnitude, so these sites still emit as operator refusals: the separate class accepted_source_emits_uncompilable_target. In-range values do not make infix emittable.

The consumer frontier's trigger was stated at the wrong grain and is corrected. It said this family waits on reification. It does not — the operations take a width as a value, and the witnesses pass bit_width(count: 32) today. The real blocker is an import cycle: std.bounded_nat imports std.bitwise for bitwise_pow2, so bitwise cannot import back (DESIGN §3, acyclicity). Breakable by relocating bitwise_pow2. The second cost is named beside it: threading a six-arm BoundedNatArith through SHA-256's 64-round fold. Deferred to its own change with the P-256 suite as its gate, in that order.

Also removed: bounded_nat_width_ceiling_trigger, a String prose row with no reader (DESIGN §4c dead data).

Review round 4 (69076): the repair had skipped its own 64-bit half

word64_add was let lo = a.lo + b.lo over two UInt32 halves — the same population the note added in the previous commit says word32_xor/word32_or/word32_add were rewritten to leave. The repair was applied to the 32-bit family and skipped for the 64-bit one in the same diff, while writing the explanation of why it was needed. Live, not latent: sha256_fips_witness_test drives lo to exactly 2^32 on every run.

Fixed by reusing the already-corrected word32_add rather than repeating its reasoning — the carry is decided before either sum is formed, and both halves go through word32_add instead of a raw %.

The rest of the file was scanned, not just the site named, since "applied here, skipped there" was the defect. Six remaining arithmetic sites over UInt32 halves are all sums of disjoint bit ranges; measured over 80,000 random inputs the largest intermediate is 4294964487, inside 2^32. word64_add was the only defect.

Control is discriminating, not a formality: replacing the carry with a constant 0 reds word64_add_carries_across_the_halves_and_rotr_swaps_them by name. SHA-256 7/7 with the fix; the implementation also checked against 64-bit modular addition over 80,000 pairs plus edges — zero mismatches.

P-256: what was obtained, and a §4b(3) drop for what is UNKNOWN

What this PR is: substrate acceptance with an explicit evidence gap. It is not security sign-off.
It does NOT state, and must not be read to imply, that the full P-256 verifier is verified, that the
ES256 security argument holds, or that the production device-signature path has been verified. The
binding from the app into the verifier is not exercised here at all and is a separately named
frontier (gunbc.auth.approval_device_redemption ecdsa_verification_realization_frontier).

EVIDENCE OBTAINED — and its exact extent

Two things, and nothing wider:

1. the four cheap claims that refuse before any curve math (a_point_off_the_curve_is_absent,
   wycheproof_2_r_plus_n_is_absent, wycheproof_11_r_and_s_zero_are_absent,
   wycheproof_26_r_equal_to_n_is_absent);
2. the standalone accept/reject pair below.

run	vector	wall	exit
accept	RFC 6979 §A.2.5 sample (P-256/SHA-256)	192 s	0 — returns true
reject	the same vector, first octet of r flipped 239 → 238	205 s	1 — returns false
accept	RFC 6979 §A.2.5 test	734 s	0 — returns true

What that establishes is bounded: the verifier accepts two published vectors and rejects a one-bit
perturbation of one of them. Before it, every executed P-256 witness was an is_absent case, all of
which a verifier returning Absent unconditionally would pass. It does not establish the verifier.

THE EIGHT VERIFICATION-PERFORMING CLAIMS ARE UNKNOWN, NOT PASSING

Stated in those words because the distinction is the whole point: five are exit=124 timeouts on a
1200 s cap under host memory pressure and one was never attempted, so no verdict exists for them in
either direction. A timeout is not a failure and is emphatically not a pass.

THE DROP — §4b(3), five parts, exact and bounded

• PREVIOUS RUNG: none held. These eight never reached a terminal verdict on any required path, so
  the honest previous state is unexecuted, not a lost guarantee.
• TEMPORARY RUNG: outside the modeled guarantee — deliberately not a rung.
• REASON: one interpreted verify costs 13.5 GiB peak RSS (VmHWM 14,132,132 kB) and
  192 s–734 s–unbounded wall depending on host residency; the required floor applies a ~8 s per-claim
  wall deadline, and the available remote runner is 7.63 GiB. A per-claim step budget would not bind
  this, because the binding constraint is resident memory.
• BOUNDED POPULATION — the exact eight, in test.claim.p256_dag_ecdsa_witness_test:
  the_rfc6979_sample_signature_verifies, the_rfc6979_test_signature_verifies,
  a_signature_for_a_different_message_is_false, the_wrong_key_is_false,
  wycheproof_1_the_malleable_signature_verifies, wycheproof_4_n_minus_r_is_false,
  wycheproof_60_the_shamir_edge_case_verifies, the_base_point_is_on_the_curve_and_has_order_n.
• RESTORATION TRIGGER, at capability grain: the dedicated P-256 instrument executes the exact
  eight-member verification population against the exact emitted native build, reaches the expected
  terminal verdict for every member, and carries a discriminating semantic control.

WHAT THE GREEN CHECK IS NOT

floor = SUCCESS on this PR is a budget refusal, not a pass. The floor emitted verdict=FloorRefused, 8 × INTERRUPTED-BEFORE-VERDICT raised_by=wall_deadline and 12 × ENROLMENT-MARGIN-REFUSED, and still concluded success — because the witness floor does not gate at all: docs/design-rung-drops.md, "The witness floor as a required merge gate", declared 2026-09-20, rung drop, deleted without replacement. Do not read coverage from it.

Not measured, stated so nothing is inferred

eval_steps for a verify is unmeasured (the floor preempts these before measuring — cost=UNMEASURED). Attribution of the cost between std.bignat mul/mod and the interpreter is unmeasured. What is measured: the three non-verifying claims cost ~288.5 K steps at ~415 ms, so ~99.8 % of a verify's wall is curve math rather than load — which separates curve math from overhead, not bignat from interpreter.

[briansrls]

EVIDENCE HOLD — exact head 2caafa5.

The restored floor established the important fact, but not P-256 verification: 4 cheap encoding/range witnesses reached verdicts; the 8 witnesses that exercise scalar/group verification were all budget-refused-before-verdict at the 8000 ms wall deadline. The floor itself classifies each as UNDECIDED with cost above 8000 ms and no upper bound. Green aggregation is therefore not verification evidence.

RULING ON THE ROUTE: a dedicated P-256 instrument with its own measured ceiling is rung-honest. It is not a waiver. It must name the exact bounded witness population, execute it, and treat ceiling expiry as refusal/unknown. A row that merely turns budget-refused-before-verdict into an accepted outcome would be rung inflation. The existing eval-step-cost-drop precedent is deliberately stricter: members still execute to verdict and wall-clock crossing still blocks; membership only changes adjudication of an eval-step overrun and does not raise the budget.

Native emission is NOT the only honest route. It is an honest long-term route for this module only if the production verifier is structurally native-only (or the interpreted production route refuses), the emitted function is this exact .dag verifier rather than a handwritten substitute, and the same positive/negative vectors execute against an exact-head emitted binary. Source→interpretation and source→native are distinct paths; native success cannot be cited as interpreter success.

Recommended recut/evidence order:

1. Instrument the cost by phase: modulus/context construction, modular inverse, point double/add, double-scalar multiplication, and SHA-256. The implementation already uses Montgomery CIOS; do not describe “move to Montgomery” as the missing repair. Likely candidates are repeated context/R² derivation, Fermat inversions, bit-by-bit Shamir multiplication, or interpreter overhead.
2. Add a dedicated instrument/runner route with an exact bounded population and a ceiling derived from one complete measurement, plus an overall job bound. Run the 8 substantive witnesses to terminal verdict on the exact head, with a deliberately mutated control that goes red by name.
3. After MachineWidth emission lands, execute the full vector set against the emitted native verifier and make that the recurring production-path evidence. Retain at least a discriminating interpreted anchor unless the interpreter route is structurally excluded from the verifier's production capability.
4. If the ordinary required floor ceases to own terminal verdicts for these identities, declare that path loss under §4b(3): previous/temporary rung, exact 8-member population, reason, owner/due date, and a capability-level restoration trigger. The drop may describe the missing standard-floor path; it may not count timeout as correctness.

The run cited in the rollup checked out bb50768, not this current head. It is valid evidence of the cost/coverage class, but final acceptance evidence must execute the selected route again at the exact merge head.

[gunbai-bot]

Answering review 69110 (dashboard artifact /api/reviews/69110/artifacts/stdout.log) without a push, because its central finding was answered by execution that postdates its read. Head is unchanged at bb50768c93e2f06be9936def4f556ffe8c4796fa.

The finding — "1,789 lines of new crypto land with their central claim never executed" — no longer holds as written. The suite has now executed, standalone, on an uncontended host:

arm	vector	wall	exit
accept	RFC 6979 §A.2.5 sample (P-256/SHA-256)	192 s	0 — returns true
reject	same vector, first octet of r flipped 239 → 238	205 s	1 — returns false
accept	RFC 6979 §A.2.5 test	734 s	0 — returns true

That is the pair the review asked for: an accepted positive control plus a discriminating red on the real acceptance path. It specifically retires the strongest form of the objection — that the four passing witnesses all assert is_absent and were therefore satisfied by a verifier returning Absent unconditionally. A function that never accepts anything cannot produce the first or third row.

The circularity the review identified was real and is fixed. The MontgomeryModulus next-rung trigger was justified by the unexecuted suite, so nothing could ever discharge it. The trigger is now a dedicated P-256 gunbc test row over the emitted native build, stated as what it must be sufficient for.

What still has not executed, declared rather than argued away — a §4b(3) drop in the body with all five parts, population named claim-by-claim: five of the eight accepting-path claims are exit=124 timeouts on a 1200 s cap under host memory pressure, and one (wycheproof_4_n_minus_r_is_false) never ran. Timeouts are reported as neither pass nor fail.

On the review's "compounding" point — it is sharper than stated, and the body now says so. Those eleven claims are discovered by the witnesses lane, and the lane reported SUCCESS anyway. floor = SUCCESS here is a budget refusal, not a pass: the floor emitted verdict=FloorRefused with 8 × INTERRUPTED-BEFORE-VERDICT raised_by=wall_deadline against a ~8 s per-claim budget, claim_executor exited nonzero, and the workflow step swallowed it under set +e. That is declared: docs/design-rung-drops.md, "The witness floor as a required merge gate — declared 2026-09-20", deleted without replacement over the whole enrolled population. So no green check on this PR should be read as coverage, and the executed receipt above is the only evidence.

Why the suite could not run in CI, measured: one interpreted verify peaks at 13.5 GiB RSS (VmHWM 14,132,132 kB) against a 7.63 GiB runner, so every remote attempt failed on memory rather than time. A per-claim step budget would not bind this; a native verify carries no interpreter heap, which is why the trigger is the native instrument row.

eval_steps for a verify remains unmeasured (the floor preempts these before measuring), and attribution between std.bignat mul/mod and the interpreter is unmeasured. Neither is estimated anywhere in the body.

— sent from wise-owl-628

[briansrls]

WIND-DOWN APPROVE, exact head bb50768. This supersedes my evidence hold 5260787321 under the operator's wind-down disposition.

The PR body now states the evidence at its actual extent: the four named pre-curve refusal claims plus the standalone P-256 accept/reject executions, and explicitly says that this does not establish the verifier. It labels the exact eight verification-performing claims UNKNOWN rather than passing, treats timeout as neither pass nor failure, and names the bounded eight-member population. The §4b(3) trigger is at capability grain: the dedicated P-256 instrument must execute that exact population against the exact emitted native build, reach every expected terminal verdict, and carry a discriminating semantic control. The body also opens the disposition as substrate acceptance with an explicit evidence gap—not security sign-off—and separately records the app-to-verifier binding as ecdsa_verification_realization_frontier.

This approval accepts the substrate under that explicit evidence gap. It is not P-256/ES256 security sign-off and does not establish the production device-signature path. No new execution or dispatch is required in this wind-down PR.

[gunbai-bot]

Review 69110 (12:02Z) is right about the state it read, and it is the state the PR now declares rather than disputes. Since then: the floor lane executed the suite (run 35509606112) — four claims passed, the eight verification-performing claims were budget-refused at 8 s each; the lane produced one standalone accept/reject pair (RFC 6979 A.2.5 verifies at 192 s; the same vector with one bit flipped in r rejects at 205 s); one interpreted verification peaks at 13.5 GiB, so no floor budget can admit it. Under the operator's wind-down the PR body was rewritten to the side chat's five constraints: the eight are declared UNKNOWN (not passing) as an exact, bounded §4b(3) drop whose trigger is the capability a dedicated P-256 gunbc test row over the emitted native build is sufficient for; the PR states it is substrate acceptance with an explicit evidence gap, not security sign-off. Side-chat WIND-DOWN APPROVE at exact head bb50768 supersedes the evidence hold; enqueued. The MontgomeryModulus next-rung trigger's circularity is real and is why the trigger is now the native execution, not this suite. — sent from eager-owl-205