1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/crypto/curve25519/field.bend as FS 4 import ../../../src/crypto/curve25519/field.bend as F 5 import ../../lib/nat.bend as N 6 import ../../lib/logic.bend as L 7 import ../../lib/u32div.bend as UD 8 import ../../lib/word.bend as WD 9 import ../../lib/arith.bend as AR 10 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 11 import ../../math/natural/arith.bend as NR 12 import ../../math/u64/u64div.bend as PD 13 import ./num.bend as M 14 15 # Limb lists: their value (FS.value, radix 2^8), shapes and bounds, the U32 16 # steps of the field code, and the carry pass (src/crypto/curve25519/field.bend 17 # `carry`): value(limbs) + 2^(8 n) carry_out == value(xs) + carry_in, every 18 # limb below 2^8, and every U32 sum below 2^32 (no wrap; the invariants of 19 # Fiat-Crypto's carry chains, Erbsen et al. 2019, and of HACL*'s 20 # Hacl.Spec.Curve25519.Field51 carry_wide). 21 22 def v(+x: U32) -> Nat: 23 U32.to_nat(x) 24 25 # 2^(8 len(xs)) x 26 def sh(xs: List<&2, U32>, +x: Nat) -> Nat: 27 match xs: 28 case Nil{}: 29 x 30 case Con{h, t}: 31 C.shift(8n, sh(t, x)) 32 33 # 2^(8 n) x 34 def shn(n: Nat, +x: Nat) -> Nat: 35 match n: 36 case 0n: 37 x 38 case 1n+m: 39 C.shift(8n, shn(m, x)) 40 41 # exactly n limbs, each at most b 42 def okb(n: Nat, xs: List<&2, U32>, +b: Nat) -> Bool: 43 match n: 44 case 0n: 45 match xs: 46 case Nil{}: 47 True{} 48 case Con{x, xt}: 49 False{} 50 case 1n+m: 51 match xs: 52 case Nil{}: 53 False{} 54 case Con{x, xt}: 55 Bool.and(Nat.is_le(U32.to_nat(x), b), okb(m, xt, b)) 56 57 # every limb at most b 58 def lea(xs: List<&2, U32>, +b: Nat) -> Bool: 59 match xs: 60 case Nil{}: 61 True{} 62 case Con{x, xt}: 63 Bool.and(Nat.is_le(U32.to_nat(x), b), lea(xt, b)) 64 65 def cl(r: F.Cr) -> List<&2, U32>: 66 F.cr_limbs(r) 67 68 def cc(r: F.Cr) -> U32: 69 F.cr_out(r) 70 71 # ---- shapes ---- 72 73 def okb_head(+n: Nat, +h: U32, +t: List<&2, U32>, +b: Nat, +e: {okb(1n+n, Con{h, t}, b) == True{} : Bool}) -> {Nat.is_le(v(h), b) == True{} : Bool}: 74 L.and_left(Nat.is_le(v(h), b), okb(n, t, b), e) 75 76 def okb_tail(+n: Nat, +h: U32, +t: List<&2, U32>, +b: Nat, +e: {okb(1n+n, Con{h, t}, b) == True{} : Bool}) -> {okb(n, t, b) == True{} : Bool}: 77 L.and_right(Nat.is_le(v(h), b), okb(n, t, b), e) 78 79 def okb_lea(+n: Nat, +xs: List<&2, U32>, +b: Nat, +e: {okb(n, xs, b) == True{} : Bool}) -> {lea(xs, b) == True{} : Bool}: 80 match n xs: 81 case 0n Nil{}: 82 {==} 83 case 0n Con{x, xt}: 84 Empty.absurd({lea(Con{x, xt}, b) == True{} : Bool}, L.false_true(e)) 85 case 1n+m Nil{}: 86 Empty.absurd({lea(Nil{}, b) == True{} : Bool}, L.false_true(e)) 87 case 1n+ +m Con{+x, +xt}: 88 L.and_intro(Nat.is_le(v(x), b), lea(xt, b), okb_head(m, x, xt, b, e), okb_lea(m, xt, b, okb_tail(m, x, xt, b, e))) 89 90 def lea_head(+h: U32, +t: List<&2, U32>, +b: Nat, +e: {lea(Con{h, t}, b) == True{} : Bool}) -> {Nat.is_le(v(h), b) == True{} : Bool}: 91 L.and_left(Nat.is_le(v(h), b), lea(t, b), e) 92 93 def lea_tail(+h: U32, +t: List<&2, U32>, +b: Nat, +e: {lea(Con{h, t}, b) == True{} : Bool}) -> {lea(t, b) == True{} : Bool}: 94 L.and_right(Nat.is_le(v(h), b), lea(t, b), e) 95 96 # a weaker bound 97 def lea_mono(+xs: List<&2, U32>, +b: Nat, +c: Nat, +hb: {Nat.is_le(b, c) == True{} : Bool}, +e: {lea(xs, b) == True{} : Bool}) -> {lea(xs, c) == True{} : Bool}: 98 match xs: 99 case Nil{}: 100 {==} 101 case Con{+x, +xt}: 102 L.and_intro(Nat.is_le(v(x), c), lea(xt, c), N.le_trans(v(x), b, c, lea_head(x, xt, b, e), hb), lea_mono(xt, b, c, hb, lea_tail(x, xt, b, e))) 103 104 def sh_okb(+n: Nat, +xs: List<&2, U32>, +b: Nat, +x: Nat, +e: {okb(n, xs, b) == True{} : Bool}) -> {sh(xs, x) == shn(n, x) : Nat}: 105 match n xs: 106 case 0n Nil{}: 107 {==} 108 case 0n Con{y, yt}: 109 Empty.absurd({sh(Con{y, yt}, x) == x : Nat}, L.false_true(e)) 110 case 1n+m Nil{}: 111 Empty.absurd({x == shn(1n+m, x) : Nat}, L.false_true(e)) 112 case 1n+ +m Con{+y, +yt}: 113 Equal.cong(Nat, Nat, z => C.shift(8n, z), sh(yt, x), shn(m, x), sh_okb(m, yt, b, x, okb_tail(m, y, yt, b, e))) 114 115 # the spec's tight (bytes_ok 32: limbs below 256) is okb 32 with bound 255 116 def bytes_okb(+n: Nat, +xs: List<&2, U32>, +e: {FS.bytes_ok(n, xs) == True{} : Bool}) -> {okb(n, xs, 255n) == True{} : Bool}: 117 match n xs: 118 case 0n Nil{}: 119 {==} 120 case 0n Con{y, yt}: 121 Empty.absurd({okb(0n, Con{y, yt}, 255n) == True{} : Bool}, L.false_true(e)) 122 case 1n+m Nil{}: 123 Empty.absurd({okb(1n+m, Nil{}, 255n) == True{} : Bool}, L.false_true(e)) 124 case 1n+ +m Con{+y, +yt}: 125 +h = L.and_left(Nat.is_lt(v(y), 256n), FS.bytes_ok(m, yt), e) 126 +t = L.and_right(Nat.is_lt(v(y), 256n), FS.bytes_ok(m, yt), e) 127 L.and_intro(Nat.is_le(v(y), 255n), okb(m, yt, 255n), N.lt_succ_le(v(y), 255n, h), bytes_okb(m, yt, t)) 128 129 def okb_bytes(+n: Nat, +xs: List<&2, U32>, +e: {okb(n, xs, 255n) == True{} : Bool}) -> {FS.bytes_ok(n, xs) == True{} : Bool}: 130 match n xs: 131 case 0n Nil{}: 132 {==} 133 case 0n Con{y, yt}: 134 Empty.absurd({FS.bytes_ok(0n, Con{y, yt}) == True{} : Bool}, L.false_true(e)) 135 case 1n+m Nil{}: 136 Empty.absurd({FS.bytes_ok(1n+m, Nil{}) == True{} : Bool}, L.false_true(e)) 137 case 1n+ +m Con{+y, +yt}: 138 L.and_intro(Nat.is_lt(v(y), 256n), FS.bytes_ok(m, yt), N.le_lt_succ(v(y), 255n, okb_head(m, y, yt, 255n, e)), okb_bytes(m, yt, okb_tail(m, y, yt, 255n, e))) 139 140 # ---- constants ---- 141 142 def k256(+one: Nat, +h1: {one == 1n : Nat}) -> {256n == WD.sc(8n, one) : Nat}: 143 L.subst(Nat, o => {256n == WD.sc(8n, o) : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==}) 144 145 def sc_pos1(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(0n, WD.sc(k, one)) == True{} : Bool}: 146 L.subst(Nat, o => {Nat.is_lt(0n, WD.sc(k, o)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), WD.sc_pos(k)) 147 148 # 2^k < 2^(k+1) 149 def sc_lt_succ(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(WD.sc(k, one), WD.sc(1n+k, one)) == True{} : Bool}: 150 +x = WD.sc(k, one) 151 +a = N.lt_add_left(0n, x, x, sc_pos1(k, one, h1)) 152 %N.add_zero(x) : {Nat.is_lt(_, WD.sc(1n+k, one)) == True{} : Bool} 153 %M.sc_dbl(k, one) : {Nat.is_lt(Nat.add(x, 0n), _) == True{} : Bool} 154 a 155 156 # 2^a < 2^(d + 1 + a) 157 def sc_lt(+d: Nat, +a: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(WD.sc(a, one), WD.sc(Nat.add(d, 1n+a), one)) == True{} : Bool}: 158 N.lt_le_trans(WD.sc(a, one), WD.sc(1n+a, one), WD.sc(Nat.add(d, 1n+a), one), sc_lt_succ(a, one, h1), M.sc_mono(d, 1n+a, one)) 159 160 # ---- U32 steps ---- 161 162 def add_v(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32, +h: {Nat.is_lt(Nat.add(v(x), v(y)), WD.sc(32n, one)) == True{} : Bool}) -> {v(U32.add(x, y)) == Nat.add(v(x), v(y)) : Nat}: 163 PD.add32(one, h1, x, y, h) 164 165 def mul_v(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32, +h: {Nat.is_lt(Nat.mul(v(x), v(y)), WD.sc(32n, one)) == True{} : Bool}) -> {v(U32.mul(x, y)) == Nat.mul(v(x), v(y)) : Nat}: 166 PD.mul32(one, h1, x, y, h) 167 168 def mod256(+x: U32) -> {v(U32.mod(x, 256)) == Nat.mod(v(x), 256n) : Nat}: 169 UD.mod_nat(x, 256, {==}) 170 171 def div256(+x: U32) -> {v(U32.div(x, 256)) == Nat.div(v(x), 256n) : Nat}: 172 UD.div_nat(x, 256, {==}) 173 174 def m256(+x: Nat) -> {Nat.mul(x, 256n) == C.shift(8n, x) : Nat}: 175 PD.mul_pow(1n, {==}, 8n, x, 256n, {==}) 176 177 # n == (n mod 256) + 2^8 (n div 256) 178 def dm256(+n: Nat) -> {Nat.add(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n))) == n : Nat}: 179 +e = Equal.sym(Nat, n, Nat.add(Nat.mul(Nat.div(n, 256n), 256n), Nat.mod(n, 256n)), NR.dm_eq(255n, n)) 180 +e2 = Equal.trans(Nat, Nat.add(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n))), Nat.add(Nat.mod(n, 256n), Nat.mul(Nat.div(n, 256n), 256n)), Nat.add(Nat.mul(Nat.div(n, 256n), 256n), Nat.mod(n, 256n)), M.cong_r(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n)), Nat.mul(Nat.div(n, 256n), 256n), Equal.sym(Nat, Nat.mul(Nat.div(n, 256n), 256n), C.shift(8n, Nat.div(n, 256n)), m256(Nat.div(n, 256n)))), NA.add_comm(Nat.mod(n, 256n), Nat.mul(Nat.div(n, 256n), 256n))) 181 Equal.trans(Nat, Nat.add(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n))), Nat.add(Nat.mul(Nat.div(n, 256n), 256n), Nat.mod(n, 256n)), n, e2, e) 182 183 # a U32 split into its low byte and the rest 184 def split_v(+s: U32) -> {Nat.add(v(U32.mod(s, 256)), C.shift(8n, v(U32.div(s, 256)))) == v(s) : Nat}: 185 %Equal.sym(Nat, v(U32.mod(s, 256)), Nat.mod(v(s), 256n), mod256(s)) : {Nat.add(_, C.shift(8n, v(U32.div(s, 256)))) == v(s) : Nat} 186 %Equal.sym(Nat, v(U32.div(s, 256)), Nat.div(v(s), 256n), div256(s)) : {Nat.add(Nat.mod(v(s), 256n), C.shift(8n, _)) == v(s) : Nat} 187 dm256(v(s)) 188 189 def lo_le(+s: U32) -> {Nat.is_le(v(U32.mod(s, 256)), 255n) == True{} : Bool}: 190 %Equal.sym(Nat, v(U32.mod(s, 256)), Nat.mod(v(s), 256n), mod256(s)) : {Nat.is_le(_, 255n) == True{} : Bool} 191 N.lt_succ_le(Nat.mod(v(s), 256n), 255n, NR.dm_lt(255n, v(s))) 192 193 # (s div 256) < 2^k when s < 2^(k + 8) 194 def hi_lt(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +s: U32, +h: {Nat.is_lt(v(s), WD.sc(Nat.add(k, 8n), one)) == True{} : Bool}) -> {Nat.is_lt(v(U32.div(s, 256)), WD.sc(k, one)) == True{} : Bool}: 195 %Equal.sym(Nat, v(U32.div(s, 256)), Nat.div(v(s), 256n), div256(s)) : {Nat.is_lt(_, WD.sc(k, one)) == True{} : Bool} 196 +n = v(s) 197 +q = Nat.div(n, 256n) 198 +r = Nat.mod(n, 256n) 199 +e = NR.dm_eq(255n, n) 200 +h2 = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(Nat.add(k, 8n), one)) == True{} : Bool}, n, Nat.add(Nat.mul(q, 256n), r), e, h) 201 +h3 = L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.mul(q, 256n), r), z) == True{} : Bool}, WD.sc(Nat.add(k, 8n), one), WD.sc(k, WD.sc(8n, one)), AR.sc_idx(k, 8n, one), h2) 202 +h4 = L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.mul(q, 256n), r), WD.sc(k, z)) == True{} : Bool}, WD.sc(8n, one), 256n, Equal.sym(Nat, 256n, WD.sc(8n, one), k256(one, h1)), h3) 203 AR.quot_lt(k, one, h1, q, 256n, r, h4) 204 205 # ---- the carry pass ---- 206 207 def cl_con(+l: U32, +r: F.Cr) -> {cl(F.carry_con(l, r)) == Con{l, cl(r)} : List<&2, U32>}: 208 match r: 209 case F.Cr{a, c}: 210 {==} 211 212 def cc_con(+l: U32, +r: F.Cr) -> {cc(F.carry_con(l, r)) == cc(r) : U32}: 213 match r: 214 case F.Cr{a, c}: 215 {==} 216 217 # carry-in at most 2^21 and a limb at most 2^28: their sum is below 2^29 218 def s_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +c: U32, +hx: {Nat.is_le(v(x), WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(v(x), v(c)), WD.sc(29n, one)) == True{} : Bool}: 219 +c28 = N.lt_le(v(c), WD.sc(28n, one), N.le_lt_trans(v(c), WD.sc(21n, one), WD.sc(28n, one), hc, sc_lt(6n, 21n, one, h1))) 220 +lt = N.le_lt_trans(Nat.add(v(x), v(c)), Nat.add(WD.sc(28n, one), WD.sc(21n, one)), Nat.add(WD.sc(28n, one), WD.sc(28n, one)), M.le_add2(v(x), v(c), WD.sc(28n, one), WD.sc(21n, one), hx, hc), N.lt_add_left(WD.sc(21n, one), WD.sc(28n, one), WD.sc(28n, one), sc_lt(6n, 21n, one, h1))) 221 %M.sc_dbl(28n, one) : {Nat.is_lt(Nat.add(v(x), v(c)), _) == True{} : Bool} 222 lt 223 224 def s_v(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +c: U32, +hx: {Nat.is_le(v(x), WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {v(U32.add(x, c)) == Nat.add(v(x), v(c)) : Nat}: 225 add_v(one, h1, x, c, N.lt_trans(Nat.add(v(x), v(c)), WD.sc(29n, one), WD.sc(32n, one), s_lt(one, h1, x, c, hx, hc), sc_lt(2n, 29n, one, h1))) 226 227 def c_next(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +c: U32, +hx: {Nat.is_le(v(x), WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {Nat.is_le(v(U32.div(U32.add(x, c), 256)), WD.sc(21n, one)) == True{} : Bool}: 228 +s = U32.add(x, c) 229 +hs = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(29n, one)) == True{} : Bool}, Nat.add(v(x), v(c)), v(s), Equal.sym(Nat, v(s), Nat.add(v(x), v(c)), s_v(one, h1, x, c, hx, hc)), s_lt(one, h1, x, c, hx, hc)) 230 N.lt_le(v(U32.div(s, 256)), WD.sc(21n, one), hi_lt(21n, one, h1, s, hs)) 231 232 # value(limbs) + 2^(8 n) carry_out == value(xs) + carry_in 233 def carry_val(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +c: U32, +hx: {lea(xs, WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {Nat.add(FS.value(cl(F.carry(xs, c))), sh(xs, v(cc(F.carry(xs, c))))) == Nat.add(FS.value(xs), v(c)) : Nat}: 234 match xs: 235 case Nil{}: 236 {==} 237 case Con{+h, +t}: 238 +hh = lea_head(h, t, WD.sc(28n, one), hx) 239 +ht = lea_tail(h, t, WD.sc(28n, one), hx) 240 +s = U32.add(h, c) 241 +lo = U32.mod(s, 256) 242 +hi = U32.div(s, 256) 243 +r = F.carry(t, hi) 244 +ih = carry_val(one, h1, t, hi, ht, c_next(one, h1, h, c, hh, hc)) 245 %Equal.sym(List<&2, U32>, cl(F.carry_con(lo, r)), Con{lo, cl(r)}, cl_con(lo, r)) : {Nat.add(FS.value(_), C.shift(8n, sh(t, v(cc(F.carry_con(lo, r)))))) == Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)) : Nat} 246 %Equal.sym(U32, cc(F.carry_con(lo, r)), cc(r), cc_con(lo, r)) : {Nat.add(FS.value(Con{lo, cl(r)}), C.shift(8n, sh(t, v(_)))) == Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)) : Nat} 247 +A = FS.value(cl(r)) 248 +B = sh(t, v(cc(r))) 249 +e1 = Equal.trans(Nat, Nat.add(Nat.add(v(lo), C.shift(8n, A)), C.shift(8n, B)), Nat.add(v(lo), Nat.add(C.shift(8n, A), C.shift(8n, B))), Nat.add(v(lo), C.shift(8n, Nat.add(A, B))), NA.add_assoc(v(lo), C.shift(8n, A), C.shift(8n, B)), M.cong_r(v(lo), Nat.add(C.shift(8n, A), C.shift(8n, B)), C.shift(8n, Nat.add(A, B)), M.sc_add(8n, A, B))) 250 +e2 = M.cong_r(v(lo), C.shift(8n, Nat.add(A, B)), C.shift(8n, Nat.add(FS.value(t), v(hi))), M.cong_sc(8n, Nat.add(A, B), Nat.add(FS.value(t), v(hi)), ih)) 251 +e3 = Equal.trans(Nat, Nat.add(v(lo), C.shift(8n, Nat.add(FS.value(t), v(hi)))), Nat.add(v(lo), Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi)))), Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), M.cong_r(v(lo), C.shift(8n, Nat.add(FS.value(t), v(hi))), Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi))), Equal.sym(Nat, Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi))), C.shift(8n, Nat.add(FS.value(t), v(hi))), M.sc_add(8n, FS.value(t), v(hi)))), 252 Equal.trans(Nat, Nat.add(v(lo), Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi)))), Nat.add(v(lo), Nat.add(C.shift(8n, v(hi)), C.shift(8n, FS.value(t)))), Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), M.cong_r(v(lo), Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi))), Nat.add(C.shift(8n, v(hi)), C.shift(8n, FS.value(t))), NA.add_comm(C.shift(8n, FS.value(t)), C.shift(8n, v(hi)))), Equal.sym(Nat, Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), Nat.add(v(lo), Nat.add(C.shift(8n, v(hi)), C.shift(8n, FS.value(t)))), NA.add_assoc(v(lo), C.shift(8n, v(hi)), C.shift(8n, FS.value(t)))))) 253 +e4 = M.cong_l(Nat.add(v(lo), C.shift(8n, v(hi))), v(s), C.shift(8n, FS.value(t)), split_v(s)) 254 +e5 = M.cong_l(v(s), Nat.add(v(h), v(c)), C.shift(8n, FS.value(t)), s_v(one, h1, h, c, hh, hc)) 255 +e6 = Equal.trans(Nat, Nat.add(Nat.add(v(h), v(c)), C.shift(8n, FS.value(t))), Nat.add(v(h), Nat.add(v(c), C.shift(8n, FS.value(t)))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), NA.add_assoc(v(h), v(c), C.shift(8n, FS.value(t))), 256 Equal.trans(Nat, Nat.add(v(h), Nat.add(v(c), C.shift(8n, FS.value(t)))), Nat.add(v(h), Nat.add(C.shift(8n, FS.value(t)), v(c))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), M.cong_r(v(h), Nat.add(v(c), C.shift(8n, FS.value(t))), Nat.add(C.shift(8n, FS.value(t)), v(c)), NA.add_comm(v(c), C.shift(8n, FS.value(t)))), Equal.sym(Nat, Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), Nat.add(v(h), Nat.add(C.shift(8n, FS.value(t)), v(c))), NA.add_assoc(v(h), C.shift(8n, FS.value(t)), v(c))))) 257 Equal.trans(Nat, Nat.add(Nat.add(v(lo), C.shift(8n, A)), C.shift(8n, B)), Nat.add(v(lo), C.shift(8n, Nat.add(A, B))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e1, 258 Equal.trans(Nat, Nat.add(v(lo), C.shift(8n, Nat.add(A, B))), Nat.add(v(lo), C.shift(8n, Nat.add(FS.value(t), v(hi)))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e2, 259 Equal.trans(Nat, Nat.add(v(lo), C.shift(8n, Nat.add(FS.value(t), v(hi)))), Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e3, 260 Equal.trans(Nat, Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), Nat.add(v(s), C.shift(8n, FS.value(t))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e4, 261 Equal.trans(Nat, Nat.add(v(s), C.shift(8n, FS.value(t))), Nat.add(Nat.add(v(h), v(c)), C.shift(8n, FS.value(t))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e5, e6))))) 262 263 # every output limb below 2^8, the same count 264 def carry_ok(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +xs: List<&2, U32>, +c: U32, +hn: {okb(n, xs, WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {okb(n, cl(F.carry(xs, c)), 255n) == True{} : Bool}: 265 match n xs: 266 case 0n Nil{}: 267 {==} 268 case 0n Con{y, yt}: 269 Empty.absurd({okb(0n, cl(F.carry(Con{y, yt}, c)), 255n) == True{} : Bool}, L.false_true(hn)) 270 case 1n+m Nil{}: 271 Empty.absurd({okb(1n+m, cl(F.carry(Nil{}, c)), 255n) == True{} : Bool}, L.false_true(hn)) 272 case 1n+ +m Con{+h, +t}: 273 +hh = okb_head(m, h, t, WD.sc(28n, one), hn) 274 +ht = okb_tail(m, h, t, WD.sc(28n, one), hn) 275 +s = U32.add(h, c) 276 +lo = U32.mod(s, 256) 277 +r = F.carry(t, U32.div(s, 256)) 278 %Equal.sym(List<&2, U32>, cl(F.carry_con(lo, r)), Con{lo, cl(r)}, cl_con(lo, r)) : {okb(1n+m, _, 255n) == True{} : Bool} 279 L.and_intro(Nat.is_le(v(lo), 255n), okb(m, cl(r), 255n), lo_le(s), carry_ok(one, h1, m, t, U32.div(s, 256), ht, c_next(one, h1, h, c, hh, hc))) 280 281 # the carry out is at most 2^21 282 def carry_cb(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +c: U32, +hx: {lea(xs, WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {Nat.is_le(v(cc(F.carry(xs, c))), WD.sc(21n, one)) == True{} : Bool}: 283 match xs: 284 case Nil{}: 285 hc 286 case Con{+h, +t}: 287 +hh = lea_head(h, t, WD.sc(28n, one), hx) 288 +ht = lea_tail(h, t, WD.sc(28n, one), hx) 289 +s = U32.add(h, c) 290 +lo = U32.mod(s, 256) 291 +r = F.carry(t, U32.div(s, 256)) 292 %Equal.sym(U32, cc(F.carry_con(lo, r)), cc(r), cc_con(lo, r)) : {Nat.is_le(v(_), WD.sc(21n, one)) == True{} : Bool} 293 carry_cb(one, h1, t, U32.div(s, 256), ht, c_next(one, h1, h, c, hh, hc))