From 2d77a2ba2fa7ad71706ef299567b2b494cb729ef Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 6 Jul 2026 16:02:23 +0200 Subject: [PATCH] Genesis publication: 8 leaves, 4 attested libraries, dogfood-signed head The public face of the Lean Transparency Log: every leaf (including the first run's honest audit-failure attestations), the full STH history (witness channel), per-component receipts, the provider public key, and a standalone stdlib-only verify.py. Co-Authored-By: Claude Fable 5 --- README.md | 39 ++ entries/000000.json | 278 +++++++++++++ entries/000001.json | 262 ++++++++++++ entries/000002.json | 266 +++++++++++++ entries/000003.json | 266 +++++++++++++ entries/000004.json | 372 ++++++++++++++++++ entries/000005.json | 340 ++++++++++++++++ entries/000006.json | 348 ++++++++++++++++ entries/000007.json | 348 ++++++++++++++++ .../anza-ed25519-verified.attestation.json | 332 ++++++++++++++++ ...etrusted-ed25519-verified.attestation.json | 340 ++++++++++++++++ .../dalek-ed25519-verified.attestation.json | 364 +++++++++++++++++ .../risc0-ed25519-verified.attestation.json | 340 ++++++++++++++++ latest-sth.json | 33 ++ log-metadata.json | 14 + provider.ed25519.pub | 3 + receipts/anza-ed25519-verified.receipt.json | 47 +++ .../betrusted-ed25519-verified.receipt.json | 47 +++ receipts/dalek-ed25519-verified.receipt.json | 47 +++ receipts/risc0-ed25519-verified.receipt.json | 47 +++ sth-history.jsonl | 1 + verify.py | 153 +++++++ 22 files changed, 4287 insertions(+) create mode 100644 README.md create mode 100644 entries/000000.json create mode 100644 entries/000001.json create mode 100644 entries/000002.json create mode 100644 entries/000003.json create mode 100644 entries/000004.json create mode 100644 entries/000005.json create mode 100644 entries/000006.json create mode 100644 entries/000007.json create mode 100644 entries/anza-ed25519-verified.attestation.json create mode 100644 entries/betrusted-ed25519-verified.attestation.json create mode 100644 entries/dalek-ed25519-verified.attestation.json create mode 100644 entries/risc0-ed25519-verified.attestation.json create mode 100644 latest-sth.json create mode 100644 log-metadata.json create mode 100644 provider.ed25519.pub create mode 100644 receipts/anza-ed25519-verified.receipt.json create mode 100644 receipts/betrusted-ed25519-verified.receipt.json create mode 100644 receipts/dalek-ed25519-verified.receipt.json create mode 100644 receipts/risc0-ed25519-verified.receipt.json create mode 100644 sth-history.jsonl create mode 100644 verify.py diff --git a/README.md b/README.md new file mode 100644 index 0000000..fd42117 --- /dev/null +++ b/README.md @@ -0,0 +1,39 @@ +# Lean Transparency Log — published mirror + +This repository is the **git-published face** of a transparency log of +formal-verification attestations: signed statements that the Lean 4 proofs +of specific cryptographic Rust libraries, at specific git commits, +re-check with exactly their documented assumptions. + +Layout: + +| Path | Content | +|---|---| +| `entries/NNNNNN.json` | one log leaf per file, append-only (git history mirrors log history) | +| `entries/.attestation.json` | the newest attestation per library, for convenience | +| `receipts/.receipt.json` | inclusion proof binding that attestation to the latest signed head | +| `sth-history.jsonl` | **every** Signed Tree Head ever issued — the witness channel: all cloners see the same heads | +| `latest-sth.json` | the current head | +| `provider.ed25519.pub` | the provider's public key (the sole trust anchor) | +| `verify.py` | standalone verifier, Python standard library only | + +Verify everything locally, no installation: + +```bash +python3 verify.py --all +python3 verify.py --receipt receipts/dalek-ed25519-verified.receipt.json +``` + +The online service (same data, live endpoints + customer documentation): +**https://zkdefi.org/lean-transparency-log** + +The provider tooling, agent tooling, and course materials: +**https://github.com/saymrwulf/proof-aware-crypto-tooling-agent** + +Honesty notes, always in force: attestations cover Rust **source** at a +pinned commit (clone it — the git hash is the content hash — and build it +yourself; compilers are declared trusted base). The log deliberately +retains early leaves recording a **failed** audit run: an append-only +trust ledger keeps its history. Tree heads are signed by the merkleized, +proof-attested Ed25519 library itself, and each signature embeds the +provider's own Merkle self-check of that library's leaf. diff --git a/entries/000000.json b/entries/000000.json new file mode 100644 index 0000000..fab46a5 --- /dev/null +++ b/entries/000000.json @@ -0,0 +1,278 @@ +{ + "index": 0, + "leaf": { + "attestation": { + "certificates": [ + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [], + "status": "failed" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T09:14:50Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/dalek-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [ + "Lean axiom audit exited with 1." + ], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": false, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 64, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "58f4bd05d7c3e1820496af5c73824a7d4ec091e22ef056a3b7637ea46899dca1", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "J3kOWCDtLQTiCLfNG7eefHFbDM1zcq6k/ooxGHl9LAGFxfQB/zva3wmoryxLE1bKeYeVViN8sfTPxufxqKtrCg==", + "status": "signed" + }, + "subject": { + "component": "dalek-ed25519-verified", + "kind": "ed25519", + "repo_commit": "8ded7bcf9a1f0016cee93f371796b935b25b7ff8", + "repo_url": "https://github.com/saymrwulf/dalek-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } + }, + "schema_version": 1, + "type": "pacta.transparency.attestation_leaf.v1" + }, + "leaf_hash": "f410f0325a5a534dd528181c8c2bd8a3e9483f994c45f7db981594364ab82185" +} diff --git a/entries/000001.json b/entries/000001.json new file mode 100644 index 0000000..25a5a67 --- /dev/null +++ b/entries/000001.json @@ -0,0 +1,262 @@ +{ + "index": 1, + "leaf": { + "attestation": { + "certificates": [ + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [], + "status": "failed" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T09:45:09Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/anza-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [ + "Lean axiom audit exited with 1." + ], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": false, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 58, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "0c24f5d9a5d97ea87c21b9c43b3f2e4fa6801fcac4d00ac56d450fc54db56cb3", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "tEXyJfXUFIetLFRNAFPGliNyxJHWVWxuoVaUjhVO1O6FmDwPIgVdZTLPXeGxW722Sws4KV9krxFJ8DtyzR+0BQ==", + "status": "signed" + }, + "subject": { + "component": "anza-ed25519-verified", + "kind": "ed25519", + "repo_commit": "673c15e10a082788f7965fcb0faeefcca0d15136", + "repo_url": "https://github.com/saymrwulf/anza-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } + }, + "schema_version": 1, + "type": "pacta.transparency.attestation_leaf.v1" + }, + "leaf_hash": "e7ec074ddb67945431c2bc9237ca5760ad351a324757de66f3374e47163c71f7" +} diff --git a/entries/000002.json b/entries/000002.json new file mode 100644 index 0000000..8eda921 --- /dev/null +++ b/entries/000002.json @@ -0,0 +1,266 @@ +{ + "index": 2, + "leaf": { + "attestation": { + "certificates": [ + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [], + "status": "failed" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T10:16:56Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/risc0-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [ + "Lean axiom audit exited with 1." + ], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": false, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 63, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "66b9000bc5c538420b8569c843d55d5c458fecded98aea6b528086a15d5ff4b5", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "e5p1i8z+0RAKlGFn+7gjSfqHXGJ3hMiKspyksEXSa7a8i8IvgzWdYz2G/B+pyYfVr1Tp+DA5vkBjfkCXmMXNDw==", + "status": "signed" + }, + "subject": { + "component": "risc0-ed25519-verified", + "kind": "ed25519", + "repo_commit": "98a13a68539b20ac0279876848aea3687e523462", + "repo_url": "https://github.com/saymrwulf/risc0-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } + }, + "schema_version": 1, + "type": "pacta.transparency.attestation_leaf.v1" + }, + "leaf_hash": "54be4a0c3aefc4999c4493d82cc4a97b7acec3b1ebb83274a43cec25e3d3a225" +} diff --git a/entries/000003.json b/entries/000003.json new file mode 100644 index 0000000..24b6427 --- /dev/null +++ b/entries/000003.json @@ -0,0 +1,266 @@ +{ + "index": 3, + "leaf": { + "attestation": { + "certificates": [ + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [], + "status": "failed" + }, + { + "axiom_status": "not_checked", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [], + "status": "failed" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T10:48:39Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/betrusted-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [ + "Lean axiom audit exited with 1." + ], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": false, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 63, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "83ebdbf3a1460bac5ea00e194465e05b6f07d289d9c8f854d84118d53b203e94", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "NFfmwHB+TB1fn6yCeGmWrtn+q/wfqCeuhtUfZz58mzzfdBQzyiA02BQhbJmIa2s+XRbOtZX46/W1//owUdFNBA==", + "status": "signed" + }, + "subject": { + "component": "betrusted-ed25519-verified", + "kind": "ed25519", + "repo_commit": "81f614a3cbd26412c6af7f0a31c0f128121fbfa4", + "repo_url": "https://github.com/saymrwulf/betrusted-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } + }, + "schema_version": 1, + "type": "pacta.transparency.attestation_leaf.v1" + }, + "leaf_hash": "c6c8bddd4536aee266214cde27e38e2bf720ebcd94a0cdaf82b35e148e6f01fc" +} diff --git a/entries/000004.json b/entries/000004.json new file mode 100644 index 0000000..3d77352 --- /dev/null +++ b/entries/000004.json @@ -0,0 +1,372 @@ +{ + "index": 4, + "leaf": { + "attestation": { + "certificates": [ + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_finalize_bytes", + "verifying.sha512_new", + "verifying.sha512_update", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_finalize_bytes", + "verifying.sha512_new", + "verifying.sha512_update", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_finalize_bytes", + "verifying.sha512_new", + "verifying.sha512_update", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_finalize_bytes", + "verifying.sha512_new", + "verifying.sha512_update", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T11:21:25Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/dalek-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": true, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 64, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "ba9c3de2b75af13cd79aaaf1226a07c3e671f2d5fe06dd2a33810588dfe21571", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "Ec0xxNT6PeyuNXUncaeZN9iDJN/q3W/WenqGrx3qWDfYu9xK5Hq7e4zLALqZKrNCBaPXBm4oSYKUd1qSNoWSBg==", + "status": "signed" + }, + "subject": { + "component": "dalek-ed25519-verified", + "kind": "ed25519", + "repo_commit": "8ded7bcf9a1f0016cee93f371796b935b25b7ff8", + "repo_url": "https://github.com/saymrwulf/dalek-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } + }, + "schema_version": 1, + "type": "pacta.transparency.attestation_leaf.v1" + }, + "leaf_hash": "ca164b6cf11aec6a4c8de2d18c2c2fa04c9323657bd7daf4e7111869201bfec2" +} diff --git a/entries/000005.json b/entries/000005.json new file mode 100644 index 0000000..6f327de --- /dev/null +++ b/entries/000005.json @@ -0,0 +1,340 @@ +{ + "index": 5, + "leaf": { + "attestation": { + "certificates": [ + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "status": "proven" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T11:51:00Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/anza-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": true, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 58, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "ff36182e67d083ac442fce5026fe31ae8127b4f04bc6b5a85b70c9cae9ed8f8d", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "fFGMNOf1a1sk14Cu2BLP2Dl4DWcipXJiPe7KlZuHyCXyhz91NEuLr4VObIa4wP9J61PThXwVwLDEnnHuOH6BCA==", + "status": "signed" + }, + "subject": { + "component": "anza-ed25519-verified", + "kind": "ed25519", + "repo_commit": "673c15e10a082788f7965fcb0faeefcca0d15136", + "repo_url": "https://github.com/saymrwulf/anza-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } + }, + "schema_version": 1, + "type": "pacta.transparency.attestation_leaf.v1" + }, + "leaf_hash": "33523f3ea6b6eab72696eead8534d0b7cac78feb60cc3907ac973a24f37adb95" +} diff --git a/entries/000006.json b/entries/000006.json new file mode 100644 index 0000000..dca4365 --- /dev/null +++ b/entries/000006.json @@ -0,0 +1,348 @@ +{ + "index": 6, + "leaf": { + "attestation": { + "certificates": [ + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T12:21:40Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/risc0-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": true, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 63, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "d921c5d45f8300eecc0299fc3e11506df67751506b52cda35fb61d517b27712b", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "iwi/AR0wLQiGF6p/jBr/3PV01d2m3lmQOXfc/00axng9Tj/YUymGejWuUi1ZleZL1X0cA9NTNKc5bbIT8AyPDA==", + "status": "signed" + }, + "subject": { + "component": "risc0-ed25519-verified", + "kind": "ed25519", + "repo_commit": "98a13a68539b20ac0279876848aea3687e523462", + "repo_url": "https://github.com/saymrwulf/risc0-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } + }, + "schema_version": 1, + "type": "pacta.transparency.attestation_leaf.v1" + }, + "leaf_hash": "bdde4e4b87cd263b5914dbbae0c85ceed468c3054596f6ca79121e54cc6a134e" +} diff --git a/entries/000007.json b/entries/000007.json new file mode 100644 index 0000000..a9bbb53 --- /dev/null +++ b/entries/000007.json @@ -0,0 +1,348 @@ +{ + "index": 7, + "leaf": { + "attestation": { + "certificates": [ + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T12:51:28Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/betrusted-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": true, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 63, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "bb1226fa66ae0e51677ccc8c8361ba121ac5464911f1cb9e305ff7c76b7d2c57", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "Lsxje95BPXHfc7l3wxQrRvDgG/5tb7WNaO3wIDsfY/xg/WYRDFrWF3Bb6frs0Dmln00QxA99Gt43PMxLUHq0Ag==", + "status": "signed" + }, + "subject": { + "component": "betrusted-ed25519-verified", + "kind": "ed25519", + "repo_commit": "81f614a3cbd26412c6af7f0a31c0f128121fbfa4", + "repo_url": "https://github.com/saymrwulf/betrusted-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } + }, + "schema_version": 1, + "type": "pacta.transparency.attestation_leaf.v1" + }, + "leaf_hash": "2791c352956ebc620a4fe12b20bfd6faa0813238c5bc0563fa4eb0130d829247" +} diff --git a/entries/anza-ed25519-verified.attestation.json b/entries/anza-ed25519-verified.attestation.json new file mode 100644 index 0000000..10a58d7 --- /dev/null +++ b/entries/anza-ed25519-verified.attestation.json @@ -0,0 +1,332 @@ +{ + "certificates": [ + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "status": "proven" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T11:51:00Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/anza-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": true, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 58, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "ff36182e67d083ac442fce5026fe31ae8127b4f04bc6b5a85b70c9cae9ed8f8d", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "fFGMNOf1a1sk14Cu2BLP2Dl4DWcipXJiPe7KlZuHyCXyhz91NEuLr4VObIa4wP9J61PThXwVwLDEnnHuOH6BCA==", + "status": "signed" + }, + "subject": { + "component": "anza-ed25519-verified", + "kind": "ed25519", + "repo_commit": "673c15e10a082788f7965fcb0faeefcca0d15136", + "repo_url": "https://github.com/saymrwulf/anza-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } +} diff --git a/entries/betrusted-ed25519-verified.attestation.json b/entries/betrusted-ed25519-verified.attestation.json new file mode 100644 index 0000000..8b82f89 --- /dev/null +++ b/entries/betrusted-ed25519-verified.attestation.json @@ -0,0 +1,340 @@ +{ + "certificates": [ + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T12:51:28Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/betrusted-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": true, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 63, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "bb1226fa66ae0e51677ccc8c8361ba121ac5464911f1cb9e305ff7c76b7d2c57", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "Lsxje95BPXHfc7l3wxQrRvDgG/5tb7WNaO3wIDsfY/xg/WYRDFrWF3Bb6frs0Dmln00QxA99Gt43PMxLUHq0Ag==", + "status": "signed" + }, + "subject": { + "component": "betrusted-ed25519-verified", + "kind": "ed25519", + "repo_commit": "81f614a3cbd26412c6af7f0a31c0f128121fbfa4", + "repo_url": "https://github.com/saymrwulf/betrusted-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } +} diff --git a/entries/dalek-ed25519-verified.attestation.json b/entries/dalek-ed25519-verified.attestation.json new file mode 100644 index 0000000..9a3bb82 --- /dev/null +++ b/entries/dalek-ed25519-verified.attestation.json @@ -0,0 +1,364 @@ +{ + "certificates": [ + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_finalize_bytes", + "verifying.sha512_new", + "verifying.sha512_update", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_finalize_bytes", + "verifying.sha512_new", + "verifying.sha512_update", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_finalize_bytes", + "verifying.sha512_new", + "verifying.sha512_update", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_finalize_bytes", + "verifying.sha512_new", + "verifying.sha512_update", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T11:21:25Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/dalek-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": true, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 64, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "ba9c3de2b75af13cd79aaaf1226a07c3e671f2d5fe06dd2a33810588dfe21571", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "Ec0xxNT6PeyuNXUncaeZN9iDJN/q3W/WenqGrx3qWDfYu9xK5Hq7e4zLALqZKrNCBaPXBm4oSYKUd1qSNoWSBg==", + "status": "signed" + }, + "subject": { + "component": "dalek-ed25519-verified", + "kind": "ed25519", + "repo_commit": "8ded7bcf9a1f0016cee93f371796b935b25b7ff8", + "repo_url": "https://github.com/saymrwulf/dalek-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } +} diff --git a/entries/risc0-ed25519-verified.attestation.json b/entries/risc0-ed25519-verified.attestation.json new file mode 100644 index 0000000..9f420e7 --- /dev/null +++ b/entries/risc0-ed25519-verified.attestation.json @@ -0,0 +1,340 @@ +{ + "certificates": [ + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T12:21:40Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/risc0-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": true, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 63, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "d921c5d45f8300eecc0299fc3e11506df67751506b52cda35fb61d517b27712b", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "iwi/AR0wLQiGF6p/jBr/3PV01d2m3lmQOXfc/00axng9Tj/YUymGejWuUi1ZleZL1X0cA9NTNKc5bbIT8AyPDA==", + "status": "signed" + }, + "subject": { + "component": "risc0-ed25519-verified", + "kind": "ed25519", + "repo_commit": "98a13a68539b20ac0279876848aea3687e523462", + "repo_url": "https://github.com/saymrwulf/risc0-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } +} diff --git a/latest-sth.json b/latest-sth.json new file mode 100644 index 0000000..a02637a --- /dev/null +++ b/latest-sth.json @@ -0,0 +1,33 @@ +{ + "hash_algorithm": "RFC9162_SHA256", + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "root_hash": "9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283", + "schema_version": 1, + "signatures": { + "ed25519": { + "payload_digest_sha256": "c9a3c000d448ebd35e313fac0c9ce0e1dc88ff03540b0828e5246407c75e2a1a", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "P8M4gjB7BCZblUvRtvJnbjfaTYKU4oO0/2LZwzpHIgp9fmOXGZqkqi7UaP5Fn1Kx4+RJSgyI2nnnK1pLpkV8CQ==", + "signing_backend": "verified-dalek-serial", + "signing_provenance": { + "self_inclusion": "verified", + "signing_backend": "verified-dalek-serial", + "signing_library_certificates_proven": "16/16", + "signing_library_component": "dalek-ed25519-verified", + "signing_library_leaf_index": 4, + "signing_library_source_commit": "aa0f6abc327ba2a54a534b21608ca8996cf73682" + }, + "status": "signed" + }, + "ml_dsa": { + "reason": "A backend appears available, but no ML-DSA signing key was configured for this log.", + "scheme": "ML-DSA-65", + "standard": "FIPS 204", + "status": "not_configured" + } + }, + "timestamp": "2026-07-06T13:59:16Z", + "tree_size": 8, + "type": "pacta.transparency.signed_tree_head.v1" +} diff --git a/log-metadata.json b/log-metadata.json new file mode 100644 index 0000000..2089a0c --- /dev/null +++ b/log-metadata.json @@ -0,0 +1,14 @@ +{ + "created_at": "2026-07-06T08:43:00Z", + "ed25519_public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "hash_algorithm": "RFC9162_SHA256", + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "provider": "local-pacta-provider", + "schema_version": 1, + "standards": [ + "RFC 9162 Merkle tree hash and inclusion/consistency proof algorithms", + "RFC 8032 Ed25519 signature verification via OpenSSL", + "FIPS 204 ML-DSA signature slot; must be required by policy only when a backend is configured" + ], + "type": "pacta.transparency.log_metadata.v1" +} diff --git a/provider.ed25519.pub b/provider.ed25519.pub new file mode 100644 index 0000000..de4000a --- /dev/null +++ b/provider.ed25519.pub @@ -0,0 +1,3 @@ +-----BEGIN PUBLIC KEY----- +MCowBQYDK2VwAyEAd6WIt2/WNJCcKMZGo67BQoZI84LbvLaYMvpwAWNXsxU= +-----END PUBLIC KEY----- diff --git a/receipts/anza-ed25519-verified.receipt.json b/receipts/anza-ed25519-verified.receipt.json new file mode 100644 index 0000000..1acea34 --- /dev/null +++ b/receipts/anza-ed25519-verified.receipt.json @@ -0,0 +1,47 @@ +{ + "hash_algorithm": "RFC9162_SHA256", + "inclusion_proof": [ + "ca164b6cf11aec6a4c8de2d18c2c2fa04c9323657bd7daf4e7111869201bfec2", + "3bb1e72abbc9c0b945dafde303acdab123996e41faeab49a35563886b1b41e96", + "04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed" + ], + "leaf_hash": "33523f3ea6b6eab72696eead8534d0b7cac78feb60cc3907ac973a24f37adb95", + "leaf_index": 5, + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "schema_version": 1, + "sth": { + "hash_algorithm": "RFC9162_SHA256", + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "root_hash": "9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283", + "schema_version": 1, + "signatures": { + "ed25519": { + "payload_digest_sha256": "c9a3c000d448ebd35e313fac0c9ce0e1dc88ff03540b0828e5246407c75e2a1a", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "P8M4gjB7BCZblUvRtvJnbjfaTYKU4oO0/2LZwzpHIgp9fmOXGZqkqi7UaP5Fn1Kx4+RJSgyI2nnnK1pLpkV8CQ==", + "signing_backend": "verified-dalek-serial", + "signing_provenance": { + "self_inclusion": "verified", + "signing_backend": "verified-dalek-serial", + "signing_library_certificates_proven": "16/16", + "signing_library_component": "dalek-ed25519-verified", + "signing_library_leaf_index": 4, + "signing_library_source_commit": "aa0f6abc327ba2a54a534b21608ca8996cf73682" + }, + "status": "signed" + }, + "ml_dsa": { + "reason": "A backend appears available, but no ML-DSA signing key was configured for this log.", + "scheme": "ML-DSA-65", + "standard": "FIPS 204", + "status": "not_configured" + } + }, + "timestamp": "2026-07-06T13:59:16Z", + "tree_size": 8, + "type": "pacta.transparency.signed_tree_head.v1" + }, + "tree_size": 8, + "type": "pacta.transparency.receipt.v1" +} diff --git a/receipts/betrusted-ed25519-verified.receipt.json b/receipts/betrusted-ed25519-verified.receipt.json new file mode 100644 index 0000000..d1373cd --- /dev/null +++ b/receipts/betrusted-ed25519-verified.receipt.json @@ -0,0 +1,47 @@ +{ + "hash_algorithm": "RFC9162_SHA256", + "inclusion_proof": [ + "bdde4e4b87cd263b5914dbbae0c85ceed468c3054596f6ca79121e54cc6a134e", + "f3724e66715b582c384cf49928d4705458475ea4293749989c483ab7fe9496ce", + "04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed" + ], + "leaf_hash": "2791c352956ebc620a4fe12b20bfd6faa0813238c5bc0563fa4eb0130d829247", + "leaf_index": 7, + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "schema_version": 1, + "sth": { + "hash_algorithm": "RFC9162_SHA256", + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "root_hash": "9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283", + "schema_version": 1, + "signatures": { + "ed25519": { + "payload_digest_sha256": "c9a3c000d448ebd35e313fac0c9ce0e1dc88ff03540b0828e5246407c75e2a1a", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "P8M4gjB7BCZblUvRtvJnbjfaTYKU4oO0/2LZwzpHIgp9fmOXGZqkqi7UaP5Fn1Kx4+RJSgyI2nnnK1pLpkV8CQ==", + "signing_backend": "verified-dalek-serial", + "signing_provenance": { + "self_inclusion": "verified", + "signing_backend": "verified-dalek-serial", + "signing_library_certificates_proven": "16/16", + "signing_library_component": "dalek-ed25519-verified", + "signing_library_leaf_index": 4, + "signing_library_source_commit": "aa0f6abc327ba2a54a534b21608ca8996cf73682" + }, + "status": "signed" + }, + "ml_dsa": { + "reason": "A backend appears available, but no ML-DSA signing key was configured for this log.", + "scheme": "ML-DSA-65", + "standard": "FIPS 204", + "status": "not_configured" + } + }, + "timestamp": "2026-07-06T13:59:16Z", + "tree_size": 8, + "type": "pacta.transparency.signed_tree_head.v1" + }, + "tree_size": 8, + "type": "pacta.transparency.receipt.v1" +} diff --git a/receipts/dalek-ed25519-verified.receipt.json b/receipts/dalek-ed25519-verified.receipt.json new file mode 100644 index 0000000..c68e6eb --- /dev/null +++ b/receipts/dalek-ed25519-verified.receipt.json @@ -0,0 +1,47 @@ +{ + "hash_algorithm": "RFC9162_SHA256", + "inclusion_proof": [ + "33523f3ea6b6eab72696eead8534d0b7cac78feb60cc3907ac973a24f37adb95", + "3bb1e72abbc9c0b945dafde303acdab123996e41faeab49a35563886b1b41e96", + "04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed" + ], + "leaf_hash": "ca164b6cf11aec6a4c8de2d18c2c2fa04c9323657bd7daf4e7111869201bfec2", + "leaf_index": 4, + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "schema_version": 1, + "sth": { + "hash_algorithm": "RFC9162_SHA256", + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "root_hash": "9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283", + "schema_version": 1, + "signatures": { + "ed25519": { + "payload_digest_sha256": "c9a3c000d448ebd35e313fac0c9ce0e1dc88ff03540b0828e5246407c75e2a1a", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "P8M4gjB7BCZblUvRtvJnbjfaTYKU4oO0/2LZwzpHIgp9fmOXGZqkqi7UaP5Fn1Kx4+RJSgyI2nnnK1pLpkV8CQ==", + "signing_backend": "verified-dalek-serial", + "signing_provenance": { + "self_inclusion": "verified", + "signing_backend": "verified-dalek-serial", + "signing_library_certificates_proven": "16/16", + "signing_library_component": "dalek-ed25519-verified", + "signing_library_leaf_index": 4, + "signing_library_source_commit": "aa0f6abc327ba2a54a534b21608ca8996cf73682" + }, + "status": "signed" + }, + "ml_dsa": { + "reason": "A backend appears available, but no ML-DSA signing key was configured for this log.", + "scheme": "ML-DSA-65", + "standard": "FIPS 204", + "status": "not_configured" + } + }, + "timestamp": "2026-07-06T13:59:16Z", + "tree_size": 8, + "type": "pacta.transparency.signed_tree_head.v1" + }, + "tree_size": 8, + "type": "pacta.transparency.receipt.v1" +} diff --git a/receipts/risc0-ed25519-verified.receipt.json b/receipts/risc0-ed25519-verified.receipt.json new file mode 100644 index 0000000..db70514 --- /dev/null +++ b/receipts/risc0-ed25519-verified.receipt.json @@ -0,0 +1,47 @@ +{ + "hash_algorithm": "RFC9162_SHA256", + "inclusion_proof": [ + "2791c352956ebc620a4fe12b20bfd6faa0813238c5bc0563fa4eb0130d829247", + "f3724e66715b582c384cf49928d4705458475ea4293749989c483ab7fe9496ce", + "04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed" + ], + "leaf_hash": "bdde4e4b87cd263b5914dbbae0c85ceed468c3054596f6ca79121e54cc6a134e", + "leaf_index": 6, + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "schema_version": 1, + "sth": { + "hash_algorithm": "RFC9162_SHA256", + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "root_hash": "9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283", + "schema_version": 1, + "signatures": { + "ed25519": { + "payload_digest_sha256": "c9a3c000d448ebd35e313fac0c9ce0e1dc88ff03540b0828e5246407c75e2a1a", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "P8M4gjB7BCZblUvRtvJnbjfaTYKU4oO0/2LZwzpHIgp9fmOXGZqkqi7UaP5Fn1Kx4+RJSgyI2nnnK1pLpkV8CQ==", + "signing_backend": "verified-dalek-serial", + "signing_provenance": { + "self_inclusion": "verified", + "signing_backend": "verified-dalek-serial", + "signing_library_certificates_proven": "16/16", + "signing_library_component": "dalek-ed25519-verified", + "signing_library_leaf_index": 4, + "signing_library_source_commit": "aa0f6abc327ba2a54a534b21608ca8996cf73682" + }, + "status": "signed" + }, + "ml_dsa": { + "reason": "A backend appears available, but no ML-DSA signing key was configured for this log.", + "scheme": "ML-DSA-65", + "standard": "FIPS 204", + "status": "not_configured" + } + }, + "timestamp": "2026-07-06T13:59:16Z", + "tree_size": 8, + "type": "pacta.transparency.signed_tree_head.v1" + }, + "tree_size": 8, + "type": "pacta.transparency.receipt.v1" +} diff --git a/sth-history.jsonl b/sth-history.jsonl new file mode 100644 index 0000000..9da0d84 --- /dev/null +++ b/sth-history.jsonl @@ -0,0 +1 @@ +{"hash_algorithm":"RFC9162_SHA256","log_id":"205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7","root_hash":"9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283","schema_version":1,"signatures":{"ed25519":{"payload_digest_sha256":"c9a3c000d448ebd35e313fac0c9ce0e1dc88ff03540b0828e5246407c75e2a1a","public_key_fingerprint_sha256":"874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a","scheme":"openssl-ed25519","signature_base64":"P8M4gjB7BCZblUvRtvJnbjfaTYKU4oO0/2LZwzpHIgp9fmOXGZqkqi7UaP5Fn1Kx4+RJSgyI2nnnK1pLpkV8CQ==","signing_backend":"verified-dalek-serial","signing_provenance":{"self_inclusion":"verified","signing_backend":"verified-dalek-serial","signing_library_certificates_proven":"16/16","signing_library_component":"dalek-ed25519-verified","signing_library_leaf_index":4,"signing_library_source_commit":"aa0f6abc327ba2a54a534b21608ca8996cf73682"},"status":"signed"},"ml_dsa":{"reason":"A backend appears available, but no ML-DSA signing key was configured for this log.","scheme":"ML-DSA-65","standard":"FIPS 204","status":"not_configured"}},"timestamp":"2026-07-06T13:59:16Z","tree_size":8,"type":"pacta.transparency.signed_tree_head.v1"} diff --git a/verify.py b/verify.py new file mode 100644 index 0000000..efc7d4a --- /dev/null +++ b/verify.py @@ -0,0 +1,153 @@ +#!/usr/bin/env python3 +"""Standalone verifier for the published Lean Transparency Log. + +Python 3 standard library ONLY - no pacta, no pip. Verifies, from the +files in this repository alone: + + 1. every entry's leaf hash, + 2. every historical Signed Tree Head against the recomputed prefix root + (this is the witness check: a split view or tampered entry fails here), + 3. every STH Ed25519 signature (via the openssl binary, if available), + 4. any receipt's inclusion proof (--receipt FILE). + +Usage: + python3 verify.py --all + python3 verify.py --receipt receipts/dalek-ed25519-verified.receipt.json +""" +import argparse +import base64 +import hashlib +import json +import shutil +import subprocess +import sys +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def leaf_hash(data: bytes) -> bytes: + return hashlib.sha256(b"\x00" + data).digest() + + +def node_hash(left: bytes, right: bytes) -> bytes: + return hashlib.sha256(b"\x01" + left + right).digest() + + +def merkle_root(leaves): + if not leaves: + return hashlib.sha256(b"").digest() + if len(leaves) == 1: + return leaf_hash(leaves[0]) + split = 1 << ((len(leaves) - 1).bit_length() - 1) + return node_hash(merkle_root(leaves[:split]), merkle_root(leaves[split:])) + + +def verify_inclusion(leaf: bytes, index: int, size: int, proof, root: bytes) -> bool: + if index >= size: + return False + fn, sn = index, size - 1 + node = leaf_hash(leaf) + for sibling in proof: + if sn == 0: + return False + if fn % 2 == 1 or fn == sn: + node = node_hash(sibling, node) + if fn % 2 == 0: + while fn % 2 == 0 and fn != 0: + fn //= 2 + sn //= 2 + else: + node = node_hash(node, sibling) + fn //= 2 + sn //= 2 + return sn == 0 and node == root + + +def canonical_json(document) -> bytes: + return json.dumps(document, sort_keys=True, separators=(",", ":"), ensure_ascii=False).encode("utf-8") + + +def load_leaves(): + leaves, problems = [], [] + for position, path in enumerate(sorted((HERE / "entries").glob("[0-9]*.json"))): + record = json.loads(path.read_text()) + data = canonical_json(record["leaf"]) + if record.get("index") != position: + problems.append(f"{path.name}: index {record.get('index')} at position {position}") + if leaf_hash(data).hex() != record.get("leaf_hash"): + problems.append(f"{path.name}: leaf_hash mismatch (tampered entry)") + leaves.append(data) + return leaves, problems + + +def check_sth_signature(head) -> str: + openssl = shutil.which("openssl") + key = HERE / "provider.ed25519.pub" + if not openssl or not key.exists(): + return "skipped (openssl or provider.ed25519.pub missing)" + signatures = head.get("signatures") or {} + ed = signatures.get("ed25519") or {} + payload = canonical_json({k: v for k, v in head.items() if k != "signatures"}) + with tempfile.TemporaryDirectory() as tmp: + payload_path = Path(tmp) / "p" + signature_path = Path(tmp) / "s" + payload_path.write_bytes(payload) + signature_path.write_bytes(base64.b64decode(ed.get("signature_base64", ""))) + result = subprocess.run( + [openssl, "pkeyutl", "-verify", "-pubin", "-inkey", str(key), "-rawin", + "-in", str(payload_path), "-sigfile", str(signature_path)], + capture_output=True, + ) + return "VALID" if result.returncode == 0 else "INVALID" + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument("--all", action="store_true") + parser.add_argument("--receipt") + args = parser.parse_args() + leaves, problems = load_leaves() + print(f"entries: {len(leaves)}") + failures = list(problems) + for problem in problems: + print("PROBLEM:", problem) + + if args.all or not args.receipt: + history_path = HERE / "sth-history.jsonl" + heads = [json.loads(line) for line in history_path.read_text().splitlines() if line.strip()] if history_path.exists() else [] + previous = -1 + for position, head in enumerate(heads): + size = int(head["tree_size"]) + expected = merkle_root(leaves[:size]).hex() + structural = "OK" if head["root_hash"] == expected and size >= previous else "MISMATCH" + if structural != "OK": + failures.append(f"STH #{position}") + signature = check_sth_signature(head) + if signature == "INVALID": + failures.append(f"STH #{position} signature") + print(f"STH #{position} size={size} root={head['root_hash'][:16]}… prefix-root:{structural} signature:{signature}") + previous = max(previous, size) + + if args.receipt: + receipt = json.loads(Path(args.receipt).read_text()) + index = int(receipt["leaf_index"]) + entry = json.loads((HERE / "entries" / f"{index:06d}.json").read_text()) + ok = verify_inclusion( + canonical_json(entry["leaf"]), + index, + int(receipt["tree_size"]), + [bytes.fromhex(h) for h in receipt["inclusion_proof"]], + bytes.fromhex(receipt["sth"]["root_hash"]), + ) + print(f"receipt leaf {index} of {receipt['tree_size']}: inclusion {'VALID' if ok else 'INVALID'}") + if not ok: + failures.append("receipt inclusion") + + print("RESULT:", "OK - the log is internally consistent" if not failures else f"FAILED ({len(failures)} problems)") + return 0 if not failures else 1 + + +if __name__ == "__main__": + sys.exit(main())