proofs/crypto/secp256k1/u32and.bend

bend-collections-laws-crypto@1.0.0.0 · 45 lines · 5 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/u32and.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/proofs/lib/logic.bend as L
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
8import bend-collections-laws-crypto@1.0.0.0/proofs/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
14def v(+x: U32) -> Nat:
15  U32.to_nat(x)
16
17# ---- generic: words, masks and the top bit ----
18
19def 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
27def 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
36def 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
43def 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