src/crypto/blake/blake2s/blake2s.bend source
src/crypto/blake/blake2s/blake2s.bend on the hub · documented module
# Generated by tools/generators/blake2s_gen.py; do not edit.import Baseimport ./types.bend as Timport ./compress.bend as C# The 64-bit byte counter t is kept as two U32 halves (t0 low, t1 high).def carry(c: Bool, hi: U32) -> U32: match c: case True{}: U32.add(hi,1) case False{}: hidef count_hi(+lo: U32, hi: U32, +n: U32) -> U32: carry(U32.is_lt(U32.add(lo,n),n),hi)def read15(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32,w12: U32,w13: U32,w14: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w15) = pair (a,C.compress(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,False{}))def read14(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32,w12: U32,w13: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w14) = pair read15(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))def read13(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32,w12: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w13) = pair read14(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))def read12(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w12) = pair read13(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))def read11(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w11) = pair read12(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))def read10(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w10) = pair read11(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))def read9(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w9) = pair read10(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))def read8(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w8) = pair read9(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))def read7(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w7) = pair read8(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))def read6(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w6) = pair read7(index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))def read5(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w5) = pair read6(index,h,t0,t1,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))def read4(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w4) = pair read5(index,h,t0,t1,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))def read3(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w3) = pair read4(index,h,t0,t1,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))def read2(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w2) = pair read3(index,h,t0,t1,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))def read1(+index: U32, h: T.State, t0: U32, t1: U32, w0: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w1) = pair read2(index,h,t0,t1,w0,w1,Array.get(U32,a,U32.add(index,2)))def read0(+index: U32, h: T.State, t0: U32, t1: U32, pair: Array<U32> & U32) -> Array<U32> & T.State: (a,w0) = pair read1(index,h,t0,t1,w0,Array.get(U32,a,U32.add(index,1)))def absorb(a: Array<U32>, +index: U32, h: T.State, t0: U32, t1: U32) -> Array<U32> & T.State: read0(index,h,t0,t1,Array.get(U32,a,index))# The final block keeps the bytes before the logical length and zeroes the rest.# keep(n, w) keeps the low n bytes of w.def keep(n: Nat, +w: U32) -> U32: match n: case 0n: 0 case 1n: U32.and(255,w) case 2n: U32.and(65535,w) case 3n: U32.and(16777215,w) case 4n+p: wdef pad_word(w: U32, +pos: Nat, +remain: Nat) -> U32: keep(Nat.sub(remain,pos),w)def pad15(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32,w12: U32,w13: U32,w14: U32, pair: Array<U32> & U32) -> T.State: (a,w15) = pair C.compress(h,pad_word(w0,0n,remain),pad_word(w1,4n,remain),pad_word(w2,8n,remain),pad_word(w3,12n,remain),pad_word(w4,16n,remain),pad_word(w5,20n,remain),pad_word(w6,24n,remain),pad_word(w7,28n,remain),pad_word(w8,32n,remain),pad_word(w9,36n,remain),pad_word(w10,40n,remain),pad_word(w11,44n,remain),pad_word(w12,48n,remain),pad_word(w13,52n,remain),pad_word(w14,56n,remain),pad_word(w15,60n,remain),t0,t1,True{})def pad14(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32,w12: U32,w13: U32, pair: Array<U32> & U32) -> T.State: (a,w14) = pair pad15(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))def pad13(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32,w12: U32, pair: Array<U32> & U32) -> T.State: (a,w13) = pair pad14(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))def pad12(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32,w11: U32, pair: Array<U32> & U32) -> T.State: (a,w12) = pair pad13(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))def pad11(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32,w10: U32, pair: Array<U32> & U32) -> T.State: (a,w11) = pair pad12(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))def pad10(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32,w9: U32, pair: Array<U32> & U32) -> T.State: (a,w10) = pair pad11(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))def pad9(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32,w8: U32, pair: Array<U32> & U32) -> T.State: (a,w9) = pair pad10(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))def pad8(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32,w7: U32, pair: Array<U32> & U32) -> T.State: (a,w8) = pair pad9(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))def pad7(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32,w6: U32, pair: Array<U32> & U32) -> T.State: (a,w7) = pair pad8(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))def pad6(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32,w5: U32, pair: Array<U32> & U32) -> T.State: (a,w6) = pair pad7(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))def pad5(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32,w4: U32, pair: Array<U32> & U32) -> T.State: (a,w5) = pair pad6(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))def pad4(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32,w3: U32, pair: Array<U32> & U32) -> T.State: (a,w4) = pair pad5(remain,index,h,t0,t1,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))def pad3(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32,w2: U32, pair: Array<U32> & U32) -> T.State: (a,w3) = pair pad4(remain,index,h,t0,t1,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))def pad2(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32,w1: U32, pair: Array<U32> & U32) -> T.State: (a,w2) = pair pad3(remain,index,h,t0,t1,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))def pad1(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, w0: U32, pair: Array<U32> & U32) -> T.State: (a,w1) = pair pad2(remain,index,h,t0,t1,w0,w1,Array.get(U32,a,U32.add(index,2)))def pad0(+remain: Nat, +index: U32, h: T.State, t0: U32, t1: U32, pair: Array<U32> & U32) -> T.State: (a,w0) = pair pad1(remain,index,h,t0,t1,w0,Array.get(U32,a,U32.add(index,1)))def finish(a: Array<U32>, +index: U32, +t0: U32, t1: U32, +remain: Nat, h: T.State) -> T.State: +n = U32.from_nat(remain) pad0(remain,index,h,U32.add(t0,n),count_hi(t0,t1,n),Array.get(U32,a,index))def blocks(n: Nat, +index: U32, +t0: U32, t1: U32, +remain: Nat, pair: Array<U32> & T.State) -> T.State: match n pair: case 0n Tuple{a,h}: finish(a,index,t0,t1,remain,h) case 1n+p Tuple{a,h}: +c0 = U32.add(t0,64) +c1 = count_hi(t0,t1,64) blocks(p,U32.add(index,16),c0,c1,remain,absorb(a,index,h,c0,c1))# Parameter block for an unkeyed 32-byte digest: h0 = IV0 ^ 0x01010020.def initial() -> T.State: T.H{1795745351,3144134277,1013904242,2773480762,1359893119,2600822924,528734635,1541459225}# Blocks before the last one: max(1, ceil(length/64)) - 1.def leading(length: Nat) -> Nat: Nat.sub(Nat.div(Nat.add(length,63n),64n),1n)def unchecked(a: Array<U32>, +length: Nat) -> T.State: +n = leading(length) blocks(n,0,0,0,Nat.sub(length,Nat.mul(64n,n)),(a,initial()))def digest(h: T.State) -> Array<U32>: match h: case T.H{h0,h1,h2,h3,h4,h5,h6,h7}: a = Array.new(U32,3n,0) a = Array.set(U32,a,0,h0) a = Array.set(U32,a,1,h1) a = Array.set(U32,a,2,h2) a = Array.set(U32,a,3,h3) a = Array.set(U32,a,4,h4) a = Array.set(U32,a,5,h5) a = Array.set(U32,a,6,h6) a = Array.set(U32,a,7,h7) adef checked(valid: Bool, a: Array<U32>, length: Nat) -> Maybe<&1,Array<U32>>: match valid: case False{}: None{} case True{}: Some{digest(unchecked(a,length))}def sized(+length: Nat, pair: Array<U32> & U32) -> Maybe<&1,Array<U32>>: (a,capacity) = pair checked(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)# BLAKE2s-256 of the first `length` bytes of `a` (four little-endian bytes per# word): the eight little-endian digest words, or None when length exceeds# 4 * the array capacity.def blake2s(a: Array<U32>, length: Nat) -> Maybe<&1,Array<U32>>: sized(length,Array.size(U32,a))