module Runtime.WordDigest import Data.SHA256 import Data.SHA256Constants import Model.Config import Model.Word32 import Std.Foundation import Std.List import Std.Natural -- One SHA-256 block-compression algorithm, specialized to a host instruction emitter. -- The emitter owns register assignment, instruction selection and branch -- flags. Loads/stores are little-endian and permit unaligned access; 8/32-bit -- loads zero-extend. Word operations wrap at 64 bits, shifts are logical, and -- 8/32-bit stores truncate. AddImm sign-extends its 32-bit operand and sets -- zero status; CmpImm supplies unsigned, zero and signed-negative status. Label and move -- operations preserve that status. These obligations are tested on each host. -- -- Registers are logical roles inherited from the original implementation: -- RDI/RSI/RDX/RCX/R8/R9 carry the six arguments; the remaining names denote -- scratch values. The emitter chooses physical registers and preserves its -- calling convention. The fixed work-area slots are part of this algorithm, -- not per-system addresses. Callers supply writable, nonoverlapping bounded -- buffers, a positive block count and body length, and valid SHA padding. family WordDigestCondition : Type 0 constructor WordDigestBelow constructor WordDigestNotZero constructor WordDigestZero constructor WordDigestNegative end-family family WordDigestBackend : Type 0 parameter erased digestBackendAssembly : Type 0 parameter erased digestBackendRegister : Type 0 constructor WordDigestBackendValue field unrestricted backendDigestLoad32 : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : digestBackendAssembly . digestBackendAssembly)))) field unrestricted backendDigestLoad64 : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : digestBackendAssembly . digestBackendAssembly)))) field unrestricted backendDigestLoad8 : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : digestBackendAssembly . digestBackendAssembly)))) field unrestricted backendDigestStore32 : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendRegister . (pi unrestricted a3 : digestBackendAssembly . digestBackendAssembly)))) field unrestricted backendDigestStore64 : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendRegister . (pi unrestricted a3 : digestBackendAssembly . digestBackendAssembly)))) field unrestricted backendDigestStore8 : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendRegister . (pi unrestricted a3 : digestBackendAssembly . digestBackendAssembly)))) field unrestricted backendDigestMov : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly))) field unrestricted backendDigestAdd : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly))) field unrestricted backendDigestAnd : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly))) field unrestricted backendDigestOr : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly))) field unrestricted backendDigestXor : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly))) field unrestricted backendDigestShl : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly))) field unrestricted backendDigestShr : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly))) field unrestricted backendDigestMovImm : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly))) field unrestricted backendDigestAddImm : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly))) field unrestricted backendDigestAndImm : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly))) field unrestricted backendDigestCmpImm : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly))) field unrestricted backendDigestMulImm : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly))) field unrestricted backendDigestLabel : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : digestBackendAssembly . digestBackendAssembly)) field unrestricted backendDigestJumpIf : (pi unrestricted a0 : (family WordDigestCondition) . (pi unrestricted a1 : Bytes . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly))) field unrestricted backendDigestReturn : (pi unrestricted a0 : digestBackendAssembly . digestBackendAssembly) field unrestricted backendDigestEnd : digestBackendAssembly field unrestricted backendDigestRAX : digestBackendRegister field unrestricted backendDigestRBX : digestBackendRegister field unrestricted backendDigestRCX : digestBackendRegister field unrestricted backendDigestRDX : digestBackendRegister field unrestricted backendDigestRSI : digestBackendRegister field unrestricted backendDigestRDI : digestBackendRegister field unrestricted backendDigestRBP : digestBackendRegister field unrestricted backendDigestR8 : digestBackendRegister field unrestricted backendDigestR9 : digestBackendRegister field unrestricted backendDigestR10 : digestBackendRegister field unrestricted backendDigestR11 : digestBackendRegister field unrestricted backendDigestR12 : digestBackendRegister field unrestricted backendDigestR13 : digestBackendRegister field unrestricted backendDigestR14 : digestBackendRegister field unrestricted backendDigestR15 : digestBackendRegister end-family def wordDigestFor = (lambda erased A : Type 0 . (lambda unrestricted count : Nat . (lambda unrestricted body : (pi unrestricted index : Nat . (pi unrestricted rest : A . A)) . (lambda unrestricted tail : A . (nat-eliminate (lambda unrestricted current : Nat . A) tail (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : A . (body (naturalSaturatingSubtract (naturalSaturatingSubtract count 1) predecessor) induction))) count))))) def digestRoundConstants = (eliminate SHA256Schedule (lambda unrestricted current : (family SHA256Schedule) . (family StdList Nat)) sha256RoundConstants (branch SHA256ScheduleEnd . (constructor StdList StdListEmpty Nat)) (branch SHA256ScheduleNext head tail induction . (constructor StdList StdListCons Nat (modelWord32ToNatural head) induction))) def digestInitialHash = (eliminate SHA256State (lambda unrestricted current : (family SHA256State) . (family StdList Nat)) sha256InitialState (branch SHA256StateValue a b c d e f g h . (constructor StdList StdListCons Nat (modelWord32ToNatural a) (constructor StdList StdListCons Nat (modelWord32ToNatural b) (constructor StdList StdListCons Nat (modelWord32ToNatural c) (constructor StdList StdListCons Nat (modelWord32ToNatural d) (constructor StdList StdListCons Nat (modelWord32ToNatural e) (constructor StdList StdListCons Nat (modelWord32ToNatural f) (constructor StdList StdListCons Nat (modelWord32ToNatural g) (constructor StdList StdListCons Nat (modelWord32ToNatural h) (constructor StdList StdListEmpty Nat))))))))))) -- The work layout follows the schedule, constants, working words, hash and -- saved registers. Round up to a cache-line boundary; no per-consumer offsets. def digestWordBytes : Nat = 4 def digestBlockBytes : Nat = 64 def digestAddressBytes : Nat = 8 def digestScheduleWords = (stdListLength Nat digestRoundConstants) def digestStateWords = (stdListLength Nat digestInitialHash) def digestScheduleBytes = (naturalMultiply digestScheduleWords digestWordBytes) def digestStateBytes = (naturalMultiply digestStateWords digestWordBytes) def digestW = (lambda unrestricted t : Nat . (naturalMultiply digestWordBytes t)) def digestK = (lambda unrestricted t : Nat . (naturalAdd digestScheduleBytes (digestW t))) def digestVariablesAt = (naturalMultiply 2 digestScheduleBytes) def digestVar = (lambda unrestricted t : Nat . (naturalAdd digestVariablesAt (digestW t))) def digestHashAt = (naturalAdd digestVariablesAt digestStateBytes) def digestH = (lambda unrestricted t : Nat . (naturalAdd digestHashAt (digestW t))) def digestSavedAt = (naturalAdd digestHashAt digestStateBytes) def digestSaved = (lambda unrestricted t : Nat . (naturalAdd digestSavedAt (naturalMultiply digestAddressBytes t))) def digestSavedRegisters : Nat = 6 -- The compression loops' remaining-pass count: the word after the saved -- registers, inside the same cache-line-rounded work area. The loops address -- each pass's schedule through RBP, which the compression saves and restores -- with the other callee-saved registers: RCX and R8 belong to callers' -- prepare/finish code (telemetry sealing keeps a count in RCX), and every -- other register is a round temporary. def digestLoopCounter = (digestSaved digestSavedRegisters) def digestWorkAlignment : Nat = 64 def digestWorkBytes = (naturalMultiply digestWorkAlignment (naturalDivideUnchecked (naturalAdd (naturalAdd digestLoopCounter digestAddressBytes) (naturalSaturatingSubtract digestWorkAlignment 1)) digestWorkAlignment)) def digestAt = (lambda unrestricted values : (family StdList Nat) . (lambda unrestricted p : Nat . (eliminate StdOption (lambda unrestricted current : (family StdOption Nat) . Nat) (stdListIndex Nat values p) (branch StdNone . 0) (branch StdSome value . value)))) def digestSlot = (lambda unrestricted v : Nat . (lambda unrestricted t : Nat . (digestVar (naturalModuloUnchecked (naturalSaturatingSubtract (naturalAdd v 64) t) 8)))) -- Runtime byte-string padding before the shared block compressor. The logical -- input/count/output/work roles are RDI/RSI/RDX/R9. The caller supplies a writable -- input followed by byteDigestPaddingBytes, and disjoint output/work regions. -- Null and negative Linux pointers, and counts above u32, refuse before writes. -- totalBytes names the original byte count register: RSI for a whole string, -- R8 for a stream tail. Its caller admits that total and the stream partition. -- Only RAX, RCX, RSI and caller-saved R10 change before the block routine saves -- its registers. RBX and the emitter's interpreter registers must survive. -- The refusal label belongs to the target entry wrapper; success falls through -- into its block routine. Both host ISAs specialize this one padding algorithm. def byteDigestPaddingBytes : Nat = (naturalMultiply 2 digestBlockBytes) def wordDigestBytePaddingFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family WordDigestBackend A R) . (lambda unrestricted totalBytes : R . (lambda unrestricted blocks : A . (eliminate WordDigestBackend (lambda unrestricted current : (family WordDigestBackend A R) . A) backend (branch WordDigestBackendValue digestLoad32 digestLoad64 digestLoad8 digestStore32 digestStore64 digestStore8 digestMov digestAdd digestAnd digestOr digestXor digestShl digestShr digestMovImm digestAddImm digestAndImm digestCmpImm digestMulImm digestLabel digestJumpIf digestReturn digestEnd digestRAX digestRBX digestRCX digestRDX digestRSI digestRDI digestRBP digestR8 digestR9 digestR10 digestR11 digestR12 digestR13 digestR14 digestR15 . (digestCmpImm digestRDI 0 (digestJumpIf (constructor WordDigestCondition WordDigestNegative) b"byte-digest-refused" (digestJumpIf (constructor WordDigestCondition WordDigestZero) b"byte-digest-refused" (digestMov digestRAX digestRSI (digestShr digestRAX 32 (digestCmpImm digestRAX 0 (digestJumpIf (constructor WordDigestCondition WordDigestNotZero) b"byte-digest-refused" (digestMov digestR10 digestRDI (digestAdd digestR10 digestRSI (digestMovImm digestRAX 0 (wordDigestFor A (naturalDivideUnchecked byteDigestPaddingBytes digestAddressBytes) (lambda unrestricted index : Nat . (digestStore64 digestR10 (naturalMultiply index digestAddressBytes) digestRAX)) (digestMovImm digestRAX 128 (digestStore8 digestR10 0 digestRAX (digestMov digestRCX totalBytes (digestShl digestRCX 3 (digestAddImm digestRSI (naturalAdd digestBlockBytes digestAddressBytes) (digestShr digestRSI 6 (digestMov digestR10 digestRSI (digestShl digestR10 6 (digestAdd digestR10 digestRDI (digestAddImm digestR10 4294967288 (wordDigestFor A digestAddressBytes (lambda unrestricted index : Nat . (lambda unrestricted rest : A . (digestMov digestRAX digestRCX (digestShr digestRAX (naturalMultiply 8 (naturalSaturatingSubtract 7 index)) (digestStore8 digestR10 index digestRAX rest))))) blocks))))))))))))))))))))))))))))) def wordDigestCompressAssemblyFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family WordDigestBackend A R) . (lambda unrestricted prepare : (pi unrestricted tail : A . A) . (lambda unrestricted initialize : (pi unrestricted tail : A . A) . (lambda unrestricted finish : (pi unrestricted tail : A . A) . (eliminate WordDigestBackend (lambda unrestricted current : (family WordDigestBackend A R) . A) backend (branch WordDigestBackendValue digestLoad32 digestLoad64 digestLoad8 digestStore32 digestStore64 digestStore8 digestMov digestAdd digestAnd digestOr digestXor digestShl digestShr digestMovImm digestAddImm digestAndImm digestCmpImm digestMulImm digestLabel digestJumpIf digestReturn digestEnd digestRAX digestRBX digestRCX digestRDX digestRSI digestRDI digestRBP digestR8 digestR9 digestR10 digestR11 digestR12 digestR13 digestR14 digestR15 . (let unrestricted digestFor = (wordDigestFor A) in (let unrestricted digestRotate = (lambda unrestricted d : R . (lambda unrestricted s : R . (lambda unrestricted n : Nat . (lambda unrestricted rest : A . (digestMov d s (digestShl d 32 (digestOr d s (digestShr d n rest)))))))) in (let unrestricted digestSigma = (lambda unrestricted d : R . (lambda unrestricted t : R . (lambda unrestricted s : R . (lambda unrestricted x : Nat . (lambda unrestricted y : Nat . (lambda unrestricted z : Nat . (lambda unrestricted shift : Nat . (lambda unrestricted rest : A . (digestRotate d s x (digestRotate t s y (digestXor d t (nat-eliminate (lambda unrestricted current : Nat . A) (digestRotate t s z (digestXor d t rest)) (lambda unrestricted p : Nat . (lambda unrestricted i : A . (digestMov t s (digestShr t z (digestXor d t rest))))) shift)))))))))))) in (let unrestricted digestConstant = (lambda unrestricted at : Nat . (lambda unrestricted value : Nat . (lambda unrestricted rest : A . (digestMovImm digestRAX value (digestStore32 digestR9 at digestRAX rest))))) in (let unrestricted digestMessageWord = (lambda unrestricted i : Nat . (lambda unrestricted rest : A . (digestLoad8 digestRAX digestRDI (naturalMultiply 4 i) (digestShl digestRAX 8 (digestLoad8 digestRBX digestRDI (naturalAdd 1 (naturalMultiply 4 i)) (digestOr digestRAX digestRBX (digestShl digestRAX 8 (digestLoad8 digestRBX digestRDI (naturalAdd 2 (naturalMultiply 4 i)) (digestOr digestRAX digestRBX (digestShl digestRAX 8 (digestLoad8 digestRBX digestRDI (naturalAdd 3 (naturalMultiply 4 i)) (digestOr digestRAX digestRBX (digestStore32 digestR9 (digestW i) digestRAX rest))))))))))))) in -- W[t] = s1(W[t-2]) + W[t-7] + s0(W[t-15]) + W[t-16], with t = 16 + k -- and `base` addressing W[k] (displacements are word offsets from it). (let unrestricted digestScheduleWord = (lambda unrestricted base : R . (lambda unrestricted k : Nat . (lambda unrestricted rest : A . (let unrestricted t = (naturalAdd 16 k) in (digestLoad32 digestRAX base (digestW (naturalSaturatingSubtract t 15)) (digestSigma digestRBX digestR10 digestRAX 7 18 3 1 (digestLoad32 digestRAX base (digestW (naturalSaturatingSubtract t 2)) (digestSigma digestR11 digestR10 digestRAX 17 19 10 1 (digestAdd digestRBX digestR11 (digestLoad32 digestR10 base (digestW (naturalSaturatingSubtract t 16)) (digestAdd digestRBX digestR10 (digestLoad32 digestR10 base (digestW (naturalSaturatingSubtract t 7)) (digestAdd digestRBX digestR10 (digestStore32 base (digestW t) digestRBX rest)))))))))))))) in -- Round t of a group of eight: the working-word slots rotate with -- t mod 8, so one group serves every round; `base` addresses W and -- K of the group's first round. (let unrestricted digestRound = (lambda unrestricted base : R . (lambda unrestricted t : Nat . (lambda unrestricted rest : A . -- t1 = h + S1(e) + ch(e, f, g) + K[t] + W[t], in rbx (digestLoad32 digestRAX digestR9 (digestSlot 4 t) (digestSigma digestRBX digestR10 digestRAX 6 11 25 0 (digestLoad32 digestR11 digestR9 (digestSlot 5 t) (digestMov digestR10 digestRAX (digestAnd digestR10 digestR11 (digestLoad32 digestR12 digestR9 (digestSlot 6 t) (digestMov digestR11 digestRAX (digestAnd digestR11 digestR12 (digestXor digestR11 digestR12 (digestXor digestR10 digestR11 (digestAdd digestRBX digestR10 (digestLoad32 digestR10 digestR9 (digestSlot 7 t) (digestAdd digestRBX digestR10 (digestLoad32 digestR10 base (digestK t) (digestAdd digestRBX digestR10 (digestLoad32 digestR10 base (digestW t) (digestAdd digestRBX digestR10 -- t2 = S0(a) + maj(a, b, c), in r10 (digestLoad32 digestRAX digestR9 (digestSlot 0 t) (digestSigma digestR10 digestR11 digestRAX 2 13 22 0 (digestLoad32 digestR11 digestR9 (digestSlot 1 t) (digestLoad32 digestR12 digestR9 (digestSlot 2 t) (digestMov digestR13 digestRAX (digestAnd digestR13 digestR11 (digestMov digestR14 digestRAX (digestAnd digestR14 digestR12 (digestXor digestR13 digestR14 (digestAnd digestR11 digestR12 (digestXor digestR13 digestR11 (digestAdd digestR10 digestR13 -- d + t1 is the next e (d's slot), t1 + t2 the next a (h's slot) (digestLoad32 digestR11 digestR9 (digestSlot 3 t) (digestAdd digestR11 digestRBX (digestStore32 digestR9 (digestSlot 3 t) digestR11 (digestAdd digestRBX digestR10 (digestStore32 digestR9 (digestSlot 7 t) digestRBX rest))))))))))))))))))))))))))))))))))))) in -- `count` passes of `body` with RBP = R9 + pass * stride: the -- schedule and constants advance, the working-word slots do not. -- The remaining count lives in the work area; RAX is free here. (let unrestricted digestLoop = (lambda unrestricted name : Bytes . (lambda unrestricted count : Nat . (lambda unrestricted stride : Nat . (lambda unrestricted body : (pi unrestricted tail : A . A) . (lambda unrestricted rest : A . (digestMov digestRBP digestR9 (digestMovImm digestRAX count (digestStore64 digestR9 digestLoopCounter digestRAX (digestLabel name (body (digestAddImm digestRBP stride (digestLoad64 digestRAX digestR9 digestLoopCounter (digestAddImm digestRAX 0xFFFFFFFF (digestStore64 digestR9 digestLoopCounter digestRAX (digestCmpImm digestRAX 0 (digestJumpIf (constructor WordDigestCondition WordDigestNotZero) name rest)))))))))))))))) in (let unrestricted digestLoadVariable = (lambda unrestricted i : Nat . (lambda unrestricted rest : A . (digestLoad32 digestRAX digestR9 (digestH i) (digestStore32 digestR9 (digestVar i) digestRAX rest)))) in (let unrestricted digestAccumulate = (lambda unrestricted i : Nat . (lambda unrestricted rest : A . (digestLoad32 digestRAX digestR9 (digestH i) (digestLoad32 digestRBX digestR9 (digestVar i) (digestAdd digestRAX digestRBX (digestStore32 digestR9 (digestH i) digestRAX rest)))))) in (let unrestricted digestSaveRegisters = (lambda unrestricted rest : A . (digestStore64 digestR9 (digestSaved 0) digestRBX (digestStore64 digestR9 (digestSaved 1) digestR12 (digestStore64 digestR9 (digestSaved 2) digestR13 (digestStore64 digestR9 (digestSaved 3) digestR14 (digestStore64 digestR9 (digestSaved 4) digestR15 (digestStore64 digestR9 (digestSaved 5) digestRBP rest))))))) in (let unrestricted digestRestoreRegisters = (lambda unrestricted rest : A . (digestLoad64 digestRBX digestR9 (digestSaved 0) (digestLoad64 digestR12 digestR9 (digestSaved 1) (digestLoad64 digestR13 digestR9 (digestSaved 2) (digestLoad64 digestR14 digestR9 (digestSaved 3) (digestLoad64 digestR15 digestR9 (digestSaved 4) (digestLoad64 digestRBP digestR9 (digestSaved 5) rest))))))) in (digestSaveRegisters (prepare (digestFor 64 (lambda unrestricted t : Nat . (digestConstant (digestK t) (digestAt digestRoundConstants t))) (initialize (digestMov digestR15 digestRDI (digestLabel b"seal-block" (digestFor 16 digestMessageWord (digestLoop b"seal-schedule" 12 16 (digestFor 4 (digestScheduleWord digestRBP)) (digestFor 8 digestLoadVariable (digestLoop b"seal-rounds" 8 32 (digestFor 8 (digestRound digestRBP)) (digestFor 8 digestAccumulate (digestAddImm digestRDI 64 (digestAddImm digestRSI 0xFFFFFFFF (digestJumpIf (constructor WordDigestCondition WordDigestNotZero) b"seal-block" (finish (digestRestoreRegisters (digestReturn digestEnd))))))))))))))))))))))))))))))))))))) -- Initialize only the chaining words; saved registers and the round scratch -- remain private to each compression call. Initialization does not erase them. def wordDigestInitializeFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family WordDigestBackend A R) . (lambda unrestricted tail : A . (eliminate WordDigestBackend (lambda unrestricted current : (family WordDigestBackend A R) . A) backend (branch WordDigestBackendValue digestLoad32 digestLoad64 digestLoad8 digestStore32 digestStore64 digestStore8 digestMov digestAdd digestAnd digestOr digestXor digestShl digestShr digestMovImm digestAddImm digestAndImm digestCmpImm digestMulImm digestLabel digestJumpIf digestReturn digestEnd digestRAX digestRBX digestRCX digestRDX digestRSI digestRDI digestRBP digestR8 digestR9 digestR10 digestR11 digestR12 digestR13 digestR14 digestR15 . (wordDigestFor A digestStateWords (lambda unrestricted i : Nat . (lambda unrestricted rest : A . (digestMovImm digestRAX (digestAt digestInitialHash i) (digestStore32 digestR9 (digestH i) digestRAX rest)))) tail))))))) def wordDigestBlocksAssemblyFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family WordDigestBackend A R) . (lambda unrestricted prepare : (pi unrestricted tail : A . A) . (lambda unrestricted finish : (pi unrestricted tail : A . A) . (wordDigestCompressAssemblyFor A R backend prepare (wordDigestInitializeFor A R backend) finish)))))) def wordDigestOutputFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family WordDigestBackend A R) . (lambda unrestricted tail : A . (eliminate WordDigestBackend (lambda unrestricted current : (family WordDigestBackend A R) . A) backend (branch WordDigestBackendValue digestLoad32 digestLoad64 digestLoad8 digestStore32 digestStore64 digestStore8 digestMov digestAdd digestAnd digestOr digestXor digestShl digestShr digestMovImm digestAddImm digestAndImm digestCmpImm digestMulImm digestLabel digestJumpIf digestReturn digestEnd digestRAX digestRBX digestRCX digestRDX digestRSI digestRDI digestRBP digestR8 digestR9 digestR10 digestR11 digestR12 digestR13 digestR14 digestR15 . (wordDigestFor A digestStateBytes (lambda unrestricted q : Nat . (lambda unrestricted rest : A . (digestLoad32 digestRAX digestR9 (digestH (naturalDivideUnchecked q digestWordBytes)) (digestShr digestRAX (naturalMultiply 8 (naturalSaturatingSubtract (naturalSaturatingSubtract digestWordBytes 1) (naturalModuloUnchecked q digestWordBytes))) (digestStore8 digestRDX q digestRAX rest))))) (digestMovImm digestRAX digestStateBytes tail)))))))) -- Raw digest ABI: padded blocks at RDI, positive count at RSI, 32-byte output -- at RDX, private work area at R9. RCX/R8 are unused. The caller proves valid -- padding and nonoverlap. Returns 32; no timestamp write and no payload copy. def wordDigestAssemblyFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family WordDigestBackend A R) . (wordDigestBlocksAssemblyFor A R backend (lambda unrestricted tail : A . tail) (wordDigestOutputFor A R backend))))) -- Same raw-block ABI as wordDigestAssemblyFor, with chaining words retained -- in the work region. The caller supplies a positive number of complete blocks. def wordDigestContinueAssemblyFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family WordDigestBackend A R) . (wordDigestCompressAssemblyFor A R backend (lambda unrestricted tail : A . tail) (lambda unrestricted tail : A . tail) (wordDigestOutputFor A R backend))))) -- A bounded stream window contains complete SHA blocks. It is a host buffering -- policy, independent of a device or OS allocation quantum. The final suffix -- needs two extra blocks. The plan's two words are full-window count and tail. def byteDigestChunkShift : Nat = 10 def byteDigestChunkBytes : Nat = (naturalPowerOfTwo byteDigestChunkShift) def byteDigestChunkPlanBytes : Nat = (naturalMultiply 2 digestAddressBytes) def byteDigestChunkBufferBytes : Nat = (naturalAdd byteDigestChunkBytes byteDigestPaddingBytes) -- RDI: total u32 bytes; RSI: writable two-word chunk plan; R9: private -- work area. Reject oversized totals before writes, initialize chaining words, -- return 32. Valid disjoint destination/work buffers are the caller contract. def wordDigestStreamStartFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family WordDigestBackend A R) . (eliminate WordDigestBackend (lambda unrestricted current : (family WordDigestBackend A R) . A) backend (branch WordDigestBackendValue digestLoad32 digestLoad64 digestLoad8 digestStore32 digestStore64 digestStore8 digestMov digestAdd digestAnd digestOr digestXor digestShl digestShr digestMovImm digestAddImm digestAndImm digestCmpImm digestMulImm digestLabel digestJumpIf digestReturn digestEnd digestRAX digestRBX digestRCX digestRDX digestRSI digestRDI digestRBP digestR8 digestR9 digestR10 digestR11 digestR12 digestR13 digestR14 digestR15 . (digestMov digestRAX digestRDI (digestShr digestRAX 32 (digestCmpImm digestRAX 0 (digestJumpIf (constructor WordDigestCondition WordDigestZero) b"stream-start" (digestMovImm digestRAX 0 (digestReturn (digestLabel b"stream-start" (digestMov digestRAX digestRDI (digestShr digestRAX byteDigestChunkShift (digestStore64 digestRSI 0 digestRAX (digestMov digestRAX digestRDI (digestAndImm digestRAX (naturalSaturatingSubtract byteDigestChunkBytes 1) (digestStore64 digestRSI digestAddressBytes digestRAX (wordDigestInitializeFor A R backend (digestMovImm digestRAX digestStateBytes (digestReturn digestEnd))))))))))))))))))))) -- Byte-digest ABI, with the original total in R8 and only the final window -- tail at RDI/RSI. Prior full windows must have been compressed in this work -- region. Zero-fill padding uses the original bit count, never the tail count. def wordDigestStreamFinishFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family WordDigestBackend A R) . (eliminate WordDigestBackend (lambda unrestricted current : (family WordDigestBackend A R) . A) backend (branch WordDigestBackendValue digestLoad32 digestLoad64 digestLoad8 digestStore32 digestStore64 digestStore8 digestMov digestAdd digestAnd digestOr digestXor digestShl digestShr digestMovImm digestAddImm digestAndImm digestCmpImm digestMulImm digestLabel digestJumpIf digestReturn digestEnd digestRAX digestRBX digestRCX digestRDX digestRSI digestRDI digestRBP digestR8 digestR9 digestR10 digestR11 digestR12 digestR13 digestR14 digestR15 . (digestMov digestRAX digestR8 (digestShr digestRAX 32 (digestCmpImm digestRAX 0 (digestJumpIf (constructor WordDigestCondition WordDigestNotZero) b"byte-digest-refused" (digestMov digestRAX digestR8 (digestAndImm digestRAX (naturalSaturatingSubtract byteDigestChunkBytes 1) (digestXor digestRAX digestRSI (digestCmpImm digestRAX 0 (digestJumpIf (constructor WordDigestCondition WordDigestNotZero) b"byte-digest-refused" (wordDigestBytePaddingFor A R backend digestR8 (wordDigestContinueAssemblyFor A R backend))))))))))))))))