1	# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/u32and.src; edit the .src
2	import Base
3	import ../../../spec/lib/common.bend as C
4	import ../../lib/logic.bend as L
5	import ../../lib/lemmas/spec/numeric.bend as S
6	import ../../lib/u32.bend as U
7	import ../../lib/word.bend as WD
8	import ../../math/typed/width.bend as WW
9	
10	# The low k bits of a U32 word by a mask: the lemma andm of
11	# proofs/math/typed/f64bits.bend, without the rest of that file (whose
12	# imports are not needed here).
13	
14	def v(+x: U32) -> Nat:
15	  U32.to_nat(x)
16	
17	# ---- generic: words, masks and the top bit ----
18	
19	def sb(+k: Nat, +x: Nat) -> {S.scale_binary(k, x) == C.shift(k, x) : Nat}:
20	  match k:
21	    case 0n:
22	      {==}
23	    case 1n+ +p:
24	      Equal.cong(Nat, Nat, t => Nat.double(t), S.scale_binary(p, x), C.shift(p, x), sb(p, x))
25	
26	# the low k bits of a word
27	def andw(+n: Nat, +k: Nat, +w: Word(n)) -> {S.unsigned(n, Word.and(n, w, WD.mask(n, k))) == C.low(k, S.unsigned(n, w)) : Nat}:
28	  +a = S.unsigned(n, Word.and(n, w, WD.mask(n, k)))
29	  +hp = WD.hi_part(n, k, w)
30	  +e1 = WD.mask_split(n, k, w)
31	  +e2 = Equal.trans(Nat, S.unsigned(n, w), Nat.add(a, S.scale_binary(k, hp)), Nat.add(a, C.shift(k, hp)), e1, Equal.cong(Nat, Nat, z => Nat.add(a, z), S.scale_binary(k, hp), C.shift(k, hp), sb(k, hp)))
32	  +hl = WD.mask_lt(n, k, 1n, {==}, w)
33	  +hl2 = L.subst(Nat, z => {Nat.is_lt(a, z) == True{} : Bool}, S.scale_binary(k, 1n), C.pow2(k), Equal.sym(Nat, C.pow2(k), S.scale_binary(k, 1n), U.pow2_scale(k)), hl)
34	  Equal.sym(Nat, C.low(k, S.unsigned(n, w)), a, Equal.trans(Nat, C.low(k, S.unsigned(n, w)), C.low(k, Nat.add(a, C.shift(k, hp))), a, Equal.cong(Nat, Nat, z => C.low(k, z), S.unsigned(n, w), Nat.add(a, C.shift(k, hp)), e2), WW.low_uniq(k, a, hp, hl2)))
35	
36	def andm0(+x: U32, +k: Nat) -> {v(U32.and(x, U32{WD.mask(32n, k)})) == C.low(k, v(x)) : Nat}:
37	  match x:
38	    case U32{+w}:
39	      +m = Word.and(32n, w, WD.mask(32n, k))
40	      Equal.trans(Nat, U32.to_nat(U32{m}), S.unsigned(32n, m), C.low(k, v(U32{w})), U.to_nat_word(m), Equal.trans(Nat, S.unsigned(32n, m), C.low(k, S.unsigned(32n, w)), C.low(k, v(U32{w})), andw(32n, k, w), Equal.cong(Nat, Nat, z => C.low(k, z), S.unsigned(32n, w), v(U32{w}), Equal.sym(Nat, v(U32{w}), S.unsigned(32n, w), U.to_nat_word(w)))))
41	
42	# x and c for a mask constant c = 2^k - 1
43	def andm(+x: U32, +k: Nat, +c: U32, +hc: {c == U32{WD.mask(32n, k)} : U32}) -> {v(U32.and(x, c)) == C.low(k, v(x)) : Nat}:
44	  L.subst(U32, z => {v(U32.and(x, z)) == C.low(k, v(x)) : Nat}, U32{WD.mask(32n, k)}, c, Equal.sym(U32, c, U32{WD.mask(32n, k)}, hc), andm0(x, k))
45