diff --git a/README.md b/README.md index ed8bf1a..68dc34e 100644 --- a/README.md +++ b/README.md @@ -216,6 +216,18 @@ pacta agent \ This is the intended trust transformation: local agents can avoid constructing the full verifier environment, but they must explicitly trust the provider identity and verification key. +## Real Evidence (shipped) + +`evidence/` contains signed, transparency-logged attestations from a REAL +guarded replay of all four verified repositories: 16/16 certificates proven +per fork with boundary-exact axiom cones, pinned to exact repo commits, +machine-protected by `lean-guard` throughout (~30 min of Lean kernel +re-checking per fork, done ONCE - verifying the signature + inclusion +receipt afterwards takes milliseconds, which is the entire point of the +provider model). The log's first four leaves honestly record a failed audit +run (two pacta bugs, fixed and documented); the ledger keeps its history. +See `evidence/README.md` to re-verify everything yourself. + ## Split-View Defense (STH Pinning) Standalone receipt verification cannot detect a provider maintaining two log views. `pacta` keeps a local STH pin store: diff --git a/evidence/README.md b/evidence/README.md new file mode 100644 index 0000000..b7d6c1a --- /dev/null +++ b/evidence/README.md @@ -0,0 +1,29 @@ +# Real Provider Evidence + +Signed, transparency-logged attestations from a REAL guarded replay of the +four `saymrwulf/*-ed25519-verified` repositories (2026-07-06/07, ~30 min of +Lean re-checking per fork under `lean-guard` memory caps). + +| File | What it is | +|---|---| +| `-ed25519.attestation.yaml` | Signed proof-check attestation: repo commit, environment, machine-protection block, and all 16 certificates with their OBSERVED axiom cones (the four apex tiers carry the fork's exact documented boundary) | +| `-ed25519.receipt.yaml` | RFC 9162-style inclusion receipt binding the attestation into the transparency log (tree size 8), with a consistency anchor | +| `provider.ed25519.pub` | The provider's public key (the PRIVATE key never leaves `provider/state/`, which is gitignored) | +| `log-metadata.json`, `latest-sth.yaml` | Log identity and the latest Signed Tree Head | +| `log-audit.txt` | Monitor self-check output (recomputed root matches the signed root) | + +The log holds EIGHT leaves: entries 0-3 are the first run's attestations, +which honestly record an AUDIT FAILURE (two bugs in pacta's audit step, +since fixed - see the commit history); entries 4-7 are the definitive +16/16-proven attestations. An append-only trust ledger keeps its bad day. + +Re-verify everything yourself (signature via the proven-path verifier if +built, STH pinning, freshness): + +```bash +pacta receipt-verify \ + --attestation evidence/dalek-ed25519.attestation.yaml \ + --receipt evidence/dalek-ed25519.receipt.yaml \ + --log-public-key evidence/provider.ed25519.pub \ + --sth-store /tmp/my-pins.json --max-sth-age-seconds 604800 +``` diff --git a/evidence/anza-ed25519.attestation.yaml b/evidence/anza-ed25519.attestation.yaml new file mode 100644 index 0000000..77552bd --- /dev/null +++ b/evidence/anza-ed25519.attestation.yaml @@ -0,0 +1,262 @@ +schema_version: 1 +provider: local-pacta-provider +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. +subject: + component: anza-ed25519-verified + repo_url: https://github.com/saymrwulf/anza-ed25519-verified.git + repo_commit: 673c15e10a082788f7965fcb0faeefcca0d15136 + verification_dir: verification + kind: ed25519 + verified_backend: serial/u64 +environment: + lean_version: Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, + Release) + lake_version: Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2) + env_script: ~/aeneas-toolchain/env.sh + lean_project_dir: /home/oho/aeneas-toolchain/aeneas/backends/lean +replay: + check_attempted: true + check_ok: true + check_log_path: provider/out/logs/lean-check.log + checked_files: 58 + failed_files: [] + diagnostics: [] + axiom_attempted: true + axiom_ok: true + axiom_log_path: provider/out/logs/axiom-audit.log + axiom_diagnostics: [] +certificates: +- name: CurveFieldProofs.fieldImplementation + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.edwardsImplementation + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: ScalarProofs.scalarImplementation + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.verify_loop_full + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.to_bytes_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.ed_compress_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: ScalarProofs.from_bytes_mod_order_wide_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.vartime_dsm_basepoint_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.enc_point_inj + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.sqrt_ratio_i_sq_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.from_bytes_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.decompress_of_canonical + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - ed_sigs.sha512_hash3 + - ed25519.Signature.r_bytes + - ed25519.Signature.s_bytes + expected_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - ed_sigs.sha512_hash3 + - ed25519.Signature.r_bytes + - ed25519.Signature.s_bytes + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff_point + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - ed_sigs.sha512_hash3 + - ed25519.Signature.r_bytes + - ed25519.Signature.s_bytes + expected_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - ed_sigs.sha512_hash3 + - ed25519.Signature.r_bytes + - ed25519.Signature.s_bytes + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff_point_eq + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - ed_sigs.sha512_hash3 + - ed25519.Signature.r_bytes + - ed25519.Signature.s_bytes + expected_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - ed_sigs.sha512_hash3 + - ed25519.Signature.r_bytes + - ed25519.Signature.s_bytes + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff_decompress + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - ed_sigs.sha512_hash3 + - ed25519.Signature.r_bytes + - ed25519.Signature.s_bytes + expected_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - ed_sigs.sha512_hash3 + - ed25519.Signature.r_bytes + - ed25519.Signature.s_bytes + diagnostics: [] +signature: + scheme: openssl-ed25519 + status: signed + payload_digest_sha256: ff36182e67d083ac442fce5026fe31ae8127b4f04bc6b5a85b70c9cae9ed8f8d + signature_base64: fFGMNOf1a1sk14Cu2BLP2Dl4DWcipXJiPe7KlZuHyCXyhz91NEuLr4VObIa4wP9J61PThXwVwLDEnnHuOH6BCA== + public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a diff --git a/evidence/anza-ed25519.receipt.yaml b/evidence/anza-ed25519.receipt.yaml new file mode 100644 index 0000000..5f06f9d --- /dev/null +++ b/evidence/anza-ed25519.receipt.yaml @@ -0,0 +1,39 @@ +schema_version: 1 +type: pacta.transparency.receipt.v1 +log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7 +hash_algorithm: RFC9162_SHA256 +attestation_path: provider/out/anza-ed25519.attestation.yaml +attestation_digest_sha256: 99d7037f592453e4a176ffbbb314245e32e6014738e38e64b3f166992d6fd9ad +leaf_index: 5 +leaf_hash: 33523f3ea6b6eab72696eead8534d0b7cac78feb60cc3907ac973a24f37adb95 +tree_size: 8 +inclusion_proof: +- ca164b6cf11aec6a4c8de2d18c2c2fa04c9323657bd7daf4e7111869201bfec2 +- 3bb1e72abbc9c0b945dafde303acdab123996e41faeab49a35563886b1b41e96 +- 04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed +consistency: + from_tree_size: 8 + from_root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283 + proof: [] + status: not_applicable +sth: + schema_version: 1 + type: pacta.transparency.signed_tree_head.v1 + log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7 + tree_size: 8 + timestamp: '2026-07-06T12:53:08Z' + root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283 + hash_algorithm: RFC9162_SHA256 + signatures: + ed25519: + scheme: openssl-ed25519 + status: signed + payload_digest_sha256: d783b70d6124bd2206bed6671ce83e9b292dec41761527326695d5e23b12eb8b + signature_base64: 0Si0Mb46p5xmPu8EJp9wm/Cle3xClHYYRLBFksjnygVci8U+RE4uBNydU0dSQT7FrnJB+xdwCn5NBRnUnjaECg== + public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a + ml_dsa: + scheme: ML-DSA-65 + standard: FIPS 204 + status: not_configured + reason: A backend appears available, but no ML-DSA signing key was configured + for this log. diff --git a/evidence/betrusted-ed25519.attestation.yaml b/evidence/betrusted-ed25519.attestation.yaml new file mode 100644 index 0000000..703a29f --- /dev/null +++ b/evidence/betrusted-ed25519.attestation.yaml @@ -0,0 +1,270 @@ +schema_version: 1 +provider: local-pacta-provider +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. +subject: + component: betrusted-ed25519-verified + repo_url: https://github.com/saymrwulf/betrusted-ed25519-verified.git + repo_commit: 81f614a3cbd26412c6af7f0a31c0f128121fbfa4 + verification_dir: verification + kind: ed25519 + verified_backend: serial/u64 +environment: + lean_version: Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, + Release) + lake_version: Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2) + env_script: ~/aeneas-toolchain/env.sh + lean_project_dir: /home/oho/aeneas-toolchain/aeneas/backends/lean +replay: + check_attempted: true + check_ok: true + check_log_path: provider/out/logs/lean-check.log + checked_files: 63 + failed_files: [] + diagnostics: [] + axiom_attempted: true + axiom_ok: true + axiom_log_path: provider/out/logs/axiom-audit.log + axiom_diagnostics: [] +certificates: +- name: CurveFieldProofs.fieldImplementation + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.edwardsImplementation + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: ScalarProofs.scalarImplementation + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.verify_loop_full + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.to_bytes_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.ed_compress_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: ScalarProofs.from_bytes_mod_order_wide_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.vartime_dsm_basepoint_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.enc_point_inj + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.sqrt_ratio_i_sq_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.from_bytes_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.decompress_of_canonical + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + expected_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff_point + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + expected_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff_point_eq + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + expected_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff_decompress + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + expected_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + diagnostics: [] +signature: + scheme: openssl-ed25519 + status: signed + payload_digest_sha256: bb1226fa66ae0e51677ccc8c8361ba121ac5464911f1cb9e305ff7c76b7d2c57 + signature_base64: Lsxje95BPXHfc7l3wxQrRvDgG/5tb7WNaO3wIDsfY/xg/WYRDFrWF3Bb6frs0Dmln00QxA99Gt43PMxLUHq0Ag== + public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a diff --git a/evidence/betrusted-ed25519.receipt.yaml b/evidence/betrusted-ed25519.receipt.yaml new file mode 100644 index 0000000..3def7df --- /dev/null +++ b/evidence/betrusted-ed25519.receipt.yaml @@ -0,0 +1,39 @@ +schema_version: 1 +type: pacta.transparency.receipt.v1 +log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7 +hash_algorithm: RFC9162_SHA256 +attestation_path: provider/out/betrusted-ed25519.attestation.yaml +attestation_digest_sha256: 5bd2a597d712a6a80e6ba82baabcdbbbd54bc913e8a77375a6ae42e2cb7b1c57 +leaf_index: 7 +leaf_hash: 2791c352956ebc620a4fe12b20bfd6faa0813238c5bc0563fa4eb0130d829247 +tree_size: 8 +inclusion_proof: +- bdde4e4b87cd263b5914dbbae0c85ceed468c3054596f6ca79121e54cc6a134e +- f3724e66715b582c384cf49928d4705458475ea4293749989c483ab7fe9496ce +- 04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed +consistency: + from_tree_size: 8 + from_root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283 + proof: [] + status: not_applicable +sth: + schema_version: 1 + type: pacta.transparency.signed_tree_head.v1 + log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7 + tree_size: 8 + timestamp: '2026-07-06T12:53:09Z' + root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283 + hash_algorithm: RFC9162_SHA256 + signatures: + ed25519: + scheme: openssl-ed25519 + status: signed + payload_digest_sha256: d5d25db2c90f0246cc10d10f912085b81c60d2a324354b5abecfdbeb8bd17ee2 + signature_base64: sI4rWnWMrX0zDaN8jofBwSuExKg1e0cmZV3OPaulbXDV97yz95aSo0Gnrfd1En2vyyV1qoEXdTAY9NDgvA8xBA== + public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a + ml_dsa: + scheme: ML-DSA-65 + standard: FIPS 204 + status: not_configured + reason: A backend appears available, but no ML-DSA signing key was configured + for this log. diff --git a/evidence/dalek-ed25519.attestation.yaml b/evidence/dalek-ed25519.attestation.yaml new file mode 100644 index 0000000..459cd68 --- /dev/null +++ b/evidence/dalek-ed25519.attestation.yaml @@ -0,0 +1,294 @@ +schema_version: 1 +provider: local-pacta-provider +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. +subject: + component: dalek-ed25519-verified + repo_url: https://github.com/saymrwulf/dalek-ed25519-verified.git + repo_commit: 8ded7bcf9a1f0016cee93f371796b935b25b7ff8 + verification_dir: verification + kind: ed25519 + verified_backend: serial/u64 +environment: + lean_version: Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, + Release) + lake_version: Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2) + env_script: ~/aeneas-toolchain/env.sh + lean_project_dir: /home/oho/aeneas-toolchain/aeneas/backends/lean +replay: + check_attempted: true + check_ok: true + check_log_path: provider/out/logs/lean-check.log + checked_files: 64 + failed_files: [] + diagnostics: [] + axiom_attempted: true + axiom_ok: true + axiom_log_path: provider/out/logs/axiom-audit.log + axiom_diagnostics: [] +certificates: +- name: CurveFieldProofs.fieldImplementation + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.edwardsImplementation + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: ScalarProofs.scalarImplementation + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.verify_loop_full + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.to_bytes_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.ed_compress_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: ScalarProofs.from_bytes_mod_order_wide_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.vartime_dsm_basepoint_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.enc_point_inj + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.sqrt_ratio_i_sq_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.from_bytes_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.decompress_of_canonical + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff + status: proven + axiom_status: clean + 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 + 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 + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff_point + status: proven + axiom_status: clean + 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 + 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 + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff_point_eq + status: proven + axiom_status: clean + 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 + 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 + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff_decompress + status: proven + axiom_status: clean + 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 + 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 + diagnostics: [] +signature: + scheme: openssl-ed25519 + status: signed + payload_digest_sha256: ba9c3de2b75af13cd79aaaf1226a07c3e671f2d5fe06dd2a33810588dfe21571 + signature_base64: Ec0xxNT6PeyuNXUncaeZN9iDJN/q3W/WenqGrx3qWDfYu9xK5Hq7e4zLALqZKrNCBaPXBm4oSYKUd1qSNoWSBg== + public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a diff --git a/evidence/dalek-ed25519.receipt.yaml b/evidence/dalek-ed25519.receipt.yaml new file mode 100644 index 0000000..5906aa9 --- /dev/null +++ b/evidence/dalek-ed25519.receipt.yaml @@ -0,0 +1,39 @@ +schema_version: 1 +type: pacta.transparency.receipt.v1 +log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7 +hash_algorithm: RFC9162_SHA256 +attestation_path: provider/out/dalek-ed25519.attestation.yaml +attestation_digest_sha256: d0921bfd2ad20980332ca5626bad79bc713a3e5c7919ce705043bb6097ecf1b3 +leaf_index: 4 +leaf_hash: ca164b6cf11aec6a4c8de2d18c2c2fa04c9323657bd7daf4e7111869201bfec2 +tree_size: 8 +inclusion_proof: +- 33523f3ea6b6eab72696eead8534d0b7cac78feb60cc3907ac973a24f37adb95 +- 3bb1e72abbc9c0b945dafde303acdab123996e41faeab49a35563886b1b41e96 +- 04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed +consistency: + from_tree_size: 8 + from_root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283 + proof: [] + status: not_applicable +sth: + schema_version: 1 + type: pacta.transparency.signed_tree_head.v1 + log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7 + tree_size: 8 + timestamp: '2026-07-06T12:53:08Z' + root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283 + hash_algorithm: RFC9162_SHA256 + signatures: + ed25519: + scheme: openssl-ed25519 + status: signed + payload_digest_sha256: d783b70d6124bd2206bed6671ce83e9b292dec41761527326695d5e23b12eb8b + signature_base64: 0Si0Mb46p5xmPu8EJp9wm/Cle3xClHYYRLBFksjnygVci8U+RE4uBNydU0dSQT7FrnJB+xdwCn5NBRnUnjaECg== + public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a + ml_dsa: + scheme: ML-DSA-65 + standard: FIPS 204 + status: not_configured + reason: A backend appears available, but no ML-DSA signing key was configured + for this log. diff --git a/evidence/latest-sth.yaml b/evidence/latest-sth.yaml new file mode 100644 index 0000000..af83287 --- /dev/null +++ b/evidence/latest-sth.yaml @@ -0,0 +1,20 @@ +schema_version: 1 +type: pacta.transparency.signed_tree_head.v1 +log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7 +tree_size: 8 +timestamp: '2026-07-06T12:53:09Z' +root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283 +hash_algorithm: RFC9162_SHA256 +signatures: + ed25519: + scheme: openssl-ed25519 + status: signed + payload_digest_sha256: d5d25db2c90f0246cc10d10f912085b81c60d2a324354b5abecfdbeb8bd17ee2 + signature_base64: sI4rWnWMrX0zDaN8jofBwSuExKg1e0cmZV3OPaulbXDV97yz95aSo0Gnrfd1En2vyyV1qoEXdTAY9NDgvA8xBA== + public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a + ml_dsa: + scheme: ML-DSA-65 + standard: FIPS 204 + status: not_configured + reason: A backend appears available, but no ML-DSA signing key was configured + for this log. diff --git a/evidence/log-audit.txt b/evidence/log-audit.txt new file mode 100644 index 0000000..e01a550 --- /dev/null +++ b/evidence/log-audit.txt @@ -0,0 +1,4 @@ +tree_size: 8 +computed_root: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283 +stored_sth_root: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283 +ok: true diff --git a/evidence/log-metadata.json b/evidence/log-metadata.json new file mode 100644 index 0000000..2089a0c --- /dev/null +++ b/evidence/log-metadata.json @@ -0,0 +1,14 @@ +{ + "created_at": "2026-07-06T08:43:00Z", + "ed25519_public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "hash_algorithm": "RFC9162_SHA256", + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "provider": "local-pacta-provider", + "schema_version": 1, + "standards": [ + "RFC 9162 Merkle tree hash and inclusion/consistency proof algorithms", + "RFC 8032 Ed25519 signature verification via OpenSSL", + "FIPS 204 ML-DSA signature slot; must be required by policy only when a backend is configured" + ], + "type": "pacta.transparency.log_metadata.v1" +} diff --git a/evidence/provider.ed25519.pub b/evidence/provider.ed25519.pub new file mode 100644 index 0000000..de4000a --- /dev/null +++ b/evidence/provider.ed25519.pub @@ -0,0 +1,3 @@ +-----BEGIN PUBLIC KEY----- +MCowBQYDK2VwAyEAd6WIt2/WNJCcKMZGo67BQoZI84LbvLaYMvpwAWNXsxU= +-----END PUBLIC KEY----- diff --git a/evidence/risc0-ed25519.attestation.yaml b/evidence/risc0-ed25519.attestation.yaml new file mode 100644 index 0000000..1f3f3fb --- /dev/null +++ b/evidence/risc0-ed25519.attestation.yaml @@ -0,0 +1,270 @@ +schema_version: 1 +provider: local-pacta-provider +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. +subject: + component: risc0-ed25519-verified + repo_url: https://github.com/saymrwulf/risc0-ed25519-verified.git + repo_commit: 98a13a68539b20ac0279876848aea3687e523462 + verification_dir: verification + kind: ed25519 + verified_backend: serial/u64 +environment: + lean_version: Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, + Release) + lake_version: Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2) + env_script: ~/aeneas-toolchain/env.sh + lean_project_dir: /home/oho/aeneas-toolchain/aeneas/backends/lean +replay: + check_attempted: true + check_ok: true + check_log_path: provider/out/logs/lean-check.log + checked_files: 63 + failed_files: [] + diagnostics: [] + axiom_attempted: true + axiom_ok: true + axiom_log_path: provider/out/logs/axiom-audit.log + axiom_diagnostics: [] +certificates: +- name: CurveFieldProofs.fieldImplementation + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.edwardsImplementation + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: ScalarProofs.scalarImplementation + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.verify_loop_full + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.to_bytes_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.ed_compress_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: ScalarProofs.from_bytes_mod_order_wide_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.vartime_dsm_basepoint_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.enc_point_inj + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.sqrt_ratio_i_sq_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.from_bytes_spec + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.decompress_of_canonical + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + expected_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff_point + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + expected_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff_point_eq + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + expected_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + diagnostics: [] +- name: CurveFieldProofs.verify_accepts_iff_decompress + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + expected_axioms: + - propext + - Classical.choice + - Quot.sound + - ed25519.Signature + - verifying.sha512_hash3 + - ed25519.Signature.to_bytes + - signature.error.Error + - signature.error.Error.new + diagnostics: [] +signature: + scheme: openssl-ed25519 + status: signed + payload_digest_sha256: d921c5d45f8300eecc0299fc3e11506df67751506b52cda35fb61d517b27712b + signature_base64: iwi/AR0wLQiGF6p/jBr/3PV01d2m3lmQOXfc/00axng9Tj/YUymGejWuUi1ZleZL1X0cA9NTNKc5bbIT8AyPDA== + public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a diff --git a/evidence/risc0-ed25519.receipt.yaml b/evidence/risc0-ed25519.receipt.yaml new file mode 100644 index 0000000..e8f742f --- /dev/null +++ b/evidence/risc0-ed25519.receipt.yaml @@ -0,0 +1,39 @@ +schema_version: 1 +type: pacta.transparency.receipt.v1 +log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7 +hash_algorithm: RFC9162_SHA256 +attestation_path: provider/out/risc0-ed25519.attestation.yaml +attestation_digest_sha256: 0f86e43e48411b7fdb12a509c12f96ade3e5cc7ecd12d21b12c83a22d0b1a700 +leaf_index: 6 +leaf_hash: bdde4e4b87cd263b5914dbbae0c85ceed468c3054596f6ca79121e54cc6a134e +tree_size: 8 +inclusion_proof: +- 2791c352956ebc620a4fe12b20bfd6faa0813238c5bc0563fa4eb0130d829247 +- f3724e66715b582c384cf49928d4705458475ea4293749989c483ab7fe9496ce +- 04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed +consistency: + from_tree_size: 8 + from_root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283 + proof: [] + status: not_applicable +sth: + schema_version: 1 + type: pacta.transparency.signed_tree_head.v1 + log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7 + tree_size: 8 + timestamp: '2026-07-06T12:53:09Z' + root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283 + hash_algorithm: RFC9162_SHA256 + signatures: + ed25519: + scheme: openssl-ed25519 + status: signed + payload_digest_sha256: d5d25db2c90f0246cc10d10f912085b81c60d2a324354b5abecfdbeb8bd17ee2 + signature_base64: sI4rWnWMrX0zDaN8jofBwSuExKg1e0cmZV3OPaulbXDV97yz95aSo0Gnrfd1En2vyyV1qoEXdTAY9NDgvA8xBA== + public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a + ml_dsa: + scheme: ML-DSA-65 + standard: FIPS 204 + status: not_configured + reason: A backend appears available, but no ML-DSA signing key was configured + for this log. diff --git a/notebooks/05_third_party_attestation_provider.ipynb b/notebooks/05_third_party_attestation_provider.ipynb index a9b5169..e284b54 100644 --- a/notebooks/05_third_party_attestation_provider.ipynb +++ b/notebooks/05_third_party_attestation_provider.ipynb @@ -126,6 +126,43 @@ "This is why transparency logging matters. A signature says \"this provider signed this.\" A transparency receipt says \"this signed result is included in an append-only public structure at this tree head.\"\n" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Real evidence, checked in this cell\n", + "\n", + "Everything above used schema fixtures. The repository now ships REAL provider evidence under `evidence/`: signed attestations from a guarded Lean replay of all four verified repositories (~30 minutes of kernel re-checking per fork), each recording the repo commit, the machine-protection block, and all sixteen certificates with their observed axiom cones. Read one and re-derive its verdicts locally - never trust the provider's own labels:\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "from pacta.attestation import load_attestation, _normalize_certificate\n", + "from pacta.config import load_config\n", + "from pacta.profiles import get_profile\n", + "from pacta.signing import verify_attestation_signature_detailed\n", + "\n", + "config = load_config(repo_root / \"examples\" / \"repos.yaml\")\n", + "repo = config.repo_named(\"dalek-ed25519-verified\")\n", + "profile = get_profile(\"ed25519\", repo)\n", + "att = load_attestation(repo_root / \"evidence\" / \"dalek-ed25519.attestation.yaml\")\n", + "\n", + "ok, error, backend = verify_attestation_signature_detailed(att, repo_root / \"evidence\" / \"provider.ed25519.pub\")\n", + "print(\"signature valid:\", ok, \"| verified on backend:\", backend)\n", + "print(\"subject commit:\", att[\"subject\"][\"repo_commit\"][:12])\n", + "print(\"machine protection:\", att[\"machine_protection\"][\"lean_guard\"].rsplit(\"/\", 2)[-1])\n", + "\n", + "rederived = [_normalize_certificate(cert, profile) for cert in att[\"certificates\"]]\n", + "clean = sum(1 for cert in rederived if cert[\"status\"] == \"proven\" and cert[\"axiom_status\"] == \"clean\")\n", + "print(f\"re-derived locally: {clean}/{len(rederived)} proven with boundary-exact cones\")\n", + "apex = [cert for cert in rederived if cert[\"name\"].endswith(\"_decompress\")][0]\n", + "print(\"full-lift tier observed cone:\", apex[\"observed_axioms\"])\n" + ] + }, { "cell_type": "markdown", "metadata": {}, diff --git a/notebooks/06_merkle_transparency_logs.ipynb b/notebooks/06_merkle_transparency_logs.ipynb index f9744f1..7310f9a 100644 --- a/notebooks/06_merkle_transparency_logs.ipynb +++ b/notebooks/06_merkle_transparency_logs.ipynb @@ -207,6 +207,38 @@ "source": [ "At real scale the same check runs on every `pacta receipt-verify --sth-store ...` and `pacta agent --sth-store ...` invocation; receipts embed a consistency anchor from the previous tree size, the provider serves proofs from arbitrary pinned sizes (`pacta_provider log-consistency --from-size N`), and `pacta_provider log-audit` is the monitor's self-check. A freshness policy (`--max-sth-age-seconds`) closes the stale-root hole: an old-but-valid tree head could hide later entries.\n", "\n", + "### The real thing\n", + "\n", + "The `evidence/` directory holds four REAL receipts from the shipped transparency log (tree size 8 - the first four leaves honestly record a failed audit run; read `evidence/README.md`). Verify all four cryptographically and watch a fresh pin store handle them:\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import tempfile\n", + "from pathlib import Path as _P\n", + "from pacta.sthstore import check_sth_against_store\n", + "from pacta.transparency import verify_receipt\n", + "from pacta.yamlio import load_data as _load\n", + "\n", + "log_key = repo_root / \"evidence\" / \"provider.ed25519.pub\"\n", + "with tempfile.TemporaryDirectory() as tmp:\n", + " store = _P(tmp) / \"pins.json\"\n", + " for fork in [\"dalek\", \"anza\", \"risc0\", \"betrusted\"]:\n", + " att = _load(repo_root / \"evidence\" / f\"{fork}-ed25519.attestation.yaml\")\n", + " receipt = _load(repo_root / \"evidence\" / f\"{fork}-ed25519.receipt.yaml\")\n", + " result = verify_receipt(att, receipt, log_key)\n", + " pin = check_sth_against_store(receipt[\"sth\"], store, consistency_from=receipt.get(\"consistency\"))\n", + " print(f\"{fork}: receipt accepted={result.accepted} backend={result.signatures.get('ed25519_backend')} pin={pin.action}\")\n" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ "## Exercises\n", "\n", "- Tamper with one leaf and show that inclusion verification fails.\n", diff --git a/scripts/build_curriculum_notebooks.py b/scripts/build_curriculum_notebooks.py index 7b9fa5e..d70c23a 100644 --- a/scripts/build_curriculum_notebooks.py +++ b/scripts/build_curriculum_notebooks.py @@ -869,6 +869,37 @@ COURSE = { This is why transparency logging matters. A signature says "this provider signed this." A transparency receipt says "this signed result is included in an append-only public structure at this tree head." """ ), + md( + """ + ## Real evidence, checked in this cell + + Everything above used schema fixtures. The repository now ships REAL provider evidence under `evidence/`: signed attestations from a guarded Lean replay of all four verified repositories (~30 minutes of kernel re-checking per fork), each recording the repo commit, the machine-protection block, and all sixteen certificates with their observed axiom cones. Read one and re-derive its verdicts locally - never trust the provider's own labels: + """ + ), + code( + """ + from pacta.attestation import load_attestation, _normalize_certificate + from pacta.config import load_config + from pacta.profiles import get_profile + from pacta.signing import verify_attestation_signature_detailed + + config = load_config(repo_root / "examples" / "repos.yaml") + repo = config.repo_named("dalek-ed25519-verified") + profile = get_profile("ed25519", repo) + att = load_attestation(repo_root / "evidence" / "dalek-ed25519.attestation.yaml") + + ok, error, backend = verify_attestation_signature_detailed(att, repo_root / "evidence" / "provider.ed25519.pub") + print("signature valid:", ok, "| verified on backend:", backend) + print("subject commit:", att["subject"]["repo_commit"][:12]) + print("machine protection:", att["machine_protection"]["lean_guard"].rsplit("/", 2)[-1]) + + rederived = [_normalize_certificate(cert, profile) for cert in att["certificates"]] + clean = sum(1 for cert in rederived if cert["status"] == "proven" and cert["axiom_status"] == "clean") + print(f"re-derived locally: {clean}/{len(rederived)} proven with boundary-exact cones") + apex = [cert for cert in rederived if cert["name"].endswith("_decompress")][0] + print("full-lift tier observed cone:", apex["observed_axioms"]) + """ + ), md( """ ## Exercises @@ -1053,6 +1084,33 @@ COURSE = { """ At real scale the same check runs on every `pacta receipt-verify --sth-store ...` and `pacta agent --sth-store ...` invocation; receipts embed a consistency anchor from the previous tree size, the provider serves proofs from arbitrary pinned sizes (`pacta_provider log-consistency --from-size N`), and `pacta_provider log-audit` is the monitor's self-check. A freshness policy (`--max-sth-age-seconds`) closes the stale-root hole: an old-but-valid tree head could hide later entries. + ### The real thing + + The `evidence/` directory holds four REAL receipts from the shipped transparency log (tree size 8 - the first four leaves honestly record a failed audit run; read `evidence/README.md`). Verify all four cryptographically and watch a fresh pin store handle them: + """ + ), + code( + """ + import tempfile + from pathlib import Path as _P + from pacta.sthstore import check_sth_against_store + from pacta.transparency import verify_receipt + from pacta.yamlio import load_data as _load + + log_key = repo_root / "evidence" / "provider.ed25519.pub" + with tempfile.TemporaryDirectory() as tmp: + store = _P(tmp) / "pins.json" + for fork in ["dalek", "anza", "risc0", "betrusted"]: + att = _load(repo_root / "evidence" / f"{fork}-ed25519.attestation.yaml") + receipt = _load(repo_root / "evidence" / f"{fork}-ed25519.receipt.yaml") + result = verify_receipt(att, receipt, log_key) + pin = check_sth_against_store(receipt["sth"], store, consistency_from=receipt.get("consistency")) + print(f"{fork}: receipt accepted={result.accepted} backend={result.signatures.get('ed25519_backend')} pin={pin.action}") + """ + ), + md( + """ + ## Exercises - Tamper with one leaf and show that inclusion verification fails. diff --git a/src/pacta/sthstore.py b/src/pacta/sthstore.py index 501ed22..330c171 100644 --- a/src/pacta/sthstore.py +++ b/src/pacta/sthstore.py @@ -118,7 +118,10 @@ def check_sth_against_store( False, [ f"LOG ROLLBACK: presented tree_size {tree_size} is smaller than the pinned size " - f"{pinned_size}. Append-only logs never shrink." + f"{pinned_size}. Append-only logs never shrink. If this receipt is simply STALE " + "(issued before the log grew), request a freshly issued receipt for the same " + "leaf - the provider's log-append is idempotent and re-issues an inclusion " + "proof against the current tree." ], "rejected", )