From ab629f34d871a48141eeb8f3e024811bbfa3accb Mon Sep 17 00:00:00 2001 From: mrwulf Date: Fri, 7 Aug 2026 10:24:35 +0200 Subject: [PATCH] replay: compile the certificate corpus, not the button's instruments; forks attest 44 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the two halves of replay-pipeline-lags-hardened-forks. (1) The generic replay compiled every .lean under verification/, including the P1-b kernel-gate instruments (Proofs/Inventory*.lean) that read other modules' object files via readModuleData and only run inside the button's environment; it died with "object file does not exist". New RepoConfig.replay_exclude (globs, per repo, in the config where a reviewer sees them) filters the compile; every exclusion actually applied is recorded in the attestation's replay.instruments_excluded, so the LEAF discloses what its replay did not compile — a silent exclusion here would be the estate's oldest defect class. The replay checks the certificates; the deeper self-auditing gates are the repository's own and run there. (2) The ed25519 profile's default list still carried the 16 pre-hardening certificates, so a successful replay would have attested 16 and the whole 16->44 point of the re-attestation would have been lost silently. Each fork entry now carries its own 44 — 27 main + 4 apex + 13 scalar — MEASURED from the fork's two buttons (CERTS arrays; apex recovered by the same pattern Phase 3c itself uses), never hand-typed. Correction to the plan on the way through: the plan said 40; the apex tier makes it 44. Suite: 152 passed, 0 failed, 0 skipped. Co-Authored-By: Claude Opus 4.8 --- examples/repos.yaml | 320 +++++++++++++++++++++++++ provider/src/pacta_provider/service.py | 24 +- src/pacta/config.py | 12 + 3 files changed, 355 insertions(+), 1 deletion(-) diff --git a/examples/repos.yaml b/examples/repos.yaml index 622132c..8ca4d64 100644 --- a/examples/repos.yaml +++ b/examples/repos.yaml @@ -16,6 +16,86 @@ repos: - compiler correctness - SIMD/AVX/accelerator paths + # certificates + imports MEASURED from the two buttons (CERTS arrays; + # apex recovered the way Phase 3c itself recovers it). replay_exclude: + # the button-owned audit instruments the replay does not compile — + # disclosed per-leaf in replay.instruments_excluded. + certificates: + - CurveFieldProofs.fieldImplementation + - CurveFieldProofs.edwardsImplementation + - CurveFieldProofs.naf_table_spec + - CurveFieldProofs.naf_select_spec + - CurveFieldProofs.proj_double_law + - CurveFieldProofs.compl_as_projective_law + - CurveFieldProofs.dsm_step_p_law + - CurveFieldProofs.dsm_step_b_law + - CurveFieldProofs.dsm_loop_spec + - CurveFieldProofs.naf_load_spec + - CurveFieldProofs.naf_exit + - CurveFieldProofs.naf_digit_loop_spec + - CurveFieldProofs.non_adjacent_form_spec + - CurveFieldProofs.run_basepoint + - CurveFieldProofs.vartime_double_base_mul_spec + - CurveFieldProofs.verify_loop_full + - CurveFieldProofs.to_bytes_spec + - CurveFieldProofs.ed_compress_spec + - ScalarProofs.from_bytes_mod_order_wide_spec + - CurveFieldProofs.vartime_dsm_basepoint_spec + - CurveFieldProofs.enc_point_inj + - CurveFieldProofs.pow_p58_spec + - CurveFieldProofs.fe_ct_eq_spec + - CurveFieldProofs.sqrt_core + - CurveFieldProofs.sqrt_ratio_i_sq_spec + - CurveFieldProofs.from_bytes_spec + - CurveFieldProofs.decompress_of_canonical + - CurveFieldProofs.verify_accepts_iff + - CurveFieldProofs.verify_accepts_iff_decompress + - CurveFieldProofs.verify_accepts_iff_point + - CurveFieldProofs.verify_accepts_iff_point_eq + - ScalarProofs.L_val + - ScalarProofs.sub_loop_spec + - ScalarProofs.cond_add_l_one_spec + - ScalarProofs.sub_val_spec + - ScalarProofs.add_val_spec + - ScalarProofs.mul_internal_spec + - ScalarProofs.part1_spec + - ScalarProofs.montgomery_reduce_spec + - ScalarProofs.mul_spec + - ScalarProofs.scalarImplementation + - ScalarProofs.montgomery_mul_spec + - ScalarProofs.bytes_unpack_spec + - ScalarProofs.from_bytes_wide_spec + axiom_imports: + - Proofs.FieldMain + - Proofs.EdMain + - Proofs.ScalarMain + - Proofs.ToBytesSpec + - Proofs.CompressSpec + - Proofs.ScalarPackSpec + - Proofs.DsmMulSpec + - Proofs.SigApexSpec + - Proofs.PointLiftSpec + - Proofs.PointEqSpec + - Proofs.DecompressSpec + - Proofs.FromBytesSpec + - Proofs.DecompressMain + - Proofs.ScalarDenote + - Proofs.ScalarLoop + - Proofs.ScalarSubSpec + - Proofs.ScalarAddSpec + - Proofs.ScalarMulSpec + - Proofs.ScalarMontSpec + - Proofs.ScalarReduceSpec + - Proofs.ScalarFullMulSpec + - Proofs.ScalarWideSpec + - Proofs.ScalarBytesSpec + - Proofs.ScalarUnpackSpec + - Proofs.ScalarFromBytesSpec + replay_exclude: + - "Proofs/Audit.lean" + - "Proofs/ScalarAudit.lean" + - "Proofs/AxiomCheck.lean" + - "Proofs/Inventory*.lean" - name: anza-ed25519-verified url: https://github.com/saymrwulf/anza-ed25519-verified.git kind: ed25519 @@ -32,6 +112,86 @@ repos: - the default HEEA/Zebra verify() path - accelerator paths + # certificates + imports MEASURED from the two buttons (CERTS arrays; + # apex recovered the way Phase 3c itself recovers it). replay_exclude: + # the button-owned audit instruments the replay does not compile — + # disclosed per-leaf in replay.instruments_excluded. + certificates: + - CurveFieldProofs.fieldImplementation + - CurveFieldProofs.edwardsImplementation + - CurveFieldProofs.naf_table_spec + - CurveFieldProofs.naf_select_spec + - CurveFieldProofs.proj_double_law + - CurveFieldProofs.compl_as_projective_law + - CurveFieldProofs.dsm_step_p_law + - CurveFieldProofs.dsm_step_b_law + - CurveFieldProofs.dsm_loop_spec + - CurveFieldProofs.naf_load_spec + - CurveFieldProofs.naf_exit + - CurveFieldProofs.naf_digit_loop_spec + - CurveFieldProofs.non_adjacent_form_spec + - CurveFieldProofs.run_basepoint + - CurveFieldProofs.vartime_double_base_mul_spec + - CurveFieldProofs.verify_loop_full + - CurveFieldProofs.to_bytes_spec + - CurveFieldProofs.ed_compress_spec + - ScalarProofs.from_bytes_mod_order_wide_spec + - CurveFieldProofs.vartime_dsm_basepoint_spec + - CurveFieldProofs.enc_point_inj + - CurveFieldProofs.pow_p58_spec + - CurveFieldProofs.fe_ct_eq_spec + - CurveFieldProofs.sqrt_core + - CurveFieldProofs.sqrt_ratio_i_sq_spec + - CurveFieldProofs.from_bytes_spec + - CurveFieldProofs.decompress_of_canonical + - CurveFieldProofs.verify_accepts_iff + - CurveFieldProofs.verify_accepts_iff_decompress + - CurveFieldProofs.verify_accepts_iff_point + - CurveFieldProofs.verify_accepts_iff_point_eq + - ScalarProofs.L_val + - ScalarProofs.sub_loop_spec + - ScalarProofs.cond_add_l_one_spec + - ScalarProofs.sub_val_spec + - ScalarProofs.add_val_spec + - ScalarProofs.mul_internal_spec + - ScalarProofs.part1_spec + - ScalarProofs.montgomery_reduce_spec + - ScalarProofs.mul_spec + - ScalarProofs.scalarImplementation + - ScalarProofs.montgomery_mul_spec + - ScalarProofs.bytes_unpack_spec + - ScalarProofs.from_bytes_wide_spec + axiom_imports: + - Proofs.FieldMain + - Proofs.EdMain + - Proofs.ScalarMain + - Proofs.ToBytesSpec + - Proofs.CompressSpec + - Proofs.ScalarPackSpec + - Proofs.DsmMulSpec + - Proofs.SigApexSpec + - Proofs.PointLiftSpec + - Proofs.PointEqSpec + - Proofs.DecompressSpec + - Proofs.FromBytesSpec + - Proofs.DecompressMain + - Proofs.ScalarDenote + - Proofs.ScalarLoop + - Proofs.ScalarSubSpec + - Proofs.ScalarAddSpec + - Proofs.ScalarMulSpec + - Proofs.ScalarMontSpec + - Proofs.ScalarReduceSpec + - Proofs.ScalarFullMulSpec + - Proofs.ScalarWideSpec + - Proofs.ScalarBytesSpec + - Proofs.ScalarUnpackSpec + - Proofs.ScalarFromBytesSpec + replay_exclude: + - "Proofs/Audit.lean" + - "Proofs/ScalarAudit.lean" + - "Proofs/AxiomCheck.lean" + - "Proofs/Inventory*.lean" - name: risc0-ed25519-verified url: https://github.com/saymrwulf/risc0-ed25519-verified.git kind: ed25519 @@ -43,6 +203,86 @@ repos: lean_guard: verification/lean-guard backend_warning: pure Rust path only; do not treat zkVM accelerator/syscall path as verified + # certificates + imports MEASURED from the two buttons (CERTS arrays; + # apex recovered the way Phase 3c itself recovers it). replay_exclude: + # the button-owned audit instruments the replay does not compile — + # disclosed per-leaf in replay.instruments_excluded. + certificates: + - CurveFieldProofs.fieldImplementation + - CurveFieldProofs.edwardsImplementation + - CurveFieldProofs.naf_table_spec + - CurveFieldProofs.naf_select_spec + - CurveFieldProofs.proj_double_law + - CurveFieldProofs.compl_as_projective_law + - CurveFieldProofs.dsm_step_p_law + - CurveFieldProofs.dsm_step_b_law + - CurveFieldProofs.dsm_loop_spec + - CurveFieldProofs.naf_load_spec + - CurveFieldProofs.naf_exit + - CurveFieldProofs.naf_digit_loop_spec + - CurveFieldProofs.non_adjacent_form_spec + - CurveFieldProofs.run_basepoint + - CurveFieldProofs.vartime_double_base_mul_spec + - CurveFieldProofs.verify_loop_full + - CurveFieldProofs.to_bytes_spec + - CurveFieldProofs.ed_compress_spec + - ScalarProofs.from_bytes_mod_order_wide_spec + - CurveFieldProofs.vartime_dsm_basepoint_spec + - CurveFieldProofs.enc_point_inj + - CurveFieldProofs.pow_p58_spec + - CurveFieldProofs.fe_ct_eq_spec + - CurveFieldProofs.sqrt_core + - CurveFieldProofs.sqrt_ratio_i_sq_spec + - CurveFieldProofs.from_bytes_spec + - CurveFieldProofs.decompress_of_canonical + - CurveFieldProofs.verify_accepts_iff + - CurveFieldProofs.verify_accepts_iff_decompress + - CurveFieldProofs.verify_accepts_iff_point + - CurveFieldProofs.verify_accepts_iff_point_eq + - ScalarProofs.L_val + - ScalarProofs.sub_loop_spec + - ScalarProofs.sub_loop1_one_spec + - ScalarProofs.sub_val_spec + - ScalarProofs.add_val_spec + - ScalarProofs.mul_internal_spec + - ScalarProofs.part1_spec + - ScalarProofs.montgomery_reduce_spec + - ScalarProofs.mul_spec + - ScalarProofs.scalarImplementation + - ScalarProofs.montgomery_mul_spec + - ScalarProofs.bytes_unpack_spec + - ScalarProofs.from_bytes_wide_spec + axiom_imports: + - Proofs.FieldMain + - Proofs.EdMain + - Proofs.ScalarMain + - Proofs.ToBytesSpec + - Proofs.CompressSpec + - Proofs.ScalarPackSpec + - Proofs.DsmMulSpec + - Proofs.SigApexSpec + - Proofs.PointLiftSpec + - Proofs.PointEqSpec + - Proofs.DecompressSpec + - Proofs.FromBytesSpec + - Proofs.DecompressMain + - Proofs.ScalarDenote + - Proofs.ScalarLoop + - Proofs.ScalarSubSpec + - Proofs.ScalarAddSpec + - Proofs.ScalarMulSpec + - Proofs.ScalarMontSpec + - Proofs.ScalarReduceSpec + - Proofs.ScalarFullMulSpec + - Proofs.ScalarWideSpec + - Proofs.ScalarBytesSpec + - Proofs.ScalarUnpackSpec + - Proofs.ScalarFromBytesSpec + replay_exclude: + - "Proofs/Audit.lean" + - "Proofs/ScalarAudit.lean" + - "Proofs/AxiomCheck.lean" + - "Proofs/Inventory*.lean" - name: betrusted-ed25519-verified url: https://github.com/saymrwulf/betrusted-ed25519-verified.git kind: ed25519 @@ -54,6 +294,86 @@ repos: lean_guard: verification/lean-guard backend_warning: pure Rust path only; do not treat Engine25519/hardware accelerator as verified + # certificates + imports MEASURED from the two buttons (CERTS arrays; + # apex recovered the way Phase 3c itself recovers it). replay_exclude: + # the button-owned audit instruments the replay does not compile — + # disclosed per-leaf in replay.instruments_excluded. + certificates: + - CurveFieldProofs.fieldImplementation + - CurveFieldProofs.edwardsImplementation + - CurveFieldProofs.naf_table_spec + - CurveFieldProofs.naf_select_spec + - CurveFieldProofs.proj_double_law + - CurveFieldProofs.compl_as_projective_law + - CurveFieldProofs.dsm_step_p_law + - CurveFieldProofs.dsm_step_b_law + - CurveFieldProofs.dsm_loop_spec + - CurveFieldProofs.naf_load_spec + - CurveFieldProofs.naf_exit + - CurveFieldProofs.naf_digit_loop_spec + - CurveFieldProofs.non_adjacent_form_spec + - CurveFieldProofs.run_basepoint + - CurveFieldProofs.vartime_double_base_mul_spec + - CurveFieldProofs.verify_loop_full + - CurveFieldProofs.to_bytes_spec + - CurveFieldProofs.ed_compress_spec + - ScalarProofs.from_bytes_mod_order_wide_spec + - CurveFieldProofs.vartime_dsm_basepoint_spec + - CurveFieldProofs.enc_point_inj + - CurveFieldProofs.pow_p58_spec + - CurveFieldProofs.fe_ct_eq_spec + - CurveFieldProofs.sqrt_core + - CurveFieldProofs.sqrt_ratio_i_sq_spec + - CurveFieldProofs.from_bytes_spec + - CurveFieldProofs.decompress_of_canonical + - CurveFieldProofs.verify_accepts_iff + - CurveFieldProofs.verify_accepts_iff_decompress + - CurveFieldProofs.verify_accepts_iff_point + - CurveFieldProofs.verify_accepts_iff_point_eq + - ScalarProofs.L_val + - ScalarProofs.sub_loop_spec + - ScalarProofs.sub_loop1_one_spec + - ScalarProofs.sub_val_spec + - ScalarProofs.add_val_spec + - ScalarProofs.mul_internal_spec + - ScalarProofs.part1_spec + - ScalarProofs.montgomery_reduce_spec + - ScalarProofs.mul_spec + - ScalarProofs.scalarImplementation + - ScalarProofs.montgomery_mul_spec + - ScalarProofs.bytes_unpack_spec + - ScalarProofs.from_bytes_wide_spec + axiom_imports: + - Proofs.FieldMain + - Proofs.EdMain + - Proofs.ScalarMain + - Proofs.ToBytesSpec + - Proofs.CompressSpec + - Proofs.ScalarPackSpec + - Proofs.DsmMulSpec + - Proofs.SigApexSpec + - Proofs.PointLiftSpec + - Proofs.PointEqSpec + - Proofs.DecompressSpec + - Proofs.FromBytesSpec + - Proofs.DecompressMain + - Proofs.ScalarDenote + - Proofs.ScalarLoop + - Proofs.ScalarSubSpec + - Proofs.ScalarAddSpec + - Proofs.ScalarMulSpec + - Proofs.ScalarMontSpec + - Proofs.ScalarReduceSpec + - Proofs.ScalarFullMulSpec + - Proofs.ScalarWideSpec + - Proofs.ScalarBytesSpec + - Proofs.ScalarUnpackSpec + - Proofs.ScalarFromBytesSpec + replay_exclude: + - "Proofs/Audit.lean" + - "Proofs/ScalarAudit.lean" + - "Proofs/AxiomCheck.lean" + - "Proofs/Inventory*.lean" - name: pasta-pallas-verified url: https://github.com/saymrwulf/pasta-pallas-verified.git kind: pasta_pallas diff --git a/provider/src/pacta_provider/service.py b/provider/src/pacta_provider/service.py index a93d12d..0053b49 100644 --- a/provider/src/pacta_provider/service.py +++ b/provider/src/pacta_provider/service.py @@ -30,8 +30,26 @@ def build_attestation( profile = get_profile(repo.kind, repo) layout = discover_layout(path, repo.verification_dir) lean_guard = resolve_lean_guard(repo.lean_guard, path) + # The replay compiles the certificate corpus, not the button's audit + # instruments (see RepoConfig.replay_exclude). Filter by the path relative + # to the verification dir; record what was actually excluded so the LEAF + # says it — a silent exclusion here would be the exact defect class the + # estate keeps finding. + import fnmatch as _fnmatch + verification_root = path / repo.verification_dir + compile_order = layout.compile_order + instruments_excluded: list[str] = [] + if repo.replay_exclude: + kept = [] + for f in compile_order: + rel = str(Path(f).resolve().relative_to(verification_root.resolve())) + if any(_fnmatch.fnmatch(rel, g) for g in repo.replay_exclude): + instruments_excluded.append(rel) + else: + kept.append(f) + compile_order = kept check = lean_check_files( - layout.compile_order, + compile_order, layout.verification_dir, timeout=timeout, log_dir=log_dir, @@ -103,6 +121,10 @@ def build_attestation( "check_log_path": check.log_path, "checked_files": len(check.checked_files), "failed_files": check.failed_files, + # The button's audit instruments this replay did NOT compile — + # disclosed in the leaf rather than silently absent. Empty for + # repositories without a replay_exclude list. + "instruments_excluded": sorted(instruments_excluded), "diagnostics": check.diagnostics, "axiom_attempted": axiom.attempted if axiom else False, "axiom_ok": axiom.ok if axiom else False, diff --git a/src/pacta/config.py b/src/pacta/config.py index a531c1f..7d4ce11 100644 --- a/src/pacta/config.py +++ b/src/pacta/config.py @@ -28,6 +28,17 @@ class RepoConfig: env_script: str | None = None lean_project_dir: str | None = None lean_guard: str | None = None + # Files the provider REPLAY does not compile (globs relative to the + # verification dir). Exists because the hardened forks ship audit + # INSTRUMENTS — kernel-gate modules that read other modules' object files + # via readModuleData and only run inside the button's own environment + # (its cwd, LEAN_PATH and compile order). The replay's generic + # topological compile breaks on them (register: + # replay-pipeline-lags-hardened-forks). The replay checks the CERTIFICATES; + # the deeper self-auditing gates are the repository's own and run there. + # Every exclusion actually applied is recorded in the attestation's replay + # block, so the leaf discloses what its replay did not compile. + replay_exclude: list[str] = field(default_factory=list) @classmethod def from_dict(cls, raw: dict[str, Any]) -> "RepoConfig": @@ -53,6 +64,7 @@ class RepoConfig: env_script=raw.get("env_script"), lean_project_dir=raw.get("lean_project_dir"), lean_guard=raw.get("lean_guard"), + replay_exclude=[str(g) for g in (raw.get("replay_exclude") or [])], )