mirror of
https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git
synced 2026-09-04 20:03:40 +00:00
REAL EVIDENCE: guarded replay of all four repos, attested, logged, dogfooded
The provider ran its full honest replay against the four verified
repositories on this machine - every Lean compile and axiom audit routed
through lean-guard (memory-capped, core-pinned, single-flight, ~30 min
per fork) - and the results are now shipped under evidence/:
- 16/16 certificates proven per fork, every axiom cone boundary-exact
(the four apex tiers carry their fork's documented SHA-512/wire
boundary axiom-for-axiom), each attestation pinned to the exact repo
commit (dalek 8ded7bc, anza 673c15e, risc0 98a13a6, betrusted
81f614a) and Ed25519-signed.
- All four appended to the persistent transparency log. The log holds
EIGHT leaves: the first four are the initial run's attestations,
which honestly recorded an AUDIT FAILURE (the two pacta bugs fixed in
e87f0e8) - an append-only trust ledger keeps its bad day, and the
fixed run's leaves sit beside it.
- Every receipt re-verified through the FULL stack: dogfood verifier
(backend verified-dalek-serial recorded), STH pin store, freshness
policy. Receipts are freshly issued against the final tree (a stale
mid-run receipt tripped the pin store's rollback defense exactly as
designed; the rollback diagnostic now hints at idempotent re-issue).
- The capstone consequence ran for real: pacta agent with trusted
provider + signature via the proven path + required receipt + pin
store + --require-verified-verifier built the R4-gated library
capsule from ATTESTED evidence (no local Lean replay needed by the
consuming agent).
Docs and teaching updated against the real artifacts: evidence/README
(inventory + re-verify instructions), README "Real Evidence" section,
lecture 5 now re-derives 16/16 verdicts from the REAL dalek attestation
(signature checked on the proven path, provider labels ignored), and
lecture 6 verifies all four REAL receipts and walks a fresh pin store
over them. Every changed notebook cell executed before commit. 49/49
tests green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
parent
e87f0e8b05
commit
71c670527c
18 changed files with 1465 additions and 1 deletions
12
README.md
12
README.md
|
|
@ -216,6 +216,18 @@ pacta agent \
|
|||
|
||||
This is the intended trust transformation: local agents can avoid constructing the full verifier environment, but they must explicitly trust the provider identity and verification key.
|
||||
|
||||
## Real Evidence (shipped)
|
||||
|
||||
`evidence/` contains signed, transparency-logged attestations from a REAL
|
||||
guarded replay of all four verified repositories: 16/16 certificates proven
|
||||
per fork with boundary-exact axiom cones, pinned to exact repo commits,
|
||||
machine-protected by `lean-guard` throughout (~30 min of Lean kernel
|
||||
re-checking per fork, done ONCE - verifying the signature + inclusion
|
||||
receipt afterwards takes milliseconds, which is the entire point of the
|
||||
provider model). The log's first four leaves honestly record a failed audit
|
||||
run (two pacta bugs, fixed and documented); the ledger keeps its history.
|
||||
See `evidence/README.md` to re-verify everything yourself.
|
||||
|
||||
## Split-View Defense (STH Pinning)
|
||||
|
||||
Standalone receipt verification cannot detect a provider maintaining two log views. `pacta` keeps a local STH pin store:
|
||||
|
|
|
|||
29
evidence/README.md
Normal file
29
evidence/README.md
Normal file
|
|
@ -0,0 +1,29 @@
|
|||
# Real Provider Evidence
|
||||
|
||||
Signed, transparency-logged attestations from a REAL guarded replay of the
|
||||
four `saymrwulf/*-ed25519-verified` repositories (2026-07-06/07, ~30 min of
|
||||
Lean re-checking per fork under `lean-guard` memory caps).
|
||||
|
||||
| File | What it is |
|
||||
|---|---|
|
||||
| `<fork>-ed25519.attestation.yaml` | Signed proof-check attestation: repo commit, environment, machine-protection block, and all 16 certificates with their OBSERVED axiom cones (the four apex tiers carry the fork's exact documented boundary) |
|
||||
| `<fork>-ed25519.receipt.yaml` | RFC 9162-style inclusion receipt binding the attestation into the transparency log (tree size 8), with a consistency anchor |
|
||||
| `provider.ed25519.pub` | The provider's public key (the PRIVATE key never leaves `provider/state/`, which is gitignored) |
|
||||
| `log-metadata.json`, `latest-sth.yaml` | Log identity and the latest Signed Tree Head |
|
||||
| `log-audit.txt` | Monitor self-check output (recomputed root matches the signed root) |
|
||||
|
||||
The log holds EIGHT leaves: entries 0-3 are the first run's attestations,
|
||||
which honestly record an AUDIT FAILURE (two bugs in pacta's audit step,
|
||||
since fixed - see the commit history); entries 4-7 are the definitive
|
||||
16/16-proven attestations. An append-only trust ledger keeps its bad day.
|
||||
|
||||
Re-verify everything yourself (signature via the proven-path verifier if
|
||||
built, STH pinning, freshness):
|
||||
|
||||
```bash
|
||||
pacta receipt-verify \
|
||||
--attestation evidence/dalek-ed25519.attestation.yaml \
|
||||
--receipt evidence/dalek-ed25519.receipt.yaml \
|
||||
--log-public-key evidence/provider.ed25519.pub \
|
||||
--sth-store /tmp/my-pins.json --max-sth-age-seconds 604800
|
||||
```
|
||||
262
evidence/anza-ed25519.attestation.yaml
Normal file
262
evidence/anza-ed25519.attestation.yaml
Normal file
|
|
@ -0,0 +1,262 @@
|
|||
schema_version: 1
|
||||
provider: local-pacta-provider
|
||||
issued_at: '2026-07-06T11:51:00Z'
|
||||
machine_protection:
|
||||
lean_guard: /home/oho/GitClone/Claude/FormalVerification/anza-ed25519-verified/verification/lean-guard
|
||||
note: All Lean compiles route through the repo's lean-guard (memory cap, core pinning,
|
||||
timeout, single-flight lock) when configured.
|
||||
subject:
|
||||
component: anza-ed25519-verified
|
||||
repo_url: https://github.com/saymrwulf/anza-ed25519-verified.git
|
||||
repo_commit: 673c15e10a082788f7965fcb0faeefcca0d15136
|
||||
verification_dir: verification
|
||||
kind: ed25519
|
||||
verified_backend: serial/u64
|
||||
environment:
|
||||
lean_version: Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc,
|
||||
Release)
|
||||
lake_version: Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)
|
||||
env_script: ~/aeneas-toolchain/env.sh
|
||||
lean_project_dir: /home/oho/aeneas-toolchain/aeneas/backends/lean
|
||||
replay:
|
||||
check_attempted: true
|
||||
check_ok: true
|
||||
check_log_path: provider/out/logs/lean-check.log
|
||||
checked_files: 58
|
||||
failed_files: []
|
||||
diagnostics: []
|
||||
axiom_attempted: true
|
||||
axiom_ok: true
|
||||
axiom_log_path: provider/out/logs/axiom-audit.log
|
||||
axiom_diagnostics: []
|
||||
certificates:
|
||||
- name: CurveFieldProofs.fieldImplementation
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.edwardsImplementation
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: ScalarProofs.scalarImplementation
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_loop_full
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.to_bytes_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.ed_compress_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: ScalarProofs.from_bytes_mod_order_wide_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.vartime_dsm_basepoint_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.enc_point_inj
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.sqrt_ratio_i_sq_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.from_bytes_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.decompress_of_canonical
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- ed_sigs.sha512_hash3
|
||||
- ed25519.Signature.r_bytes
|
||||
- ed25519.Signature.s_bytes
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- ed_sigs.sha512_hash3
|
||||
- ed25519.Signature.r_bytes
|
||||
- ed25519.Signature.s_bytes
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff_point
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- ed_sigs.sha512_hash3
|
||||
- ed25519.Signature.r_bytes
|
||||
- ed25519.Signature.s_bytes
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- ed_sigs.sha512_hash3
|
||||
- ed25519.Signature.r_bytes
|
||||
- ed25519.Signature.s_bytes
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff_point_eq
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- ed_sigs.sha512_hash3
|
||||
- ed25519.Signature.r_bytes
|
||||
- ed25519.Signature.s_bytes
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- ed_sigs.sha512_hash3
|
||||
- ed25519.Signature.r_bytes
|
||||
- ed25519.Signature.s_bytes
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff_decompress
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- ed_sigs.sha512_hash3
|
||||
- ed25519.Signature.r_bytes
|
||||
- ed25519.Signature.s_bytes
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- ed_sigs.sha512_hash3
|
||||
- ed25519.Signature.r_bytes
|
||||
- ed25519.Signature.s_bytes
|
||||
diagnostics: []
|
||||
signature:
|
||||
scheme: openssl-ed25519
|
||||
status: signed
|
||||
payload_digest_sha256: ff36182e67d083ac442fce5026fe31ae8127b4f04bc6b5a85b70c9cae9ed8f8d
|
||||
signature_base64: fFGMNOf1a1sk14Cu2BLP2Dl4DWcipXJiPe7KlZuHyCXyhz91NEuLr4VObIa4wP9J61PThXwVwLDEnnHuOH6BCA==
|
||||
public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a
|
||||
39
evidence/anza-ed25519.receipt.yaml
Normal file
39
evidence/anza-ed25519.receipt.yaml
Normal file
|
|
@ -0,0 +1,39 @@
|
|||
schema_version: 1
|
||||
type: pacta.transparency.receipt.v1
|
||||
log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7
|
||||
hash_algorithm: RFC9162_SHA256
|
||||
attestation_path: provider/out/anza-ed25519.attestation.yaml
|
||||
attestation_digest_sha256: 99d7037f592453e4a176ffbbb314245e32e6014738e38e64b3f166992d6fd9ad
|
||||
leaf_index: 5
|
||||
leaf_hash: 33523f3ea6b6eab72696eead8534d0b7cac78feb60cc3907ac973a24f37adb95
|
||||
tree_size: 8
|
||||
inclusion_proof:
|
||||
- ca164b6cf11aec6a4c8de2d18c2c2fa04c9323657bd7daf4e7111869201bfec2
|
||||
- 3bb1e72abbc9c0b945dafde303acdab123996e41faeab49a35563886b1b41e96
|
||||
- 04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed
|
||||
consistency:
|
||||
from_tree_size: 8
|
||||
from_root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283
|
||||
proof: []
|
||||
status: not_applicable
|
||||
sth:
|
||||
schema_version: 1
|
||||
type: pacta.transparency.signed_tree_head.v1
|
||||
log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7
|
||||
tree_size: 8
|
||||
timestamp: '2026-07-06T12:53:08Z'
|
||||
root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283
|
||||
hash_algorithm: RFC9162_SHA256
|
||||
signatures:
|
||||
ed25519:
|
||||
scheme: openssl-ed25519
|
||||
status: signed
|
||||
payload_digest_sha256: d783b70d6124bd2206bed6671ce83e9b292dec41761527326695d5e23b12eb8b
|
||||
signature_base64: 0Si0Mb46p5xmPu8EJp9wm/Cle3xClHYYRLBFksjnygVci8U+RE4uBNydU0dSQT7FrnJB+xdwCn5NBRnUnjaECg==
|
||||
public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a
|
||||
ml_dsa:
|
||||
scheme: ML-DSA-65
|
||||
standard: FIPS 204
|
||||
status: not_configured
|
||||
reason: A backend appears available, but no ML-DSA signing key was configured
|
||||
for this log.
|
||||
270
evidence/betrusted-ed25519.attestation.yaml
Normal file
270
evidence/betrusted-ed25519.attestation.yaml
Normal file
|
|
@ -0,0 +1,270 @@
|
|||
schema_version: 1
|
||||
provider: local-pacta-provider
|
||||
issued_at: '2026-07-06T12:51:28Z'
|
||||
machine_protection:
|
||||
lean_guard: /home/oho/GitClone/Claude/FormalVerification/betrusted-ed25519-verified/verification/lean-guard
|
||||
note: All Lean compiles route through the repo's lean-guard (memory cap, core pinning,
|
||||
timeout, single-flight lock) when configured.
|
||||
subject:
|
||||
component: betrusted-ed25519-verified
|
||||
repo_url: https://github.com/saymrwulf/betrusted-ed25519-verified.git
|
||||
repo_commit: 81f614a3cbd26412c6af7f0a31c0f128121fbfa4
|
||||
verification_dir: verification
|
||||
kind: ed25519
|
||||
verified_backend: serial/u64
|
||||
environment:
|
||||
lean_version: Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc,
|
||||
Release)
|
||||
lake_version: Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)
|
||||
env_script: ~/aeneas-toolchain/env.sh
|
||||
lean_project_dir: /home/oho/aeneas-toolchain/aeneas/backends/lean
|
||||
replay:
|
||||
check_attempted: true
|
||||
check_ok: true
|
||||
check_log_path: provider/out/logs/lean-check.log
|
||||
checked_files: 63
|
||||
failed_files: []
|
||||
diagnostics: []
|
||||
axiom_attempted: true
|
||||
axiom_ok: true
|
||||
axiom_log_path: provider/out/logs/axiom-audit.log
|
||||
axiom_diagnostics: []
|
||||
certificates:
|
||||
- name: CurveFieldProofs.fieldImplementation
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.edwardsImplementation
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: ScalarProofs.scalarImplementation
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_loop_full
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.to_bytes_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.ed_compress_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: ScalarProofs.from_bytes_mod_order_wide_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.vartime_dsm_basepoint_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.enc_point_inj
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.sqrt_ratio_i_sq_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.from_bytes_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.decompress_of_canonical
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff_point
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff_point_eq
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff_decompress
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
diagnostics: []
|
||||
signature:
|
||||
scheme: openssl-ed25519
|
||||
status: signed
|
||||
payload_digest_sha256: bb1226fa66ae0e51677ccc8c8361ba121ac5464911f1cb9e305ff7c76b7d2c57
|
||||
signature_base64: Lsxje95BPXHfc7l3wxQrRvDgG/5tb7WNaO3wIDsfY/xg/WYRDFrWF3Bb6frs0Dmln00QxA99Gt43PMxLUHq0Ag==
|
||||
public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a
|
||||
39
evidence/betrusted-ed25519.receipt.yaml
Normal file
39
evidence/betrusted-ed25519.receipt.yaml
Normal file
|
|
@ -0,0 +1,39 @@
|
|||
schema_version: 1
|
||||
type: pacta.transparency.receipt.v1
|
||||
log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7
|
||||
hash_algorithm: RFC9162_SHA256
|
||||
attestation_path: provider/out/betrusted-ed25519.attestation.yaml
|
||||
attestation_digest_sha256: 5bd2a597d712a6a80e6ba82baabcdbbbd54bc913e8a77375a6ae42e2cb7b1c57
|
||||
leaf_index: 7
|
||||
leaf_hash: 2791c352956ebc620a4fe12b20bfd6faa0813238c5bc0563fa4eb0130d829247
|
||||
tree_size: 8
|
||||
inclusion_proof:
|
||||
- bdde4e4b87cd263b5914dbbae0c85ceed468c3054596f6ca79121e54cc6a134e
|
||||
- f3724e66715b582c384cf49928d4705458475ea4293749989c483ab7fe9496ce
|
||||
- 04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed
|
||||
consistency:
|
||||
from_tree_size: 8
|
||||
from_root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283
|
||||
proof: []
|
||||
status: not_applicable
|
||||
sth:
|
||||
schema_version: 1
|
||||
type: pacta.transparency.signed_tree_head.v1
|
||||
log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7
|
||||
tree_size: 8
|
||||
timestamp: '2026-07-06T12:53:09Z'
|
||||
root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283
|
||||
hash_algorithm: RFC9162_SHA256
|
||||
signatures:
|
||||
ed25519:
|
||||
scheme: openssl-ed25519
|
||||
status: signed
|
||||
payload_digest_sha256: d5d25db2c90f0246cc10d10f912085b81c60d2a324354b5abecfdbeb8bd17ee2
|
||||
signature_base64: sI4rWnWMrX0zDaN8jofBwSuExKg1e0cmZV3OPaulbXDV97yz95aSo0Gnrfd1En2vyyV1qoEXdTAY9NDgvA8xBA==
|
||||
public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a
|
||||
ml_dsa:
|
||||
scheme: ML-DSA-65
|
||||
standard: FIPS 204
|
||||
status: not_configured
|
||||
reason: A backend appears available, but no ML-DSA signing key was configured
|
||||
for this log.
|
||||
294
evidence/dalek-ed25519.attestation.yaml
Normal file
294
evidence/dalek-ed25519.attestation.yaml
Normal file
|
|
@ -0,0 +1,294 @@
|
|||
schema_version: 1
|
||||
provider: local-pacta-provider
|
||||
issued_at: '2026-07-06T11:21:25Z'
|
||||
machine_protection:
|
||||
lean_guard: /home/oho/GitClone/Claude/FormalVerification/dalek-ed25519-verified/verification/lean-guard
|
||||
note: All Lean compiles route through the repo's lean-guard (memory cap, core pinning,
|
||||
timeout, single-flight lock) when configured.
|
||||
subject:
|
||||
component: dalek-ed25519-verified
|
||||
repo_url: https://github.com/saymrwulf/dalek-ed25519-verified.git
|
||||
repo_commit: 8ded7bcf9a1f0016cee93f371796b935b25b7ff8
|
||||
verification_dir: verification
|
||||
kind: ed25519
|
||||
verified_backend: serial/u64
|
||||
environment:
|
||||
lean_version: Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc,
|
||||
Release)
|
||||
lake_version: Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)
|
||||
env_script: ~/aeneas-toolchain/env.sh
|
||||
lean_project_dir: /home/oho/aeneas-toolchain/aeneas/backends/lean
|
||||
replay:
|
||||
check_attempted: true
|
||||
check_ok: true
|
||||
check_log_path: provider/out/logs/lean-check.log
|
||||
checked_files: 64
|
||||
failed_files: []
|
||||
diagnostics: []
|
||||
axiom_attempted: true
|
||||
axiom_ok: true
|
||||
axiom_log_path: provider/out/logs/axiom-audit.log
|
||||
axiom_diagnostics: []
|
||||
certificates:
|
||||
- name: CurveFieldProofs.fieldImplementation
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.edwardsImplementation
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: ScalarProofs.scalarImplementation
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_loop_full
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.to_bytes_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.ed_compress_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: ScalarProofs.from_bytes_mod_order_wide_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.vartime_dsm_basepoint_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.enc_point_inj
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.sqrt_ratio_i_sq_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.from_bytes_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.decompress_of_canonical
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- sha2.Sha512
|
||||
- verifying.sha512_finalize_bytes
|
||||
- verifying.sha512_new
|
||||
- verifying.sha512_update
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- sha2.Sha512
|
||||
- verifying.sha512_new
|
||||
- verifying.sha512_update
|
||||
- verifying.sha512_finalize_bytes
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff_point
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- sha2.Sha512
|
||||
- verifying.sha512_finalize_bytes
|
||||
- verifying.sha512_new
|
||||
- verifying.sha512_update
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- sha2.Sha512
|
||||
- verifying.sha512_new
|
||||
- verifying.sha512_update
|
||||
- verifying.sha512_finalize_bytes
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff_point_eq
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- sha2.Sha512
|
||||
- verifying.sha512_finalize_bytes
|
||||
- verifying.sha512_new
|
||||
- verifying.sha512_update
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- sha2.Sha512
|
||||
- verifying.sha512_new
|
||||
- verifying.sha512_update
|
||||
- verifying.sha512_finalize_bytes
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff_decompress
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- sha2.Sha512
|
||||
- verifying.sha512_finalize_bytes
|
||||
- verifying.sha512_new
|
||||
- verifying.sha512_update
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- sha2.Sha512
|
||||
- verifying.sha512_new
|
||||
- verifying.sha512_update
|
||||
- verifying.sha512_finalize_bytes
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
diagnostics: []
|
||||
signature:
|
||||
scheme: openssl-ed25519
|
||||
status: signed
|
||||
payload_digest_sha256: ba9c3de2b75af13cd79aaaf1226a07c3e671f2d5fe06dd2a33810588dfe21571
|
||||
signature_base64: Ec0xxNT6PeyuNXUncaeZN9iDJN/q3W/WenqGrx3qWDfYu9xK5Hq7e4zLALqZKrNCBaPXBm4oSYKUd1qSNoWSBg==
|
||||
public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a
|
||||
39
evidence/dalek-ed25519.receipt.yaml
Normal file
39
evidence/dalek-ed25519.receipt.yaml
Normal file
|
|
@ -0,0 +1,39 @@
|
|||
schema_version: 1
|
||||
type: pacta.transparency.receipt.v1
|
||||
log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7
|
||||
hash_algorithm: RFC9162_SHA256
|
||||
attestation_path: provider/out/dalek-ed25519.attestation.yaml
|
||||
attestation_digest_sha256: d0921bfd2ad20980332ca5626bad79bc713a3e5c7919ce705043bb6097ecf1b3
|
||||
leaf_index: 4
|
||||
leaf_hash: ca164b6cf11aec6a4c8de2d18c2c2fa04c9323657bd7daf4e7111869201bfec2
|
||||
tree_size: 8
|
||||
inclusion_proof:
|
||||
- 33523f3ea6b6eab72696eead8534d0b7cac78feb60cc3907ac973a24f37adb95
|
||||
- 3bb1e72abbc9c0b945dafde303acdab123996e41faeab49a35563886b1b41e96
|
||||
- 04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed
|
||||
consistency:
|
||||
from_tree_size: 8
|
||||
from_root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283
|
||||
proof: []
|
||||
status: not_applicable
|
||||
sth:
|
||||
schema_version: 1
|
||||
type: pacta.transparency.signed_tree_head.v1
|
||||
log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7
|
||||
tree_size: 8
|
||||
timestamp: '2026-07-06T12:53:08Z'
|
||||
root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283
|
||||
hash_algorithm: RFC9162_SHA256
|
||||
signatures:
|
||||
ed25519:
|
||||
scheme: openssl-ed25519
|
||||
status: signed
|
||||
payload_digest_sha256: d783b70d6124bd2206bed6671ce83e9b292dec41761527326695d5e23b12eb8b
|
||||
signature_base64: 0Si0Mb46p5xmPu8EJp9wm/Cle3xClHYYRLBFksjnygVci8U+RE4uBNydU0dSQT7FrnJB+xdwCn5NBRnUnjaECg==
|
||||
public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a
|
||||
ml_dsa:
|
||||
scheme: ML-DSA-65
|
||||
standard: FIPS 204
|
||||
status: not_configured
|
||||
reason: A backend appears available, but no ML-DSA signing key was configured
|
||||
for this log.
|
||||
20
evidence/latest-sth.yaml
Normal file
20
evidence/latest-sth.yaml
Normal file
|
|
@ -0,0 +1,20 @@
|
|||
schema_version: 1
|
||||
type: pacta.transparency.signed_tree_head.v1
|
||||
log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7
|
||||
tree_size: 8
|
||||
timestamp: '2026-07-06T12:53:09Z'
|
||||
root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283
|
||||
hash_algorithm: RFC9162_SHA256
|
||||
signatures:
|
||||
ed25519:
|
||||
scheme: openssl-ed25519
|
||||
status: signed
|
||||
payload_digest_sha256: d5d25db2c90f0246cc10d10f912085b81c60d2a324354b5abecfdbeb8bd17ee2
|
||||
signature_base64: sI4rWnWMrX0zDaN8jofBwSuExKg1e0cmZV3OPaulbXDV97yz95aSo0Gnrfd1En2vyyV1qoEXdTAY9NDgvA8xBA==
|
||||
public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a
|
||||
ml_dsa:
|
||||
scheme: ML-DSA-65
|
||||
standard: FIPS 204
|
||||
status: not_configured
|
||||
reason: A backend appears available, but no ML-DSA signing key was configured
|
||||
for this log.
|
||||
4
evidence/log-audit.txt
Normal file
4
evidence/log-audit.txt
Normal file
|
|
@ -0,0 +1,4 @@
|
|||
tree_size: 8
|
||||
computed_root: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283
|
||||
stored_sth_root: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283
|
||||
ok: true
|
||||
14
evidence/log-metadata.json
Normal file
14
evidence/log-metadata.json
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
{
|
||||
"created_at": "2026-07-06T08:43:00Z",
|
||||
"ed25519_public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a",
|
||||
"hash_algorithm": "RFC9162_SHA256",
|
||||
"log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7",
|
||||
"provider": "local-pacta-provider",
|
||||
"schema_version": 1,
|
||||
"standards": [
|
||||
"RFC 9162 Merkle tree hash and inclusion/consistency proof algorithms",
|
||||
"RFC 8032 Ed25519 signature verification via OpenSSL",
|
||||
"FIPS 204 ML-DSA signature slot; must be required by policy only when a backend is configured"
|
||||
],
|
||||
"type": "pacta.transparency.log_metadata.v1"
|
||||
}
|
||||
3
evidence/provider.ed25519.pub
Normal file
3
evidence/provider.ed25519.pub
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
-----BEGIN PUBLIC KEY-----
|
||||
MCowBQYDK2VwAyEAd6WIt2/WNJCcKMZGo67BQoZI84LbvLaYMvpwAWNXsxU=
|
||||
-----END PUBLIC KEY-----
|
||||
270
evidence/risc0-ed25519.attestation.yaml
Normal file
270
evidence/risc0-ed25519.attestation.yaml
Normal file
|
|
@ -0,0 +1,270 @@
|
|||
schema_version: 1
|
||||
provider: local-pacta-provider
|
||||
issued_at: '2026-07-06T12:21:40Z'
|
||||
machine_protection:
|
||||
lean_guard: /home/oho/GitClone/Claude/FormalVerification/risc0-ed25519-verified/verification/lean-guard
|
||||
note: All Lean compiles route through the repo's lean-guard (memory cap, core pinning,
|
||||
timeout, single-flight lock) when configured.
|
||||
subject:
|
||||
component: risc0-ed25519-verified
|
||||
repo_url: https://github.com/saymrwulf/risc0-ed25519-verified.git
|
||||
repo_commit: 98a13a68539b20ac0279876848aea3687e523462
|
||||
verification_dir: verification
|
||||
kind: ed25519
|
||||
verified_backend: serial/u64
|
||||
environment:
|
||||
lean_version: Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc,
|
||||
Release)
|
||||
lake_version: Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)
|
||||
env_script: ~/aeneas-toolchain/env.sh
|
||||
lean_project_dir: /home/oho/aeneas-toolchain/aeneas/backends/lean
|
||||
replay:
|
||||
check_attempted: true
|
||||
check_ok: true
|
||||
check_log_path: provider/out/logs/lean-check.log
|
||||
checked_files: 63
|
||||
failed_files: []
|
||||
diagnostics: []
|
||||
axiom_attempted: true
|
||||
axiom_ok: true
|
||||
axiom_log_path: provider/out/logs/axiom-audit.log
|
||||
axiom_diagnostics: []
|
||||
certificates:
|
||||
- name: CurveFieldProofs.fieldImplementation
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.edwardsImplementation
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: ScalarProofs.scalarImplementation
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_loop_full
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.to_bytes_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.ed_compress_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: ScalarProofs.from_bytes_mod_order_wide_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.vartime_dsm_basepoint_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.enc_point_inj
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.sqrt_ratio_i_sq_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.from_bytes_spec
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.decompress_of_canonical
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff_point
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff_point_eq
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
diagnostics: []
|
||||
- name: CurveFieldProofs.verify_accepts_iff_decompress
|
||||
status: proven
|
||||
axiom_status: clean
|
||||
observed_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
expected_axioms:
|
||||
- propext
|
||||
- Classical.choice
|
||||
- Quot.sound
|
||||
- ed25519.Signature
|
||||
- verifying.sha512_hash3
|
||||
- ed25519.Signature.to_bytes
|
||||
- signature.error.Error
|
||||
- signature.error.Error.new
|
||||
diagnostics: []
|
||||
signature:
|
||||
scheme: openssl-ed25519
|
||||
status: signed
|
||||
payload_digest_sha256: d921c5d45f8300eecc0299fc3e11506df67751506b52cda35fb61d517b27712b
|
||||
signature_base64: iwi/AR0wLQiGF6p/jBr/3PV01d2m3lmQOXfc/00axng9Tj/YUymGejWuUi1ZleZL1X0cA9NTNKc5bbIT8AyPDA==
|
||||
public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a
|
||||
39
evidence/risc0-ed25519.receipt.yaml
Normal file
39
evidence/risc0-ed25519.receipt.yaml
Normal file
|
|
@ -0,0 +1,39 @@
|
|||
schema_version: 1
|
||||
type: pacta.transparency.receipt.v1
|
||||
log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7
|
||||
hash_algorithm: RFC9162_SHA256
|
||||
attestation_path: provider/out/risc0-ed25519.attestation.yaml
|
||||
attestation_digest_sha256: 0f86e43e48411b7fdb12a509c12f96ade3e5cc7ecd12d21b12c83a22d0b1a700
|
||||
leaf_index: 6
|
||||
leaf_hash: bdde4e4b87cd263b5914dbbae0c85ceed468c3054596f6ca79121e54cc6a134e
|
||||
tree_size: 8
|
||||
inclusion_proof:
|
||||
- 2791c352956ebc620a4fe12b20bfd6faa0813238c5bc0563fa4eb0130d829247
|
||||
- f3724e66715b582c384cf49928d4705458475ea4293749989c483ab7fe9496ce
|
||||
- 04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed
|
||||
consistency:
|
||||
from_tree_size: 8
|
||||
from_root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283
|
||||
proof: []
|
||||
status: not_applicable
|
||||
sth:
|
||||
schema_version: 1
|
||||
type: pacta.transparency.signed_tree_head.v1
|
||||
log_id: 205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7
|
||||
tree_size: 8
|
||||
timestamp: '2026-07-06T12:53:09Z'
|
||||
root_hash: 9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283
|
||||
hash_algorithm: RFC9162_SHA256
|
||||
signatures:
|
||||
ed25519:
|
||||
scheme: openssl-ed25519
|
||||
status: signed
|
||||
payload_digest_sha256: d5d25db2c90f0246cc10d10f912085b81c60d2a324354b5abecfdbeb8bd17ee2
|
||||
signature_base64: sI4rWnWMrX0zDaN8jofBwSuExKg1e0cmZV3OPaulbXDV97yz95aSo0Gnrfd1En2vyyV1qoEXdTAY9NDgvA8xBA==
|
||||
public_key_fingerprint_sha256: 874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a
|
||||
ml_dsa:
|
||||
scheme: ML-DSA-65
|
||||
standard: FIPS 204
|
||||
status: not_configured
|
||||
reason: A backend appears available, but no ML-DSA signing key was configured
|
||||
for this log.
|
||||
|
|
@ -126,6 +126,43 @@
|
|||
"This is why transparency logging matters. A signature says \"this provider signed this.\" A transparency receipt says \"this signed result is included in an append-only public structure at this tree head.\"\n"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## Real evidence, checked in this cell\n",
|
||||
"\n",
|
||||
"Everything above used schema fixtures. The repository now ships REAL provider evidence under `evidence/`: signed attestations from a guarded Lean replay of all four verified repositories (~30 minutes of kernel re-checking per fork), each recording the repo commit, the machine-protection block, and all sixteen certificates with their observed axiom cones. Read one and re-derive its verdicts locally - never trust the provider's own labels:\n"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"from pacta.attestation import load_attestation, _normalize_certificate\n",
|
||||
"from pacta.config import load_config\n",
|
||||
"from pacta.profiles import get_profile\n",
|
||||
"from pacta.signing import verify_attestation_signature_detailed\n",
|
||||
"\n",
|
||||
"config = load_config(repo_root / \"examples\" / \"repos.yaml\")\n",
|
||||
"repo = config.repo_named(\"dalek-ed25519-verified\")\n",
|
||||
"profile = get_profile(\"ed25519\", repo)\n",
|
||||
"att = load_attestation(repo_root / \"evidence\" / \"dalek-ed25519.attestation.yaml\")\n",
|
||||
"\n",
|
||||
"ok, error, backend = verify_attestation_signature_detailed(att, repo_root / \"evidence\" / \"provider.ed25519.pub\")\n",
|
||||
"print(\"signature valid:\", ok, \"| verified on backend:\", backend)\n",
|
||||
"print(\"subject commit:\", att[\"subject\"][\"repo_commit\"][:12])\n",
|
||||
"print(\"machine protection:\", att[\"machine_protection\"][\"lean_guard\"].rsplit(\"/\", 2)[-1])\n",
|
||||
"\n",
|
||||
"rederived = [_normalize_certificate(cert, profile) for cert in att[\"certificates\"]]\n",
|
||||
"clean = sum(1 for cert in rederived if cert[\"status\"] == \"proven\" and cert[\"axiom_status\"] == \"clean\")\n",
|
||||
"print(f\"re-derived locally: {clean}/{len(rederived)} proven with boundary-exact cones\")\n",
|
||||
"apex = [cert for cert in rederived if cert[\"name\"].endswith(\"_decompress\")][0]\n",
|
||||
"print(\"full-lift tier observed cone:\", apex[\"observed_axioms\"])\n"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
|
|
|
|||
|
|
@ -207,6 +207,38 @@
|
|||
"source": [
|
||||
"At real scale the same check runs on every `pacta receipt-verify --sth-store ...` and `pacta agent --sth-store ...` invocation; receipts embed a consistency anchor from the previous tree size, the provider serves proofs from arbitrary pinned sizes (`pacta_provider log-consistency --from-size N`), and `pacta_provider log-audit` is the monitor's self-check. A freshness policy (`--max-sth-age-seconds`) closes the stale-root hole: an old-but-valid tree head could hide later entries.\n",
|
||||
"\n",
|
||||
"### The real thing\n",
|
||||
"\n",
|
||||
"The `evidence/` directory holds four REAL receipts from the shipped transparency log (tree size 8 - the first four leaves honestly record a failed audit run; read `evidence/README.md`). Verify all four cryptographically and watch a fresh pin store handle them:\n"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"import tempfile\n",
|
||||
"from pathlib import Path as _P\n",
|
||||
"from pacta.sthstore import check_sth_against_store\n",
|
||||
"from pacta.transparency import verify_receipt\n",
|
||||
"from pacta.yamlio import load_data as _load\n",
|
||||
"\n",
|
||||
"log_key = repo_root / \"evidence\" / \"provider.ed25519.pub\"\n",
|
||||
"with tempfile.TemporaryDirectory() as tmp:\n",
|
||||
" store = _P(tmp) / \"pins.json\"\n",
|
||||
" for fork in [\"dalek\", \"anza\", \"risc0\", \"betrusted\"]:\n",
|
||||
" att = _load(repo_root / \"evidence\" / f\"{fork}-ed25519.attestation.yaml\")\n",
|
||||
" receipt = _load(repo_root / \"evidence\" / f\"{fork}-ed25519.receipt.yaml\")\n",
|
||||
" result = verify_receipt(att, receipt, log_key)\n",
|
||||
" pin = check_sth_against_store(receipt[\"sth\"], store, consistency_from=receipt.get(\"consistency\"))\n",
|
||||
" print(f\"{fork}: receipt accepted={result.accepted} backend={result.signatures.get('ed25519_backend')} pin={pin.action}\")\n"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## Exercises\n",
|
||||
"\n",
|
||||
"- Tamper with one leaf and show that inclusion verification fails.\n",
|
||||
|
|
|
|||
|
|
@ -869,6 +869,37 @@ COURSE = {
|
|||
This is why transparency logging matters. A signature says "this provider signed this." A transparency receipt says "this signed result is included in an append-only public structure at this tree head."
|
||||
"""
|
||||
),
|
||||
md(
|
||||
"""
|
||||
## Real evidence, checked in this cell
|
||||
|
||||
Everything above used schema fixtures. The repository now ships REAL provider evidence under `evidence/`: signed attestations from a guarded Lean replay of all four verified repositories (~30 minutes of kernel re-checking per fork), each recording the repo commit, the machine-protection block, and all sixteen certificates with their observed axiom cones. Read one and re-derive its verdicts locally - never trust the provider's own labels:
|
||||
"""
|
||||
),
|
||||
code(
|
||||
"""
|
||||
from pacta.attestation import load_attestation, _normalize_certificate
|
||||
from pacta.config import load_config
|
||||
from pacta.profiles import get_profile
|
||||
from pacta.signing import verify_attestation_signature_detailed
|
||||
|
||||
config = load_config(repo_root / "examples" / "repos.yaml")
|
||||
repo = config.repo_named("dalek-ed25519-verified")
|
||||
profile = get_profile("ed25519", repo)
|
||||
att = load_attestation(repo_root / "evidence" / "dalek-ed25519.attestation.yaml")
|
||||
|
||||
ok, error, backend = verify_attestation_signature_detailed(att, repo_root / "evidence" / "provider.ed25519.pub")
|
||||
print("signature valid:", ok, "| verified on backend:", backend)
|
||||
print("subject commit:", att["subject"]["repo_commit"][:12])
|
||||
print("machine protection:", att["machine_protection"]["lean_guard"].rsplit("/", 2)[-1])
|
||||
|
||||
rederived = [_normalize_certificate(cert, profile) for cert in att["certificates"]]
|
||||
clean = sum(1 for cert in rederived if cert["status"] == "proven" and cert["axiom_status"] == "clean")
|
||||
print(f"re-derived locally: {clean}/{len(rederived)} proven with boundary-exact cones")
|
||||
apex = [cert for cert in rederived if cert["name"].endswith("_decompress")][0]
|
||||
print("full-lift tier observed cone:", apex["observed_axioms"])
|
||||
"""
|
||||
),
|
||||
md(
|
||||
"""
|
||||
## Exercises
|
||||
|
|
@ -1053,6 +1084,33 @@ COURSE = {
|
|||
"""
|
||||
At real scale the same check runs on every `pacta receipt-verify --sth-store ...` and `pacta agent --sth-store ...` invocation; receipts embed a consistency anchor from the previous tree size, the provider serves proofs from arbitrary pinned sizes (`pacta_provider log-consistency --from-size N`), and `pacta_provider log-audit` is the monitor's self-check. A freshness policy (`--max-sth-age-seconds`) closes the stale-root hole: an old-but-valid tree head could hide later entries.
|
||||
|
||||
### The real thing
|
||||
|
||||
The `evidence/` directory holds four REAL receipts from the shipped transparency log (tree size 8 - the first four leaves honestly record a failed audit run; read `evidence/README.md`). Verify all four cryptographically and watch a fresh pin store handle them:
|
||||
"""
|
||||
),
|
||||
code(
|
||||
"""
|
||||
import tempfile
|
||||
from pathlib import Path as _P
|
||||
from pacta.sthstore import check_sth_against_store
|
||||
from pacta.transparency import verify_receipt
|
||||
from pacta.yamlio import load_data as _load
|
||||
|
||||
log_key = repo_root / "evidence" / "provider.ed25519.pub"
|
||||
with tempfile.TemporaryDirectory() as tmp:
|
||||
store = _P(tmp) / "pins.json"
|
||||
for fork in ["dalek", "anza", "risc0", "betrusted"]:
|
||||
att = _load(repo_root / "evidence" / f"{fork}-ed25519.attestation.yaml")
|
||||
receipt = _load(repo_root / "evidence" / f"{fork}-ed25519.receipt.yaml")
|
||||
result = verify_receipt(att, receipt, log_key)
|
||||
pin = check_sth_against_store(receipt["sth"], store, consistency_from=receipt.get("consistency"))
|
||||
print(f"{fork}: receipt accepted={result.accepted} backend={result.signatures.get('ed25519_backend')} pin={pin.action}")
|
||||
"""
|
||||
),
|
||||
md(
|
||||
"""
|
||||
|
||||
## Exercises
|
||||
|
||||
- Tamper with one leaf and show that inclusion verification fails.
|
||||
|
|
|
|||
|
|
@ -118,7 +118,10 @@ def check_sth_against_store(
|
|||
False,
|
||||
[
|
||||
f"LOG ROLLBACK: presented tree_size {tree_size} is smaller than the pinned size "
|
||||
f"{pinned_size}. Append-only logs never shrink."
|
||||
f"{pinned_size}. Append-only logs never shrink. If this receipt is simply STALE "
|
||||
"(issued before the log grew), request a freshly issued receipt for the same "
|
||||
"leaf - the provider's log-append is idempotent and re-issues an inclusion "
|
||||
"proof against the current tree."
|
||||
],
|
||||
"rejected",
|
||||
)
|
||||
|
|
|
|||
Loading…
Reference in a new issue