# Generated by tools/generators/blake2s_gen.py; do not edit.
import Base
import ./types.bend as T
import ./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{}: hi

def 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: w

def 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)
      a

def 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))