mirror of
https://github.com/saymrwulf/lean-transparency-log.git
synced 2026-09-03 19:53:47 +00:00
log update: leaf 12 - attestation of ltl-accumulator-verified@172a1d0 (mechanized-model scope; KNOWN-GAPS 14/15)
The log now carries kernel-checked proofs of its own accumulator machinery. Entry 13 attests the ltl-accumulator-verified corpus at freeze 172a1d0: 61 certificates, all proven with exact axiom cones, single opaque-SHA-256 axiom boundary. Scope (in the leaf): the mechanized recursive model is kernel-checked; deployed-verifier correspondence is finite differential testing; the deployed consistency verifier is not extensionally equal to the model and relies on an unmechanized authentic-size/root invariant (gaps 14/15). tree 12 -> 13, root 3488a2d0; head signed verified-dalek-serial. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
parent
ec12dda9cb
commit
1726e8ec01
9 changed files with 2022 additions and 29 deletions
975
entries/000012.json
Normal file
975
entries/000012.json
Normal file
|
|
@ -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"
|
||||||
|
}
|
||||||
967
entries/ltl-accumulator-verified.attestation.json
Normal file
967
entries/ltl-accumulator-verified.attestation.json
Normal file
|
|
@ -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"
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -1,14 +1,14 @@
|
||||||
{
|
{
|
||||||
"hash_algorithm": "RFC9162_SHA256",
|
"hash_algorithm": "RFC9162_SHA256",
|
||||||
"log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7",
|
"log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7",
|
||||||
"root_hash": "bcd15f9d7ea1c9e5bd0a9e64fa8d846208b1e29ee167d4f1eac19b30e6913ee9",
|
"root_hash": "3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d",
|
||||||
"schema_version": 1,
|
"schema_version": 1,
|
||||||
"signatures": {
|
"signatures": {
|
||||||
"ed25519": {
|
"ed25519": {
|
||||||
"payload_digest_sha256": "fab790262c7e1b1eadc0fbf1d10481da0984cd7b99d6e19d98820d2c33d5f34d",
|
"payload_digest_sha256": "bd7d61897fd48a9113efa9935c25b6dc9e4ddd078de3561bd710442219bb03d4",
|
||||||
"public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a",
|
"public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a",
|
||||||
"scheme": "openssl-ed25519",
|
"scheme": "openssl-ed25519",
|
||||||
"signature_base64": "GYsT/T61aokWWbv+dqrMt1CtJTeGAC/aX0K1MazlXDo7tpEiex3O1uvox9mU/FWFIxwuBg/l2X8gB0DjYjc1Cw==",
|
"signature_base64": "3NM25ZQblJCjp4sjdL3O7wkn5lDYXAZYIsA+jolZqiqAlYf928vOz/3GLQ2d8Oop1tfjAw5SiMTgcVjDEUlxAQ==",
|
||||||
"signing_backend": "verified-dalek-serial",
|
"signing_backend": "verified-dalek-serial",
|
||||||
"signing_provenance": {
|
"signing_provenance": {
|
||||||
"self_inclusion": "verified",
|
"self_inclusion": "verified",
|
||||||
|
|
@ -27,7 +27,7 @@
|
||||||
"status": "not_configured"
|
"status": "not_configured"
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
"timestamp": "2026-07-07T19:12:17Z",
|
"timestamp": "2026-07-16T17:55:20Z",
|
||||||
"tree_size": 12,
|
"tree_size": 13,
|
||||||
"type": "pacta.transparency.signed_tree_head.v1"
|
"type": "pacta.transparency.signed_tree_head.v1"
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -3,6 +3,7 @@
|
||||||
"inclusion_proof": [
|
"inclusion_proof": [
|
||||||
"072b178a18d64012987903179d634cf22d1378d71f7e2a0d79fa29c95b0c3856",
|
"072b178a18d64012987903179d634cf22d1378d71f7e2a0d79fa29c95b0c3856",
|
||||||
"906823a87681cb8b448d0cb04a36a8f3e0583e2a13259fa849b55506ba903134",
|
"906823a87681cb8b448d0cb04a36a8f3e0583e2a13259fa849b55506ba903134",
|
||||||
|
"8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a",
|
||||||
"9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283"
|
"9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283"
|
||||||
],
|
],
|
||||||
"leaf_hash": "b1034bc68193c9c4eeee03289acd5641fc514615900cba7ee2457eaf25ef743b",
|
"leaf_hash": "b1034bc68193c9c4eeee03289acd5641fc514615900cba7ee2457eaf25ef743b",
|
||||||
|
|
@ -12,14 +13,14 @@
|
||||||
"sth": {
|
"sth": {
|
||||||
"hash_algorithm": "RFC9162_SHA256",
|
"hash_algorithm": "RFC9162_SHA256",
|
||||||
"log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7",
|
"log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7",
|
||||||
"root_hash": "bcd15f9d7ea1c9e5bd0a9e64fa8d846208b1e29ee167d4f1eac19b30e6913ee9",
|
"root_hash": "3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d",
|
||||||
"schema_version": 1,
|
"schema_version": 1,
|
||||||
"signatures": {
|
"signatures": {
|
||||||
"ed25519": {
|
"ed25519": {
|
||||||
"payload_digest_sha256": "fab790262c7e1b1eadc0fbf1d10481da0984cd7b99d6e19d98820d2c33d5f34d",
|
"payload_digest_sha256": "bd7d61897fd48a9113efa9935c25b6dc9e4ddd078de3561bd710442219bb03d4",
|
||||||
"public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a",
|
"public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a",
|
||||||
"scheme": "openssl-ed25519",
|
"scheme": "openssl-ed25519",
|
||||||
"signature_base64": "GYsT/T61aokWWbv+dqrMt1CtJTeGAC/aX0K1MazlXDo7tpEiex3O1uvox9mU/FWFIxwuBg/l2X8gB0DjYjc1Cw==",
|
"signature_base64": "3NM25ZQblJCjp4sjdL3O7wkn5lDYXAZYIsA+jolZqiqAlYf928vOz/3GLQ2d8Oop1tfjAw5SiMTgcVjDEUlxAQ==",
|
||||||
"signing_backend": "verified-dalek-serial",
|
"signing_backend": "verified-dalek-serial",
|
||||||
"signing_provenance": {
|
"signing_provenance": {
|
||||||
"self_inclusion": "verified",
|
"self_inclusion": "verified",
|
||||||
|
|
@ -38,10 +39,10 @@
|
||||||
"status": "not_configured"
|
"status": "not_configured"
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
"timestamp": "2026-07-07T19:12:17Z",
|
"timestamp": "2026-07-16T17:55:20Z",
|
||||||
"tree_size": 12,
|
"tree_size": 13,
|
||||||
"type": "pacta.transparency.signed_tree_head.v1"
|
"type": "pacta.transparency.signed_tree_head.v1"
|
||||||
},
|
},
|
||||||
"tree_size": 12,
|
"tree_size": 13,
|
||||||
"type": "pacta.transparency.receipt.v1"
|
"type": "pacta.transparency.receipt.v1"
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -3,6 +3,7 @@
|
||||||
"inclusion_proof": [
|
"inclusion_proof": [
|
||||||
"ed368f5f9b3714b5c633bc55971b61c31af55a8022ac9fb567515810007b527f",
|
"ed368f5f9b3714b5c633bc55971b61c31af55a8022ac9fb567515810007b527f",
|
||||||
"3253f2e4dcb5515e0caf021b1e4a257a15bd04df969aaf08174da745d72cd00f",
|
"3253f2e4dcb5515e0caf021b1e4a257a15bd04df969aaf08174da745d72cd00f",
|
||||||
|
"8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a",
|
||||||
"9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283"
|
"9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283"
|
||||||
],
|
],
|
||||||
"leaf_hash": "ad7ccbb6def18dccba7176f4be36ad1ce731c1456672c19310e73e87c4f312df",
|
"leaf_hash": "ad7ccbb6def18dccba7176f4be36ad1ce731c1456672c19310e73e87c4f312df",
|
||||||
|
|
@ -12,14 +13,14 @@
|
||||||
"sth": {
|
"sth": {
|
||||||
"hash_algorithm": "RFC9162_SHA256",
|
"hash_algorithm": "RFC9162_SHA256",
|
||||||
"log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7",
|
"log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7",
|
||||||
"root_hash": "bcd15f9d7ea1c9e5bd0a9e64fa8d846208b1e29ee167d4f1eac19b30e6913ee9",
|
"root_hash": "3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d",
|
||||||
"schema_version": 1,
|
"schema_version": 1,
|
||||||
"signatures": {
|
"signatures": {
|
||||||
"ed25519": {
|
"ed25519": {
|
||||||
"payload_digest_sha256": "fab790262c7e1b1eadc0fbf1d10481da0984cd7b99d6e19d98820d2c33d5f34d",
|
"payload_digest_sha256": "bd7d61897fd48a9113efa9935c25b6dc9e4ddd078de3561bd710442219bb03d4",
|
||||||
"public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a",
|
"public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a",
|
||||||
"scheme": "openssl-ed25519",
|
"scheme": "openssl-ed25519",
|
||||||
"signature_base64": "GYsT/T61aokWWbv+dqrMt1CtJTeGAC/aX0K1MazlXDo7tpEiex3O1uvox9mU/FWFIxwuBg/l2X8gB0DjYjc1Cw==",
|
"signature_base64": "3NM25ZQblJCjp4sjdL3O7wkn5lDYXAZYIsA+jolZqiqAlYf928vOz/3GLQ2d8Oop1tfjAw5SiMTgcVjDEUlxAQ==",
|
||||||
"signing_backend": "verified-dalek-serial",
|
"signing_backend": "verified-dalek-serial",
|
||||||
"signing_provenance": {
|
"signing_provenance": {
|
||||||
"self_inclusion": "verified",
|
"self_inclusion": "verified",
|
||||||
|
|
@ -38,10 +39,10 @@
|
||||||
"status": "not_configured"
|
"status": "not_configured"
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
"timestamp": "2026-07-07T19:12:17Z",
|
"timestamp": "2026-07-16T17:55:20Z",
|
||||||
"tree_size": 12,
|
"tree_size": 13,
|
||||||
"type": "pacta.transparency.signed_tree_head.v1"
|
"type": "pacta.transparency.signed_tree_head.v1"
|
||||||
},
|
},
|
||||||
"tree_size": 12,
|
"tree_size": 13,
|
||||||
"type": "pacta.transparency.receipt.v1"
|
"type": "pacta.transparency.receipt.v1"
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -3,6 +3,7 @@
|
||||||
"inclusion_proof": [
|
"inclusion_proof": [
|
||||||
"b1034bc68193c9c4eeee03289acd5641fc514615900cba7ee2457eaf25ef743b",
|
"b1034bc68193c9c4eeee03289acd5641fc514615900cba7ee2457eaf25ef743b",
|
||||||
"906823a87681cb8b448d0cb04a36a8f3e0583e2a13259fa849b55506ba903134",
|
"906823a87681cb8b448d0cb04a36a8f3e0583e2a13259fa849b55506ba903134",
|
||||||
|
"8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a",
|
||||||
"9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283"
|
"9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283"
|
||||||
],
|
],
|
||||||
"leaf_hash": "072b178a18d64012987903179d634cf22d1378d71f7e2a0d79fa29c95b0c3856",
|
"leaf_hash": "072b178a18d64012987903179d634cf22d1378d71f7e2a0d79fa29c95b0c3856",
|
||||||
|
|
@ -12,14 +13,14 @@
|
||||||
"sth": {
|
"sth": {
|
||||||
"hash_algorithm": "RFC9162_SHA256",
|
"hash_algorithm": "RFC9162_SHA256",
|
||||||
"log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7",
|
"log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7",
|
||||||
"root_hash": "bcd15f9d7ea1c9e5bd0a9e64fa8d846208b1e29ee167d4f1eac19b30e6913ee9",
|
"root_hash": "3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d",
|
||||||
"schema_version": 1,
|
"schema_version": 1,
|
||||||
"signatures": {
|
"signatures": {
|
||||||
"ed25519": {
|
"ed25519": {
|
||||||
"payload_digest_sha256": "fab790262c7e1b1eadc0fbf1d10481da0984cd7b99d6e19d98820d2c33d5f34d",
|
"payload_digest_sha256": "bd7d61897fd48a9113efa9935c25b6dc9e4ddd078de3561bd710442219bb03d4",
|
||||||
"public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a",
|
"public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a",
|
||||||
"scheme": "openssl-ed25519",
|
"scheme": "openssl-ed25519",
|
||||||
"signature_base64": "GYsT/T61aokWWbv+dqrMt1CtJTeGAC/aX0K1MazlXDo7tpEiex3O1uvox9mU/FWFIxwuBg/l2X8gB0DjYjc1Cw==",
|
"signature_base64": "3NM25ZQblJCjp4sjdL3O7wkn5lDYXAZYIsA+jolZqiqAlYf928vOz/3GLQ2d8Oop1tfjAw5SiMTgcVjDEUlxAQ==",
|
||||||
"signing_backend": "verified-dalek-serial",
|
"signing_backend": "verified-dalek-serial",
|
||||||
"signing_provenance": {
|
"signing_provenance": {
|
||||||
"self_inclusion": "verified",
|
"self_inclusion": "verified",
|
||||||
|
|
@ -38,10 +39,10 @@
|
||||||
"status": "not_configured"
|
"status": "not_configured"
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
"timestamp": "2026-07-07T19:12:17Z",
|
"timestamp": "2026-07-16T17:55:20Z",
|
||||||
"tree_size": 12,
|
"tree_size": 13,
|
||||||
"type": "pacta.transparency.signed_tree_head.v1"
|
"type": "pacta.transparency.signed_tree_head.v1"
|
||||||
},
|
},
|
||||||
"tree_size": 12,
|
"tree_size": 13,
|
||||||
"type": "pacta.transparency.receipt.v1"
|
"type": "pacta.transparency.receipt.v1"
|
||||||
}
|
}
|
||||||
|
|
|
||||||
46
receipts/ltl-accumulator-verified.receipt.json
Normal file
46
receipts/ltl-accumulator-verified.receipt.json
Normal file
|
|
@ -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"
|
||||||
|
}
|
||||||
|
|
@ -3,6 +3,7 @@
|
||||||
"inclusion_proof": [
|
"inclusion_proof": [
|
||||||
"ad7ccbb6def18dccba7176f4be36ad1ce731c1456672c19310e73e87c4f312df",
|
"ad7ccbb6def18dccba7176f4be36ad1ce731c1456672c19310e73e87c4f312df",
|
||||||
"3253f2e4dcb5515e0caf021b1e4a257a15bd04df969aaf08174da745d72cd00f",
|
"3253f2e4dcb5515e0caf021b1e4a257a15bd04df969aaf08174da745d72cd00f",
|
||||||
|
"8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a",
|
||||||
"9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283"
|
"9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283"
|
||||||
],
|
],
|
||||||
"leaf_hash": "ed368f5f9b3714b5c633bc55971b61c31af55a8022ac9fb567515810007b527f",
|
"leaf_hash": "ed368f5f9b3714b5c633bc55971b61c31af55a8022ac9fb567515810007b527f",
|
||||||
|
|
@ -12,14 +13,14 @@
|
||||||
"sth": {
|
"sth": {
|
||||||
"hash_algorithm": "RFC9162_SHA256",
|
"hash_algorithm": "RFC9162_SHA256",
|
||||||
"log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7",
|
"log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7",
|
||||||
"root_hash": "bcd15f9d7ea1c9e5bd0a9e64fa8d846208b1e29ee167d4f1eac19b30e6913ee9",
|
"root_hash": "3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d",
|
||||||
"schema_version": 1,
|
"schema_version": 1,
|
||||||
"signatures": {
|
"signatures": {
|
||||||
"ed25519": {
|
"ed25519": {
|
||||||
"payload_digest_sha256": "fab790262c7e1b1eadc0fbf1d10481da0984cd7b99d6e19d98820d2c33d5f34d",
|
"payload_digest_sha256": "bd7d61897fd48a9113efa9935c25b6dc9e4ddd078de3561bd710442219bb03d4",
|
||||||
"public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a",
|
"public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a",
|
||||||
"scheme": "openssl-ed25519",
|
"scheme": "openssl-ed25519",
|
||||||
"signature_base64": "GYsT/T61aokWWbv+dqrMt1CtJTeGAC/aX0K1MazlXDo7tpEiex3O1uvox9mU/FWFIxwuBg/l2X8gB0DjYjc1Cw==",
|
"signature_base64": "3NM25ZQblJCjp4sjdL3O7wkn5lDYXAZYIsA+jolZqiqAlYf928vOz/3GLQ2d8Oop1tfjAw5SiMTgcVjDEUlxAQ==",
|
||||||
"signing_backend": "verified-dalek-serial",
|
"signing_backend": "verified-dalek-serial",
|
||||||
"signing_provenance": {
|
"signing_provenance": {
|
||||||
"self_inclusion": "verified",
|
"self_inclusion": "verified",
|
||||||
|
|
@ -38,10 +39,10 @@
|
||||||
"status": "not_configured"
|
"status": "not_configured"
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
"timestamp": "2026-07-07T19:12:17Z",
|
"timestamp": "2026-07-16T17:55:20Z",
|
||||||
"tree_size": 12,
|
"tree_size": 13,
|
||||||
"type": "pacta.transparency.signed_tree_head.v1"
|
"type": "pacta.transparency.signed_tree_head.v1"
|
||||||
},
|
},
|
||||||
"tree_size": 12,
|
"tree_size": 13,
|
||||||
"type": "pacta.transparency.receipt.v1"
|
"type": "pacta.transparency.receipt.v1"
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -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":"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":"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":"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"}
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue