saymrwulf/proof-aware-crypto-tooling-agent
1
0
Fork 0
mirror of https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git synced 2026-09-03 19:53:43 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

replay: compile the certificate corpus, not the button's instruments; forks attest 44

Browse source 
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 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-08-07 10:24:35 +02:00
parent 3a7a56c4e5
commit ab629f34d8
3 changed files with 355 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

320
examples/repos.yaml
View file

@ -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

24
provider/src/pacta_provider/service.py
View file

@ -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,

12
src/pacta/config.py
View file

@ -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 [])],
)