proofs/lib/lemmas/proofs/word_value.bend

bend-collections-laws-crypto@1.0.0.0 · 115 lines · 19 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as Routing
5
6# Every natural below 2^n is represented exactly by from_nat(n, v): its
7# unsigned value is v. Built on the actual Base Nat.divmod definition.
8def le_refl(n: Nat) -> {Nat.is_le(n, n) == True{} : Bool}:
9  match n:
10    case 0n: {==}
11    case 1n+p: le_refl(p)
12
13def le_succ(r: Nat, x: Nat, h: {Nat.is_le(r, x) == True{} : Bool}) -> {Nat.is_le(r, 1n+x) == True{} : Bool}:
14  match r x:
15    case 0n x0: {==}
16    case 1n+rp 0n: Empty.absurd({Nat.is_le(1n+rp, 1n) == True{} : Bool}, Routing.false_true(h))
17    case 1n+rp 1n+xp: le_succ(rp, xp, h)
18
19def le_add(m: Nat, +r: Nat) -> {Nat.is_le(r, Nat.add(m, r)) == True{} : Bool}:
20  match m:
21    case 0n: le_refl(r)
22    case 1n++p: le_succ(r, Nat.add(p, r), le_add(p, r))
23
24# (M + r) + (1 + n) == (M + (1 + r)) + n
25def shift_count(+m: Nat, +r: Nat, +n: Nat) -> {Nat.add(Nat.add(m, r), 1n+n) == Nat.add(Nat.add(m, 1n+r), n) : Nat}:
26  %Equal.sym(Nat, Nat.add(m, 1n+r), 1n+Nat.add(m, r), A.add_succ(m, r)) : {Nat.add(Nat.add(m, r), 1n+n) == Nat.add(_, n) : Nat}
27  A.add_succ(Nat.add(m, r), n)
28
29# (M + r) + (1 + n) == ((1+bp) + M + 0) + n when r == bp
30def shift_carry(+bp: Nat, +n: Nat, +m: Nat, +r: Nat, inv: {Nat.add(0n, r) == bp : Nat}) -> {Nat.add(Nat.add(m, r), 1n+n) == Nat.add(Nat.add(Nat.add(1n+bp, m), 0n), n) : Nat}:
31  %Equal.sym(Nat, Nat.add(Nat.add(1n+bp, m), 0n), Nat.add(1n+bp, m), A.add_zero(Nat.add(1n+bp, m))) : {Nat.add(Nat.add(m, r), 1n+n) == Nat.add(_, n) : Nat}
32  %Equal.sym(Nat, Nat.add(0n, r), bp, inv) : {Nat.add(Nat.add(m, _), 1n+n) == 1n+Nat.add(Nat.add(bp, m), n) : Nat}
33  %A.add_comm(m, bp) : {Nat.add(Nat.add(m, bp), 1n+n) == 1n+Nat.add(_, n) : Nat}
34  A.add_succ(Nat.add(m, bp), n)
35
36def go_equation(bp: Nat, n: Nat, m: Nat, d: Nat, r: Nat) -> Type:
37  {Nat.add(Nat.add(Nat.mul(d, 1n+bp), r), n) == Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r))) : Nat} & {Nat.is_le(Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)), bp) == True{} : Bool}
38
39def bound_zero(+bp: Nat, +m: Nat, +r: Nat, inv: {Nat.add(m, r) == bp : Nat}) -> {Nat.is_le(r, bp) == True{} : Bool}:
40  %inv : {Nat.is_le(r, _) == True{} : Bool}
41  le_add(m, r)
42
43def extend(+a: Nat, +b: Nat, +c: Nat, -L: Type, pre: {a == b : Nat}, ih: {b == c : Nat} & L) -> {a == c : Nat} & L:
44  (eq, le) = ih
45  (Equal.trans(Nat, a, b, c, pre, eq), le)
46
47# Invariant of the actual division loop: remaining countdown m plus the running
48# remainder r is the divisor minus one.
49def go(+bp: Nat, n: Nat, m: Nat, +d: Nat, +r: Nat, +inv: {Nat.add(m, r) == bp : Nat}) -> go_equation(bp, n, m, d, r):
50  match n:
51    case 0n:
52      (A.add_zero(Nat.add(Nat.mul(d, 1n+bp), r)), bound_zero(bp, m, r, inv))
53    case 1n++np:
54      match m:
55        case 0n:
56          extend(Nat.add(Nat.add(Nat.mul(d, 1n+bp), r), 1n+np), Nat.add(Nat.add(Nat.mul(1n+d, 1n+bp), 0n), np), Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n))), {Nat.is_le(Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), bp) == True{} : Bool}, shift_carry(bp, np, Nat.mul(d, 1n+bp), r, inv), go(bp, np, r, 1n+d, 0n, Equal.trans(Nat, Nat.add(r, 0n), r, bp, A.add_zero(r), inv)))
57        case 1n++mp:
58          extend(Nat.add(Nat.add(Nat.mul(d, 1n+bp), r), 1n+np), Nat.add(Nat.add(Nat.mul(d, 1n+bp), 1n+r), np), Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r))), {Nat.is_le(Pair.snd(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r)), bp) == True{} : Bool}, shift_count(Nat.mul(d, 1n+bp), r, np), go(bp, np, mp, d, 1n+r, Equal.trans(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), bp, A.add_succ(mp, r), inv)))
59
60# v == 2*(v/2) + v%2 and v%2 <= 1, for the actual Nat.divmod.
61def half(+v: Nat) -> {Nat.add(Nat.add(Nat.mul(0n, 2n), 0n), v) == Nat.add(Nat.mul(Nat.div(v, 2n), 2n), Nat.mod(v, 2n)) : Nat} & {Nat.is_le(Nat.mod(v, 2n), 1n) == True{} : Bool}:
62  go(1n, v, 1n, 0n, 0n, {==})
63
64def remainder_bit(r: Nat, le: {Nat.is_le(r, 1n) == True{} : Bool}) -> {S.bit_value(Nat.is_eq(r, 1n)) == r : Nat}:
65  match r:
66    case 0n: {==}
67    case 1n+x:
68      match x:
69        case 0n: {==}
70        case 1n+y: Empty.absurd({S.bit_value(Nat.is_eq(2n+y, 1n)) == 2n+y : Nat}, Routing.false_true(le))
71
72def not_below_zero(n: Nat) -> {Nat.is_lt(n, 0n) == False{} : Bool}:
73  match n:
74    case 0n: {==}
75    case 1n+p: {==}
76
77def lt_double(q: Nat, x: Nat, +r: Nat, h: {Nat.is_lt(Nat.add(Nat.double(q), r), Nat.double(x)) == True{} : Bool}) -> {Nat.is_lt(q, x) == True{} : Bool}:
78  match q x:
79    case q0 0n: Empty.absurd({Nat.is_lt(q0, 0n) == True{} : Bool}, Routing.false_true(Equal.trans(Bool, False{}, Nat.is_lt(Nat.add(Nat.double(q0), r), 0n), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(Nat.double(q0), r), 0n), False{}, not_below_zero(Nat.add(Nat.double(q0), r))), h)))
80    case 0n 1n+xp: {==}
81    case 1n+qp 1n+xp: lt_double(qp, xp, r, h)
82
83def two_times(+q: Nat) -> {Nat.mul(q, 2n) == Nat.double(q) : Nat}:
84  Equal.trans(Nat, Nat.mul(q, 2n), Nat.mul(2n, q), Nat.double(q), A.mul_comm(q, 2n), Equal.sym(Nat, Nat.double(q), Nat.mul(2n, q), A.double_mul(q)))
85
86# v < 2 * 2^p, rewritten as 2*(v/2) + v%2 < double(2^p)
87def rescale(+p: Nat, +v: Nat, eq: {v == Nat.add(Nat.mul(Nat.div(v, 2n), 2n), Nat.mod(v, 2n)) : Nat}, bound: {Nat.is_lt(v, Nat.mul(2n, Nat.pow(2n, p))) == True{} : Bool}) -> {Nat.is_lt(Nat.add(Nat.double(Nat.div(v, 2n)), Nat.mod(v, 2n)), Nat.double(Nat.pow(2n, p))) == True{} : Bool}:
88  %Equal.sym(Nat, Nat.double(Nat.pow(2n, p)), Nat.mul(2n, Nat.pow(2n, p)), A.double_mul(Nat.pow(2n, p))) : {Nat.is_lt(Nat.add(Nat.double(Nat.div(v, 2n)), Nat.mod(v, 2n)), _) == True{} : Bool}
89  %two_times(Nat.div(v, 2n)) : {Nat.is_lt(Nat.add(_, Nat.mod(v, 2n)), Nat.mul(2n, Nat.pow(2n, p))) == True{} : Bool}
90  %eq : {Nat.is_lt(_, Nat.mul(2n, Nat.pow(2n, p))) == True{} : Bool}
91  bound
92
93def from_nat_step(+p: Nat, +v: Nat, parts: {v == Nat.add(Nat.mul(Nat.div(v, 2n), 2n), Nat.mod(v, 2n)) : Nat} & {Nat.is_le(Nat.mod(v, 2n), 1n) == True{} : Bool}, bound: {Nat.is_lt(v, Nat.mul(2n, Nat.pow(2n, p))) == True{} : Bool}, ih: @+q: Nat -> @hq: {Nat.is_lt(q, Nat.pow(2n, p)) == True{} : Bool} -> {S.unsigned(p, S.from_nat(p, q)) == q : Nat}) -> {S.unsigned(1n+p, S.from_nat(1n+p, v)) == v : Nat}:
94  (+eq, le) = parts
95  %Equal.sym(Nat, S.unsigned(p, S.from_nat(p, Nat.div(v, 2n))), Nat.div(v, 2n), ih(Nat.div(v, 2n), lt_double(Nat.div(v, 2n), Nat.pow(2n, p), Nat.mod(v, 2n), rescale(p, v, eq, bound)))) : {Nat.add(S.bit_value(Nat.is_eq(Nat.mod(v, 2n), 1n)), Nat.double(_)) == v : Nat}
96  %Equal.sym(Nat, S.bit_value(Nat.is_eq(Nat.mod(v, 2n), 1n)), Nat.mod(v, 2n), remainder_bit(Nat.mod(v, 2n), le)) : {Nat.add(_, Nat.double(Nat.div(v, 2n))) == v : Nat}
97  %Equal.sym(Nat, v, Nat.add(Nat.mul(Nat.div(v, 2n), 2n), Nat.mod(v, 2n)), eq) : {Nat.add(Nat.mod(v, 2n), Nat.double(Nat.div(v, 2n))) == _ : Nat}
98  %Equal.sym(Nat, Nat.mul(Nat.div(v, 2n), 2n), Nat.double(Nat.div(v, 2n)), two_times(Nat.div(v, 2n))) : {Nat.add(Nat.mod(v, 2n), Nat.double(Nat.div(v, 2n))) == Nat.add(_, Nat.mod(v, 2n)) : Nat}
99  A.add_comm(Nat.mod(v, 2n), Nat.double(Nat.div(v, 2n)))
100
101def below_one(v: Nat, h: {Nat.is_lt(v, 1n) == True{} : Bool}) -> {0n == v : Nat}:
102  match v:
103    case 0n: {==}
104    case 1n+x:
105      match x:
106        case 0n: Empty.absurd({0n == 1n : Nat}, Routing.false_true(h))
107        case 1n+y: Empty.absurd({0n == 2n+y : Nat}, Routing.false_true(h))
108
109def half_parts(+v: Nat) -> {v == Nat.add(Nat.mul(Nat.div(v, 2n), 2n), Nat.mod(v, 2n)) : Nat} & {Nat.is_le(Nat.mod(v, 2n), 1n) == True{} : Bool}:
110  half(v)
111
112def from_nat_value(n: Nat, +v: Nat, h: {Nat.is_lt(v, Nat.pow(2n, n)) == True{} : Bool}) -> {S.unsigned(n, S.from_nat(n, v)) == v : Nat}:
113  match n:
114    case 0n: below_one(v, h)
115    case 1n++p: from_nat_step(p, v, half_parts(v), h, q => hq => from_nat_value(p, q, hq))