proofs/crypto/secp256k1/bitsrel.bend

bend-collections-laws-crypto@1.0.0.0 · 131 lines · 12 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/bitsrel.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
10import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY
13
14# The bits of a scalar's limbs (src/crypto/secp256k1/limbs.bend bits) are
15# the specification's bits of its value, most significant first:
16# bits(k) = [bit(255, K), ..., bit(0, K)] (spec/crypto/secp256k1/curve.bend bit).
17
18# bits off + i - 1 down to off of K
19def sb(i: Nat, +off: Nat, +k: Nat) -> List<&2, Nat>:
20  match i:
21    case 0n: Nil{}
22    case 1n+ +j: CV.bit(Nat.add(off, j), k) <> sb(j, off, k)
23
24def app_nat(xs: List<&2, Nat>, +ys: List<&2, Nat>, +zs: List<&2, Nat>) -> {List.append(&2, Nat, List.append(&2, Nat, xs, ys), zs) == List.append(&2, Nat, xs, List.append(&2, Nat, ys, zs)) : List<&2, Nat>}:
25  match xs:
26    case Nil{}:
27      {==}
28    case +x <> +t:
29      Equal.cong(List<&2, Nat>, List<&2, Nat>, l => x <> l, List.append(&2, Nat, List.append(&2, Nat, t, ys), zs), List.append(&2, Nat, t, List.append(&2, Nat, ys, zs)), app_nat(t, ys, zs))
30
31def div2(x: Nat) -> {Nat.div(x, 2n) == C.half(x) : Nat}:
32  match x:
33    case 0n:
34      {==}
35    case 1n:
36      {==}
37    case 2n+ +q:
38      %Equal.sym(Nat, Nat.div(Nat.add(2n, q), 2n), 1n+Nat.div(q, 2n), N.div2_step(q)) : {_ == 1n+C.half(q) : Nat}
39      Equal.cong(Nat, Nat, z => 1n+z, Nat.div(q, 2n), C.half(q), div2(q))
40
41# offset 1 is offset 0 of the half
42def sb_one(j: Nat, +x: Nat) -> {sb(j, 1n, x) == sb(j, 0n, C.half(x)) : List<&2, Nat>}:
43  match j:
44    case 0n:
45      {==}
46    case 1n+ +i:
47      Equal.cong(List<&2, Nat>, List<&2, Nat>, l => CV.bit(i, C.half(x)) <> l, sb(i, 1n, x), sb(i, 0n, C.half(x)), sb_one(i, x))
48
49# the last bit comes off the end
50def sb_last(j: Nat, +x: Nat) -> {sb(1n+j, 0n, x) == List.append(&2, Nat, sb(j, 1n, x), [CV.bit(0n, x)]) : List<&2, Nat>}:
51  match j:
52    case 0n:
53      {==}
54    case 1n+ +i:
55      Equal.cong(List<&2, Nat>, List<&2, Nat>, l => CV.bit(1n+i, x) <> l, sb(1n+i, 0n, x), List.append(&2, Nat, sb(i, 1n, x), [CV.bit(0n, x)]), sb_last(i, x))
56
57def bits_of_sb(j: Nat, +x: Nat) -> {L.bits_of(j, x) == sb(j, 0n, x) : List<&2, Nat>}:
58  match j:
59    case 0n:
60      {==}
61    case 1n+ +i:
62      %Equal.sym(List<&2, Nat>, L.bits_of(i, Nat.div(x, 2n)), sb(i, 0n, Nat.div(x, 2n)), bits_of_sb(i, Nat.div(x, 2n))) : {List.append(&2, Nat, _, [Nat.mod(x, 2n)]) == sb(1n+i, 0n, x) : List<&2, Nat>}
63      %Equal.sym(Nat, Nat.div(x, 2n), C.half(x), div2(x)) : {List.append(&2, Nat, sb(i, 0n, _), [Nat.mod(x, 2n)]) == sb(1n+i, 0n, x) : List<&2, Nat>}
64      %Equal.sym(Nat, Nat.mod(x, 2n), C.bit(x), Equal.sym(Nat, C.bit(x), Nat.mod(x, 2n), WW.bit_mod(x))) : {List.append(&2, Nat, sb(i, 0n, C.half(x)), [_]) == sb(1n+i, 0n, x) : List<&2, Nat>}
65      %Equal.sym(List<&2, Nat>, sb(1n+i, 0n, x), List.append(&2, Nat, sb(i, 1n, x), [CV.bit(0n, x)]), sb_last(i, x)) : {List.append(&2, Nat, sb(i, 0n, C.half(x)), [C.bit(x)]) == _ : List<&2, Nat>}
66      %Equal.sym(List<&2, Nat>, sb(i, 1n, x), sb(i, 0n, C.half(x)), sb_one(i, x)) : {List.append(&2, Nat, sb(i, 0n, C.half(x)), [C.bit(x)]) == List.append(&2, Nat, _, [CV.bit(0n, x)]) : List<&2, Nat>}
67      {==}
68
69# sb(a + b, 0) = sb(a, b) ++ sb(b, 0)
70def sb_split(a: Nat, +b: Nat, +k: Nat) -> {sb(Nat.add(a, b), 0n, k) == List.append(&2, Nat, sb(a, b, k), sb(b, 0n, k)) : List<&2, Nat>}:
71  match a:
72    case 0n:
73      {==}
74    case 1n+ +i:
75      %Equal.sym(List<&2, Nat>, sb(Nat.add(i, b), 0n, k), List.append(&2, Nat, sb(i, b, k), sb(b, 0n, k)), sb_split(i, b, k)) : {CV.bit(Nat.add(i, b), k) <> _ == CV.bit(Nat.add(b, i), k) <> List.append(&2, Nat, sb(i, b, k), sb(b, 0n, k)) : List<&2, Nat>}
76      %Equal.sym(Nat, Nat.add(i, b), Nat.add(b, i), NA.add_comm(i, b)) : {CV.bit(_, k) <> List.append(&2, Nat, sb(i, b, k), sb(b, 0n, k)) == CV.bit(Nat.add(b, i), k) <> List.append(&2, Nat, sb(i, b, k), sb(b, 0n, k)) : List<&2, Nat>}
77      {==}
78
79# above 16: the bits of the rest
80def sb_hi(i: Nat, +x: Nat, +r: Nat, +f16: {C.fits(16n, x) == True{} : Bool}) -> {sb(i, 16n, Nat.add(x, C.shift(16n, r))) == sb(i, 0n, r) : List<&2, Nat>}:
81  match i:
82    case 0n:
83      {==}
84    case 1n+ +j:
85      %Equal.sym(List<&2, Nat>, sb(j, 16n, Nat.add(x, C.shift(16n, r))), sb(j, 0n, r), sb_hi(j, x, r, f16)) : {C.bit(C.high(Nat.add(16n, j), Nat.add(x, C.shift(16n, r)))) <> _ == C.bit(C.high(j, r)) <> sb(j, 0n, r) : List<&2, Nat>}
86      %Equal.sym(Nat, C.high(Nat.add(16n, j), Nat.add(x, C.shift(16n, r))), C.high(j, C.high(16n, Nat.add(x, C.shift(16n, r)))), WW.high_comp(j, 16n, Nat.add(x, C.shift(16n, r)))) : {C.bit(_) <> sb(j, 0n, r) == C.bit(C.high(j, r)) <> sb(j, 0n, r) : List<&2, Nat>}
87      %Equal.sym(Nat, C.high(16n, Nat.add(x, C.shift(16n, r))), Nat.add(C.high(16n, x), r), WW.high_add_shift(16n, x, r)) : {C.bit(C.high(j, _)) <> sb(j, 0n, r) == C.bit(C.high(j, r)) <> sb(j, 0n, r) : List<&2, Nat>}
88      %Equal.sym(Nat, C.high(16n, x), 0n, N.eq_from_is_eq(C.high(16n, x), 0n, f16)) : {C.bit(C.high(j, Nat.add(_, r))) <> sb(j, 0n, r) == C.bit(C.high(j, r)) <> sb(j, 0n, r) : List<&2, Nat>}
89      {==}
90
91# below 16: the bits of the limb (j + 1 + d = 16)
92def bit_lo(+j: Nat, +d: Nat, +x: Nat, +r: Nat) -> {C.bit(C.high(j, Nat.add(x, C.shift(Nat.add(j, 1n+d), r)))) == C.bit(C.high(j, x)) : Nat}:
93  %Equal.sym(Nat, C.shift(Nat.add(j, 1n+d), r), C.shift(j, C.shift(1n+d, r)), WW.shift_comp(j, 1n+d, r)) : {C.bit(C.high(j, Nat.add(x, _))) == C.bit(C.high(j, x)) : Nat}
94  %Equal.sym(Nat, C.high(j, Nat.add(x, C.shift(j, C.shift(1n+d, r)))), Nat.add(C.high(j, x), C.shift(1n+d, r)), WW.high_add_shift(j, x, C.shift(1n+d, r))) : {C.bit(_) == C.bit(C.high(j, x)) : Nat}
95  WW.bit_dbl(C.high(j, x), C.shift(d, r))
96
97def sh_idx(+j: Nat, +d: Nat, +r: Nat) -> {C.shift(Nat.add(1n+j, d), r) == C.shift(Nat.add(j, 1n+d), r) : Nat}:
98  %Equal.sym(Nat, Nat.add(j, 1n+d), 1n+Nat.add(j, d), NA.add_succ(j, d)) : {C.shift(Nat.add(1n+j, d), r) == C.shift(_, r) : Nat}
99  {==}
100
101def sb_lo(i: Nat, +d: Nat, +x: Nat, +r: Nat) -> {sb(i, 0n, Nat.add(x, C.shift(Nat.add(i, d), r))) == sb(i, 0n, x) : List<&2, Nat>}:
102  match i:
103    case 0n:
104      {==}
105    case 1n+ +j:
106      %Equal.sym(Nat, C.shift(Nat.add(1n+j, d), r), C.shift(Nat.add(j, 1n+d), r), sh_idx(j, d, r)) : {C.bit(C.high(j, Nat.add(x, _))) <> sb(j, 0n, Nat.add(x, C.shift(Nat.add(1n+j, d), r))) == C.bit(C.high(j, x)) <> sb(j, 0n, x) : List<&2, Nat>}
107      %Equal.sym(Nat, C.shift(Nat.add(1n+j, d), r), C.shift(Nat.add(j, 1n+d), r), sh_idx(j, d, r)) : {C.bit(C.high(j, Nat.add(x, C.shift(Nat.add(j, 1n+d), r)))) <> sb(j, 0n, Nat.add(x, _)) == C.bit(C.high(j, x)) <> sb(j, 0n, x) : List<&2, Nat>}
108      %Equal.sym(List<&2, Nat>, sb(j, 0n, Nat.add(x, C.shift(Nat.add(j, 1n+d), r))), sb(j, 0n, x), sb_lo(j, 1n+d, x, r)) : {C.bit(C.high(j, Nat.add(x, C.shift(Nat.add(j, 1n+d), r)))) <> _ == C.bit(C.high(j, x)) <> sb(j, 0n, x) : List<&2, Nat>}
109      %Equal.sym(Nat, C.bit(C.high(j, Nat.add(x, C.shift(Nat.add(j, 1n+d), r)))), C.bit(C.high(j, x)), bit_lo(j, d, x, r)) : {_ <> sb(j, 0n, x) == C.bit(C.high(j, x)) <> sb(j, 0n, x) : List<&2, Nat>}
110      {==}
111
112# the bits of n limbs below 2^16
113def bits_sb(+one: Nat, +h1: {one == 1n : Nat}, n: Nat, xs: List<&2, Nat>, +h: {FS.limbs16(one, n, xs) == True{} : Bool}) -> {L.bits(xs) == sb(Nat.mul(n, 16n), 0n, LV.ev(xs)) : List<&2, Nat>}:
114  match n xs:
115    case 0n Nil{}:
116      {==}
117    case 0n x <> t:
118      Empty.absurd({L.bits(x <> t) == sb(Nat.mul(0n, 16n), 0n, LV.ev(x <> t)) : List<&2, Nat>}, Lg.false_true(h))
119    case 1n+k Nil{}:
120      Empty.absurd({L.bits([]) == sb(Nat.mul(1n+k, 16n), 0n, LV.ev([])) : List<&2, Nat>}, Lg.false_true(h))
121    case 1n+ +k +x <> +t:
122      +hx = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), h)
123      +ht = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), h)
124      +f16 = BY.fits_one(16n, one, h1, x, hx)
125      %Equal.sym(Nat, Nat.add(16n, Nat.mul(k, 16n)), Nat.add(Nat.mul(k, 16n), 16n), NA.add_comm(16n, Nat.mul(k, 16n))) : {List.append(&2, Nat, L.bits(t), L.bits_of(16n, x)) == sb(_, 0n, Nat.add(x, C.shift(16n, LV.ev(t)))) : List<&2, Nat>}
126      %Equal.sym(List<&2, Nat>, sb(Nat.add(Nat.mul(k, 16n), 16n), 0n, Nat.add(x, C.shift(16n, LV.ev(t)))), List.append(&2, Nat, sb(Nat.mul(k, 16n), 16n, Nat.add(x, C.shift(16n, LV.ev(t)))), sb(16n, 0n, Nat.add(x, C.shift(16n, LV.ev(t))))), sb_split(Nat.mul(k, 16n), 16n, Nat.add(x, C.shift(16n, LV.ev(t))))) : {List.append(&2, Nat, L.bits(t), L.bits_of(16n, x)) == _ : List<&2, Nat>}
127      %Equal.sym(List<&2, Nat>, sb(Nat.mul(k, 16n), 16n, Nat.add(x, C.shift(16n, LV.ev(t)))), sb(Nat.mul(k, 16n), 0n, LV.ev(t)), sb_hi(Nat.mul(k, 16n), x, LV.ev(t), f16)) : {List.append(&2, Nat, L.bits(t), L.bits_of(16n, x)) == List.append(&2, Nat, _, sb(16n, 0n, Nat.add(x, C.shift(16n, LV.ev(t))))) : List<&2, Nat>}
128      %Equal.sym(List<&2, Nat>, L.bits(t), sb(Nat.mul(k, 16n), 0n, LV.ev(t)), bits_sb(one, h1, k, t, ht)) : {List.append(&2, Nat, _, L.bits_of(16n, x)) == List.append(&2, Nat, sb(Nat.mul(k, 16n), 0n, LV.ev(t)), sb(16n, 0n, Nat.add(x, C.shift(16n, LV.ev(t))))) : List<&2, Nat>}
129      %Equal.sym(List<&2, Nat>, L.bits_of(16n, x), sb(16n, 0n, x), bits_of_sb(16n, x)) : {List.append(&2, Nat, sb(Nat.mul(k, 16n), 0n, LV.ev(t)), _) == List.append(&2, Nat, sb(Nat.mul(k, 16n), 0n, LV.ev(t)), sb(16n, 0n, Nat.add(x, C.shift(16n, LV.ev(t))))) : List<&2, Nat>}
130      %Equal.sym(List<&2, Nat>, sb(16n, 0n, Nat.add(x, C.shift(16n, LV.ev(t)))), sb(16n, 0n, x), sb_lo(16n, 0n, x, LV.ev(t))) : {List.append(&2, Nat, sb(Nat.mul(k, 16n), 0n, LV.ev(t)), sb(16n, 0n, x)) == List.append(&2, Nat, sb(Nat.mul(k, 16n), 0n, LV.ev(t)), _) : List<&2, Nat>}
131      {==}