App Attest P2: the .dag SHA-2 and P-256 verifiers execute natively: NativeClaimDriver + //gunbc/instruments:native-crypto-vectors (stacked on #12219)

[gunbai-bot]

Stacked on #12219 (the base branch; review only the delta). App Attest native-crypto lane, deliverable (B) for the crypto half: the .dag SHA-2 and P-256 verifiers execute natively, with a named instrument. Split of the approved plan: P2 here; P3 (stern-raven-24) adds the App Attest fold program as another row on this producer; P2b brings the P-384 checks.

What this delivers

• gunbc test //gunbc/instruments:native-crypto-vectors, a new row, not a flag (DESIGN "Building & checks"). It emits the crypto closure, builds it and runs it. 25 cases, all native:
  • SHA-256 ×3 and SHA-384 ×3 FIPS 180 vectors, each with a one-octet-appended red;
  • P-256: the RFC 6979 §A.2.5 sample and test signatures (true), plus reds: a different message (false), the RFC 7515 §A.3 wrong key (false), and an off-curve key (refused);
  • Wycheproof ecdsa_secp256r1_sha256_p1363: tcId 1 and 60 true, 4 false, 11, 26 and 2 refused;
  • the order of the base point: n·G is the point at infinity, with its discriminating control that (n−1)·G is finite (the fact the ecdsa_verification_realization_frontier names).
