diff --git a/entries/000012.json b/entries/000012.json new file mode 100644 index 0000000..6360533 --- /dev/null +++ b/entries/000012.json @@ -0,0 +1,975 @@ +{ + "index": 12, + "leaf": { + "attestation": { + "certificates": [ + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.ConsRec", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [], + "name": "LTLAcc.Hash", + "observed_axioms": [], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "LTLAcc.sha256" + ], + "name": "LTLAcc.IsCollision", + "observed_axioms": [ + "LTLAcc.sha256" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.MTH", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.MTH_single", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.MTH_split", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.Path", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.Root", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.Root_left", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.Root_one", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.Root_one_cons", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.Root_right", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.acceptCons", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.acceptCons_sound", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.acceptIncl", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.acceptIncl_complete", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.acceptIncl_sound", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.consRecBinding", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "LTLAcc.consRec_base_false_eq", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext" + ], + "name": "LTLAcc.consRec_base_true_eq", + "observed_axioms": [ + "propext" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.consRec_some_le", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [], + "name": "LTLAcc.domsep", + "observed_axioms": [], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext" + ], + "name": "LTLAcc.eq_dropLast_append_of_getLast?", + "observed_axioms": [ + "propext" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "LTLAcc.exists_singleton_of_length_one", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractCons", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractConsNode", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractCons_correct", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractCons_correct_paper", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractCons_nonvacuous", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractIncl", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractIncl_correct", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractIncl_nonvacuous", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractMTH", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractMTH_correct", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractMTH_nonvacuous", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.fork_distinct", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.getD_drop", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.getD_take", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "LTLAcc.sha256" + ], + "name": "LTLAcc.hleaf", + "observed_axioms": [ + "LTLAcc.sha256" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "LTLAcc.sha256" + ], + "name": "LTLAcc.hnode", + "observed_axioms": [ + "LTLAcc.sha256" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext" + ], + "name": "LTLAcc.hnode_preimage_inj", + "observed_axioms": [ + "propext" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.incl_complete", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [], + "name": "LTLAcc.instDecidableEqHash", + "observed_axioms": [], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext" + ], + "name": "LTLAcc.instInhabitedHash", + "observed_axioms": [ + "propext" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.kbelow", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.kbelow_eq_of_pow2_between", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.kbelow_lt", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.kbelow_pos", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.kbelow_pow2", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.kbelow_prefix_eq", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.le_two_kbelow", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.pinAccept", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.pinAccept_monotone", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.pinExtract", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.pin_prefix_correct", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.pin_prefix_nonvacuous", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.pow2_exp_unique", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext" + ], + "name": "LTLAcc.take_all", + "observed_axioms": [ + "propext" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [], + "name": "LTLAcc.take_append_drop", + "observed_axioms": [], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "LTLAcc.take_drop_prefix", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.take_take_le", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "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": "$AENEAS_HOME/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-16T17:54:02Z", + "machine_protection": { + "lean_guard": "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": "/tmp/entry13/out/logs/axiom-audit.log", + "axiom_ok": true, + "check_attempted": true, + "check_log_path": "/tmp/entry13/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 12, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "scope": { + "deployment_constraints": [ + "Attestation scope: this corpus kernel-checks the listed theorems about the mechanized recursive accumulator model. Correspondence with the deployed inclusion verifier is supported by finite differential testing over the pinned families. The deployed consistency verifier is not extensionally equal to the model; applying the mechanized soundness result to the deployed consumer flow additionally relies on an unmechanized authentic-size/root invariant (KNOWN-GAPS 14/15)." + ], + "exclusions": [ + "SHA-256 collision resistance (the single opaque boundary axiom; soundness theorems CONSTRUCT collisions)", + "deployed-verifier extensional equality (KNOWN-GAPS 14/15 - lied-size divergence, one-sided; refinement invariant unmechanized)", + "signature/STH layer and evidence transferability (gap 4)", + "asymptotic cost claims (gap 9)" + ], + "guarantees": [] + }, + "signature": { + "payload_digest_sha256": "c25970028b0266c3c280a3934600119eaa4338673c00c22e0ed20f8462660bcf", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "IQ8wjNjYHQ6+sqcFJglQ+yTPCBlwsDF8zYkNb40olK6ScHf5HEH3kEYBLko9w+gvYT/LpWRAy3/Vajn7BGjbDA==", + "signing_backend": "verified-dalek-serial", + "status": "signed" + }, + "subject": { + "component": "ltl-accumulator-verified", + "kind": "merkle_accumulator", + "repo_commit": "172a1d0653f489d5b7cb73ac7942a57cbb496532", + "repo_url": "https://github.com/saymrwulf/ltl-accumulator-verified.git", + "verification_dir": "verification", + "verified_backend": "rfc9162-sha256/lean-model" + } + }, + "schema_version": 1, + "type": "pacta.transparency.attestation_leaf.v1" + }, + "leaf_hash": "8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a" +} diff --git a/entries/ltl-accumulator-verified.attestation.json b/entries/ltl-accumulator-verified.attestation.json new file mode 100644 index 0000000..c68c696 --- /dev/null +++ b/entries/ltl-accumulator-verified.attestation.json @@ -0,0 +1,967 @@ +{ + "certificates": [ + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.ConsRec", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [], + "name": "LTLAcc.Hash", + "observed_axioms": [], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "LTLAcc.sha256" + ], + "name": "LTLAcc.IsCollision", + "observed_axioms": [ + "LTLAcc.sha256" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.MTH", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.MTH_single", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.MTH_split", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.Path", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.Root", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.Root_left", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.Root_one", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.Root_one_cons", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.Root_right", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.acceptCons", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.acceptCons_sound", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.acceptIncl", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.acceptIncl_complete", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.acceptIncl_sound", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.consRecBinding", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "LTLAcc.consRec_base_false_eq", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext" + ], + "name": "LTLAcc.consRec_base_true_eq", + "observed_axioms": [ + "propext" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.consRec_some_le", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [], + "name": "LTLAcc.domsep", + "observed_axioms": [], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext" + ], + "name": "LTLAcc.eq_dropLast_append_of_getLast?", + "observed_axioms": [ + "propext" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "LTLAcc.exists_singleton_of_length_one", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractCons", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractConsNode", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractCons_correct", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractCons_correct_paper", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractCons_nonvacuous", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractIncl", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractIncl_correct", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractIncl_nonvacuous", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractMTH", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractMTH_correct", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.extractMTH_nonvacuous", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.fork_distinct", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.getD_drop", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.getD_take", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "LTLAcc.sha256" + ], + "name": "LTLAcc.hleaf", + "observed_axioms": [ + "LTLAcc.sha256" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "LTLAcc.sha256" + ], + "name": "LTLAcc.hnode", + "observed_axioms": [ + "LTLAcc.sha256" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext" + ], + "name": "LTLAcc.hnode_preimage_inj", + "observed_axioms": [ + "propext" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.incl_complete", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [], + "name": "LTLAcc.instDecidableEqHash", + "observed_axioms": [], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext" + ], + "name": "LTLAcc.instInhabitedHash", + "observed_axioms": [ + "propext" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.kbelow", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.kbelow_eq_of_pow2_between", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.kbelow_lt", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.kbelow_pos", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.kbelow_pow2", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.kbelow_prefix_eq", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.le_two_kbelow", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.pinAccept", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.pinAccept_monotone", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.pinExtract", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.pin_prefix_correct", + "observed_axioms": [ + "propext", + "Classical.choice", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "name": "LTLAcc.pin_prefix_nonvacuous", + "observed_axioms": [ + "propext", + "LTLAcc.sha256", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.pow2_exp_unique", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext" + ], + "name": "LTLAcc.take_all", + "observed_axioms": [ + "propext" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [], + "name": "LTLAcc.take_append_drop", + "observed_axioms": [], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "LTLAcc.take_drop_prefix", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Quot.sound" + ], + "name": "LTLAcc.take_take_le", + "observed_axioms": [ + "propext", + "Quot.sound" + ], + "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": "$AENEAS_HOME/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-16T17:54:02Z", + "machine_protection": { + "lean_guard": "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": "/tmp/entry13/out/logs/axiom-audit.log", + "axiom_ok": true, + "check_attempted": true, + "check_log_path": "/tmp/entry13/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 12, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "scope": { + "deployment_constraints": [ + "Attestation scope: this corpus kernel-checks the listed theorems about the mechanized recursive accumulator model. Correspondence with the deployed inclusion verifier is supported by finite differential testing over the pinned families. The deployed consistency verifier is not extensionally equal to the model; applying the mechanized soundness result to the deployed consumer flow additionally relies on an unmechanized authentic-size/root invariant (KNOWN-GAPS 14/15)." + ], + "exclusions": [ + "SHA-256 collision resistance (the single opaque boundary axiom; soundness theorems CONSTRUCT collisions)", + "deployed-verifier extensional equality (KNOWN-GAPS 14/15 - lied-size divergence, one-sided; refinement invariant unmechanized)", + "signature/STH layer and evidence transferability (gap 4)", + "asymptotic cost claims (gap 9)" + ], + "guarantees": [] + }, + "signature": { + "payload_digest_sha256": "c25970028b0266c3c280a3934600119eaa4338673c00c22e0ed20f8462660bcf", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "IQ8wjNjYHQ6+sqcFJglQ+yTPCBlwsDF8zYkNb40olK6ScHf5HEH3kEYBLko9w+gvYT/LpWRAy3/Vajn7BGjbDA==", + "signing_backend": "verified-dalek-serial", + "status": "signed" + }, + "subject": { + "component": "ltl-accumulator-verified", + "kind": "merkle_accumulator", + "repo_commit": "172a1d0653f489d5b7cb73ac7942a57cbb496532", + "repo_url": "https://github.com/saymrwulf/ltl-accumulator-verified.git", + "verification_dir": "verification", + "verified_backend": "rfc9162-sha256/lean-model" + } +} diff --git a/latest-sth.json b/latest-sth.json index 531c7ba..33af967 100644 --- a/latest-sth.json +++ b/latest-sth.json @@ -1,14 +1,14 @@ { "hash_algorithm": "RFC9162_SHA256", "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", - "root_hash": "bcd15f9d7ea1c9e5bd0a9e64fa8d846208b1e29ee167d4f1eac19b30e6913ee9", + "root_hash": "3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d", "schema_version": 1, "signatures": { "ed25519": { - "payload_digest_sha256": "fab790262c7e1b1eadc0fbf1d10481da0984cd7b99d6e19d98820d2c33d5f34d", + "payload_digest_sha256": "bd7d61897fd48a9113efa9935c25b6dc9e4ddd078de3561bd710442219bb03d4", "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", "scheme": "openssl-ed25519", - "signature_base64": "GYsT/T61aokWWbv+dqrMt1CtJTeGAC/aX0K1MazlXDo7tpEiex3O1uvox9mU/FWFIxwuBg/l2X8gB0DjYjc1Cw==", + "signature_base64": "3NM25ZQblJCjp4sjdL3O7wkn5lDYXAZYIsA+jolZqiqAlYf928vOz/3GLQ2d8Oop1tfjAw5SiMTgcVjDEUlxAQ==", "signing_backend": "verified-dalek-serial", "signing_provenance": { "self_inclusion": "verified", @@ -27,7 +27,7 @@ "status": "not_configured" } }, - "timestamp": "2026-07-07T19:12:17Z", - "tree_size": 12, + "timestamp": "2026-07-16T17:55:20Z", + "tree_size": 13, "type": "pacta.transparency.signed_tree_head.v1" } diff --git a/receipts/anza-ed25519-verified.receipt.json b/receipts/anza-ed25519-verified.receipt.json index 6383718..d53208d 100644 --- a/receipts/anza-ed25519-verified.receipt.json +++ b/receipts/anza-ed25519-verified.receipt.json @@ -3,6 +3,7 @@ "inclusion_proof": [ "072b178a18d64012987903179d634cf22d1378d71f7e2a0d79fa29c95b0c3856", "906823a87681cb8b448d0cb04a36a8f3e0583e2a13259fa849b55506ba903134", + "8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a", "9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283" ], "leaf_hash": "b1034bc68193c9c4eeee03289acd5641fc514615900cba7ee2457eaf25ef743b", @@ -12,14 +13,14 @@ "sth": { "hash_algorithm": "RFC9162_SHA256", "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", - "root_hash": "bcd15f9d7ea1c9e5bd0a9e64fa8d846208b1e29ee167d4f1eac19b30e6913ee9", + "root_hash": "3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d", "schema_version": 1, "signatures": { "ed25519": { - "payload_digest_sha256": "fab790262c7e1b1eadc0fbf1d10481da0984cd7b99d6e19d98820d2c33d5f34d", + "payload_digest_sha256": "bd7d61897fd48a9113efa9935c25b6dc9e4ddd078de3561bd710442219bb03d4", "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", "scheme": "openssl-ed25519", - "signature_base64": "GYsT/T61aokWWbv+dqrMt1CtJTeGAC/aX0K1MazlXDo7tpEiex3O1uvox9mU/FWFIxwuBg/l2X8gB0DjYjc1Cw==", + "signature_base64": "3NM25ZQblJCjp4sjdL3O7wkn5lDYXAZYIsA+jolZqiqAlYf928vOz/3GLQ2d8Oop1tfjAw5SiMTgcVjDEUlxAQ==", "signing_backend": "verified-dalek-serial", "signing_provenance": { "self_inclusion": "verified", @@ -38,10 +39,10 @@ "status": "not_configured" } }, - "timestamp": "2026-07-07T19:12:17Z", - "tree_size": 12, + "timestamp": "2026-07-16T17:55:20Z", + "tree_size": 13, "type": "pacta.transparency.signed_tree_head.v1" }, - "tree_size": 12, + "tree_size": 13, "type": "pacta.transparency.receipt.v1" } diff --git a/receipts/betrusted-ed25519-verified.receipt.json b/receipts/betrusted-ed25519-verified.receipt.json index 8935b0f..8d79dfa 100644 --- a/receipts/betrusted-ed25519-verified.receipt.json +++ b/receipts/betrusted-ed25519-verified.receipt.json @@ -3,6 +3,7 @@ "inclusion_proof": [ "ed368f5f9b3714b5c633bc55971b61c31af55a8022ac9fb567515810007b527f", "3253f2e4dcb5515e0caf021b1e4a257a15bd04df969aaf08174da745d72cd00f", + "8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a", "9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283" ], "leaf_hash": "ad7ccbb6def18dccba7176f4be36ad1ce731c1456672c19310e73e87c4f312df", @@ -12,14 +13,14 @@ "sth": { "hash_algorithm": "RFC9162_SHA256", "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", - "root_hash": "bcd15f9d7ea1c9e5bd0a9e64fa8d846208b1e29ee167d4f1eac19b30e6913ee9", + "root_hash": "3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d", "schema_version": 1, "signatures": { "ed25519": { - "payload_digest_sha256": "fab790262c7e1b1eadc0fbf1d10481da0984cd7b99d6e19d98820d2c33d5f34d", + "payload_digest_sha256": "bd7d61897fd48a9113efa9935c25b6dc9e4ddd078de3561bd710442219bb03d4", "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", "scheme": "openssl-ed25519", - "signature_base64": "GYsT/T61aokWWbv+dqrMt1CtJTeGAC/aX0K1MazlXDo7tpEiex3O1uvox9mU/FWFIxwuBg/l2X8gB0DjYjc1Cw==", + "signature_base64": "3NM25ZQblJCjp4sjdL3O7wkn5lDYXAZYIsA+jolZqiqAlYf928vOz/3GLQ2d8Oop1tfjAw5SiMTgcVjDEUlxAQ==", "signing_backend": "verified-dalek-serial", "signing_provenance": { "self_inclusion": "verified", @@ -38,10 +39,10 @@ "status": "not_configured" } }, - "timestamp": "2026-07-07T19:12:17Z", - "tree_size": 12, + "timestamp": "2026-07-16T17:55:20Z", + "tree_size": 13, "type": "pacta.transparency.signed_tree_head.v1" }, - "tree_size": 12, + "tree_size": 13, "type": "pacta.transparency.receipt.v1" } diff --git a/receipts/dalek-ed25519-verified.receipt.json b/receipts/dalek-ed25519-verified.receipt.json index d715552..dfc3c38 100644 --- a/receipts/dalek-ed25519-verified.receipt.json +++ b/receipts/dalek-ed25519-verified.receipt.json @@ -3,6 +3,7 @@ "inclusion_proof": [ "b1034bc68193c9c4eeee03289acd5641fc514615900cba7ee2457eaf25ef743b", "906823a87681cb8b448d0cb04a36a8f3e0583e2a13259fa849b55506ba903134", + "8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a", "9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283" ], "leaf_hash": "072b178a18d64012987903179d634cf22d1378d71f7e2a0d79fa29c95b0c3856", @@ -12,14 +13,14 @@ "sth": { "hash_algorithm": "RFC9162_SHA256", "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", - "root_hash": "bcd15f9d7ea1c9e5bd0a9e64fa8d846208b1e29ee167d4f1eac19b30e6913ee9", + "root_hash": "3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d", "schema_version": 1, "signatures": { "ed25519": { - "payload_digest_sha256": "fab790262c7e1b1eadc0fbf1d10481da0984cd7b99d6e19d98820d2c33d5f34d", + "payload_digest_sha256": "bd7d61897fd48a9113efa9935c25b6dc9e4ddd078de3561bd710442219bb03d4", "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", "scheme": "openssl-ed25519", - "signature_base64": "GYsT/T61aokWWbv+dqrMt1CtJTeGAC/aX0K1MazlXDo7tpEiex3O1uvox9mU/FWFIxwuBg/l2X8gB0DjYjc1Cw==", + "signature_base64": "3NM25ZQblJCjp4sjdL3O7wkn5lDYXAZYIsA+jolZqiqAlYf928vOz/3GLQ2d8Oop1tfjAw5SiMTgcVjDEUlxAQ==", "signing_backend": "verified-dalek-serial", "signing_provenance": { "self_inclusion": "verified", @@ -38,10 +39,10 @@ "status": "not_configured" } }, - "timestamp": "2026-07-07T19:12:17Z", - "tree_size": 12, + "timestamp": "2026-07-16T17:55:20Z", + "tree_size": 13, "type": "pacta.transparency.signed_tree_head.v1" }, - "tree_size": 12, + "tree_size": 13, "type": "pacta.transparency.receipt.v1" } diff --git a/receipts/ltl-accumulator-verified.receipt.json b/receipts/ltl-accumulator-verified.receipt.json new file mode 100644 index 0000000..a86445e --- /dev/null +++ b/receipts/ltl-accumulator-verified.receipt.json @@ -0,0 +1,46 @@ +{ + "hash_algorithm": "RFC9162_SHA256", + "inclusion_proof": [ + "d564975516d79d8fc6b0c17db318223ae86a918f050ba508c5f4134951b7b6f9", + "9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283" + ], + "leaf_hash": "8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a", + "leaf_index": 12, + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "schema_version": 1, + "sth": { + "hash_algorithm": "RFC9162_SHA256", + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "root_hash": "3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d", + "schema_version": 1, + "signatures": { + "ed25519": { + "payload_digest_sha256": "bd7d61897fd48a9113efa9935c25b6dc9e4ddd078de3561bd710442219bb03d4", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "3NM25ZQblJCjp4sjdL3O7wkn5lDYXAZYIsA+jolZqiqAlYf928vOz/3GLQ2d8Oop1tfjAw5SiMTgcVjDEUlxAQ==", + "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": 8, + "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-16T17:55:20Z", + "tree_size": 13, + "type": "pacta.transparency.signed_tree_head.v1" + }, + "tree_size": 13, + "type": "pacta.transparency.receipt.v1" +} diff --git a/receipts/risc0-ed25519-verified.receipt.json b/receipts/risc0-ed25519-verified.receipt.json index f3515a7..be0418e 100644 --- a/receipts/risc0-ed25519-verified.receipt.json +++ b/receipts/risc0-ed25519-verified.receipt.json @@ -3,6 +3,7 @@ "inclusion_proof": [ "ad7ccbb6def18dccba7176f4be36ad1ce731c1456672c19310e73e87c4f312df", "3253f2e4dcb5515e0caf021b1e4a257a15bd04df969aaf08174da745d72cd00f", + "8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a", "9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283" ], "leaf_hash": "ed368f5f9b3714b5c633bc55971b61c31af55a8022ac9fb567515810007b527f", @@ -12,14 +13,14 @@ "sth": { "hash_algorithm": "RFC9162_SHA256", "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", - "root_hash": "bcd15f9d7ea1c9e5bd0a9e64fa8d846208b1e29ee167d4f1eac19b30e6913ee9", + "root_hash": "3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d", "schema_version": 1, "signatures": { "ed25519": { - "payload_digest_sha256": "fab790262c7e1b1eadc0fbf1d10481da0984cd7b99d6e19d98820d2c33d5f34d", + "payload_digest_sha256": "bd7d61897fd48a9113efa9935c25b6dc9e4ddd078de3561bd710442219bb03d4", "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", "scheme": "openssl-ed25519", - "signature_base64": "GYsT/T61aokWWbv+dqrMt1CtJTeGAC/aX0K1MazlXDo7tpEiex3O1uvox9mU/FWFIxwuBg/l2X8gB0DjYjc1Cw==", + "signature_base64": "3NM25ZQblJCjp4sjdL3O7wkn5lDYXAZYIsA+jolZqiqAlYf928vOz/3GLQ2d8Oop1tfjAw5SiMTgcVjDEUlxAQ==", "signing_backend": "verified-dalek-serial", "signing_provenance": { "self_inclusion": "verified", @@ -38,10 +39,10 @@ "status": "not_configured" } }, - "timestamp": "2026-07-07T19:12:17Z", - "tree_size": 12, + "timestamp": "2026-07-16T17:55:20Z", + "tree_size": 13, "type": "pacta.transparency.signed_tree_head.v1" }, - "tree_size": 12, + "tree_size": 13, "type": "pacta.transparency.receipt.v1" } diff --git a/sth-history.jsonl b/sth-history.jsonl index 98f0741..4806be1 100644 --- a/sth-history.jsonl +++ b/sth-history.jsonl @@ -3,3 +3,4 @@ {"hash_algorithm":"RFC9162_SHA256","log_id":"205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7","root_hash":"a3788367f56caeca89cc7d5545cf57a7dba8055a0ecd48fa2de8d793b3554dda","schema_version":1,"signatures":{"ed25519":{"payload_digest_sha256":"d036c0413cddf628c90cc6b5e36356dca11f9030eacfdecc2b9ab7ba46441267","public_key_fingerprint_sha256":"874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a","scheme":"openssl-ed25519","signature_base64":"GI1/V5DFmYM7FkHcPPR6obkm0lgGOx9XFe2d3aZkb0EGYtah6qc9dRia3oLDq6RHaDNR+/DH81CATij2HJltCA==","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":8,"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-07T19:12:16Z","tree_size":10,"type":"pacta.transparency.signed_tree_head.v1"} {"hash_algorithm":"RFC9162_SHA256","log_id":"205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7","root_hash":"96f2a27d1a668a2dfe832d26e8870d997cec5447fa636b13d51ec25f441360b4","schema_version":1,"signatures":{"ed25519":{"payload_digest_sha256":"ed6632201f4eb36dd7d909ae37df8d82117125fbdaf6a733bf1c6483d3495ea7","public_key_fingerprint_sha256":"874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a","scheme":"openssl-ed25519","signature_base64":"kK9Ia8HyUBVeWVZlm7IVGyuBzrFS9S3sSn1vfUxlEr2u9hh+A02T+vYxeyPjXD7ZbUL6xlxx8qP5ul7wj5ZTDw==","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":8,"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-07T19:12:16Z","tree_size":11,"type":"pacta.transparency.signed_tree_head.v1"} {"hash_algorithm":"RFC9162_SHA256","log_id":"205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7","root_hash":"bcd15f9d7ea1c9e5bd0a9e64fa8d846208b1e29ee167d4f1eac19b30e6913ee9","schema_version":1,"signatures":{"ed25519":{"payload_digest_sha256":"fab790262c7e1b1eadc0fbf1d10481da0984cd7b99d6e19d98820d2c33d5f34d","public_key_fingerprint_sha256":"874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a","scheme":"openssl-ed25519","signature_base64":"GYsT/T61aokWWbv+dqrMt1CtJTeGAC/aX0K1MazlXDo7tpEiex3O1uvox9mU/FWFIxwuBg/l2X8gB0DjYjc1Cw==","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":8,"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-07T19:12:17Z","tree_size":12,"type":"pacta.transparency.signed_tree_head.v1"} +{"hash_algorithm":"RFC9162_SHA256","log_id":"205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7","root_hash":"3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d","schema_version":1,"signatures":{"ed25519":{"payload_digest_sha256":"bd7d61897fd48a9113efa9935c25b6dc9e4ddd078de3561bd710442219bb03d4","public_key_fingerprint_sha256":"874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a","scheme":"openssl-ed25519","signature_base64":"3NM25ZQblJCjp4sjdL3O7wkn5lDYXAZYIsA+jolZqiqAlYf928vOz/3GLQ2d8Oop1tfjAw5SiMTgcVjDEUlxAQ==","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":8,"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-16T17:55:20Z","tree_size":13,"type":"pacta.transparency.signed_tree_head.v1"}