chore: Lean specification draft

[aakoshh]

Problem Resolved

We want to have formal specification for our cryptographic libraries. This PR uses lampe to extract the Noir code into Lean, give it a specification, and prove that the extracted code satisfies it. The main correctness theorem, sha256_var_correct, is fully proved: for any input and any message_size within the array bounds, the Lampe translation of sha256_var returns the SHA-256 digest of the first message_size bytes of the message.

Summary of Changes

1. The Noir code has been extracted into Lean by running lampe in the root directory. The extraction now works on the source code as-is: Stack overflow: Large array literals reilabs/lampe#270 and Application type mismatch trying to "overwrite" a vector during pop reilabs/lampe#263, which previously required local workarounds, have been fixed upstream, so Extracted/ is reproducible from a pristine checkout. One caveat: extraction currently requires the pending fix in fix: extract inclusive for-loop ranges with their final iteration reilabs/lampe#310 — without it, lampe drops the final iteration of the inclusive loop in build_msg_block, and the spec for it becomes unprovable.
2. The Lean code is built by running lake build in the sha256/lampe directory (Lean v4.29.1, Lampe pinned to the extractor's commit). The extracted test vectors need a deeper elaborator stack, configured in lakefile.toml per the resolution of Stack overflow: Large array literals reilabs/lampe#270.
3. lampe/sha256-0.0.0/Spec.lean contains a reference implementation of SHA-256 written directly from FIPS 180-4, checked at compile time against test vectors from src/sha256/tests.nr and the standard, plus STHoare theorems relating each extracted function to it. Functions that depend on the builtin sha256CompressionFn take a lambda so the reference compression implementation can be executed in tests while the (noncomputable) builtin is used in the theorems.
4. All theorems are proved — there are no sorrys. The proof of sha256_var_correct composes specs for process_full_blocks, build_msg_block, add_padding_byte_and_compress_if_needed, attach_len_to_msg_block, hash_final_block and finalize_sha256_blocks, covering both the compression fold and the lookup-table construction of the constrained path.
5. Three theorem statements gained hypotheses they were unprovable (or false) without, all discharged at the call sites:
   • a field-size bound 2^64 < p — the asserts that pin the unconstrained oracles' outputs (encode_len, build_msg_block_helper) only do so in a large enough field;
   • msg_start % 4 = 0 for build_msg_block — the word-boundary asserts assume aligned starts, which all callers satisfy;
   • message_size <= N for process_full_blocks — without it the constrained lookup table returns the initial state while the reference folds compressions, so the original statement was false. This is supplied by sha256_var's own assert(message_size <= N).
6. The remaining trusted base is: the sha256Compression builtin behaving as some fixed compression function (the explicit h_comp hypothesis), the lampe extraction, and Lean's kernel.
7. Supporting proof infrastructure that may be worth upstreaming to lampe: an STHoare associativity lemma for the nested letIn blocks the extractor emits, a steps closer for the uGeq builtin, and a u32 instantiation of the stdlib's generic min spec.

This PR is currently based on #62, since that fixes soundness bugs in the source that would otherwise be extracted; once #62 merges this rebases onto main cleanly.

PR Checklist

• I have tested the changes locally.
• I have formatted the changes with Prettier and/or cargo fmt on default settings.