Skip to content

aarch64 SHA-256 on the SHA-2 instructions is proven - #552

Merged
kixelated merged 7 commits into
mainfrom
quest/m2/verified/sha256-aarch64-hw
Nov 10, 2026
Merged

aarch64 SHA-256 on the SHA-2 instructions is proven#552
kixelated merged 7 commits into
mainfrom
quest/m2/verified/sha256-aarch64-hw

Conversation

@kixelated

@kixelated kixelated commented Nov 10, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Closes quest/m2/verified/sha256-aarch64-hw.md.

On aarch64 with the crypto extension, SHA-256 now earns the ✓, along with HMAC-SHA256 and HKDF-SHA256 (and PBKDF2 over it, which has no benchmark row). The routine is aws-lc's sha256_block_data_order_hw, exactly as rind's release build emits it. rind's own HOL Light proof shows it computes s2n-bignum's FIPS 180-4 spec from awslabs/s2n-bignum#415. Lean restates that theorem as an axiom over the Rust wrapper and proves the spec equal to Rind/HashSpec.lean's. This is the calibration quest, so most of this body is the measurement.

What changed

  • HOL Light proof. proofs/hol-light/aarch64/sha256_block_data_order_hw.ml proves SHA256_HW_SUBROUTINE_CORRECT. Calling the naked function with n ≥ 1 blocks leaves the state at sha256_hash_blocks m h n, then returns to the caller under the ABI's frame. Its only axioms are HOL Light's three.
    • Before the loop, the proof checks the K256 table the build links against FIPS 180-4's constants.
    • The loop invariant tracks the hash after i blocks, the data pointer, and the counter.
    • It steps the 115-instruction body symbolically. Each sha256h/sha256h2 pair is rewritten to four spec rounds, and each sha256su0/sha256su1 pair to four schedule words.
  • The pinned spec. proofs/hol-light/s2n-bignum/x86/proofs/utils/sha256_spec.ml is perf(ed25519): verify without ADX through curve25519-dalek's AVX2 backend #415's file, unchanged, at 79120e64ed55e37c9652565ff272b7ef17f76738. It sits ahead of the submodule on HOL Light's load path. The submodule stays at merged upstream. proofs/README.md records the PR and commit.
  • admin/prove. A naked function now comes out as an object file named <file>.o. It holds the function's whole section, its relocations, and the one .rodata section they reach. define_assert_relocs_from_elf checks the instructions and relocations, so no transliteration is trusted, and the table's bytes come from the build too. asm_function finds the function and its relocations with rind_symbol and relocations, which moq-dev/rind#551 added on main.
  • Rust. low::aarch64::sha256 dispatches through compress_hw(HaveCryptoExt, ..) and compress_nohw(..), as sha512.rs does, so Aeneas translates the dispatch. The emitted naked function is byte-identical; the extracted object matches the one the proof was developed on.
  • Lean.
    • Rind/S2nSha256.lean transliterates s2n-bignum's spec and proves block_words and hashBlocks_eq, which together say it is HashSpec's sha256.compress folded over the blocks.
    • Rind/Aarch64/Sha256Hw.lean restates the HOL theorem as sha256_block_data_order_hw_spec and proves that the dispatch meets Compresses whenever HaveCryptoExt::check returns Some.
  • ShaBlocks split. It becomes Sha1Blocks and Sha256Blocks on both targets, so a SHA-256 theorem no longer assumes SHA-1's unproven contract.
    • On aarch64, Sha256Blocks is only the CPU check plus the entry checks.
    • On x86_64, its fields are the old SHA-256 ones.
    • RunsDigest takes ShaBlocksOf a, and RunsHmac picks per algorithm.
    • aarch64's HashAxioms.lean is now hand-written, since its SHA-256 theorems rest on the new axiom.
  • The ✓. benchmarks/verified.toml gains the entry, which notes the pin, and BENCHMARKS.md is re-rendered.
  • Quests. The quest is deleted with every link to it. x86_64 SHA-NI SHA-256 now records how unmerged upstream comes in, as settled here.

