~/jendhub

proofs/crypto/curve25519/num.bend

bend-collections-laws-crypto@1.0.0.0 · 96 lines · 18 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
7
8# Order and power-of-two helpers for the curve25519 proofs. Powers of two
9# are WD.sc(k, one) with a symbolic one (spec/crypto/curve25519/field.bend).
10
11# ---- equalities ----
12
13def cong_l(+x: Nat, +y: Nat, +z: Nat, +e: {x == y : Nat}) -> {Nat.add(x, z) == Nat.add(y, z) : Nat}:
14  Equal.cong(Nat, Nat, t => Nat.add(t, z), x, y, e)
15
16def cong_r(+z: Nat, +x: Nat, +y: Nat, +e: {x == y : Nat}) -> {Nat.add(z, x) == Nat.add(z, y) : Nat}:
17  Equal.cong(Nat, Nat, t => Nat.add(z, t), x, y, e)
18
19def cong_add(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +e1: {a == b : Nat}, +e2: {c == d : Nat}) -> {Nat.add(a, c) == Nat.add(b, d) : Nat}:
20  Equal.trans(Nat, Nat.add(a, c), Nat.add(b, c), Nat.add(b, d), cong_l(a, b, c, e1), cong_r(b, c, d, e2))
21
22def cong_mul(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +e1: {a == b : Nat}, +e2: {c == d : Nat}) -> {Nat.mul(a, c) == Nat.mul(b, d) : Nat}:
23  Equal.trans(Nat, Nat.mul(a, c), Nat.mul(b, c), Nat.mul(b, d), Equal.cong(Nat, Nat, t => Nat.mul(t, c), a, b, e1), Equal.cong(Nat, Nat, t => Nat.mul(b, t), c, d, e2))
24
25def cong_sc(+k: Nat, +x: Nat, +y: Nat, +e: {x == y : Nat}) -> {WD.sc(k, x) == WD.sc(k, y) : Nat}:
26  Equal.cong(Nat, Nat, t => WD.sc(k, t), x, y, e)
27
28def cong_mod(+m: Nat, +x: Nat, +y: Nat, +e: {x == y : Nat}) -> {Nat.mod(x, m) == Nat.mod(y, m) : Nat}:
29  Equal.cong(Nat, Nat, t => Nat.mod(t, m), x, y, e)
30
31# (a + b) + (c + d) == (a + c) + (b + d)
32def add4(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}:
33  Equal.trans(Nat, Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(a, Nat.add(b, Nat.add(c, d))), Nat.add(Nat.add(a, c), Nat.add(b, d)), NA.add_assoc(a, b, Nat.add(c, d)),
34    Equal.trans(Nat, Nat.add(a, Nat.add(b, Nat.add(c, d))), Nat.add(a, Nat.add(c, Nat.add(b, d))), Nat.add(Nat.add(a, c), Nat.add(b, d)), cong_r(a, Nat.add(b, Nat.add(c, d)), Nat.add(c, Nat.add(b, d)), NA.add_swap(b, c, d)),
35      Equal.sym(Nat, Nat.add(Nat.add(a, c), Nat.add(b, d)), Nat.add(a, Nat.add(c, Nat.add(b, d))), NA.add_assoc(a, c, Nat.add(b, d)))))
36
37# 2^k x + 2^k y == 2^k (x + y)
38def sc_add(+k: Nat, +x: Nat, +y: Nat) -> {Nat.add(WD.sc(k, x), WD.sc(k, y)) == WD.sc(k, Nat.add(x, y)) : Nat}:
39  match k:
40    case 0n:
41      {==}
42    case 1n+q:
43      +e = sc_add(q, x, y)
44      +d = Equal.sym(Nat, Nat.double(Nat.add(WD.sc(q, x), WD.sc(q, y))), Nat.add(Nat.double(WD.sc(q, x)), Nat.double(WD.sc(q, y))), NA.double_add(WD.sc(q, x), WD.sc(q, y)))
45      Equal.trans(Nat, Nat.add(Nat.double(WD.sc(q, x)), Nat.double(WD.sc(q, y))), Nat.double(Nat.add(WD.sc(q, x), WD.sc(q, y))), Nat.double(WD.sc(q, Nat.add(x, y))), d, Equal.cong(Nat, Nat, t => Nat.double(t), Nat.add(WD.sc(q, x), WD.sc(q, y)), WD.sc(q, Nat.add(x, y)), e))
46
47# 2^k x + 2^k x == 2^(k+1) x
48def sc_dbl(+k: Nat, +x: Nat) -> {Nat.add(WD.sc(k, x), WD.sc(k, x)) == WD.sc(1n+k, x) : Nat}:
49  Equal.sym(Nat, Nat.double(WD.sc(k, x)), Nat.add(WD.sc(k, x), WD.sc(k, x)), NA.double_self(WD.sc(k, x)))
50
51# 2^j (2^k x) == 2^(j+k) x
52def sc_sc(+j: Nat, +k: Nat, +x: Nat) -> {WD.sc(j, WD.sc(k, x)) == WD.sc(Nat.add(j, k), x) : Nat}:
53  Equal.sym(Nat, WD.sc(Nat.add(j, k), x), WD.sc(j, WD.sc(k, x)), AR.sc_idx(j, k, x))
54
55# x 2^k == 2^k x
56def mul_sc_r(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat) -> {Nat.mul(x, WD.sc(k, one)) == WD.sc(k, x) : Nat}:
57  AR.mul_sc1(k, one, h1, x)
58
59# (2^j x)(2^k y) == 2^(j+k) (x y)
60def mul_sc2(+j: Nat, +k: Nat, +x: Nat, +y: Nat) -> {Nat.mul(WD.sc(j, x), WD.sc(k, y)) == WD.sc(Nat.add(j, k), Nat.mul(x, y)) : Nat}:
61  +a = Equal.sym(Nat, WD.sc(j, Nat.mul(x, WD.sc(k, y))), Nat.mul(WD.sc(j, x), WD.sc(k, y)), AR.sc_mul(j, x, WD.sc(k, y)))
62  +b0 = Equal.trans(Nat, Nat.mul(x, WD.sc(k, y)), Nat.mul(WD.sc(k, y), x), WD.sc(k, Nat.mul(y, x)), NA.mul_comm(x, WD.sc(k, y)), Equal.sym(Nat, WD.sc(k, Nat.mul(y, x)), Nat.mul(WD.sc(k, y), x), AR.sc_mul(k, y, x)))
63  +b = Equal.trans(Nat, Nat.mul(x, WD.sc(k, y)), WD.sc(k, Nat.mul(y, x)), WD.sc(k, Nat.mul(x, y)), b0, cong_sc(k, Nat.mul(y, x), Nat.mul(x, y), NA.mul_comm(y, x)))
64  Equal.trans(Nat, Nat.mul(WD.sc(j, x), WD.sc(k, y)), WD.sc(j, Nat.mul(x, WD.sc(k, y))), WD.sc(Nat.add(j, k), Nat.mul(x, y)), a,
65    Equal.trans(Nat, WD.sc(j, Nat.mul(x, WD.sc(k, y))), WD.sc(j, WD.sc(k, Nat.mul(x, y))), WD.sc(Nat.add(j, k), Nat.mul(x, y)), cong_sc(j, Nat.mul(x, WD.sc(k, y)), WD.sc(k, Nat.mul(x, y)), b), sc_sc(j, k, Nat.mul(x, y))))
66
67# ---- order ----
68
69def le_refl(+x: Nat) -> {Nat.is_le(x, x) == True{} : Bool}:
70  N.le_refl(x)
71
72# x <= a -> x + y <= a + y
73def le_add_r(+x: Nat, +a: Nat, +y: Nat, +h: {Nat.is_le(x, a) == True{} : Bool}) -> {Nat.is_le(Nat.add(x, y), Nat.add(a, y)) == True{} : Bool}:
74  +e1 = N.le_add_left(x, a, y, h)
75  %NA.add_comm(y, x) : {Nat.is_le(_, Nat.add(a, y)) == True{} : Bool}
76  %NA.add_comm(y, a) : {Nat.is_le(Nat.add(y, x), _) == True{} : Bool}
77  e1
78
79def le_add2(+x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_le(x, a) == True{} : Bool}, +hy: {Nat.is_le(y, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(x, y), Nat.add(a, b)) == True{} : Bool}:
80  N.le_trans(Nat.add(x, y), Nat.add(a, y), Nat.add(a, b), le_add_r(x, a, y, hx), N.le_add_left(y, b, a, hy))
81
82# x <= a, y <= b -> x y <= a b
83def le_mul2(+x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_le(x, a) == True{} : Bool}, +hy: {Nat.is_le(y, b) == True{} : Bool}) -> {Nat.is_le(Nat.mul(x, y), Nat.mul(a, b)) == True{} : Bool}:
84  +e1 = AR.mul_le(x, a, y, hx)
85  +e2 = AR.mul_le(y, b, a, hy)
86  +e2c = L.subst(Nat, z => {Nat.is_le(z, Nat.mul(b, a)) == True{} : Bool}, Nat.mul(y, a), Nat.mul(a, y), NA.mul_comm(y, a), e2)
87  +e2d = L.subst(Nat, z => {Nat.is_le(Nat.mul(a, y), z) == True{} : Bool}, Nat.mul(b, a), Nat.mul(a, b), NA.mul_comm(b, a), e2c)
88  N.le_trans(Nat.mul(x, y), Nat.mul(a, y), Nat.mul(a, b), e1, e2d)
89
90def le_sc(+k: Nat, +x: Nat, +a: Nat, +h: {Nat.is_le(x, a) == True{} : Bool}) -> {Nat.is_le(WD.sc(k, x), WD.sc(k, a)) == True{} : Bool}:
91  AR.sc_le(k, x, a, h)
92
93# 2^a <= 2^b for a <= b, with b = d + a
94def sc_mono(+d: Nat, +a: Nat, +x: Nat) -> {Nat.is_le(WD.sc(a, x), WD.sc(Nat.add(d, a), x)) == True{} : Bool}:
95  %sc_sc(d, a, x) : {Nat.is_le(WD.sc(a, x), _) == True{} : Bool}
96  AR.le_sc(d, WD.sc(a, x))