Add a pure Lean BLAKE3 implementation with checked proofs - #50
Conversation
| @@ -0,0 +1,47 @@ | |||
| //! Regenerate Tests/PureVectors.lean with: | |||
There was a problem hiding this comment.
Why generate a Lean file? The following options are simpler, with the latter being much simpler than the former:
- Generate a raw text file, which can be read in IO and parsed. The regeneration entanglement and syntax conforming is not necessary
- Call Rust directly from Lean via FFI
There was a problem hiding this comment.
These are test vectors. Doing 1 means Lean has to run IO and a parser, which is overhead. 2 means we have to bring in https://github.com/argumentcomputer/lean-ffi which is a large dependency. If we were in ix I would encode these using ixon syntax, but I don't have that dependency here.
I've added a change to clarify that we're just generating data though to minimize entanglement, separating out the Lean logic into a non-regened file and having the regen just be something morally json-ish
Move the vector schema into Tests/Vectors.lean and have rust/examples/pure_vectors.rs emit one Blake3.PureTests.Vectors literal with named fields, so the generated file is data only: an import, one def line, and records with trailing commas. Tests/Pure.lean reads the records by field name, parent records carry their salt, and the recorded crate version is checked against the linked Rust backend. 32-byte values are lowercase hex strings rather than byte lists. A single declaration holding both record lists as List UInt8 exceeds a code generator recursion cliff at roughly 8k bindings and fails with "maximum recursion depth has been reached" even though it elaborates; hex keeps each record at a few bindings and matches the BLAKE3 team's own test vector format. The vector values are unchanged.
| println!("import Tests.Vectors"); | ||
| println!(); | ||
| println!("def Blake3.PureTests.vectors : Blake3.PureTests.Vectors := {{"); | ||
| println!(" reference := \"1.8.7\","); |
There was a problem hiding this comment.
Marking this as likely to become stale.
2 participants
Formal developments using this library currently obtain hashes through opaque C or Rust functions. Add
Blake3.Pure.hash : ByteArray → Blake3Hash, a total Lean implementation of standard unkeyed 32-byte BLAKE3 whose definitions are exposed for kernel reduction and proof. It has no Ix dependency and imports neither FFI backend.Blake3.Pure.Proofsproves byte/word round trips, rotation and message-schedule properties, exact block framing, canonical tree correctness and uniqueness, and chunk-counter bounds under the native input-length bound. The test audit traverses checked types, bodies and inductive constructors for 50 proof roots, enforces their exact standard-Lean axiom sets, and rejects BLAKE3 FFI dependencies, opaque implementations and implementation replacements. It also checks the safe sources of the three generated recursion workers.The pure API supports one-shot unkeyed hashing. Streaming, keyed hashing, key derivation and variable-length output remain available through the existing C and Rust backends. The proofs establish the stated algorithmic properties; collision resistance and universal refinement of C or Rust are separate obligations.
Validation:
lake build --wfail Blake3Testpasses, including the 50-root audit.lake testpasses the existing C/Rust hash, keyed, derivation and sponge tests, plus two standard known answers, 258 pure/native boundary cases, 58 subtree compositions, 42 native chunk vectors and 64 internal-parent/digest-pair vectors. Both native backends report BLAKE3 1.8.7.cargo clippy --locked --release --all-targets -- -D warningsandcargo fmt --all -- --checkpass inrust/.rust/examples/pure_vectors.rsgenerator using the pinned BLAKE3 dependency.