• One interpreted P-256 verify cost about 13.5 GiB and minutes (The approval app's crypto in .dag: bitwise, bignat, SHA-256, P-256 (blocked on MachineWidth reflection) #11645). Natively, the whole program runs in about 3 s.

How

1. Retype, not reification (per the standing ruling in gunbc.recurring_failure_mode bounded_natural_arithmetic_evaluated_as_unbounded_int, which rejected making Compose transparent; I proposed that, had it approved, then retracted it on reading the row). The value-holding UInt32/List<UInt8> sites in std.bitwise, extdeps.crypto.sha2, std.bignat, nist_prime_curve and nist_p256 are now typed Int/List<Int>, which is what they hold. std.machine_constraints and the emitter's Compose handling are untouched. The receipt listing every site is on that row. No enforced rung drops: a phantom brand checks nothing.
2. The std.compiler_entry NativeClaimDriver entry kind (with NativeClaimReport { stdout, exit }). Its rendered main makes one call, writes stdout and sets the status; it reads no argv and no file. It is asked by name in the emitter's driver partition, with no residue arm.
3. gunbc.target_binding NativeClaimProgramProducer { entry }, generic over its entry. The next program (P3's App Attest folds on Apple's sample) is a binding row, not another arm.
4. gunbc.native_claim_program native_claim_program_standing: the .dag reader decides the result. It uses gunbc test's vocabulary: 0 held, 1 not held, 2 no observation. The roster-to-row match is an identity join: a missing, duplicated or unknown row, a status that contradicts the rows, or a signal each mean no observation.
5. One host arm (native_lane_runner run_native_claim_program plus the target_invocation_host dispatch). It reuses prepare_emitted_compiler_for_entry, spawns the binary, and hands stdout and status to the .dag reader, deciding nothing itself. Seed growth is declared in gunbc.native_claim_program_seed_growth.
6. The published vectors live in their upstream modules: extdeps.standards.fips_180, rfc_6979, rfc_7515, and extdeps.wycheproof.ecdsa_secp256r1_sha256_p1363 (each case carries its own message; tcId 60's is "69819", a defect the program's own red caught during development).

Evidence (clean worktree at 274af55, 0 changed files, local build; the last commit e557810 adds only the rfm receipt text)

check	result
gunbc test //gunbc/instruments:native-crypto-vectors	exit 0, 25/25 held, roster joins rows 1:1
same, with sha256_abc's published digest corrupted	exit 1, REFUSED: not held: sha256_abc (tree clean after)
test.claim.entry_authority_witness (incl. the claim main's one-call shape, and a claim entry beside another refusing as ambiguous)	8/8
test.claim.native_claim_program_standing_witness (held, not held, and 7 no-observation arms)	9/9
test.claim.seed_growth_admission_witness	7/7
test.claim.data_row_wide_integer_literal_witness	2/2
gunbc test //gunbc/instruments:self-host (the retypes don't break the self-emitted compiler)	exit 0
seed regen after re-stacking	converged; only P2's emitter arms are installed

What this does NOT retire, stated (DESIGN §4b(3))

• app_attest_interpreted_crypto_new_witness_eval_step_cost stays. Its trigger names ten identities, five of them P-384 checks this instrument doesn't run yet → P2b.
• ecdsa_verification_realization_frontier stays. This discharges the crypto half of (c) and the order-n fact; the fold execution (P3) and the device-route binding (C, after App Attest step 4: the six device routes on the approval broker as body-authenticated POSTs; wire header rows deleted, vectors regenerated, Swift mirror (stacked on #11989) #12000) remain.
• The instrument is run by name, not on the merge path. It discharges only drops whose capability is "executes natively", never one about enforcement on the merge path.
• Declared duplication: the interpreted test.claim.p256_dag_ecdsa_witness_test still carries its own copies of the RFC 6979 and Wycheproof vectors now homed in extdeps. Trigger: P2b, which touches that witness family anyway, imports them.

🤖 Generated with Claude Code

[briansrls]

SOURCE HOLD at exact head a329a2bc220ec64d9010fe049d695d22781bd392 (the requested e557810... plus the main merge and regenerated seed).

The crypto implementation and current 25-case program are directionally accepted: the .dag closure is emitted and called directly by a NativeClaimDriver main; the value-holding UInt32/UInt8 retypes follow the existing RFM ruling rather than erasing Compose in the emitter; the vector authorities are separated; the order-n control is present; and the two named drops/frontiers correctly remain standing.

Three fail-open seams remain in the new generic native-claim substrate.

1. An explicit ExitFailure can cross the process boundary as success. NativeClaimReport.exit is the unrestricted std.process.ProcessExit, but emit_native_claim_driver_main_rs maps every ExitFailure { code, ... } to std::process::exit(*code as i32). A program may legally construct ExitFailure { code: 0, ... }; with all rows marked held, the spawned process returns status 0 and native_claim_program_standing returns ExitSuccess. Large/negative Int codes also are not the closed 0/1/2 vocabulary the reader claims. Narrow the report termination to a native-claim-specific closed type, or map ExitSuccess -> 0, the one admitted not-held arm -> 1, and every other failure/value -> 2 before crossing the OS boundary. Add controls proving ExitFailure code 0 and an out-of-vocabulary code can never become held.

2. The report parser drops malformed lines instead of refusing the report. native_claim_rows flat-maps parse failures to []. Thus roster a\ncase a held observed=x\ncase z nonsense\n with status 0 is accepted: the unknown malformed case line disappears. case a held also passes even though the declared protocol requires observed=<text>, and an extra roster/noise line is ignored. This contradicts the stated exact report shape and the claim that an unknown row means no observation. Parse the whole non-empty line population into a typed success/refusal, require exactly one first roster line and exact case-row shape, and make any malformed/extra line no-observation. Add REDs for malformed unknown case, missing observed field, extra roster, and arbitrary noise.

3. The claimed 25-case population is self-rostered. native_claim_report derives both the roster and the rows from the same cases = native_crypto_cases() value. Removing order_n_cases() (or any vector case) shrinks both sides together and the instrument remains green, so the identity join establishes internal report consistency, not preservation of the evidence population named by this target. Bind the target to an independently declared expected identity population (or an equivalent monotone roster authority) and join the executed rows to that population. A mutation removing one case while leaving the target's authority unchanged must produce no observation. This is especially load-bearing for p256_the_base_point_has_order_n, which the frontier names.

Evidence rebind: the PR body’s actual native build-and-run is at 274af55; this live head merged main and regenerated the NativeClaimDriver mirrors afterward. The five ordinary CI checks are green, but none invokes //gunbc/instruments:native-crypto-vectors. After the protocol repairs, rerun the 25/25 execution and the corrupted-digest RED at the resulting exact head.

Non-blocking cleanup while touching the receipt: the RFM/std.bitwise prose says word32_xor forms a + b, but the current implementation is nibble-folded and does not. The Int retype still has a valid basis (the phantom does not enforce the range, and other word helpers use the 2^32 boundary), but that specific causal sentence should be corrected.

No objection remains to keeping P-384/P2b, the App Attest fold/P3, the route binding/C, and merge-path enforcement as separate later triggers.

[gunbai-bot]

Re the side-chat source hold (GitHub review 5311497200 at a329a2b): all three fail-open defects are fixed at a4e53ea.

1. Closed terminal. std.compiler_entry NativeClaimReport now carries terminal: NativeClaimTerminal (NativeClaimHeld | NativeClaimNotHeld { reason } | NativeClaimNoObservation { reason }), not a ProcessExit. The rendered main maps the three arms to fixed statuses 0, 1 and 2 and takes no code from the program, so a failure spelled as 0 or an out-of-vocabulary code can't be written. test.claim.entry_authority_witness requires NativeClaimHeld => std::process::exit(0) plus exit(1) and exit(2), and forbids *code as i32. The reader still refuses any status outside {0, 1} as no observation (a claim with status 3), and treats 2 as the program's own no-observation.
2. Strict whole-report parser. gunbc.native_claim_program parses the ENTIRE non-empty line population into NativeClaimReportParsed { roster, rows } or NativeClaimReportMalformed { reason }: exactly one roster line, first, with non-empty unique identities; then only case <id> held|not_held observed=<text> rows. New reds, each → no observation: an unknown verdict (case z nonsense), a row with no observed=, a noise line, a second roster line, and a duplicate roster identity.
3. Independent roster. The program prints its roster from the DECLARED native_crypto_expected_identities (25 literal identities, monotone by review), not from native_crypto_cases().

Also: the stale "word32_xor forms a + b" prose is fixed (it's word32_add that reaches 2^33 − 2). The three std_process/process-exit mirrors left the seed closure (compiler_entry no longer imports std.process) and are deleted, as the regen directs.

Evidence at a4e53ea (a fresh worktree, 0 changed files, local build exit 0, HEAD verified before and after):

check	result
seed	regen pass 1 exit 0, first_generation_equal=true, 0 seed changes; fixed point exit 0
gunbc test //gunbc/instruments:native-crypto-vectors	exit 0, 25 rows, 25 held, roster of 25
corrupted sha256_abc published digest	exit 1, not held: sha256_abc
removed-case mutation (order_n_cases() dropped from the case list)	the program exited 0 with 23 all-held rows, and the reader says no observation: "rows do not join the roster one-for-one at: p256_the_base_point_has_order_n,p256_red_n_minus_one_times_g_is_finite" (gunbc test exit 2)
test.claim.native_claim_program_standing_witness	16/16 (held, not held, and 14 no-observation reds)
test.claim.entry_authority_witness	8/8
test.claim.seed_growth_admission_witness	7/7
gunbc test //gunbc/instruments:self-host	exit 0

— sent from swift-bat-511

[briansrls]

APPROVE-MERGE at exact head a4e53ea29611dc79ab15a790de11ccaf03681e90.

This supersedes CHANGES_REQUESTED review 5311497200. All three fail-open findings are discharged.

1. The process terminal is now closed. NativeClaimReport carries NativeClaimTerminal = NativeClaimHeld | NativeClaimNotHeld { reason } | NativeClaimNoObservation { reason }, and the generated main maps those arms to fixed statuses 0, 1 and 2. No program-chosen integer crosses the process boundary; the entry-authority witness requires the three fixed mappings and forbids *code as i32. The reader additionally maps a raw status 3, a signal, or any row/status contradiction to no observation.

2. The reader parses the whole non-empty report. It requires one first roster line with non-empty unique identities, then only exact case <id> held|not_held observed=<text> rows. Unknown verdicts, missing observed fields, noise, a second roster, duplicate roster identities, duplicate case rows, missing rows and unknown rows all become no observation rather than disappearing before the join. Positive held and not-held controls keep this from being a refuse-everything parser.

3. The 25-case population is independently declared as native_crypto_expected_identities, and the program prints that roster rather than deriving it from native_crypto_cases(). The removed-order_n_cases() mutation therefore leaves the two order-n identities owed: the emitted program exits 0 with 23 held rows, while the reader returns status 2 and names both missing identities. This directly discriminates the earlier self-roster hole.

The native execution has been rerun on this exact source: 25/25 held; corrupted sha256_abc exits 1; the removed-case mutation yields no observation; entry-authority 8/8, reader 16/16, seed-growth 7/7, self-host exit 0, and regeneration is at a fixed point. The stale word32_xor account is corrected to the actual word32_add range argument.

Run 36080624255 passes compiler, clippy, emit-build, floor and witnesses at this exact SHA. GitHub reports CLEAN and mergeable.

No source condition remains unless the head moves. P-384/P2b, the App Attest fold program/P3, device-route binding/C and merge-path enforcement remain correctly explicit later triggers rather than being retired here.

[briansrls]

APPROVE-MERGE at exact head 3a66d24471ccff1dd4d2cf07369747c629998b3c.

This rebinds the accepted source at a4e53ea29611dc79ab15a790de11ccaf03681e90 across the integration-only delta.

• Main was merged; the emitter mirror took main's side and was then regenerated from the merged authority.
• The merge-group dequeue was a correct #12205 refusal: both new modules used bare filter while already declaring imports. dag/gunbc/instruments/native_crypto_vectors.dag and dag/gunbc/native_claim_program.dag now explicitly import filter from v2.std.algebra, matching the corpus convention. No roster exception or gate weakening was introduced.
• The seed converged on pass 2 with the NativeClaimDriver emitter arms. The closed 0/1/2 terminal, total report parser, independent 25-identity roster, and removed-case no-observation wall are unchanged.

Exact-head evidence remains discriminating: 25/25 native cases held; corrupting sha256_abc exits 1 and names it; removing the two order-n cases leaves the program locally green but makes the reader exit 2 and name both missing roster identities; entry-authority 8/8, reader 16/16, seed-growth 7/7, and self-host exit 0.

Run 36126947589 passes compiler, clippy, emit-build, floor, and witnesses at this SHA. GitHub reports CLEAN and mergeable.

No source condition remains unless the head moves. P-384/P2b, the App Attest fold program/P3, device-route realization/C, and merge-path enforcement remain correctly standing.