diff --git a/examples/wallet-evidence/anza-ed25519-verified.attestation.json b/examples/wallet-evidence/anza-ed25519-verified.attestation.json new file mode 100644 index 0000000..10a58d7 --- /dev/null +++ b/examples/wallet-evidence/anza-ed25519-verified.attestation.json @@ -0,0 +1,332 @@ +{ + "certificates": [ + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "ed_sigs.sha512_hash3", + "ed25519.Signature.r_bytes", + "ed25519.Signature.s_bytes" + ], + "status": "proven" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T11:51:00Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/anza-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": true, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 58, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "ff36182e67d083ac442fce5026fe31ae8127b4f04bc6b5a85b70c9cae9ed8f8d", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "fFGMNOf1a1sk14Cu2BLP2Dl4DWcipXJiPe7KlZuHyCXyhz91NEuLr4VObIa4wP9J61PThXwVwLDEnnHuOH6BCA==", + "status": "signed" + }, + "subject": { + "component": "anza-ed25519-verified", + "kind": "ed25519", + "repo_commit": "673c15e10a082788f7965fcb0faeefcca0d15136", + "repo_url": "https://github.com/saymrwulf/anza-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } +} diff --git a/examples/wallet-evidence/anza-ed25519-verified.receipt.json b/examples/wallet-evidence/anza-ed25519-verified.receipt.json new file mode 100644 index 0000000..1acea34 --- /dev/null +++ b/examples/wallet-evidence/anza-ed25519-verified.receipt.json @@ -0,0 +1,47 @@ +{ + "hash_algorithm": "RFC9162_SHA256", + "inclusion_proof": [ + "ca164b6cf11aec6a4c8de2d18c2c2fa04c9323657bd7daf4e7111869201bfec2", + "3bb1e72abbc9c0b945dafde303acdab123996e41faeab49a35563886b1b41e96", + "04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed" + ], + "leaf_hash": "33523f3ea6b6eab72696eead8534d0b7cac78feb60cc3907ac973a24f37adb95", + "leaf_index": 5, + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "schema_version": 1, + "sth": { + "hash_algorithm": "RFC9162_SHA256", + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "root_hash": "9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283", + "schema_version": 1, + "signatures": { + "ed25519": { + "payload_digest_sha256": "c9a3c000d448ebd35e313fac0c9ce0e1dc88ff03540b0828e5246407c75e2a1a", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "P8M4gjB7BCZblUvRtvJnbjfaTYKU4oO0/2LZwzpHIgp9fmOXGZqkqi7UaP5Fn1Kx4+RJSgyI2nnnK1pLpkV8CQ==", + "signing_backend": "verified-dalek-serial", + "signing_provenance": { + "self_inclusion": "verified", + "signing_backend": "verified-dalek-serial", + "signing_library_certificates_proven": "16/16", + "signing_library_component": "dalek-ed25519-verified", + "signing_library_leaf_index": 4, + "signing_library_source_commit": "aa0f6abc327ba2a54a534b21608ca8996cf73682" + }, + "status": "signed" + }, + "ml_dsa": { + "reason": "A backend appears available, but no ML-DSA signing key was configured for this log.", + "scheme": "ML-DSA-65", + "standard": "FIPS 204", + "status": "not_configured" + } + }, + "timestamp": "2026-07-06T13:59:16Z", + "tree_size": 8, + "type": "pacta.transparency.signed_tree_head.v1" + }, + "tree_size": 8, + "type": "pacta.transparency.receipt.v1" +} diff --git a/examples/wallet-evidence/betrusted-ed25519-verified.attestation.json b/examples/wallet-evidence/betrusted-ed25519-verified.attestation.json new file mode 100644 index 0000000..8b82f89 --- /dev/null +++ b/examples/wallet-evidence/betrusted-ed25519-verified.attestation.json @@ -0,0 +1,340 @@ +{ + "certificates": [ + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T12:51:28Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/betrusted-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": true, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 63, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "bb1226fa66ae0e51677ccc8c8361ba121ac5464911f1cb9e305ff7c76b7d2c57", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "Lsxje95BPXHfc7l3wxQrRvDgG/5tb7WNaO3wIDsfY/xg/WYRDFrWF3Bb6frs0Dmln00QxA99Gt43PMxLUHq0Ag==", + "status": "signed" + }, + "subject": { + "component": "betrusted-ed25519-verified", + "kind": "ed25519", + "repo_commit": "81f614a3cbd26412c6af7f0a31c0f128121fbfa4", + "repo_url": "https://github.com/saymrwulf/betrusted-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } +} diff --git a/examples/wallet-evidence/betrusted-ed25519-verified.receipt.json b/examples/wallet-evidence/betrusted-ed25519-verified.receipt.json new file mode 100644 index 0000000..d1373cd --- /dev/null +++ b/examples/wallet-evidence/betrusted-ed25519-verified.receipt.json @@ -0,0 +1,47 @@ +{ + "hash_algorithm": "RFC9162_SHA256", + "inclusion_proof": [ + "bdde4e4b87cd263b5914dbbae0c85ceed468c3054596f6ca79121e54cc6a134e", + "f3724e66715b582c384cf49928d4705458475ea4293749989c483ab7fe9496ce", + "04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed" + ], + "leaf_hash": "2791c352956ebc620a4fe12b20bfd6faa0813238c5bc0563fa4eb0130d829247", + "leaf_index": 7, + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "schema_version": 1, + "sth": { + "hash_algorithm": "RFC9162_SHA256", + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "root_hash": "9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283", + "schema_version": 1, + "signatures": { + "ed25519": { + "payload_digest_sha256": "c9a3c000d448ebd35e313fac0c9ce0e1dc88ff03540b0828e5246407c75e2a1a", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "P8M4gjB7BCZblUvRtvJnbjfaTYKU4oO0/2LZwzpHIgp9fmOXGZqkqi7UaP5Fn1Kx4+RJSgyI2nnnK1pLpkV8CQ==", + "signing_backend": "verified-dalek-serial", + "signing_provenance": { + "self_inclusion": "verified", + "signing_backend": "verified-dalek-serial", + "signing_library_certificates_proven": "16/16", + "signing_library_component": "dalek-ed25519-verified", + "signing_library_leaf_index": 4, + "signing_library_source_commit": "aa0f6abc327ba2a54a534b21608ca8996cf73682" + }, + "status": "signed" + }, + "ml_dsa": { + "reason": "A backend appears available, but no ML-DSA signing key was configured for this log.", + "scheme": "ML-DSA-65", + "standard": "FIPS 204", + "status": "not_configured" + } + }, + "timestamp": "2026-07-06T13:59:16Z", + "tree_size": 8, + "type": "pacta.transparency.signed_tree_head.v1" + }, + "tree_size": 8, + "type": "pacta.transparency.receipt.v1" +} diff --git a/examples/wallet-evidence/dalek-ed25519-verified.attestation.json b/examples/wallet-evidence/dalek-ed25519-verified.attestation.json new file mode 100644 index 0000000..9a3bb82 --- /dev/null +++ b/examples/wallet-evidence/dalek-ed25519-verified.attestation.json @@ -0,0 +1,364 @@ +{ + "certificates": [ + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_finalize_bytes", + "verifying.sha512_new", + "verifying.sha512_update", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_finalize_bytes", + "verifying.sha512_new", + "verifying.sha512_update", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_finalize_bytes", + "verifying.sha512_new", + "verifying.sha512_update", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_new", + "verifying.sha512_update", + "verifying.sha512_finalize_bytes", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "sha2.Sha512", + "verifying.sha512_finalize_bytes", + "verifying.sha512_new", + "verifying.sha512_update", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T11:21:25Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/dalek-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": true, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 64, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "ba9c3de2b75af13cd79aaaf1226a07c3e671f2d5fe06dd2a33810588dfe21571", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "Ec0xxNT6PeyuNXUncaeZN9iDJN/q3W/WenqGrx3qWDfYu9xK5Hq7e4zLALqZKrNCBaPXBm4oSYKUd1qSNoWSBg==", + "status": "signed" + }, + "subject": { + "component": "dalek-ed25519-verified", + "kind": "ed25519", + "repo_commit": "8ded7bcf9a1f0016cee93f371796b935b25b7ff8", + "repo_url": "https://github.com/saymrwulf/dalek-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } +} diff --git a/examples/wallet-evidence/dalek-ed25519-verified.receipt.json b/examples/wallet-evidence/dalek-ed25519-verified.receipt.json new file mode 100644 index 0000000..c68e6eb --- /dev/null +++ b/examples/wallet-evidence/dalek-ed25519-verified.receipt.json @@ -0,0 +1,47 @@ +{ + "hash_algorithm": "RFC9162_SHA256", + "inclusion_proof": [ + "33523f3ea6b6eab72696eead8534d0b7cac78feb60cc3907ac973a24f37adb95", + "3bb1e72abbc9c0b945dafde303acdab123996e41faeab49a35563886b1b41e96", + "04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed" + ], + "leaf_hash": "ca164b6cf11aec6a4c8de2d18c2c2fa04c9323657bd7daf4e7111869201bfec2", + "leaf_index": 4, + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "schema_version": 1, + "sth": { + "hash_algorithm": "RFC9162_SHA256", + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "root_hash": "9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283", + "schema_version": 1, + "signatures": { + "ed25519": { + "payload_digest_sha256": "c9a3c000d448ebd35e313fac0c9ce0e1dc88ff03540b0828e5246407c75e2a1a", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "P8M4gjB7BCZblUvRtvJnbjfaTYKU4oO0/2LZwzpHIgp9fmOXGZqkqi7UaP5Fn1Kx4+RJSgyI2nnnK1pLpkV8CQ==", + "signing_backend": "verified-dalek-serial", + "signing_provenance": { + "self_inclusion": "verified", + "signing_backend": "verified-dalek-serial", + "signing_library_certificates_proven": "16/16", + "signing_library_component": "dalek-ed25519-verified", + "signing_library_leaf_index": 4, + "signing_library_source_commit": "aa0f6abc327ba2a54a534b21608ca8996cf73682" + }, + "status": "signed" + }, + "ml_dsa": { + "reason": "A backend appears available, but no ML-DSA signing key was configured for this log.", + "scheme": "ML-DSA-65", + "standard": "FIPS 204", + "status": "not_configured" + } + }, + "timestamp": "2026-07-06T13:59:16Z", + "tree_size": 8, + "type": "pacta.transparency.signed_tree_head.v1" + }, + "tree_size": 8, + "type": "pacta.transparency.receipt.v1" +} diff --git a/examples/wallet-evidence/log.pub b/examples/wallet-evidence/log.pub new file mode 100644 index 0000000..de4000a --- /dev/null +++ b/examples/wallet-evidence/log.pub @@ -0,0 +1,3 @@ +-----BEGIN PUBLIC KEY----- +MCowBQYDK2VwAyEAd6WIt2/WNJCcKMZGo67BQoZI84LbvLaYMvpwAWNXsxU= +-----END PUBLIC KEY----- diff --git a/examples/wallet-evidence/risc0-ed25519-verified.attestation.json b/examples/wallet-evidence/risc0-ed25519-verified.attestation.json new file mode 100644 index 0000000..9f420e7 --- /dev/null +++ b/examples/wallet-evidence/risc0-ed25519-verified.attestation.json @@ -0,0 +1,340 @@ +{ + "certificates": [ + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.fieldImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.edwardsImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.scalarImplementation", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.verify_loop_full", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.to_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.ed_compress_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "ScalarProofs.from_bytes_mod_order_wide_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.vartime_dsm_basepoint_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.enc_point_inj", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.sqrt_ratio_i_sq_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.from_bytes_spec", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "name": "CurveFieldProofs.decompress_of_canonical", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_point_eq", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + }, + { + "axiom_status": "clean", + "diagnostics": [], + "expected_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "name": "CurveFieldProofs.verify_accepts_iff_decompress", + "observed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound", + "ed25519.Signature", + "verifying.sha512_hash3", + "ed25519.Signature.to_bytes", + "signature.error.Error", + "signature.error.Error.new" + ], + "status": "proven" + } + ], + "environment": { + "env_script": "~/aeneas-toolchain/env.sh", + "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", + "lean_project_dir": "/home/oho/aeneas-toolchain/aeneas/backends/lean", + "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" + }, + "issued_at": "2026-07-06T12:21:40Z", + "machine_protection": { + "lean_guard": "/home/oho/GitClone/Claude/FormalVerification/risc0-ed25519-verified/verification/lean-guard", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." + }, + "provider": "local-pacta-provider", + "replay": { + "axiom_attempted": true, + "axiom_diagnostics": [], + "axiom_log_path": "provider/out/logs/axiom-audit.log", + "axiom_ok": true, + "check_attempted": true, + "check_log_path": "provider/out/logs/lean-check.log", + "check_ok": true, + "checked_files": 63, + "diagnostics": [], + "failed_files": [] + }, + "schema_version": 1, + "signature": { + "payload_digest_sha256": "d921c5d45f8300eecc0299fc3e11506df67751506b52cda35fb61d517b27712b", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "iwi/AR0wLQiGF6p/jBr/3PV01d2m3lmQOXfc/00axng9Tj/YUymGejWuUi1ZleZL1X0cA9NTNKc5bbIT8AyPDA==", + "status": "signed" + }, + "subject": { + "component": "risc0-ed25519-verified", + "kind": "ed25519", + "repo_commit": "98a13a68539b20ac0279876848aea3687e523462", + "repo_url": "https://github.com/saymrwulf/risc0-ed25519-verified.git", + "verification_dir": "verification", + "verified_backend": "serial/u64" + } +} diff --git a/examples/wallet-evidence/risc0-ed25519-verified.receipt.json b/examples/wallet-evidence/risc0-ed25519-verified.receipt.json new file mode 100644 index 0000000..db70514 --- /dev/null +++ b/examples/wallet-evidence/risc0-ed25519-verified.receipt.json @@ -0,0 +1,47 @@ +{ + "hash_algorithm": "RFC9162_SHA256", + "inclusion_proof": [ + "2791c352956ebc620a4fe12b20bfd6faa0813238c5bc0563fa4eb0130d829247", + "f3724e66715b582c384cf49928d4705458475ea4293749989c483ab7fe9496ce", + "04541cffd46cf5a97d7453ed8ae681b1a1fedb879eb8c7a262e05b3176159eed" + ], + "leaf_hash": "bdde4e4b87cd263b5914dbbae0c85ceed468c3054596f6ca79121e54cc6a134e", + "leaf_index": 6, + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "schema_version": 1, + "sth": { + "hash_algorithm": "RFC9162_SHA256", + "log_id": "205e4c389cb143e08f0d2d58bdc8e425e47e3cbe7f2108cc58bbe835d2cc41d7", + "root_hash": "9a15b9a1379edc07ae43d3fc61b52dc4446b56770bff6538e88ed98746ac2283", + "schema_version": 1, + "signatures": { + "ed25519": { + "payload_digest_sha256": "c9a3c000d448ebd35e313fac0c9ce0e1dc88ff03540b0828e5246407c75e2a1a", + "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", + "scheme": "openssl-ed25519", + "signature_base64": "P8M4gjB7BCZblUvRtvJnbjfaTYKU4oO0/2LZwzpHIgp9fmOXGZqkqi7UaP5Fn1Kx4+RJSgyI2nnnK1pLpkV8CQ==", + "signing_backend": "verified-dalek-serial", + "signing_provenance": { + "self_inclusion": "verified", + "signing_backend": "verified-dalek-serial", + "signing_library_certificates_proven": "16/16", + "signing_library_component": "dalek-ed25519-verified", + "signing_library_leaf_index": 4, + "signing_library_source_commit": "aa0f6abc327ba2a54a534b21608ca8996cf73682" + }, + "status": "signed" + }, + "ml_dsa": { + "reason": "A backend appears available, but no ML-DSA signing key was configured for this log.", + "scheme": "ML-DSA-65", + "standard": "FIPS 204", + "status": "not_configured" + } + }, + "timestamp": "2026-07-06T13:59:16Z", + "tree_size": 8, + "type": "pacta.transparency.signed_tree_head.v1" + }, + "tree_size": 8, + "type": "pacta.transparency.receipt.v1" +} diff --git a/tests/test_quorum.py b/tests/test_quorum.py new file mode 100644 index 0000000..91981f9 --- /dev/null +++ b/tests/test_quorum.py @@ -0,0 +1,124 @@ +"""Quorum boundary: divergence taxonomy, unanimity, edge flags. + +Unit tests use fake verifier binaries (tiny shell scripts with fixed +verdicts) so the taxonomy logic is exercised without needing cargo or the +pinned sources. An integration test runs the REAL built quorum when the +binaries are present, and skips cleanly otherwise. +""" + +import os +import stat +from pathlib import Path + +import pytest + +from pacta.quorum import ( + QuorumVerifier, + SMALL_ORDER_ENCODINGS, + binary_path, + load_quorum, + semantic_edge_flags, +) + + +def _fake_member(path: Path, verdict: str) -> None: + """verdict in {accept, reject, error}.""" + code = {"accept": 0, "reject": 1, "error": 2}[verdict] + out = {"accept": "OK", "reject": "INVALID", "error": "boom"}[verdict] + path.write_text(f"#!/bin/sh\necho {out}\nexit {code}\n") + path.chmod(path.stat().st_mode | stat.S_IEXEC) + + +def _quorum(tmp_path: Path, verdicts: dict[str, str]) -> QuorumVerifier: + members = {} + for name, verdict in verdicts.items(): + binary = tmp_path / f"pacta-verify-{name}" + _fake_member(binary, verdict) + members[name] = binary + return QuorumVerifier(members, min_members=2) + + +def test_unanimous_accept(tmp_path): + q = _quorum(tmp_path, {"a": "accept", "b": "accept", "c": "accept"}) + r = q.verify(b"payload", b"\x01" * 64, b"\x02" * 32) + assert r.accepted + assert r.classification == "unanimous-accept" + assert r.incident is None + + +def test_unanimous_reject(tmp_path): + q = _quorum(tmp_path, {"a": "reject", "b": "reject"}) + r = q.verify(b"payload", b"\x01" * 64, b"\x02" * 32) + assert not r.accepted + assert r.classification == "unanimous-reject" + + +def test_divergence_on_ordinary_input_is_tamper(tmp_path): + # Members disagree with no documented edge -> unexplained/tamper. + q = _quorum(tmp_path, {"a": "accept", "b": "reject"}) + r = q.verify(b"payload", b"\x01" * 64, b"\x02" * 32) + assert not r.accepted + assert r.classification == "unexplained" + assert r.incident["severity"] == "tamper" + + +def test_divergence_on_small_order_R_is_semantic_edge(tmp_path): + # Members disagree AND R is on the legacy exclusion list -> note, not tamper. + small_order_R = sorted(SMALL_ORDER_ENCODINGS)[0] + signature = small_order_R + b"\x00" * 32 + q = _quorum(tmp_path, {"dalek": "accept", "anza": "reject"}) + r = q.verify(b"payload", signature, b"\x02" * 32) + assert not r.accepted + assert r.classification == "semantic-edge" + assert r.incident["severity"] == "note" + assert any("small-order-R" in f for f in r.edge_flags) + + +def test_member_error_forces_unexplained(tmp_path): + # A member that errors (exit 2) can never be a benign semantic edge. + small_order_R = sorted(SMALL_ORDER_ENCODINGS)[0] + signature = small_order_R + b"\x00" * 32 + q = _quorum(tmp_path, {"a": "accept", "b": "error"}) + r = q.verify(b"payload", signature, b"\x02" * 32) + assert r.classification == "unexplained" + assert r.incident["severity"] == "tamper" + + +def test_edge_flags_detect_classes(): + zero_key = b"\x00" * 32 + assert "zero-public-key" in semantic_edge_flags(zero_key, b"\x00" * 64) + # non-canonical s: all 0xff is well above the group order + flags = semantic_edge_flags(b"\x02" * 32, b"\x01" * 32 + b"\xff" * 32) + assert any("non-canonical-s" in f for f in flags) + + +def test_quorum_requires_min_members(tmp_path): + with pytest.raises(ValueError): + _quorum(tmp_path, {"only": "accept"}) + + +def test_missing_binary_rejected(tmp_path): + with pytest.raises(ValueError): + QuorumVerifier({"a": tmp_path / "nope", "b": tmp_path / "nope2"}, min_members=2) + + +def test_real_quorum_agrees_on_valid_and_invalid(tmp_path): + if not all(binary_path(b).exists() for b in ("dalek", "anza")): + pytest.skip("real quorum binaries not built (run `pacta wallet build-quorum`)") + from pacta.dogfood import locate_verifier, pem_public_key_to_raw, sign_payload_dogfood + from pacta.signing import generate_ed25519_keypair + + verifier = locate_verifier() + if verifier is None: + pytest.skip("dogfood signer not built") + key = tmp_path / "k.pem" + pub = tmp_path / "k.pub" + generate_ed25519_keypair(key, pub) + payload = b"real quorum integration payload" + signature = sign_payload_dogfood(payload, key, verifier) + public_key = pem_public_key_to_raw(pub) + q = load_quorum(min_members=2) + good = q.verify(payload, signature, public_key) + assert good.accepted and good.classification == "unanimous-accept" + bad = q.verify(payload, bytes([signature[0] ^ 0xFF]) + signature[1:], public_key) + assert not bad.accepted and bad.classification == "unanimous-reject" diff --git a/tests/test_wallet.py b/tests/test_wallet.py new file mode 100644 index 0000000..6369f89 --- /dev/null +++ b/tests/test_wallet.py @@ -0,0 +1,194 @@ +"""Wallet core: ledger chaining, outbound firewall, latch, refusals. + +Most tests seal a wallet by hand with fake verifier binaries so the +custody logic (hash-chained ledger, firewall quarantine, latch, +machine-actionable refusals) is exercised without cargo or the pinned +sources. A live integration test does the real R4 init against the built +quorum + fetched evidence when both are present, and skips otherwise. +""" + +import hashlib +import json +import stat +from pathlib import Path + +import pytest + +from pacta.quorum import binary_path +from pacta.signing import generate_ed25519_keypair +from pacta.wallet import AirgapSigner, PendingAirgap, Refusal, Wallet + + +def _fake_member(path: Path, verdict: str) -> None: + code = {"accept": 0, "reject": 1}[verdict] + out = {"accept": "OK", "reject": "INVALID"}[verdict] + path.write_text(f"#!/bin/sh\necho {out}\nexit {code}\n") + path.chmod(path.stat().st_mode | stat.S_IEXEC) + + +def _sha256(data: bytes) -> str: + return hashlib.sha256(data).hexdigest() + + +def _seal_wallet(tmp_path: Path, verdicts: dict[str, str], state_dir: Path) -> Wallet: + """Create a wallet directory by hand: fake quorum members + a capsule + that pins their hashes, bypassing the (separately tested) R4 gate.""" + state_dir.mkdir(parents=True, exist_ok=True) + members = [] + for name, verdict in verdicts.items(): + binary = binary_path(name, state_dir) + _fake_member(binary, verdict) + members.append({ + "backend": name, + "component": f"{name}-ed25519-verified", + "semantics": "test", + "entry_point": "test", + "source_commit": "deadbeef" * 5, + "repo_commit": "cafe" * 10, + "binary_sha256": _sha256(binary.read_bytes()), + "backend_cfg": "test", + "risk_tier": "R4", + "evidence": {"leaf_hash": "00", "leaf_index": 0, "tree_size": 1, + "inclusion_proof": [], "sth": {"timestamp": "2099-01-01T00:00:00Z"}}, + }) + wallet_dir = tmp_path / "w" + wallet = Wallet(wallet_dir) + for sub in (wallet.keys_dir, wallet.incidents_dir, wallet.receipts_dir, + wallet.quarantine_dir, wallet.airgap_dir / "outbox", wallet.airgap_dir / "inbox"): + sub.mkdir(parents=True, exist_ok=True) + capsule = { + "type": "pacta.wallet.custody_capsule.v1", + "created_at": "2026-07-06T00:00:00Z", + "members": members, + "policy": {"require_unanimity": True, "min_members": 2, "require_tier": "R4", + "freshness_max_age_days": 0}, + "signing": {"backend": "test"}, + "problems_at_init": [], + } + capsule_bytes = json.dumps(capsule, sort_keys=True, separators=(",", ":")).encode() + wallet.capsule_path.write_text(json.dumps(capsule, indent=2, sort_keys=True) + "\n") + wallet._append_ledger("genesis", {"type": "pacta.wallet.ledger_genesis.v1", + "capsule_sha256": _sha256(capsule_bytes)}) + generate_ed25519_keypair(wallet.keys_dir / "warden.key.pem", wallet.keys_dir / "warden.pub.pem") + wallet._test_state_dir = state_dir # type: ignore[attr-defined] + return wallet + + +def _payload_intent(payload: bytes) -> dict: + return {"purpose": "test signature", "payload_sha256": _sha256(payload)} + + +def test_ledger_is_hash_chained(tmp_path): + wallet = _seal_wallet(tmp_path, {"a": "accept", "b": "accept"}, tmp_path / "state") + payload = b"hello" + wallet.request_signature(_payload_intent(payload), payload, state_dir=wallet._test_state_dir) + ok, problems = wallet.verify_ledger() + assert ok, problems + # tamper with a middle entry and prove the chain catches it + lines = wallet.ledger_path.read_text().splitlines() + entry = json.loads(lines[1]) + entry["body"]["intent"] = {"purpose": "SNEAKY"} + lines[1] = json.dumps(entry, sort_keys=True) + wallet.ledger_path.write_text("\n".join(lines) + "\n") + ok2, problems2 = wallet.verify_ledger() + assert not ok2 and problems2 + + +def test_outbound_firewall_releases_when_quorum_agrees(tmp_path): + from pacta.dogfood import locate_verifier + + if locate_verifier() is None: + pytest.skip("dogfood signer not built") + wallet = _seal_wallet(tmp_path, {"a": "accept", "b": "accept"}, tmp_path / "state") + payload = b"release me" + result = wallet.request_signature(_payload_intent(payload), payload, state_dir=wallet._test_state_dir) + assert not isinstance(result, Refusal) + assert result["firewall"]["classification"] == "unanimous-accept" + + +def test_outbound_firewall_quarantines_and_latches(tmp_path): + from pacta.dogfood import locate_verifier + + if locate_verifier() is None: + pytest.skip("dogfood signer not built") + # Members disagree on the produced signature -> quarantine + latch. + wallet = _seal_wallet(tmp_path, {"a": "accept", "b": "reject"}, tmp_path / "state") + payload = b"tampered path" + result = wallet.request_signature(_payload_intent(payload), payload, state_dir=wallet._test_state_dir) + assert isinstance(result, Refusal) + assert result.code == "FIREWALL_QUARANTINE" + assert wallet.latch_state()["latched"] + assert list(wallet.quarantine_dir.glob("*.json")) + # once latched, further outbound is refused with CUSTODY_LATCHED + again = wallet.request_signature(_payload_intent(b"x"), b"x", state_dir=wallet._test_state_dir) + assert isinstance(again, Refusal) and again.code == "CUSTODY_LATCHED" + # and the latched refusal is honestly unsigned + assert again.receipt["signature"]["status"] == "unsigned" + + +def test_unlatch_records_note(tmp_path): + wallet = _seal_wallet(tmp_path, {"a": "accept", "b": "reject"}, tmp_path / "state") + wallet._latch("test latch", "0000") + assert wallet.latch_state()["latched"] + wallet.unlatch("operator reviewed incident 0000, false alarm") + assert not wallet.latch_state()["latched"] + entries = [e for e in wallet._ledger_entries() if e["entry_type"] == "unlatch"] + assert entries and "false alarm" in entries[-1]["body"]["operator_note"] + + +def test_malformed_intent_refused(tmp_path): + wallet = _seal_wallet(tmp_path, {"a": "accept", "b": "accept"}, tmp_path / "state") + result = wallet.request_signature({"purpose": ""}, b"data", state_dir=wallet._test_state_dir) + assert isinstance(result, Refusal) + assert result.code == "MALFORMED_INTENT" + + +def test_intent_must_bind_payload(tmp_path): + wallet = _seal_wallet(tmp_path, {"a": "accept", "b": "accept"}, tmp_path / "state") + bad = {"purpose": "ok", "payload_sha256": "wrong"} + result = wallet.request_signature(bad, b"data", state_dir=wallet._test_state_dir) + assert isinstance(result, Refusal) and result.code == "MALFORMED_INTENT" + + +def test_binary_hash_change_is_detected(tmp_path): + wallet = _seal_wallet(tmp_path, {"a": "accept", "b": "accept"}, tmp_path / "state") + # Swap a member binary for a different one; the capsule pin must catch it. + _fake_member(binary_path("a", wallet._test_state_dir), "reject") + from pacta.wallet import WalletError + + with pytest.raises(WalletError): + wallet.quorum(state_dir=wallet._test_state_dir) + + +def test_airgap_signer_parks_then_completes(tmp_path): + airgap = AirgapSigner(tmp_path / "airgap", wait_seconds=0.0) + payload = b"cross the gap" + with pytest.raises(PendingAirgap) as excinfo: + airgap.sign(payload, tmp_path / "unused.pem", request_id="req1") + assert (tmp_path / "airgap" / "outbox" / "req1.request.json").exists() + # simulate the device dropping a response + (tmp_path / "airgap" / "inbox" / "req1.response.json").write_text( + json.dumps({"signature_hex": "ab" * 64}) + ) + sig = airgap.sign(payload, tmp_path / "unused.pem", request_id="req1") + assert len(sig) == 64 + assert excinfo.value.request_id == "req1" + + +def test_real_wallet_init_r4_gate(tmp_path): + """The showcase: real R4 init against built binaries + example evidence.""" + if not all(binary_path(b).exists() for b in ("dalek", "anza", "risc0", "betrusted")): + pytest.skip("real quorum not built") + evidence = Path("examples") / "wallet-evidence" + log_key = evidence / "log.pub" + if not evidence.exists() or not log_key.exists(): + pytest.skip("example wallet evidence / log key not present") + wallet = Wallet.init( + tmp_path / "w", + evidence, + log_key, + trusted_provider="local-pacta-provider", + ) + capsule = wallet.capsule() + assert len(capsule["members"]) >= 2 + assert all(m["risk_tier"] == "R4" for m in capsule["members"]) diff --git a/tests/test_walletmcp.py b/tests/test_walletmcp.py new file mode 100644 index 0000000..7e4e6f2 --- /dev/null +++ b/tests/test_walletmcp.py @@ -0,0 +1,193 @@ +"""The agent-native MCP surface: JSON-RPC plumbing + structured errors. + +Protocol plumbing and read-only tools are tested with a hand-sealed +wallet (no live quorum needed). The crypto tools (verify_inbound, +request_signature, posture_challenge) are covered by the live end-to-end +test when the real quorum + dogfood signer are present. +""" + +import base64 +import hashlib +import json +import stat +from pathlib import Path + +import pytest + +from pacta.quorum import binary_path +from pacta.signing import generate_ed25519_keypair +from pacta.wallet import Wallet +from pacta.walletmcp import TOOLS, WalletMCP + + +def _sha256(data: bytes) -> str: + return hashlib.sha256(data).hexdigest() + + +def _fake_member(path: Path, verdict: str) -> None: + code = {"accept": 0, "reject": 1}[verdict] + out = {"accept": "OK", "reject": "INVALID"}[verdict] + path.write_text(f"#!/bin/sh\necho {out}\nexit {code}\n") + path.chmod(path.stat().st_mode | stat.S_IEXEC) + + +def _seal_wallet(tmp_path: Path, verdicts: dict, state_dir: Path) -> Wallet: + state_dir.mkdir(parents=True, exist_ok=True) + members = [] + for name, verdict in verdicts.items(): + binary = binary_path(name, state_dir) + _fake_member(binary, verdict) + members.append({ + "backend": name, "component": f"{name}-ed25519-verified", "semantics": "test", + "entry_point": "test", "source_commit": "de" * 20, "repo_commit": "ca" * 20, + "binary_sha256": _sha256(binary.read_bytes()), "backend_cfg": "test", "risk_tier": "R4", + "evidence": {"leaf_hash": "00", "leaf_index": 0, "tree_size": 1, "inclusion_proof": [], + "sth": {"timestamp": "2099-01-01T00:00:00Z"}}, + }) + wallet = Wallet(tmp_path / "w") + for sub in (wallet.keys_dir, wallet.incidents_dir, wallet.receipts_dir, + wallet.quarantine_dir, wallet.airgap_dir / "outbox", wallet.airgap_dir / "inbox"): + sub.mkdir(parents=True, exist_ok=True) + capsule = {"type": "pacta.wallet.custody_capsule.v1", "created_at": "2026-07-06T00:00:00Z", + "members": members, + "policy": {"require_unanimity": True, "min_members": 2, "require_tier": "R4", + "freshness_max_age_days": 0}, + "signing": {"backend": "test"}, "problems_at_init": []} + wallet.capsule_path.write_text(json.dumps(capsule, indent=2, sort_keys=True) + "\n") + wallet._append_ledger("genesis", {"capsule_sha256": "x"}) + generate_ed25519_keypair(wallet.keys_dir / "warden.key.pem", wallet.keys_dir / "warden.pub.pem") + wallet._test_state_dir = state_dir # type: ignore[attr-defined] + return wallet + + +def _mcp(tmp_path): + wallet = _seal_wallet(tmp_path, {"a": "accept", "b": "accept"}, tmp_path / "state") + srv = WalletMCP(wallet.dir) + return srv, wallet + + +def _call(srv, method, params=None, msg_id=1): + return srv.handle({"jsonrpc": "2.0", "id": msg_id, "method": method, "params": params or {}}) + + +def test_initialize_advertises_server(tmp_path): + srv, _ = _mcp(tmp_path) + res = _call(srv, "initialize")["result"] + assert res["serverInfo"]["name"] == "warden" + assert "protocolVersion" in res + + +def test_initialized_notification_has_no_response(tmp_path): + srv, _ = _mcp(tmp_path) + assert srv.handle({"jsonrpc": "2.0", "method": "notifications/initialized"}) is None + + +def test_tools_list_matches_declared(tmp_path): + srv, _ = _mcp(tmp_path) + names = {t["name"] for t in _call(srv, "tools/list")["result"]["tools"]} + assert names == {t["name"] for t in TOOLS} + assert "request_signature" in names + + +def test_every_tool_has_a_strict_schema(): + for tool in TOOLS: + schema = tool["inputSchema"] + assert schema["type"] == "object" + assert schema.get("additionalProperties") is False, tool["name"] + + +def test_unknown_tool_is_jsonrpc_error(tmp_path): + srv, _ = _mcp(tmp_path) + res = _call(srv, "tools/call", {"name": "nope", "arguments": {}}) + assert res["error"]["code"] == -32602 + + +def test_wallet_status_tool(tmp_path): + srv, _ = _mcp(tmp_path) + res = _call(srv, "tools/call", {"name": "wallet_status"})["result"] + assert not res["isError"] + assert res["structuredContent"]["type"] == "pacta.wallet.posture.v1" + + +def test_custody_card_is_self_proving_shape(tmp_path): + srv, _ = _mcp(tmp_path) + card = _call(srv, "tools/call", {"name": "custody_card"})["result"]["structuredContent"] + assert card["type"] == "pacta.wallet.custody_card.v1" + for member in card["quorum"]["members"]: + assert "transparency_evidence" in member + + +def test_structured_error_on_bad_base64(tmp_path): + srv, _ = _mcp(tmp_path) + res = _call(srv, "tools/call", { + "name": "verify_inbound", + "arguments": {"payload_b64": "x", "signature_b64": "!!!", "public_key_b64": "!!!"}, + })["result"] + assert res["isError"] + body = res["structuredContent"] + assert set(body) >= {"code", "reason", "missing", "remediation"} + assert body["code"] == "MALFORMED_INTENT" + + +def test_explain_refusal_when_none(tmp_path): + srv, _ = _mcp(tmp_path) + res = _call(srv, "tools/call", {"name": "explain_refusal"})["result"] + assert res["isError"] + assert res["structuredContent"]["code"] == "EVIDENCE_REQUIRED" + + +def test_server_never_crashes_on_garbage(tmp_path): + srv, _ = _mcp(tmp_path) + # missing method + res = _call(srv, "does/not/exist") + assert res["error"]["code"] == -32601 + + +def test_request_signature_and_verify_roundtrip_live(tmp_path): + if not all(binary_path(b).exists() for b in ("dalek", "anza")): + pytest.skip("real quorum not built") + from pacta.dogfood import locate_verifier + + if locate_verifier() is None: + pytest.skip("dogfood signer not built") + # seal against the REAL default-location binaries + real_hashes = {b: _sha256(binary_path(b).read_bytes()) for b in ("dalek", "anza", "risc0", "betrusted") + if binary_path(b).exists()} + wallet = Wallet(tmp_path / "w") + for sub in (wallet.keys_dir, wallet.incidents_dir, wallet.receipts_dir, + wallet.quarantine_dir, wallet.airgap_dir / "outbox", wallet.airgap_dir / "inbox"): + sub.mkdir(parents=True, exist_ok=True) + members = [{ + "backend": b, "component": f"{b}-ed25519-verified", "semantics": "t", "entry_point": "t", + "source_commit": "x", "repo_commit": "y", "binary_sha256": h, "backend_cfg": "t", + "risk_tier": "R4", + "evidence": {"leaf_hash": "00", "leaf_index": 0, "tree_size": 1, "inclusion_proof": [], + "sth": {"timestamp": "2099-01-01T00:00:00Z"}}, + } for b, h in real_hashes.items()] + capsule = {"type": "pacta.wallet.custody_capsule.v1", "created_at": "2026-07-06T00:00:00Z", + "members": members, + "policy": {"require_unanimity": True, "min_members": 2, "require_tier": "R4", + "freshness_max_age_days": 0}, + "signing": {"backend": "test"}, "problems_at_init": []} + wallet.capsule_path.write_text(json.dumps(capsule, indent=2, sort_keys=True) + "\n") + wallet._append_ledger("genesis", {"capsule_sha256": "x"}) + generate_ed25519_keypair(wallet.keys_dir / "warden.key.pem", wallet.keys_dir / "warden.pub.pem") + + srv = WalletMCP(wallet.dir) + payload = b"live mcp roundtrip" + res = _call(srv, "tools/call", { + "name": "request_signature", + "arguments": {"payload_b64": base64.b64encode(payload).decode(), "purpose": "test"}, + })["result"] + assert not res["isError"], res["structuredContent"] + sig = bytes.fromhex(res["structuredContent"]["signature_hex"]) + pub = bytes.fromhex(res["structuredContent"]["public_key_hex"]) + vi = _call(srv, "tools/call", { + "name": "verify_inbound", + "arguments": { + "payload_b64": base64.b64encode(payload).decode(), + "signature_b64": base64.b64encode(sig).decode(), + "public_key_b64": base64.b64encode(pub).decode(), + }, + })["result"] + assert vi["structuredContent"]["classification"] == "unanimous-accept"