Repository navigation
Repair #12000: device routes gated on the native crypto realization; App Attest counter committed before reads and push updates - #12072
Merged
gunbai-bot[bot] merged 24 commits intoSep 22, 2026
Conversation
…rop app_attest_verifier_new_witness_eval_step_cost for the six App Attest verifier claims (they execute; only the eval-step overrun is reported); the two P-256 seam verifications leave the floor for the native row; transcribed cost figures replaced by the instrument the roadmap row names Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…arable: eight interpreted-crypto identities admitted at floor_cost_debt_typed_admissions (they keep executing), the two single-block SHA-384 vectors leave the floor; review 69917's group-law closure claims land with their disposition The eval-step drop landed in 6bcd8b3 cleared one gate and the PR floor then refused on another: ENROLMENT-MARGIN-REFUSED for all eight new identities, cause enrolment_measured_over_margin, against the 302ms margin the runner envelope implies (v2.workflow.floor_enrolment_margin; figures from the required-floor job of run 35685032399, enrolment-margin lines). claims_failed=0 -- they execute and pass; only the margin refuses. The sanctioned route that keeps them EXECUTING is the typed cost-debt admission (v2.workflow.floor_cost_debt_admission floor_cost_debt_typed_admissions), which carries an identity and a reason and never a reading: whether a row is still expensive is decided by the run that judges it, so it cannot outlive its cost. A long home would have been the other option and is refused here: nothing executes test.claim.long., so re-homing would delete the only execution of the P-384 parameters and SHA-384 on the acceptance path. The two single-block SHA-384 published vectors are NOT admitted, and that is the honest part. They measured inside the gate's coin-flip band -- over the 302ms margin and at or beside the 500ms per-subject line -- where a typed admission goes stale and blocks. A one-block hash is already the cheapest case, so there is nothing to reduce. They take the disposition the three P-384 signature verifications took: ordinary fns, consumer the native row the frontier names. SHA-384 keeps executing evidence on the floor: the two-block published vector and the one-octet discriminating red. Review 69917's work lands with this: bignat_below / bignat_nonzero_below move to std.bignat (ordering over BigNat is that layer's fact), curve_jacobian_on_curve and curve_negate give the group law its own evidence without an inversion, and two claims assert that doubling and addition close over the curve with a discriminating red on an off-curve point. Both are members of the eval-step drop and of the typed admissions. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…e floor, and the dangling vf_root goes The drop beside this file said the P-256 verifications "left the required floor and run on the native row", and they were still declared `test fn`, so the floor planned them. That made the drop's sentence false and left an 8 s wall crossing covered by no declared population, which DESIGN section 4b(3) does not permit. They are ordinary fns now, the disposition the sibling test.claim.signature_verify_join_witness_test already took, and the file's comment says why rather than restating the old budget-refused state. vf_root had no call site -- the root is reached through verify_attestation's own fold -- so it was a declaration with no consumer (DESIGN section 3c). Deleted, with the rfc_7468 import and the app_attest root-PEM import it was the only reader of. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ep3b docs/design-rung-drops.md refused under GeneratedArtifactConcurrentDivergence (both sides changed the projection since the merge base). Resolved by the path's declared route: the merged-in side's bytes taken verbatim, no hand editing, no local regeneration. Set-difference check at row-identity grain shows no row from that side went dark. One row IS dark and is named here rather than left to be discovered: this branch's own app_attest_verifier_new_witness_eval_step_cost heading is absent from the projection, which is exactly the state the route hands to heal -- it derives the projection from the merged authorities and heal-publish commits the sealed candidate onto this branch. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…e empty message stays on the floor Review 69978 on #11981 raised two things. One does not hold; the other does, and this is the fix for it. DOES NOT HOLD: the finding reads "clears the line decisively" as CHEAP and infers a contradiction between a 2x claim being admitted and a 1x claim sitting in the coin-flip band. The gate refuses the other way -- v2.workflow.floor_enrolment_margin: "at or under the line it is stale and blocks" -- so clearing the line means being reliably OVER budget. The two records were consistent. Answered on the PR rather than changed. DOES HOLD: with both single-block vectors demoted off the floor, the padding-only path of FIPS 180-2 section 5.1.2 had NO executing evidence left -- a zero-length message is all padding, and the one-octet red exercises single-block padding only against "abc"/"abd", never a published value and never at length zero. That is a real coverage loss this PR introduced. THE FIX, which takes the reviewer's "re-enrol" option without re-entering the cliff: the three published vectors (empty, one-block, two-block) fold into ONE claim over ONE interface -- sha384_hex reproduces the FIPS 180-2 Appendix D published values. Three inputs to one boundary is a table, not the conjunction of independent cases DESIGN section 3 says to split; splitting loses no coverage only if each piece can be ENROLLED, which is exactly what fails at the line. Folded, the claim bills their sum, which is above the line by construction because each summand was measured at or above it, so ONE typed admission covers it and cannot go stale while the interpreter realizes SHA-384 this way. The drop row's measured_by no longer cites a run that never measured this identity: it states that the cited runs measured the three vectors SEPARATELY and that this row is their sum, with the PR floor run on this head confirming the folded figure. Local receipt on this tree (claim_batch, seed interpreter), corroborating the derivation rather than replacing the floor's reading: PASS sha384_reproduces_the_published_fips_180_2_vectors cpu=1379ms PASS sha384_of_a_one_octet_change_is_a_different_digest cpu=757ms Both decisively above the 500ms per-subject line; the split single-block vectors are what sat at it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…le fallback and its name table delete Review 69983 on #11989, verified against the tree and fixed at the root it names rather than at the symptom. THE DEFECT. validation_category_refusal and bundle_version_refusal each returned the whole AttestationRefusal sum while their real range was three constructors apiece. That made the range invisible to consumers, so the two assertion mappers each carried a `_ => other` arm covering ten constructors the reader cannot emit -- and to print anything, that arm needed attestation_refusal_name: thirteen rows hand-transcribing the sum's own constructor names. Both call sites of that function were the unreachable arms, so the table was reachable from nothing. Two authority rules, both cited by the review and both correct here. DESIGN section 4b: a check whose forbidden state cannot be expressed where the check runs "is not a weak wall but a decoration -- permanently green by construction, carrying no information, and worse than absent because it will be cited as coverage." DESIGN section 3: a hand-written table of constructor names is a second naming authority for what the Node tree already names. THE FIX IS CONSTRUCTION, NOT A BETTER FALLBACK. Each reader now returns its own narrow sum naming exactly what it can conclude: ValidationCategoryReading = Admitted | ReadAbsent | ReadRefused { category } | ReadUndecodable { cause } BundleVersionReading = Matched | ReadAbsent | ReadUnexpected { declared } | ReadUndecodable { cause } Both consumers map from the READING. The attestation fold keeps its AttestationRefusal? shape through thin total mappers, so its call sites are unchanged; the assertion mappers map each reading to its assertion twin with every arm reachable. attestation_refusal_name is deleted. There is no wildcard left that could regress to review 69702's defect of reporting a malformed category as absent -- that arm is now impossible to write, not merely avoided. app_attest_undecodable is an identity wrapper, so the cause string the assertion path carries is byte-identical to before; this is a representation change with no behavioural difference on any reachable input. Evidence, run against this tree: PASS the_sample_passes_every_step_before_the_extension_steps PASS each_expectation_reds_its_own_step PASS a_malformed_object_refuses_before_any_step PASS the_sample_assertion_counter_is_the_published_one PASS the_sample_assertion_passes_rp_id_and_refuses_on_absent_extensions PASS an_undecodable_stored_key_is_absent_not_a_false_verdict PASS chain_link_refuses_an_unsupported_algorithm_or_curve_by_absence Also merges step3, carrying the SHA-384 published-vector consolidation. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ion that discriminates it
Reverses my own previous commit's fold, on a design ruling I asked for and
agree with.
WHY THE FOLD WAS WRONG. I folded the three published vectors into one claim so
their summed bill cleared the per-subject line. The counterfactual condemns it:
removing the abc vector changes no semantic fact about the other two yet can
make the admission stale, and adding an unrelated fourth vector strengthens no
existing fact yet makes the admission more stable. A cost ground that moves with
its neighbours is not a ground for the subject it claims to admit -- it is the
enrolment gate dodged by aggregation, which is what I had told the reviewer I
was not doing. DESIGN section 3 names the shape directly: a conjunction of
independent cases forced through one budget when splitting them loses no
coverage.
WHAT IS HERE INSTEAD. Three claims, one per published vector, each paired with
the mutation that proves that vector's equality discriminates:
empty message + a one-octet message cpu 664ms
abc + abd cpu 641ms
896-bit vector + a last-block mutation cpu 1156ms
The second evaluation in each pair is not ballast bought to clear a budget: it
is the RED that DESIGN section 4b requires of the rung anyway ("a discriminating
RED refused on the real acceptance path plus an accepted positive control"). So
each claim's cost is caused by its own boundary, and no claim's admission
depends on a vector belonging to a different path.
All three measured decisively above the 500ms per-subject line, so the boundary
condition does not arise: no vector needed a bounded evidence gap, and none was
padded to cross the line. The empty message -- the only executing evidence of
the padding-only path of FIPS 180-2 section 5.1.2 -- is back on the floor on its
own merits.
Both rosters now carry three identities where they carried one folded one plus
the old bare red, and each measured_by states its own reading.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rs; the projection is regenerated Review 70011 on #11981. Both findings are real and both are mine: I split the SHA-384 vectors into three paired claims and updated the ROWS without carrying the change into the declaration that bounds them or its generated projection. FINDING 1, the declaration contradicted its own population. The prose said "THE TWO SINGLE-BLOCK SHA-384 VECTORS ARE NOT MEMBERS EITHER" while the population authority it imports enrols exactly those vectors, and subject, restoration trigger and the roster header all said "eight identities" against a list of nine (4 P-384 point + 3 SHA-384 + 2 group-law). DESIGN 4b(3) requires a drop to declare a BOUNDED POPULATION; a declaration whose text excludes members its population includes is not bounding anything. Corrected to nine throughout, and the excluding paragraph is replaced by one that states what is actually true: the three published vectors ARE members, one per vector, each paired with the mutation that discriminates it, each measured decisively above the per-subject line on its own subject. It also records WHY the two earlier cuts were wrong -- excluded-as-too-cheap, then folded-into-one -- because the second is the failure worth not repeating: a summed bill moves with its neighbours rather than with the subject. Note the population itself was never wrong: it is DERIVED from floor_eval_step_cost_drop_interpreted_crypto_rows rather than hand-listed, so only the prose around it had drifted. That is the single-authority arrangement working as intended, and it is exactly why the drift was prose-only. FINDING 2, the generated projection was stale, naming two identities that no longer exist. docs/design-rung-drops.md is a projection, so it is REGENERATED rather than hand-edited: gunbc run --entry dag/gunbc/instruments/docs_projection_gate.dag --function regen. The other two projections that actuator writes were already at their fixed point; only this one moved. Verified after: zero occurrences of either stale identity, all three real identities present, "nine" carried through. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…member does not do what the other five do Review 70013 on #11989, verified and fixed -- plus the same defect one link further along, which the review did not name. THE FINDING, CONFIRMED. One measured_by was pasted verbatim across all six rows of floor_eval_step_cost_drop_app_attest_verifier_rows, claiming each member decodes Apple's real attestation object -- CBOR, three DER certificates, SHA-256 over the TBS and the nonce. That is false of test.claim.signature_verify_join_witness_test.malformed_carriers_refuse_before_the_curve, which touches no Apple object, no DER certificate and no SHA-256: it decodes two base64url carriers of the RFC 6979 A.2.5 vectors through extdeps.crypto.signature verify_signature, and the 33-octet key is refused against the suite's 65 on the SIZE check before any curve arithmetic runs. The list header said the same false thing. DESIGN 4b(3) requires a drop to declare its reason and bounded population; a population row whose stated reason does not hold for that row is the declaration failing at its one job. I CHECKED MEMBERSHIP RATHER THAN ASSUMING IT. If a claim refuses before the curve, it is worth asking whether it belongs in an eval-step drop at all. The new-witness budget is required_floor_new_witness_envelope_ms (100) through the pinned floor_eval_step_calibration rate (723 steps/ms); re-derived by claim_batch --entry dag/test/claim/signature_verify_join_witness_test.dag --function malformed_carriers_refuse_before_the_curve, this claim measures over that budget by more than an order of magnitude. So membership is right and only the reason was false. The row now says what it actually bills, and the header says what the six members genuinely share -- the interpreter walking real-sized octet lists byte by byte -- rather than a decode five of them perform. THE SAME SENTENCE HAD PROPAGATED. The drop declaration's restoration_trigger read "while each still decodes Apple's real object through the production readers", false for the same member and in the one field that decides when the drop retires. A trigger that cannot be true of a member cannot retire the drop for it. Reworded to name each member's own real bytes: Apple's object for the five verifier claims, the RFC 6979 carriers for the carrier join. docs/design-rung-drops.md is regenerated, not hand-edited, and a second regen reproduces it byte for byte (fixed point). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… hand-resolved The only conflict was docs/design-rung-drops.md, which is a PROJECTION and has no authority of its own -- both branches had regenerated it from authorities they each changed. Resolving such a file by choosing hunks would invent a state neither authority implies, so it is resolved by regenerating from the MERGED authorities instead. The .dag authorities merged cleanly and both sides' edits survived: step3's "nine identities" correction to the interpreted-crypto drop, and step3b's per-row billed work for the verifier drop's sixth member. Verified on the regenerated artifact rather than on the absence of conflict markers -- a marker grep reads clean whenever one side simply won: nine interpreted P-384 ... : 2 occurrences (step3's side present) THIS ROW'S BILLED WORK ... : 1 occurrence (step3b's side present) stale sha384 identities : 0 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review 70033 asked for this, and the edit is right, but its stated GROUND is not -- so the reason recorded here is the measured one, not the assumed one. WHAT CHANGED. Each claim wrote `sha384(...)` for the discriminating red and then `sha384_hex(...)` over the same message for the published comparison. Since sha384_hex is base16_encode_lower(sha384(m)), the claims now compute the digest once and encode THAT value. Clearer, and it no longer asks the reader to know anything about node sharing to see that one hash is one hash. WHAT IT DID NOT CHANGE: THE COST. The review called this blocking on the ground that the drop's cost story -- "no repeated demand to remove" -- is thereby false. It is not false, and the instrument says so. Removing an entire SHA-384 from each claim moved eval_steps by 3, 69 and 4 steps out of roughly a million: empty pair 1074019 -> 1074016 abc pair 1041203 -> 1041134 two-block pair 1862125 -> 1862121 That is not what removing a 500k-step computation looks like. A discriminating control, run and then deleted rather than left as floor cost: the same hash written ONCE 571962 steps the same hash written THREE times 537186 steps three DISTINCT hashes 1534872 steps Writing one pure expression three times costs what writing it once costs; three different ones cost three times as much. Identical pure subexpressions are ONE node in the content-hashed dependency graph (DESIGN section 4), so the repetition was lexical only and the demand graph never carried it. The drop's ground stands as written, and it stood before this commit. This is worth stating rather than accepting silently: had I taken the finding's reasoning, I would have recorded a false reason for a true edit, and the next reader would have inherited the belief that these claims once paid for a hash they never paid for. Measured after the change: empty 698ms, abc 709ms, two-block 1235ms -- all still decisively above the 500ms per-subject line, so no admission moves. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…into step3b-sync3
Review 70054 on #11981. Correct, and it is a consequence of the previous commit rather than something that arrived with the feature: when the three vector claims stopped calling sha384_hex and encoded the digest they had already computed, sha384_hex became a declaration nothing in the tree consumes. DESIGN section 3c: a declaration with no call site in the closure is dangling, and it is red regardless of how well modeled it is. VERIFIED WIDER THAN THE FINDING DID. The review grepped '*.dag'; sha384_hex occurs exactly once across EVERY file type in the tree, at its own definition. No .rs mirror, no emitted artifact, no consumer of any kind. WHY DELETE RATHER THAN RE-CONSUME. The review offered both arms. Re-consuming would cost nothing -- sha384_hex(m) is base16_encode_lower(sha384(m)), and the inner sha384(m) node is shared with the claim's own, which the control in the previous commit established -- but it would re-open review 70033's legibility objection, since the claims deliberately spell base16_encode_lower(octets: a) to make it visible that one hash is computed once. Deletion satisfies both reviews; re-consuming satisfies one at the other's expense. The sibling sha256_hex stays: it HAS consumers (sha256_fips_witness_test, x509_rfc5280_witness_test). Parity is not a reason to keep an unconsumed declaration, and the asymmetry is the honest state rather than a defect. Claims unchanged and re-run: empty 671ms, abc 661ms, two-block 1146ms, with eval_steps identical to the previous head (1074016 / 1041134 / 1862121) -- the deletion removed a declaration, not executed work. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…into step3b-sync4
…as behind Review 70064 on #11981. Correct, and it is residue of this PR's own move: when P-256's Jacobian arithmetic went into extdeps.crypto.nist_prime_curve, p256_is_infinity stayed behind as a wrapper identical in signature and body to jacobian_is_infinity. DESIGN section 6: "invent or reuse on proven coincidence, never bare-alias"; section 3: a second name for one concept is the recurring violation. WHY THIS ONE AND NOT ITS SIBLINGS. p256_affine and p256_double_scalar are genuine partial applications -- each binds p256_curve, so each carries a fact. p256_is_infinity binds nothing: infinity is a property of a JacobianPoint's z coordinate and is the same question on every curve. The reviewer's tell is the sharpest one available: the NEW nist_p384 module mints no such alias and its witness calls jacobian_is_infinity directly, so the asymmetry between two halves of one family is the evidence that the wrapper is residue rather than design. The single caller, the P-256 witness, now imports jacobian_is_infinity from the family module and calls it directly, exactly as the P-384 witness does. No reference to p256_is_infinity remains anywhere in the tree (.dag or .rs). Evidence: all 12 claims of test.claim.p256_dag_ecdsa_witness_test pass, including the_base_point_is_on_the_curve_and_has_order_n, which is the claim that exercises the rewired call. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…into step3b-sync5
…claim that could not reach a verdict Two things: review 70083's finding, and the CI red my previous commit caused. REVIEW 70083 -- TRANSCRIBED MEASUREMENTS. The three SHA-384 rows carried "cpu 664ms" and friends, citing a branch-local claim_batch run rather than a re-derivable artifact. DESIGN section 6: name the instrument, never transcribe its output; a transcribed number is unreachable from the thing that owns it, so it rots. These figures were the whole ground for the "decisively above the line" argument that admits the un-aggregated form, which is the worst place for a number to rot -- the argument keeps reading as sound after the figure stops being true. The rows now name required floor run 35708011844 and artifact required-ci-measurement-receipt, and carry the same never-copy clause the live-forecast sibling already uses. I left two number-shaped things alone, deliberately: the 302ms margin and 500ms per-subject line are POLICY figures naming a modeled constant, not instrument output; and "wall under 2000ms" in the four P-384 sibling rows is the original author's text stating a satisfied bound rather than a standing figure. Flagging rather than silently deciding. THE CI RED, WHICH I CAUSED. Deleting p256_is_infinity meant editing the P-256 witness, and changed-witness selection then PLANNED every claim in that file. the_base_point_is_on_the_curve_and_has_order_n needs a full n*G scalar multiplication; it hit the 8000ms wall deadline and was INTERRUPTED BEFORE ANY VERDICT, which blocks. It was latently broken, not newly broken: the PR had not otherwise touched that file, and the identity appears ZERO times in the earlier passing run. It has been over the wall deadline all along, invisible because nothing selected it. SPLIT RATHER THAN DEMOTED, because an interrupted claim establishes NOTHING -- so while the two facts shared one claim, the cheap one was being lost with the expensive one. G being on the curve is one curve equation and now executes on the acceptance path; n*G = infinity crosses the wall deadline, which no declared eval-step drop may cover, so it takes the frontier disposition this PR already gives the P-256 and P-384 signature verifications. Demoting both would have been deleting evidence to turn CI green. The split half is over the new-witness eval-step budget, so it is rostered with its own reason and admission exactly as its P-384 sibling is -- nine members to ten, corrected in the roster header, the drop declaration and the subject. docs/design-rung-drops.md regenerated; verified it carries the new row and no transcribed cpu figure. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…condition is declared Review 70082 on #11989. The one predicate was realized as a ten-way string equality chain, and this PR cut three PER-CHARACTER folds over whole source trees onto it -- up to a 5x constant on the innermost predicate of each. DESIGN section 6, bare minimum cost: a proven cost-shape defect is always fixed regardless of the realized n, because "n is small here" is not a time-stable fact. The consolidation into one authority was right and stays; only the body changes. WHAT I CHECKED BEFORE ACCEPTING THE ONE-LINE FIX, because it is not purely a notation change. String ordering is LEXICOGRAPHIC, so "12" >= "0" and "12" <= "9" both hold: multi-character text answers TRUE under the ordering form where the equality chain answered FALSE. That is a real narrowing of a std predicate's contract, so I traced every call site rather than assuming. All five reach it through char_at -- decimal_digits_from; char_is_ident via leading_ident_from in gunbc.rust_item_scan; digits_from in gunbc.rust_item_host_observation; leading_digits_from in gunbc.build_cache.build_cache_endpoint_observe; and is_digit in gunbc.auth.approval_capability, whose own caller folds char_at over the offsets. No current consumer can reach the divergence. The precondition is DECLARED on the carrier rather than left implicit. An undeclared narrowing is the silent assumption section 6b names: the next caller inherits it without being told, and a longer string would answer wrongly. I kept the plain two-comparison form the review asked for rather than adding a length guard: it is what char_is_ident's neighbouring a-z and A-Z range tests already use, so it adds no new convention, and a guard would put a third operation back on the innermost predicate this change exists to cheapen. Evidence over the real consumers, not the predicate in isolation: PASS witness_starttime_reads_after_the_final_paren (leading_digits_from) PASS witness_listen_entry_yields_its_inode PASS witness_stat_type_word_decodes_socket_and_absence PASS rust_item_identity_key_includes_impl_subject (char_is_ident) PASS same_name_in_two_inline_modules_yields_two_keys Also merges step3. docs/design-rung-drops.md conflicted, as it does whenever two branches regenerate it; resolved by regenerating from the merged authorities and verifying both sides survive, never by choosing hunks. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…dent joins the row that already owns its class Two design rulings, acted on. FIRST: THE FRONTIER MUST NAME WHAT VERIFICATION DOES NOT ESTABLISH. Routing the_base_point_has_order_n to ecdsa_verification_realization_frontier was not enough while that frontier's SUFFICIENT FOR clause promised only that the device routes mint SignatureVerified, AttestationVerified and AssertionAuthentic from real bytes. A PASSING SIGNATURE VECTOR DOES NOT IMPLY THE PUBLISHED BASE POINT HAS THE DECLARED ORDER, so that frontier could have retired with the order fact still dead -- DESIGN section 4b(3), a trigger naming less than the capability it restores is satisfied while the capability stays dead. The clause now names the identity explicitly, or a native claim asserting exactly n*G == infinity with a discriminating control that (n-1)*G != infinity, and states why it is named there rather than folded into the generic verifier sentence. SECOND: NO NEW FAILURE-MODE ROW -- THE CLASS ALREADY HAS AN AUTHORITY. I had proposed one for "a witness too expensive to reach a verdict is invisible until an unrelated edit enrols it". gunbc.recurring_failure_mode ceiling_never_exercised_for_a_population_the_census_cannot_plan already states that invalid state almost word for word, including the recognition rule and the declared-minus-planned set difference. A new row would have been a nickname for it (DESIGN section 3), so this is appended as a SECOND SPECIMEN instead. I verified the row exists and matches before appending rather than taking the citation on faith. The specimen strengthens the class rather than repeating it: the first is a CPU LINE exceeded by four milliseconds, which still yields a verdict and a reading; this one is a WALL DEADLINE reached with NO VERDICT AT ALL, so the claim established neither of the two independent facts it asserted and the cheap conjunct died with the expensive one. It also records the repair that must NOT be made -- narrowing changed-witness selection would have hidden the witness again, because selection is what exposed the defect. docs/design-failure-modes.md is gitignored, an on-demand combined view rather than a merge surface, so the specimen projects without a committed artifact; verified by regenerating and finding the specimen and its run id in that view. docs/design-rung-drops.md is unchanged, correctly: neither edit touches a drop. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ed, not picked THE LENGTH GUARD, WHERE I WAS OVERRULED AND THE ARGUMENT IS RIGHT. I had argued for the bare two-comparison form with the single-character precondition stated in an annotation, on the evidence that all five call sites reach it through char_at. That evidence proves CALL-SITE COMPATIBILITY, not contract preservation: the parameter's enforced domain is String, this is a PUBLIC std predicate, and "12" >= "0" && "12" <= "9" both hold lexicographically. A precondition that lives only in an annotation is not a wall -- no Accepted program can read one (DESIGN section 4c) -- so a later caller may legally pass "12" and be told it is a digit. Section 5 prefers construction to prose, and one length check is a small price beside the nine comparisons this still removes. The annotation now says the guard dissolves when a typed single-character carrier exists, which is the real construction. THE MERGE CONFLICT WAS A GENUINE ONE, AND NEITHER SIDE WAS SIMPLY NEWER. ecdsa_verification_realization_frontier was edited on both branches: step3b ADVANCED it (the verifier folds have landed and are described as authored, with Apple's real assertion signature verifying under the sample credential key by execution) and replaced a transcribed "13.5 GiB and minutes" with the named instrument; step3 appended the order-n clause to the older body. Picking either hunk would have dropped the other's fact. Resolved as a UNION AT THE MEANING LEVEL: step3b's advanced body, with step3's order-n clause appended to its SUFFICIENT FOR. Verified all three facts survive -- the by-execution advance present, no 13.5 GiB transcription, the order-n identity named. Evidence for the guard, over the real consumers rather than the predicate alone: PASS witness_starttime_reads_after_the_final_paren PASS witness_listen_entry_yields_its_inode Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… into repair-12000
… Attest counter committed before a read or push update Every verifier-dependent route asks gunbc.auth.approval_device_crypto_realization device_crypto_admission first and refuses 503 with the typed cause while no natively emitted handler is bound; a bound receipt must cover the named population, the P-256 base-point order fact included. admit_device_read commits the assertion counter through gunbc.auth.approval_assertion_counter (one CAS advance per enrolment) before the operation runs; the redemption POST keeps its challenge + one-decision CAS slot as its replay wall. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
6 tasks
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 23, 2026
Review 70621 repeated two comments that predate #12072 and #12080: the read residual ('the counter is not stored ... replays inside its window') and PlatformRedemptionProof's 'THE ASSERTION COUNTER IS NOT STORED'. Reads and the push update are replay-refused by the per-enrolment counter committed before they run; the redemption is deliberately exempt (challenge plus one-decision slot). Both comments now point at gunbc.auth.approval_assertion_counter and approval_device_routes admit_device_read instead of restating them. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
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.
Repair of #12000 against the two blocking cross-stack findings. Stacked on #12000's branch (
session/nimble-eagle-216-step4) so its owner can take it in one merge.Parent merged first. #11989's current head
2a7c38cb5cis merged in with a merge commit. The merge was clean; I expecteddocs/design-rung-drops.mdto conflict and it did not. I still regenerated the file (tools.docs_projection_gate regen) and the output matched the merged bytes exactly. Step3b's "six App Attest verifier claims" drop is present. Step4 changed nothing underdocs/ordag/gunbc/rung_drop, so there was nothing from that side to lose.Finding 1: routes consumed the crypto frontier with nothing in front of them
gunbc.auth.approval_device_crypto_realization:DeviceCryptoRealization = NativeDeviceCryptoBound { receipt: DeviceCryptoHandlerReceipt { handler_identity, exact_revision, covered } } | NativeDeviceCryptoUnavailable { cause }.approval_device_crypto_realizationis Unavailable.device_crypto_admissionright after wire, segment and writer checks. That is before any enrolment-store read, base64 decode orverify_*call.admit_device_read; enrol and redeem do it inline.P256SignatureVerification | AppAttestAttestationVerification | AppAttestAssertionVerification | P256BasePointOrder.test.claim.p256_dag_ecdsa_witness_test the_base_point_has_order_nand its(n-1)*G != infinitycontrol.Finding 2: counter carried then discarded
gunbc.auth.approval_assertion_counter:AssertionCounterStanding { enrollment_id, last_admitted_counter, generation }, onegunbc.durable_cas_file_storeslot per enrolment.admit_assertion_counterreads the standing and refuses whenobserved <= stored(a replay gets 403).observedby CAS against the generation it read. A lost race gets 409.admit_device_readadmits only after that commit, so the three reads and the push update run their operation only after the counter has advanced.SignedRedemption's signing input, the Swift mirror and the vectors, so it belongs in its own change. I recommend that follow-up.cas_max_generation_probegenerations, and each admitted assertion adds one.Evidence (claim_batch
--wet, local build of this head)All green by execution. Each RED below was produced by mutating the source and confirming the claim fails, then restoring it.
approval_assertion_counter_wet_witness_test:a_replayed_assertion_counter_is_refused_and_a_higher_one_admittedruns against a real/tmpstore: 5 is admitted, 5 is refused, 4 is refused, 6 is admitted, 6 again is refused. RED:<=→<fails it.the_counter_standing_is_per_enrolmentis green.approval_device_routes_witness_test:the_three_reads_…,the_push_update_…,the_enrolment_…andthe_redemption_refuses_503_before_any_crypto_while_the_native_handler_is_unboundare green. RED: making the Unavailable arm admit fails the read and writer claims.a_bound_realization_passes_the_read_past_the_gateis the control: the same read under a bound receipt does not answer the gate reason.a_bound_handler_without_the_base_point_order_fact_is_refusedis green. RED: droppingP256BasePointOrderfrom the population fails it..daghas an indented//.What I could NOT establish
AuthenticAssertion.counterfromadmit_device_readinto the admission needs a realAssertionAuthentic, and minting one means an interpreted P-256 verification, which is the very cost this PR fences off. The admission interface runs for real; the join from the route to it holds by construction only. Its inhabitance claim waits on the native handler.🤖 Generated with Claude Code