1	# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/bitsrel.src; edit the .src
2	import Base
3	import ../../../spec/lib/common.bend as C
4	import ../../../spec/crypto/secp256k1/field.bend as FS
5	import ../../../spec/crypto/secp256k1/curve.bend as CV
6	import ../../../src/crypto/secp256k1/limbs.bend as L
7	import ../../lib/nat.bend as N
8	import ../../lib/logic.bend as Lg
9	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
10	import ../../math/typed/width.bend as WW
11	import ./limbs.bend as LV
12	import ./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
19	def 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	
24	def 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	
31	def 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
42	def 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
50	def 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	
57	def 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)
70	def 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
80	def 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)
92	def 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	
97	def 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	
101	def 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
113	def 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	      {==}