{ "attestation": { "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": "CurveFieldProofs.naf_table_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "CurveFieldProofs.naf_select_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "CurveFieldProofs.proj_double_law", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "CurveFieldProofs.compl_as_projective_law", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "CurveFieldProofs.dsm_step_p_law", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "CurveFieldProofs.dsm_step_b_law", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "CurveFieldProofs.dsm_loop_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "CurveFieldProofs.naf_load_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "CurveFieldProofs.naf_exit", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "CurveFieldProofs.naf_digit_loop_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "CurveFieldProofs.non_adjacent_form_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "CurveFieldProofs.run_basepoint", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "CurveFieldProofs.vartime_double_base_mul_spec", "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.pow_p58_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "CurveFieldProofs.fe_ct_eq_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "CurveFieldProofs.sqrt_core", "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_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" }, { "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" ], "name": "ScalarProofs.L_val", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "ScalarProofs.sub_loop_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "ScalarProofs.cond_add_l_one_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "ScalarProofs.sub_val_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "ScalarProofs.add_val_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "ScalarProofs.mul_internal_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "ScalarProofs.part1_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "ScalarProofs.montgomery_reduce_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "ScalarProofs.mul_spec", "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": "ScalarProofs.montgomery_mul_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" }, { "axiom_status": "clean", "diagnostics": [], "expected_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "name": "ScalarProofs.bytes_unpack_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_wide_spec", "observed_axioms": [ "propext", "Classical.choice", "Quot.sound" ], "status": "proven" } ], "environment": { "env_script": "~/aeneas-toolchain/env.sh", "lake_version": "Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)", "lean_project_dir": "$AENEAS_HOME/backends/lean", "lean_version": "Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)" }, "issued_at": "2026-08-07T09:37:13Z", "machine_protection": { "lean_guard": "verification/lean-guard", "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured." }, "provider": "local-provider", "replay": { "axiom_attempted": true, "axiom_diagnostics": [], "axiom_log_path": "/tmp/claude-1000/-home-oho-GitClone-Claude-FormalVerification/371a28b5-864a-4953-a400-61066a13ba91/scratchpad/rehearsal/replay-logs4/dalek-ed25519-verified/axiom-audit.log", "axiom_ok": true, "check_attempted": true, "check_log_path": "/tmp/claude-1000/-home-oho-GitClone-Claude-FormalVerification/371a28b5-864a-4953-a400-61066a13ba91/scratchpad/rehearsal/replay-logs4/dalek-ed25519-verified/lean-check.log", "check_ok": true, "checked_files": 64, "diagnostics": [], "failed_files": [], "instruments_excluded": [ "Proofs/Audit.lean", "Proofs/Inventory.lean", "Proofs/InventoryBasic.lean", "Proofs/InventoryCore.lean", "Proofs/InventoryScalar.lean", "Proofs/ScalarAudit.lean" ] }, "schema_version": 1, "scope": { "deployment_constraints": [ "Use exact pinned source or reviewed diff.", "Use verified serial/u64 backend only.", "Disable accelerator, syscall, hardware, SIMD, and AVX paths unless separately certified.", "Verification-side evidence only: keep signing/key custody behind HSM, MPC, or policy firewall.", "SHA-512 remains an unverified dependency; pin and monitor the hash implementation.", "Use ordinary tests and fuzzing at wire-parse, API, and transaction boundaries (parse specs are hypothesis-parametric)." ], "exclusions": [ "SHA-512 itself is not verified; it enters the apex theorems as an opaque oracle with NO assumed properties (the theorems hold for whatever bytes it produces).", "Signature parse/filter outcomes are hypothesis-parametric: the apex tiers assume the wire parse succeeded; the parsers' own byte-level specs are separate work.", "Signing (key generation, nonce derivation, the signer) is out of scope; only verification is certified.", "Rust compiler correctness is out of scope.", "Charon/Aeneas translation faithfulness is out of scope.", "Side-channel resistance is out of scope.", "SIMD, AVX, hardware, zkVM, accelerator, and syscall paths are out of scope (extraction pins the serial path).", "Wallet policy, transaction construction, RPC, oracle, market, and LLM decision safety are out of scope.", "SHA-512 implementation (opaque oracle in the apex theorems)", "wire parser/filter byte-level specs (hypothesis-parametric)", "signing-side correctness", "side-channel resistance", "compiler correctness", "SIMD/AVX/accelerator paths" ], "guarantees": [ "FieldElement51 arithmetic is checked through denotation over F_p, p = 2^255 - 19, for the configured backend.", "Complete twisted Edwards point-operation laws are checked under ExtValid and OnCurveExt invariants.", "Scalar arithmetic mod l (add, sub, Montgomery mul, wide hash-to-scalar reduction) is checked through denotation.", "Point compression emits the canonical encoding (to_bytes canonicity + compress semantics are certified).", "Point decompression is constructively certified: canonical encodings of valid on-curve points decompress to them (from_bytes exactness, sqrt_ratio_i even root, sign-bit selection).", "THE SIGNATURE APEX, four button-enforced tiers: the extracted verifier accepts iff compress([s]B - [k]A) = R byte-for-byte, iff R is the canonical encoding of [k](-A) + [s]B, iff any point canonically encoded by R equals it, and iff R decompresses to a valid on-curve point equal to it.", "Each apex tier's axiom cone is pinned to EXACTLY the fork's documented SHA-512/wire-format boundary by the repo's own check script.", "Panic and overflow freedom evidence applies under the stated limb-bound preconditions." ] }, "signature": { "payload_digest_sha256": "5536d4fea7aea67538221a1971c016c09edbf4d0417e56d8705303f53357d731", "public_key_fingerprint_sha256": "874c8a008a607021528b2493fa1caf059f9d5c123d29193dfabc09a6d1e7a56a", "scheme": "openssl-ed25519", "signature_base64": "qFIKL+WWcRYVgyY+2Yt0FmMRd6RqYKSWDh5G5xzkSq/OQJ6GXqH9vbmDzTGpn11fPg1OaEalGcY7e+bUU4vuBA==", "signing_backend": "verified-dalek-serial", "status": "signed" }, "subject": { "component": "dalek-ed25519-verified", "kind": "ed25519", "repo_commit": "fa22ececa7c218eb5b69e1137731d514d8373b72", "repo_url": "https://github.com/saymrwulf/dalek-ed25519-verified.git", "verification_dir": "verification", "verified_backend": "serial/u64" } }, "leaf_hash": "fd7a2579b37fe9a2a8e49ee52914d0525b09e7d034762c5c176cea31aa321718", "leaf_index": 13 }