Public API impact

None. The change is in low::aarch64::sha256's private functions and in the proofs.

Measurement

HOL Light proof

The routine is 124 instructions with one loop and no branch beyond the loop's cbnz. Every instruction is already in s2n-bignum's aarch64 model.

Part Lines
Instruction listing (checked against the build) 134
Lemmas: four rounds per sha256h/h2, schedule per su0/su1, constants table, loads 285
Proof: loop invariant, entry, body, back edge, exit, then the subroutine wrapper 174
Header and comments 28
Total 621
Additions to the instruction model 0
  • Sessions and time. One agent session, Claude Opus 5.5 at high effort, continued across two context compactions. It took about 2 h 50 min of wall time from claim (19:41) to the proved subroutine theorem (22:30), including the toolchain setup and the stalls below.
  • Check time. admin/prove hol-light compiles the aarch64 proofs (bignum_eq and this one) to native code with HOL Light's base.ml, and the binary checks them in 49 s. That is well within the prove workflow's hol-light job, which has 30 minutes (the Lean job has 60). Interactively, the 115-step body takes about 5 s.
  • Stalls, and what unblocked each:
    1. Gated jobs sat queued until they were killed at 2 hours, and later a nix GC removed the toolchain. I switched to one niced HOL Light REPL for development and kept gated runs for the real checks.
    2. The simulator discards every read c s fact about a state other than the current one, including facts about the ghost memory mem0. Wrapping the data and table facts in one defined predicate, sha256_hw_inputs, keeps them.
    3. DATA64_CONV only splits a table at an address written word (k + 0). Rewriting k to k + 0 first fixed it.
    4. Building goals with subst captured bound variables. mk_abs and list_mk_forall with explicit types fixed it.
    5. In the loop body, ld1 {v4-v7} read memory at addresses normalized differently from the data facts. Q5 to Q7 then held unknown values and were discarded, which looked like Q0/Q1 vanishing about 20 steps later. Abbreviating d = data + 64·i before stepping fixed it; bisecting by single steps found it.
    6. ARM_ADD_RETURN_STACK_TAC left the bytes_loaded precondition unproven at the core's entry. Rewriting it to a bytes read, as upstream's BYTES_LOADED_DATA does, fixed it.
  • Scale. Upstream's x86_64 proofs of the same spec are 13,570 lines for chore(quest): scope the post-quantum algorithms and plan a leaf per algorithm #450's SHA-NI routine (plus about 200 lines of model additions) and 12,830 for perf(ed25519): verify without ADX through curve25519-dalek's AVX2 backend #415's scalar one. This proof is about 20 times shorter than chore(quest): scope the post-quantum algorithms and plan a leaf per algorithm #450. The main reason is that it never states per-instruction intermediate values. The four-round and schedule lemmas let the simulator's own rewriting carry spec terms through the whole body.

Lean side

