1 import Base 2 import ./core.bend as Core 3 import ../state.bend as S 4 5 # Packed big-endian words: four bytes per U32. Array is flat u32 storage in native C. 6 def at(a: Array, i: U32) -> Array & U32: 7 Array.get(U32,a,i) 8 9 def partial(+w: U32, delta: Nat) -> U32: 10 match delta: 11 case 0n: 2147483648 12 case 1n: U32.or(U32.and(w,4278190080),8388608) 13 case 2n: U32.or(U32.and(w,4294901760),32768) 14 case 3n: U32.or(U32.and(w,4294967040),128) 15 case _: w 16 17 def pad_choose(c: Cmp, w: U32, delta: Nat) -> U32: 18 match c: 19 case GT{}: 0 20 case EQ{}: 2147483648 21 case LT{}: partial(w,delta) 22 23 def pad_word(w: U32, +pos: Nat, +remain: Nat) -> U32: 24 pad_choose(Nat.cmp(pos,remain),w,Nat.sub(remain,pos)) 25 26 def length_word(short: Bool, w: U32, length: U32) -> U32: 27 match short: 28 case True{}: length 29 case False{}: w 30 31 def read16(+extra: Nat,+index: U32, s: S.State, 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) -> Array & S.State: 32 (a, w15) = pair 33 (a,Core.fips_compress16(w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,extra,s)) 34 35 def read15(+extra: Nat,+index: U32, s: S.State, 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) -> Array & S.State: 36 (a, w14) = pair 37 read16(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,at(a,U32.inc(index))) 38 39 def read14(+extra: Nat,+index: U32, s: S.State, 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) -> Array & S.State: 40 (a, w13) = pair 41 read15(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,at(a,U32.inc(index))) 42 43 def read13(+extra: Nat,+index: U32, s: S.State, 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) -> Array & S.State: 44 (a, w12) = pair 45 read14(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,at(a,U32.inc(index))) 46 47 def read12(+extra: Nat,+index: U32, s: S.State, 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) -> Array & S.State: 48 (a, w11) = pair 49 read13(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,at(a,U32.inc(index))) 50 51 def read11(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, pair: Array & U32) -> Array & S.State: 52 (a, w10) = pair 53 read12(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,at(a,U32.inc(index))) 54 55 def read10(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, pair: Array & U32) -> Array & S.State: 56 (a, w9) = pair 57 read11(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,at(a,U32.inc(index))) 58 59 def read9(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, pair: Array & U32) -> Array & S.State: 60 (a, w8) = pair 61 read10(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,w8,at(a,U32.inc(index))) 62 63 def read8(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, pair: Array & U32) -> Array & S.State: 64 (a, w7) = pair 65 read9(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,at(a,U32.inc(index))) 66 67 def read7(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, pair: Array & U32) -> Array & S.State: 68 (a, w6) = pair 69 read8(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,at(a,U32.inc(index))) 70 71 def read6(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, pair: Array & U32) -> Array & S.State: 72 (a, w5) = pair 73 read7(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,at(a,U32.inc(index))) 74 75 def read5(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, pair: Array & U32) -> Array & S.State: 76 (a, w4) = pair 77 read6(extra,U32.inc(index),s,w0,w1,w2,w3,w4,at(a,U32.inc(index))) 78 79 def read4(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, pair: Array & U32) -> Array & S.State: 80 (a, w3) = pair 81 read5(extra,U32.inc(index),s,w0,w1,w2,w3,at(a,U32.inc(index))) 82 83 def read3(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, pair: Array & U32) -> Array & S.State: 84 (a, w2) = pair 85 read4(extra,U32.inc(index),s,w0,w1,w2,at(a,U32.inc(index))) 86 87 def read2(+extra: Nat,+index: U32, s: S.State, w0: U32, pair: Array & U32) -> Array & S.State: 88 (a, w1) = pair 89 read3(extra,U32.inc(index),s,w0,w1,at(a,U32.inc(index))) 90 91 def read1(+extra: Nat,+index: U32, s: S.State, pair: Array & U32) -> Array & S.State: 92 (a, w0) = pair 93 read2(extra,U32.inc(index),s,w0,at(a,U32.inc(index))) 94 95 def pad16(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, 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) -> Array & S.State: 96 (a, w15) = pair 97 (a,Core.fips_compress16(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),length_word(Nat.is_lt(remain,56n),pad_word(w14,56n,remain),Core.len_hi(total)),length_word(Nat.is_lt(remain,56n),pad_word(w15,60n,remain),Core.len_lo(total)),extra,s)) 98 99 def pad15(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, 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) -> Array & S.State: 100 (a, w14) = pair 101 pad16(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,at(a,U32.inc(index))) 102 103 def pad14(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, 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) -> Array & S.State: 104 (a, w13) = pair 105 pad15(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,at(a,U32.inc(index))) 106 107 def pad13(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, 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) -> Array & S.State: 108 (a, w12) = pair 109 pad14(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,at(a,U32.inc(index))) 110 111 def pad12(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, 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) -> Array & S.State: 112 (a, w11) = pair 113 pad13(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,at(a,U32.inc(index))) 114 115 def pad11(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, pair: Array & U32) -> Array & S.State: 116 (a, w10) = pair 117 pad12(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,at(a,U32.inc(index))) 118 119 def pad10(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, pair: Array & U32) -> Array & S.State: 120 (a, w9) = pair 121 pad11(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,at(a,U32.inc(index))) 122 123 def pad9(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, pair: Array & U32) -> Array & S.State: 124 (a, w8) = pair 125 pad10(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,w8,at(a,U32.inc(index))) 126 127 def pad8(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, pair: Array & U32) -> Array & S.State: 128 (a, w7) = pair 129 pad9(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,at(a,U32.inc(index))) 130 131 def pad7(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, pair: Array & U32) -> Array & S.State: 132 (a, w6) = pair 133 pad8(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,at(a,U32.inc(index))) 134 135 def pad6(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, pair: Array & U32) -> Array & S.State: 136 (a, w5) = pair 137 pad7(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,at(a,U32.inc(index))) 138 139 def pad5(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, pair: Array & U32) -> Array & S.State: 140 (a, w4) = pair 141 pad6(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,at(a,U32.inc(index))) 142 143 def pad4(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, pair: Array & U32) -> Array & S.State: 144 (a, w3) = pair 145 pad5(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,at(a,U32.inc(index))) 146 147 def pad3(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, pair: Array & U32) -> Array & S.State: 148 (a, w2) = pair 149 pad4(extra,U32.inc(index),s,remain,total,w0,w1,w2,at(a,U32.inc(index))) 150 151 def pad2(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, pair: Array & U32) -> Array & S.State: 152 (a, w1) = pair 153 pad3(extra,U32.inc(index),s,remain,total,w0,w1,at(a,U32.inc(index))) 154 155 def pad1(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, pair: Array & U32) -> Array & S.State: 156 (a, w0) = pair 157 pad2(extra,U32.inc(index),s,remain,total,w0,at(a,U32.inc(index))) 158 159 def final_extra(+extra: Nat,more: Bool, +total: Nat, pair: Array & S.State) -> Array & S.State: 160 match more pair: 161 case False{} Tuple{a,s}: (a,s) 162 case True{} Tuple{a,s}: 163 (a,Core.fips_compress16(0,0,0,0,0,0,0,0,0,0,0,0,0,0,Core.len_hi(total),Core.len_lo(total),extra,s)) 164 165 def blocks(+extra: Nat,n: Nat, +index: U32, +remain: Nat, +total: Nat, pair: Array & S.State) -> Array & S.State: 166 match n pair: 167 case 0n Tuple{a,s}: 168 final_extra(extra,Nat.is_ge(remain,56n),total,pad1(extra,index,s,remain,total,at(a,index))) 169 case 1n+p Tuple{a,s}: 170 blocks(extra,p,U32.add(index,16),remain,total,read1(extra,index,s,at(a,index))) 171 172 def take_state(pair: Array & S.State) -> S.State: 173 Pair.snd(Array,S.State,pair) 174 175 # Internal entry; callers must establish length <= 4*array capacity. 176 def hash_unchecked(a: Array, +length: Nat) -> S.State: 177 take_state(blocks(48n,Nat.div(length,64n),0,Nat.mod(length,64n),length,(a,Core.initial()))) 178 179 def checked(valid: Bool, a: Array, length: Nat) -> Maybe<&2,S.State>: 180 match valid: 181 case False{}: None{} 182 case True{}: Some{hash_unchecked(a,length)} 183 184 def sized(+length: Nat, pair: Array & U32) -> Maybe<&2,S.State>: 185 (a,capacity) = pair 186 checked(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length) 187 188 # Public bounded API; consumes the input array, without constructing a byte list. 189 def hash(a: Array, length: Nat) -> Maybe<&2,S.State>: 190 sized(length,Array.size(U32,a))