~/jendhub

proofs/math/natural/bits.bend

bend-collections-laws-crypto@1.0.0.0 · 117 lines · 14 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/spec/lib/common.bend as SC
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
6import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
7import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as R
8
9# bit_length(n) is the number of binary digits of n: n < 2^bit_length(n),
10# and 2^(bit_length(n) - 1) <= n for n > 0, stated as 2^L <= 2 n
11# (Lean 4 Mathlib Mathlib/Data/Nat/Size: Nat.lt_size_self and
12# Nat.size_le; Python's int.bit_length). bit_length(0) == 0.
13
14# ---- halving ----
15
16# n == 2 (n / 2) + n mod 2
17def half_eq(+n: Nat) -> {n == Nat.add(Nat.double(Nat.div(n, 2n)), Nat.mod(n, 2n)) : Nat}:
18  %Equal.sym(Nat, Nat.double(Nat.div(n, 2n)), Nat.mul(Nat.div(n, 2n), 2n), Equal.trans(Nat, Nat.double(Nat.div(n, 2n)), Nat.mul(2n, Nat.div(n, 2n)), Nat.mul(Nat.div(n, 2n), 2n), A.double_mul(Nat.div(n, 2n)), A.mul_comm(2n, Nat.div(n, 2n)))) : {n == Nat.add(_, Nat.mod(n, 2n)) : Nat}
19  R.dm_eq(1n, n)
20
21# a + (1 + b) <= a is false
22def add_succ_nle(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.add(a, 1n+b), a) == False{} : Bool}:
23  match a:
24    case 0n:
25      {==}
26    case 1n+ +ap:
27      add_succ_nle(ap, b)
28
29# n / 2 < n for n > 0
30def half_lt(+np: Nat) -> {Nat.is_lt(Nat.div(1n+np, 2n), 1n+np) == True{} : Bool}:
31  +n = {1n+np : Nat}
32  +e = Equal.trans(Bool, Nat.is_le(n, Nat.div(n, 2n)), Nat.is_le(Nat.mul(n, 2n), n), False{}, R.le_div(1n, n, n),
33    Equal.trans(Bool, Nat.is_le(Nat.mul(n, 2n), n), Nat.is_le(Nat.add(n, Nat.add(n, 0n)), n), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, n), Nat.mul(n, 2n), Nat.add(n, Nat.add(n, 0n)), A.mul_comm(n, 2n)),
34      Equal.trans(Bool, Nat.is_le(Nat.add(n, Nat.add(n, 0n)), n), Nat.is_le(Nat.add(n, n), n), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(Nat.add(n, z), n), Nat.add(n, 0n), n, A.add_zero(n)), add_succ_nle(n, np))))
35  N.not_le_lt(n, Nat.div(n, 2n), e)
36
37# n mod 2 <= 1
38def half_rem(+n: Nat) -> {Nat.is_lt(Nat.mod(n, 2n), 2n) == True{} : Bool}:
39  R.dm_lt(1n, n)
40
41# ---- bit_length ----
42
43def go_acc(fuel: Nat, +n: Nat, +k: Nat) -> {M.bit_length_go(fuel, n, 1n+k) == 1n+M.bit_length_go(fuel, n, k) : Nat}:
44  match fuel n:
45    case 0n n0:
46      {==}
47    case 1n+f 0n:
48      {==}
49    case 1n+ +f 1n+ +np:
50      go_acc(f, Nat.div(1n+np, 2n), 1n+k)
51
52def go_zero(+fuel: Nat, +k: Nat) -> {M.bit_length_go(fuel, 0n, k) == k : Nat}:
53  match fuel:
54    case 0n:
55      {==}
56    case 1n+f:
57      {==}
58
59# the halved argument stays within the fuel
60def half_fuel(+np: Nat, +f: Nat, +hf: {Nat.is_le(np, f) == True{} : Bool}) -> {Nat.is_le(Nat.div(1n+np, 2n), f) == True{} : Bool}:
61  N.le_trans(Nat.div(1n+np, 2n), np, f, N.lt_succ_le(Nat.div(1n+np, 2n), np, half_lt(np)), hf)
62
63# 2 h + r < 2 (1 + h) for r < 2
64def half_bound(+np: Nat) -> {Nat.is_lt(1n+np, Nat.double(1n+Nat.div(1n+np, 2n))) == True{} : Bool}:
65  +h = Nat.div(1n+np, 2n)
66  %Equal.sym(Nat, 1n+np, Nat.add(Nat.double(h), Nat.mod(1n+np, 2n)), half_eq(1n+np)) : {Nat.is_lt(_, Nat.double(1n+h)) == True{} : Bool}
67  %Equal.sym(Nat, Nat.add(2n, Nat.double(h)), Nat.add(Nat.double(h), 2n), A.add_comm(2n, Nat.double(h))) : {Nat.is_lt(Nat.add(Nat.double(h), Nat.mod(1n+np, 2n)), _) == True{} : Bool}
68  N.lt_add_left(Nat.mod(1n+np, 2n), 2n, Nat.double(h), half_rem(1n+np))
69
70def lt_go(fuel: Nat, +n: Nat, +hf: {Nat.is_le(n, fuel) == True{} : Bool}) -> {Nat.is_lt(n, SC.pow2(M.bit_length_go(fuel, n, 0n))) == True{} : Bool}:
71  match fuel n:
72    case 0n 0n:
73      {==}
74    case 0n 1n+np:
75      Empty.absurd({Nat.is_lt(1n+np, SC.pow2(M.bit_length_go(0n, 1n+np, 0n))) == True{} : Bool}, L.false_true(hf))
76    case 1n+f 0n:
77      {==}
78    case 1n+ +f 1n+ +np:
79      +h = Nat.div(1n+np, 2n)
80      +x = M.bit_length_go(f, h, 0n)
81      +ih = lt_go(f, h, half_fuel(np, f, hf))
82      %Equal.sym(Nat, M.bit_length_go(f, h, 1n), 1n+x, go_acc(f, h, 0n)) : {Nat.is_lt(1n+np, SC.pow2(_)) == True{} : Bool}
83      N.lt_le_trans(1n+np, Nat.double(1n+h), Nat.double(SC.pow2(x)), half_bound(np), N.double_le(1n+h, SC.pow2(x), N.lt_succ_le_succ(h, SC.pow2(x), ih)))
84
85# n < 2^bit_length(n)   (Mathlib Nat.lt_size_self)
86def bit_length_lt(+n: Nat) -> {Nat.is_lt(n, SC.pow2(M.bit_length(n))) == True{} : Bool}:
87  lt_go(n, n, N.le_refl(n))
88
89# the lower bound, as 2^L <= max(1, 2 n)
90def le_step(+np: Nat, +h: Nat, +x: Nat, +e: {1n+np == Nat.add(Nat.double(h), Nat.mod(1n+np, 2n)) : Nat}, +ih: {Nat.is_le(SC.pow2(x), Nat.max(1n, Nat.double(h))) == True{} : Bool}) -> {Nat.is_le(SC.pow2(x), 1n+np) == True{} : Bool}:
91  match h:
92    case 0n:
93      N.le_trans(SC.pow2(x), 1n, 1n+np, ih, N.lt_succ_le_succ(0n, 1n+np, {==}))
94    case 1n+ +hp:
95      N.le_trans(SC.pow2(x), Nat.double(1n+hp), 1n+np, ih, N.le_trans(Nat.double(1n+hp), Nat.add(Nat.double(1n+hp), Nat.mod(1n+np, 2n)), 1n+np, N.le_add_right(Nat.double(1n+hp), Nat.mod(1n+np, 2n)), N.eq_le(Nat.add(Nat.double(1n+hp), Nat.mod(1n+np, 2n)), 1n+np, Equal.sym(Nat, 1n+np, Nat.add(Nat.double(1n+hp), Nat.mod(1n+np, 2n)), e))))
96
97def le_go(fuel: Nat, +n: Nat, +hf: {Nat.is_le(n, fuel) == True{} : Bool}) -> {Nat.is_le(SC.pow2(M.bit_length_go(fuel, n, 0n)), Nat.max(1n, Nat.double(n))) == True{} : Bool}:
98  match fuel n:
99    case 0n 0n:
100      {==}
101    case 0n 1n+np:
102      Empty.absurd({Nat.is_le(SC.pow2(M.bit_length_go(0n, 1n+np, 0n)), Nat.max(1n, Nat.double(1n+np))) == True{} : Bool}, L.false_true(hf))
103    case 1n+f 0n:
104      {==}
105    case 1n+ +f 1n+ +np:
106      +h = Nat.div(1n+np, 2n)
107      +x = M.bit_length_go(f, h, 0n)
108      +ih = le_go(f, h, half_fuel(np, f, hf))
109      %Equal.sym(Nat, M.bit_length_go(f, h, 1n), 1n+x, go_acc(f, h, 0n)) : {Nat.is_le(SC.pow2(_), Nat.max(1n, Nat.double(1n+np))) == True{} : Bool}
110      N.double_le(SC.pow2(x), 1n+np, le_step(np, h, x, half_eq(1n+np), ih))
111
112# 2^bit_length(n) <= 2 n for n > 0, i.e. 2^(bit_length(n) - 1) <= n   (Mathlib Nat.size_le)
113def bit_length_le(+np: Nat) -> {Nat.is_le(SC.pow2(M.bit_length(1n+np)), Nat.double(1n+np)) == True{} : Bool}:
114  le_go(1n+np, 1n+np, N.le_refl(1n+np))
115
116def bit_length_zero() -> {M.bit_length(0n) == 0n : Nat}:
117  {==}