Part Lines Check time
Axiom restatement and dispatch theorem (Sha256Hw.lean) 60 8 s
Spec transliteration (S2nSha256.lean, trusted as a transcription) 73 18 s, both parts
Bridge from the transliteration to HashSpec (S2nSha256.lean) 148
aarch64 HashAxioms.lean, now hand-written 68 3 s
ShaBlocks split and its consumers, both targets about 170 changed 3.5 s (aarch64), 9 s (x86_64)
  • Sessions. The first session wrote the Lean side in about an hour but could not compile it: the gated build sat queued behind two cargo-mutants runs. A second session (this one) got it through admin/prove lean in about 2 hours, most of it waiting in quest gate on a loaded host.
  • What the build found:
    • Four rewrites in S2nSha256.lean that no longer matched. getElem!_append_left/_right did not unify, and the strong induction in blocks_eq left the goal in n instead of bytes.length. Deprecated if_pos/if_neg became ite_eq_left/ite_eq_right.
    • choose_eq and maj_eq used bv_decide. Its native axioms (*._native.bv_decide.ax_1_5, through Lean.ofReduceBool) showed up in every SHA-256 theorem's axiom list. They are now per-bit case splits, so the Lean side trusts no compiled code.
    • The dispatch proof's empty-input case timed out unfolding blocks under simp_all, and it now rewrites blocks 64 [] directly.
    • The axiom guards. HMAC's start, update, and finish theorems and digest_ctx_new_spec turned out not to rest on the new axiom, since they compress nothing or take the block function as a hypothesis. The HMAC, KDF, and P-256 signature entries in aarch64's Axioms.lean gain sha256_block_data_order_hw_spec.
  • Check time. A full admin/prove lean from a cold .tmp/prove took 22 min on this loaded host (24 cores, load average above 100), extraction included, inside the prove workflow's 60 minutes. The new and changed modules add about 40 s of it. admin/prove hol-light ran in 192 s, 67 s of it checking.

Second route: Lean bv_decide

I wrote the Arm pseudocode for sha256h, sha256h2, sha256su0, sha256su1 and the vector add as Lean BitVec functions, following s2n-bignum's arm/proofs/sha256.ml, and checked them with bv_decide (core Lean 4.35, CaDiCaL, LRAT-checked):

Goal Result
sha256h/sha256h2 equal four spec rounds proved, 1.0 s
sha256su0+sha256su1 equal four schedule words proved, 1.0 s
The routine's dataflow for one block against the spec, 4 rounds proved, 16 s
Same, 8 rounds proved, 80 s (SAT 71 s)
Same, 16 rounds stopped at the 20-minute limit
Same, 64 rounds not attempted after 16 failed

Every intermediate value was named as a hypothesis so the terms stay linear. The time goes to SAT, and it grows about 5 to 15 times per doubling of rounds.

  • Where it stopped.
    • A whole block does not bit-blast.
    • The instruction-level lemmas, which took the HOL proof several hand-built lemmas, take about a second each. So a decomposed bv_decide proof could replace the lemma layer.
    • It cannot replace the stepping. Rind has no Lean model of AArch64 machine code: the dataflow above is transcribed by hand from the listing, not decoded from the object code.
    • Closing that gap means adopting a Lean Arm model such as AWS's LNSym, which pins its own older toolchain and lacks the SHA-256 instructions, or writing one.
  • What it trusts beyond the HOL route:
    • Lean.ofReduceBool, the compiled LRAT checker.
    • A hand transcription of the instructions' semantics, not s2n-bignum's model, which is tested against hardware.
    • A hand transcription of the routine's dataflow, rather than its bytes.
    • Under the composition rule, its theorem would enter as a Lean theorem, not an axiom, but about a transcription. That is weaker than the HOL theorem about the emitted object code.
  • Cost. About 40 minutes, roughly 150 lines of Lean plus a 70-line generator.

Proposed sizes for the quests that require this one

These are calibrated on this quest: 124 instructions, a loop, no model additions, about 600 lines and one session. Scalar routines unroll 64 to 80 rounds into about 1,000 instructions each. The per-round rewriting approach should carry over, but each needs its own round lemma for the ALU sequence.

