1 import Base 2 3 # Arithmetic modulo m = 2^256 - c on little-endian lists of natural-number 4 # limbs in radix 2^16 (secp256k1's p and n are both of this form, with 5 # c = 2^32 + 977 and c < 2^129). A list [l0, l1, ...] stands for 6 # l0 + 2^16 l1 + 2^32 l2 + ... ; a reduced element is 16 limbs, each below 7 # 2^16, with value below m. 8 # 9 # Bend's native runtime holds a Nat in one machine word and checks it stays 10 # below 2^48 (it aborts otherwise, it never wraps). The products of two 11 # limbs are below 2^32, a column of the schoolbook product below 2^36, and 12 # every other intermediate below 2^40, so no operation here comes near the 13 # bound (proofs/crypto/secp256k1/ proves the values; the bounds are shown in 14 # docs/CRYPTO_CONTRACTS.md). 15 # 16 # Only the constants 2, 255 and 256 appear: a 16-bit limb is split into two 17 # bytes with div/mod 256 (which compile to shifts and masks), so the proof 18 # checker, which keeps natural numbers in unary, never meets 2^16 as a 19 # literal. 20 # 21 # The reduction follows the folding reductions of libsecp256k1 22 # (secp256k1_fe_mul_inner, secp256k1_scalar_reduce_512) and of Fiat-Crypto's 23 # "solinas" reduction: with 2^256 = m + c, the high part hi of 24 # x = lo + 2^256 hi is folded as x == lo + c hi (mod m); a fixed number of 25 # folds (3 for p, 4 for n) brings any product of two reduced elements below 26 # 2^256, and one conditional subtraction of m (computed branch-free as 27 # "add c and look at bit 256") gives the representative below m. 28 # 29 # No function branches on a limb value: selection is arithmetic 30 # (b * x + (1 - b) * y with b in {0, 1}), every list has a fixed length, 31 # and loops run over public counts. Bend has no timing model, so this is a 32 # property of the code's shape, not a proved fact. 33 34 # ---- 16-bit limbs from bytes ---- 35 36 # s mod 2^16 and s div 2^16 37 def lo16(+s: Nat) -> Nat: 38 Nat.add(Nat.mod(s, 256n), Nat.mul(Nat.mod(Nat.div(s, 256n), 256n), 256n)) 39 40 def hi16(+s: Nat) -> Nat: 41 Nat.div(Nat.div(s, 256n), 256n) 42 43 # 2^16 - 1 - x for x below 2^16 44 def comp1(+x: Nat) -> Nat: 45 Nat.add(Nat.sub(255n, Nat.mod(x, 256n)), Nat.mul(Nat.sub(255n, Nat.div(x, 256n)), 256n)) 46 47 # ---- limb lists ---- 48 49 def hd0(xs: List<&2, Nat>) -> Nat: 50 match xs: 51 case Nil{}: 0n 52 case x <> t: x 53 54 def tl(xs: List<&2, Nat>) -> List<&2, Nat>: 55 match xs: 56 case Nil{}: Nil{} 57 case x <> t: t 58 59 # limb-wise sum; the longer tail is kept 60 def add(xs: List<&2, Nat>, ys: List<&2, Nat>) -> List<&2, Nat>: 61 match xs ys: 62 case Nil{} _: ys 63 case x <> xt Nil{}: x <> xt 64 case x <> xt y <> yt: Nat.add(x, y) <> add(xt, yt) 65 66 # every limb times a 67 def scal(+a: Nat, ys: List<&2, Nat>) -> List<&2, Nat>: 68 match ys: 69 case Nil{}: Nil{} 70 case y <> yt: Nat.mul(y, a) <> scal(a, yt) 71 72 # the schoolbook product without carries: conv(x :: xs, ys) = x ys + 2^16 conv(xs, ys) 73 def conv(xs: List<&2, Nat>, +ys: List<&2, Nat>) -> List<&2, Nat>: 74 match xs: 75 case Nil{}: Nil{} 76 case x <> xt: add(scal(x, ys), 0n <> conv(xt, ys)) 77 78 def take(n: Nat, xs: List<&2, Nat>) -> List<&2, Nat>: 79 match n xs: 80 case 0n _: Nil{} 81 case 1n+k Nil{}: Nil{} 82 case 1n+k x <> t: x <> take(k, t) 83 84 def drop(n: Nat, xs: List<&2, Nat>) -> List<&2, Nat>: 85 match n xs: 86 case 0n _: xs 87 case 1n+k Nil{}: Nil{} 88 case 1n+k x <> t: drop(k, t) 89 90 # the value of the limbs (only ever of an empty list at run time: see carry) 91 def horner(xs: List<&2, Nat>) -> Nat: 92 match xs: 93 case Nil{}: 0n 94 case x <> t: Nat.add(Nat.mul(Nat.mul(horner(t), 256n), 256n), x) 95 96 # A carry pass: n limbs, each below 2^16, then one limb holding the carry u 97 # out of them plus the value of whatever is left of xs past n limbs (on 98 # every call below xs has at most n limbs, so that is the carry alone). 99 # Every function here looks at its list before producing anything, so that 100 # on a symbolic argument the proof checker stops at once. 101 def carry(n: Nat, xs: List<&2, Nat>, u: Nat) -> List<&2, Nat>: 102 match n xs: 103 case 0n Nil{}: [u] 104 case 0n x <> t: [Nat.add(u, horner(x <> t))] 105 case 1n+k Nil{}: 106 +s = Nat.add(u, 0n) 107 lo16(s) <> carry(k, Nil{}, hi16(s)) 108 case 1n+k x <> t: 109 +s = Nat.add(u, x) 110 lo16(s) <> carry(k, t, hi16(s)) 111 112 # every limb x becomes 2^16 - 1 - x 113 def comp(xs: List<&2, Nat>) -> List<&2, Nat>: 114 match xs: 115 case Nil{}: Nil{} 116 case x <> t: comp1(x) <> comp(t) 117 118 # b x + (1 - b) y, limb-wise, for b in {0, 1} 119 def pick1(+b: Nat, +x: Nat, +y: Nat) -> Nat: 120 Nat.add(Nat.mul(x, b), Nat.mul(y, Nat.sub(1n, b))) 121 122 def select(+b: Nat, xs: List<&2, Nat>, ys: List<&2, Nat>) -> List<&2, Nat>: 123 match xs ys: 124 case x <> xt y <> yt: pick1(b, x, y) <> select(b, xt, yt) 125 case _ _: Nil{} 126 127 # ---- reduction modulo m = 2^256 - c ---- 128 129 # the normalized form of a value below 2^256: exactly 16 limbs below 2^16 130 def norm16(xs: List<&2, Nat>) -> List<&2, Nat>: 131 take(16n, carry(32n, xs, 0n)) 132 133 # lo + c hi, for x = lo + 2^256 hi: congruent to x modulo m 134 def fold(+c: List<&2, Nat>, +xs: List<&2, Nat>) -> List<&2, Nat>: 135 add(take(16n, xs), conv(drop(16n, xs), c)) 136 137 def rounds(k: Nat, +c: List<&2, Nat>, xs: List<&2, Nat>) -> List<&2, Nat>: 138 match k: 139 case 0n: xs 140 case 1n+j: rounds(j, c, carry(32n, fold(c, xs), 0n)) 141 142 # the part of a carried value above 2^256 (0 or 1 below) 143 def top(xs: List<&2, Nat>) -> Nat: 144 horner(drop(16n, xs)) 145 146 # t (16 limbs, value below 2^256) mod m: t + c has bit 256 set exactly when 147 # t >= m, and then its low 256 bits are t - m 148 def canon(+c: List<&2, Nat>, +t: List<&2, Nat>) -> List<&2, Nat>: 149 +u = carry(32n, add(t, c), 0n) 150 select(top(u), take(16n, u), t) 151 152 def reduce_go(+c: List<&2, Nat>, k: Nat, xs: List<&2, Nat>) -> List<&2, Nat>: 153 canon(c, take(16n, rounds(k, c, carry(32n, xs, 0n)))) 154 155 # x mod m for x below 2^512, in k folds (x is looked at first, so that the 156 # proof checker keeps an unknown reduction folded) 157 def reduce(+c: List<&2, Nat>, k: Nat, xs: List<&2, Nat>) -> List<&2, Nat>: 158 match xs: 159 case Nil{}: reduce_go(c, k, Nil{}) 160 case x <> t: reduce_go(c, k, x <> t) 161 162 # ---- negation and comparison modulo m, from c ---- 163 164 # m - b = (2^256 - 1 - (b + c)) + 1, for b < m (so b + c < 2^256); no 165 # constant but c is ever formed 166 def neg_raw(+c: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>: 167 add(comp(norm16(add(b, c))), [1n]) 168 169 # x < m, i.e. x + c < 2^256, for x of 16 limbs below 2^16 170 def ltm(+c: List<&2, Nat>, x: List<&2, Nat>) -> Bool: 171 Nat.is_eq(top(carry(32n, add(x, c), 0n)), 0n) 172 173 # ---- comparisons and bits ---- 174 175 def b2n(b: Bool) -> Nat: 176 match b: 177 case True{}: 1n 178 case False{}: 0n 179 180 # 1 when the value of xs is below the value of ys plus br, else 0 (the 181 # borrow out of xs - ys - br), for lists of the same length 182 def borrow(xs: List<&2, Nat>, ys: List<&2, Nat>, br: Nat) -> Nat: 183 match xs ys: 184 case x <> xt y <> yt: borrow(xt, yt, b2n(Nat.is_lt(x, Nat.add(br, y)))) 185 case _ _: br 186 187 def lt(xs: List<&2, Nat>, ys: List<&2, Nat>) -> Bool: 188 Nat.is_eq(borrow(xs, ys, 0n), 1n) 189 190 # OR of all limbs being nonzero, without an early exit 191 def nonzero(xs: List<&2, Nat>, acc: Nat) -> Nat: 192 match xs: 193 case Nil{}: acc 194 case x <> t: nonzero(t, Nat.add(acc, x)) 195 196 def is_zero(xs: List<&2, Nat>) -> Bool: 197 Nat.is_eq(nonzero(xs, 0n), 0n) 198 199 def diff(xs: List<&2, Nat>, ys: List<&2, Nat>, acc: Nat) -> Nat: 200 match xs ys: 201 case +x <> xt +y <> yt: diff(xt, yt, Nat.add(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x)))) 202 case _ _: acc 203 204 def eq(xs: List<&2, Nat>, ys: List<&2, Nat>) -> Bool: 205 Nat.is_eq(diff(xs, ys, 0n), 0n) 206 207 # the k low bits of x, most significant first 208 def bits_of(k: Nat, +x: Nat) -> List<&2, Nat>: 209 match k: 210 case 0n: Nil{} 211 case 1n+j: List.append(&2, Nat, bits_of(j, Nat.div(x, 2n)), [Nat.mod(x, 2n)]) 212 213 # every bit flipped: the bits of 2^k - 1 - x from those of x 214 def cbits(bs: List<&2, Nat>) -> List<&2, Nat>: 215 match bs: 216 case Nil{}: Nil{} 217 case b <> t: Nat.sub(1n, b) <> cbits(t) 218 219 # all bits of a limb list, most significant first (16 per limb) 220 def bits(xs: List<&2, Nat>) -> List<&2, Nat>: 221 match xs: 222 case Nil{}: Nil{} 223 case x <> t: List.append(&2, Nat, bits(t), bits_of(16n, x))