mirror of
https://github.com/saymrwulf/lean-transparency-log.git
synced 2026-09-04 20:03:43 +00:00
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 <noreply@anthropic.com>
This commit is contained in:
commit
2d77a2ba2f
22 changed files with 4287 additions and 0 deletions
39
README.md
Normal file
39
README.md
Normal file
|
|
@ -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/<component>.attestation.json` | the newest attestation per library, for convenience |
|
||||
| `receipts/<component>.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.
|
||||
278
entries/000000.json
Normal file
278
entries/000000.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
262
entries/000001.json
Normal file
262
entries/000001.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
266
entries/000002.json
Normal file
266
entries/000002.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
266
entries/000003.json
Normal file
266
entries/000003.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
372
entries/000004.json
Normal file
372
entries/000004.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
340
entries/000005.json
Normal file
340
entries/000005.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
348
entries/000006.json
Normal file
348
entries/000006.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
348
entries/000007.json
Normal file
348
entries/000007.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
332
entries/anza-ed25519-verified.attestation.json
Normal file
332
entries/anza-ed25519-verified.attestation.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
}
|
||||
340
entries/betrusted-ed25519-verified.attestation.json
Normal file
340
entries/betrusted-ed25519-verified.attestation.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
}
|
||||
364
entries/dalek-ed25519-verified.attestation.json
Normal file
364
entries/dalek-ed25519-verified.attestation.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
}
|
||||
340
entries/risc0-ed25519-verified.attestation.json
Normal file
340
entries/risc0-ed25519-verified.attestation.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
}
|
||||
33
latest-sth.json
Normal file
33
latest-sth.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
14
log-metadata.json
Normal file
14
log-metadata.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
3
provider.ed25519.pub
Normal file
3
provider.ed25519.pub
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
-----BEGIN PUBLIC KEY-----
|
||||
MCowBQYDK2VwAyEAd6WIt2/WNJCcKMZGo67BQoZI84LbvLaYMvpwAWNXsxU=
|
||||
-----END PUBLIC KEY-----
|
||||
47
receipts/anza-ed25519-verified.receipt.json
Normal file
47
receipts/anza-ed25519-verified.receipt.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
47
receipts/betrusted-ed25519-verified.receipt.json
Normal file
47
receipts/betrusted-ed25519-verified.receipt.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
47
receipts/dalek-ed25519-verified.receipt.json
Normal file
47
receipts/dalek-ed25519-verified.receipt.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
47
receipts/risc0-ed25519-verified.receipt.json
Normal file
47
receipts/risc0-ed25519-verified.receipt.json
Normal file
|
|
@ -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"
|
||||
}
|
||||
1
sth-history.jsonl
Normal file
1
sth-history.jsonl
Normal file
|
|
@ -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"}
|
||||
153
verify.py
Normal file
153
verify.py
Normal file
|
|
@ -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())
|
||||
Loading…
Reference in a new issue