Quest Routines (instructions) Model gaps Proposed
x86_64 SHA-NI SHA-256 SHA-NI routine (#450's 299-line source) sha256rnds2, sha256msg1/2: #450 adds about 200 lines M (was L): vendor #450's model additions on the same pin, and write the proof in this style
SHA-1 everywhere aarch64 nohw (about 1,000), x86 avx/ssse3/nohw (about 1,100 to 1,200 each), x86 SHA-NI, aarch64 hw aarch64 lacks every SHA-1 instruction; x86 lacks sha1rnds4/sha1nexte/sha1msg1/2 XL (was L), or split by tier: model additions on two architectures plus five routines
x86_64 SHA-2 without AVX2 sha256 avx/ssse3/nohw (about 1,000 to 1,300 each), sha512 nohw vpalignr is absent L (unchanged)
aarch64 AES-192-GCM 8x enc/dec 192 (about 1,000 each), loops and tail branches none (AES, PMULL, EXT are modeled) XL (unchanged); re-size after #490 as planned
x86_64 RSAZ IFMA amm52x20/30/40 (285 to 508) vpmadd52luq/huq are absent XL (unchanged)
x86_64 RSA Montgomery mul4x (348), mulx4x (269), sqr8x (115), mul_mont (163), all loops with variable trip counts none expected L (was XL): scalar, modeled, and s2n-bignum's bignum loop lemmas apply
aarch64 ChaCha20-Poly1305 seal/open (about 1,100 to 1,300 each), poly_hash_ad (76) none expected XL (unchanged)
AArch32 model, armv7 assembly a new model everything XL (unchanged); this calibration says nothing about the cost of a model

Decisions

  • Vendoring layout (chosen without asking, for review). The spec lives under proofs/hol-light/s2n-bignum/, at its upstream path, so the proof's needs line is the same with or without it. When the submodule moves past perf(ed25519): verify without ADX through curve25519-dalek's AVX2 backend #415's merge, deleting the directory is the whole migration.

  • Offer the HOL Light proof to awslabs/s2n-bignum (maintainer, 2026-11-10, comment): ✅ keep it vendored in rind (rejected: offer it after x86_64 sha256 block compression implementation without SIMD and without sha-specific instructions + functional proof + safety proof + Windows awslabs/s2n-bignum#415 merges, offer it now).

  • Apply the proposed quest sizes (maintainer, 2026-11-10, /quest-complete): ✅ apply them in this PR (rejected: defer to the next /quest-audit, ignore them). x86_64 SHA-NI SHA-256 is now M, SHA-1 XL, x86_64 RSA Montgomery L; the rest are unchanged.

  • ALGORITHMS.md's inventory refreshed (chosen without asking). The hol-light job's bytes check found it stale: rind's aarch64 release build no longer defines bignum_negmodinv or bignum_sqr_p521 as symbols (LLVM inlines them into their callers), so admin/prove-bytes inventory lists them as not imported on aarch64. The table is the tool's output, unedited.

  • Splitting ShaBlocks (chosen without asking). Otherwise the ✓ would have rested on a hypothesis about SHA-1's routine.

  • The ✓ covers sha256/*, hmac-sha256/* and hkdf-sha256/* (chosen without asking). It applies on aarch64 with aes, pmull, sha2, the features HaveCryptoExt checks. ECDSA already had its ✓, which leaves the message hash out.

  • No bv_decide in the trusted Lean (chosen without asking). Its native axioms would have joined every SHA-256 theorem's trust base for two one-line bitwise identities.

  • The wrapper's hypotheses follow s2n-bignum's subroutine theorems:

    • the state, data, table, code and the 16-byte frame below the stack pointer do not overlap;
    • the stack pointer is 16-byte aligned;
    • adrp_within_bounds holds for the table.

    Sha256Hw.lean says why each holds for every call the Rust allows.

Follow-ups

  • Move to perf(ed25519): verify without ADX through curve25519-dalek's AVX2 backend #415's spec once it merges: bump the submodule and delete proofs/hol-light/s2n-bignum/x86/. Recommend: no quest, since the quest that bumps the submodule does it.
  • The SHA-256 nohw routine on aarch64 (906 instructions), for CPUs without the crypto extension. Recommend: plan it, sized L. It is the same spec with a scalar round lemma.

Models

Size: L
Implementer: Claude Code, claude-opus-5-5, high effort
Implementer: Claude Code, claude-opus-5-5, high effort (iterate, L)
Implementer: Claude Code, claude-opus-5-5, low effort (iterate, S)

(Written by Opus 5.5 with high; iterated by Opus 5.5 with low)

🤖 Generated with Claude Code

Review

Rewritten by quest review after each round.

  • Reviewer: Codex, gpt-6.1-sol, high effort
  • Session: 01a1c6ef-8480-78c0-b14d-e49f935dc849, round 2
  • Head: 0380421
  • Base: origin/main at f67def2
  • Score: 9/10, No actionable defects were found in the documentation and quest-estimate updates since the previous review; builds and tests were not run, as instructed.
  • Findings: none

kixelated and others added 3 commits November 9, 2026 19:41
@kixelated
chore(quest): claim quest/m2/verified/sha256-aarch64-hw.md
6c7dd27 
Quest-Claim: b08e8d3e702deab2
@kixelated @claude
feat(proofs): prove aarch64's SHA-256 routine for the crypto extensio…
10bdf8c 
…n in HOL Light

WIP checkpoint: the HOL Light proof and admin/prove's extraction are done;
the Lean axiom and bridge await a build.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@kixelated @claude
fix(proofs): update the hand models' quotes, and write aarch64's Hash…
fd25fd2 
…Axioms

Three hand models' Rust quotes had drifted from the source, so admin/prove
failed before translating: Digest::id, #[must_use] on hmac::Context::sign,
and the doc comment on PublicKey::verify. None changes a model.

aarch64's SHA-256 theorems now rest on sha256_block_data_order_hw_spec, so its
HashAxioms.lean is written by hand rather than copied from x86_64's. Its
expected axiom lists are not yet checked by a build.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@kixelated

kixelated commented Nov 10, 2026

Copy link
Copy Markdown
Collaborator Author

Maintainer decision (2026-11-10, /quest-complete): offer the HOL Light proof to awslabs/s2n-bignum: ✅ keep it vendored in rind (rejected: offer it after awslabs/s2n-bignum#415 merges; offer it now). Remove that Waiting item. The remaining work is the agent's Lean build (admin/prove lean), and fixing what it reports.

(Written by Claude Opus 5.5 with low)

kixelated and others added 3 commits November 10, 2026 09:27
@kixelated
Merge remote-tracking branch 'origin/main' into quest/m2/verified/sha…
6472073 
…256-aarch64-hw

# Conflicts:
#	admin/prove
@kixelated @claude
fix(proofs): make the aarch64 SHA-256 Lean side check
7b2405f 
S2nSha256's schedule and blocks lemmas used rewrites that no longer
matched, and its choose/maj bridges used bv_decide, whose native
axioms would have entered the trust base; they are now case splits.
The dispatch proof in Sha256Hw.lean is rewritten against the
translation, and the axiom guards hold what Lean reports.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@kixelated @claude
chore(quest): finish quest/m2/verified/sha256-aarch64-hw.md
1ebc3dd 
Delete the quest and every link to it, and point the prose that cited
it at the PR, recording how unmerged upstream comes in.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@kixelated
kixelated marked this pull request as ready for review November 10, 2026 19:31
@pullfrog

pullfrog Bot commented Nov 10, 2026 •
edited
Loading

Copy link
Copy Markdown

Your OpenCode Go account is out of credit. Top it up, then re-trigger Pullfrog.

OpenCode Go's response 
provider error: Insufficient balance (402)

Top up OpenCode Go →

Pullfrog  ｜ Rerun failed job ➔ ｜ View workflow run ｜ via Pullfrog ｜ Using glm-5.3

@coderabbitai

coderabbitai Bot commented Nov 10, 2026 •
edited
Loading

Copy link
Copy Markdown

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 15 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

Run configuration

  • Source mode: Auto
  • Repository: Unavailable
  • Branch: Unavailable
  • File: No configuration file from this repository applied
  • Commit: Unavailable
  • Layers: Organization UI
  • Review profile: CHILL
  • Plan: Advanced
  • Run ID: 4a149c3d-4552-4389-b37e-277cc78a3300
Commits

Reviewing files that changed from the base of the PR and between 53fcf3a and 0380421.

Files ignored due to path filters: 4

  • benchmarks/kixtop-dark.svg is excluded by !**/*.svg
  • benchmarks/kixtop.svg is excluded by !**/*.svg
  • benchmarks/overview-dark.svg is excluded by !**/*.svg
  • benchmarks/overview.svg is excluded by !**/*.svg
Files selected for processing: 49

  • .gitignore
  • ALGORITHMS.md
  • BENCHMARKS.md
  • admin/prove
  • benchmarks/verified.toml
  • proofs/README.md
  • proofs/Rind/Aarch64/Axioms.lean
  • proofs/Rind/Aarch64/FunsExternal.lean
  • proofs/Rind/Aarch64/HashAxioms.lean
  • proofs/Rind/Aarch64/P256Signature.lean
  • proofs/Rind/Aarch64/Sha256Hw.lean
  • proofs/Rind/Aarch64/ShaBlocks.lean
  • proofs/Rind/Aarch64/TypesExternal.lean
  • proofs/Rind/S2nSha256.lean
  • proofs/Rind/X86_64/DigestApi.lean
  • proofs/Rind/X86_64/FunsExternal.lean
  • proofs/Rind/X86_64/HashAxioms.lean
  • proofs/Rind/X86_64/Hmac.lean
  • proofs/Rind/X86_64/HmacApi.lean
  • proofs/Rind/X86_64/Sha.lean
  • proofs/Rind/X86_64/ShaBlocks.lean
  • proofs/hol-light/aarch64/sha256_block_data_order_hw.ml
  • proofs/hol-light/s2n-bignum/x86/proofs/utils/sha256_spec.ml
  • quest/m2/verified/README.md
  • quest/m2/verified/sha256-aarch64-hw.md
  • quest/m3/verified/README.md
  • quest/m3/verified/sha256-block.md
  • quest/m4/verified/README.md
  • quest/m4/verified/aes-gcm-aarch64-192.md
  • quest/m4/verified/aes-gcm-x86-vaes.md
  • quest/m4/verified/aes-modes.md
  • quest/m4/verified/chacha20-poly1305-aarch64.md
  • quest/m4/verified/chacha20-poly1305-x86.md
  • quest/m4/verified/p256-x86.md
  • quest/m4/verified/rsa-aarch64-mont.md
  • quest/m4/verified/rsa-x86-ifma.md
  • quest/m4/verified/rsa-x86-mont.md
  • quest/m4/verified/sha256-x86-avx2.md
  • quest/m4/verified/sha512-aarch64-hw.md
  • quest/m4/verified/sha512-x86-avx2.md
  • quest/m4/verified/sha512-x86-ext.md
  • quest/m5/verified-armv7/assembly.md
  • quest/m5/verified-armv7/curve25519.md
  • quest/m5/verified-armv7/model.md
  • quest/m5/verified/aarch64-no-crypto.md
  • quest/m5/verified/sha1.md
  • quest/m5/verified/sha2-x86-no-avx2.md
  • quest/m5/verified/x86-no-aesni.md
  • rind/src/low/aarch64/sha256.rs
  • Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

@kixelated @claude
chore: resize the quests this calibration informs, and refresh ALGORI…
0380421 
…THMS.md's inventory

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@kixelated
kixelated added this pull request to the merge queue Nov 10, 2026
Merged via the queue into main with commit 273aa3b Nov 10, 2026
6 of 7 checks passed
@moq-bot moq-bot Bot mentioned this pull request Nov 10, 2026
Open
@kixelated kixelated mentioned this pull request Nov 11, 2026
Merged
@kixelated
kixelated deleted the quest/m2/verified/sha256-aarch64-hw branch November 11, 2026 21:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@kixelated