~/jendhub

proofs/lib/u32half.bend

bend-collections-laws-crypto@1.0.0.0 · 168 lines · 15 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
5import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
7
8# U32 halving as a Nat operation, and the midpoint bounds.
9#
10# proofs/lib/u32.bend deliberately avoids `U32.add` (its comment explains
11# why: `inc`/`shl`/`shr`/`sub` have Nat meanings that can be stated with a
12# bound `i < 2^k` for a variable k). The graph's binary search needs the
13# midpoint `(lo + hi) / 2`, so the two missing bridges are proved here from
14# the retained word lemmas: full-width ripple addition conserves the value
15# `shr` is exact halving, so the midpoint can be written with sub and shr
16# alone.
17
18# ---- halving ----
19
20# The Nat halving the checker can compute structurally (no Nat.div).
21def hlf(n: Nat) -> Nat:
22  match n:
23    case 0n:
24      0n
25    case 1n+p:
26      match p:
27        case 0n:
28          0n
29        case 1n+q:
30          1n+hlf(q)
31
32def hlf_double(+q: Nat) -> {hlf(Nat.double(q)) == q : Nat}:
33  match q:
34    case 0n:
35      {==}
36    case 1n+p:
37      Equal.cong(Nat, Nat, n => 1n+n, hlf(Nat.double(p)), p, hlf_double(p))
38
39def hlf_double_succ(+q: Nat) -> {hlf(1n+Nat.double(q)) == q : Nat}:
40  match q:
41    case 0n:
42      {==}
43    case 1n+p:
44      Equal.cong(Nat, Nat, n => 1n+n, hlf(1n+Nat.double(p)), p, hlf_double_succ(p))
45
46def hlf_bit(+b: Bool, +q: Nat) -> {hlf(Nat.add(S.bit_value(b), Nat.double(q))) == q : Nat}:
47  match b:
48    case False{}:
49      hlf_double(q)
50    case True{}:
51      hlf_double_succ(q)
52
53def shr_value(+x: U32) -> {U32.to_nat(U32.shr(x)) == hlf(U32.to_nat(x)) : Nat}:
54  %Equal.sym(Nat, U32.to_nat(x), Nat.add(S.bit_value(U.low_bit(x)), Nat.double(U32.to_nat(U32.shr(x)))), U.shr_split(x)) : {U32.to_nat(U32.shr(x)) == hlf(_) : Nat}
55  Equal.sym(Nat, hlf(Nat.add(S.bit_value(U.low_bit(x)), Nat.double(U32.to_nat(U32.shr(x))))), U32.to_nat(U32.shr(x)),
56    hlf_bit(U.low_bit(x), U32.to_nat(U32.shr(x))))
57
58# ---- halving respects the order ----
59
60def hlf_le(+n: Nat) -> {Nat.is_le(hlf(n), n) == True{} : Bool}:
61  match n:
62    case 0n:
63      {==}
64    case 1n+p:
65      match p:
66        case 0n:
67          {==}
68        case 1n+q:
69          N.le_trans(hlf(q), q, 1n+q, hlf_le(q), N.le_succ(q))
70
71def hlf_succ_le(+q: Nat) -> {Nat.is_le(hlf(1n+q), q) == True{} : Bool}:
72  match q:
73    case 0n:
74      {==}
75    case 1n+r:
76      hlf_le(r)
77
78# The midpoint of a nonempty range lies inside it: a <= hlf(a+b) < b
79# whenever a < b.
80def hlf_lower(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(a, hlf(Nat.add(a, b))) == True{} : Bool}:
81  match a b:
82    case 0n b0:
83      N.zero_le(hlf(Nat.add(0n, b0)))
84    case 1n+p 0n:
85      Empty.absurd({Nat.is_le(1n+p, hlf(Nat.add(1n+p, 0n))) == True{} : Bool}, L.false_true(h))
86    case 1n+ +p 1n+ +q:
87      %Equal.sym(Nat, Nat.add(p, 1n+q), 1n+Nat.add(p, q), N.add_succ(p, q)) : {Nat.is_le(1n+p, hlf(1n+_)) == True{} : Bool}
88      hlf_lower(p, q, h)
89
90def hlf_upper(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(hlf(Nat.add(a, b)), b) == True{} : Bool}:
91  match a b:
92    case 0n 0n:
93      Empty.absurd({Nat.is_lt(hlf(Nat.add(0n, 0n)), 0n) == True{} : Bool}, L.false_true(h))
94    case 0n 1n+ +q:
95      N.le_lt_trans(hlf(1n+q), q, 1n+q, hlf_succ_le(q), N.lt_succ(q))
96    case 1n+p 0n:
97      Empty.absurd({Nat.is_lt(hlf(Nat.add(1n+p, 0n)), 0n) == True{} : Bool}, L.false_true(h))
98    case 1n+ +p 1n+ +q:
99      %Equal.sym(Nat, Nat.add(p, 1n+q), 1n+Nat.add(p, q), N.add_succ(p, q)) : {Nat.is_lt(hlf(1n+_), 1n+q) == True{} : Bool}
100      hlf_upper(p, q, h)
101
102# ---- from_nat / sub bridges used with the halving one ----
103
104# The graph implementation avoids `U32.add` entirely (its Nat meaning would
105# need a 2^32 bound, and the checker cannot expand 2^32 as a unary Nat), so
106# only halving and subtraction bridges are needed. Subtraction is
107# proofs/lib/u32.bend `sub_nat`; halving is `shr_value` above.
108
109def hlf_bound(+i: Nat, +k: Nat, +h: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}) -> {Nat.is_lt(hlf(i), SC.pow2(k)) == True{} : Bool}:
110  N.le_lt_trans(hlf(i), i, SC.pow2(k), hlf_le(i), h)
111
112def shr_bridge(+i: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}) -> {U32.shr(U32.from_nat(i)) == U32.from_nat(hlf(i)) : U32}:
113  +ri = U.to_nat_from_nat(i, k, hk, hi)
114  U.injective(U32.shr(U32.from_nat(i)), U32.from_nat(hlf(i)),
115    Equal.trans(Nat, U32.to_nat(U32.shr(U32.from_nat(i))), hlf(i), U32.to_nat(U32.from_nat(hlf(i))),
116      Equal.trans(Nat, U32.to_nat(U32.shr(U32.from_nat(i))), hlf(U32.to_nat(U32.from_nat(i))), hlf(i),
117        shr_value(U32.from_nat(i)),
118        Equal.cong(Nat, Nat, hlf, U32.to_nat(U32.from_nat(i)), i, ri)),
119      Equal.sym(Nat, U32.to_nat(U32.from_nat(hlf(i))), hlf(i),
120        U.to_nat_from_nat(hlf(i), k, hk, hlf_bound(i, k, hi)))))
121
122# ---- the halving measure used by the binary search ----
123
124# s < 2m gives s/2 < m: one narrowing step of a search range that started
125# below 2^f lands below 2^(f-1).
126def hlf_lt(+s: Nat, +m: Nat, +h: {Nat.is_lt(s, Nat.double(m)) == True{} : Bool}) -> {Nat.is_lt(hlf(s), m) == True{} : Bool}:
127  match s m:
128    case s0 0n:
129      Empty.absurd({Nat.is_lt(hlf(s0), 0n) == True{} : Bool}, N.lt_zero_absurd(s0, h))
130    case 0n 1n+q:
131      {==}
132    case 1n+0n 1n+q:
133      {==}
134    case 1n+1n+r 1n+q:
135      hlf_lt(r, q, h)
136
137# The size after one step is at most s/2, so it stays below the halved bound.
138def step_bound(+s2: Nat, +s: Nat, +m: Nat, +hle: {Nat.is_le(s2, hlf(s)) == True{} : Bool}, +h: {Nat.is_lt(s, Nat.double(m)) == True{} : Bool}) -> {Nat.is_lt(s2, m) == True{} : Bool}:
139  N.le_lt_trans(s2, hlf(s), m, hle, hlf_lt(s, m, h))
140
141# ---- subtraction bridge ----
142
143# U32.sub is exact whenever the subtrahend is not larger (no borrow), so it
144# is the Nat subtraction of the two indices.
145def sub_le(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}:
146  match a b:
147    case a0 0n:
148      L.subst(Nat, z => {Nat.is_le(z, a0) == True{} : Bool}, a0, Nat.sub(a0, 0n), Equal.sym(Nat, Nat.sub(a0, 0n), a0, N.sub_zero(a0)), N.le_refl(a0))
149    case 0n 1n+q:
150      N.zero_le(Nat.sub(0n, 1n+q))
151    case 1n+p 1n+q:
152      N.le_trans(Nat.sub(p, q), p, 1n+p, sub_le(p, q), N.le_succ(p))
153
154def sub_bridge(+a: Nat, +b: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +ha: {Nat.is_lt(a, SC.pow2(k)) == True{} : Bool}, +hb: {Nat.is_le(b, a) == True{} : Bool}) -> {U32.sub(U32.from_nat(a), U32.from_nat(b)) == U32.from_nat(Nat.sub(a, b)) : U32}:
155  +hb2 = N.le_lt_trans(b, a, SC.pow2(k), hb, ha)
156  +ra = U.to_nat_from_nat(a, k, hk, ha)
157  +rb = U.to_nat_from_nat(b, k, hk, hb2)
158  +le = L.subst(Nat, z => {Nat.is_le(z, U32.to_nat(U32.from_nat(a))) == True{} : Bool}, b, U32.to_nat(U32.from_nat(b)), Equal.sym(Nat, U32.to_nat(U32.from_nat(b)), b, rb),
159          L.subst(Nat, z => {Nat.is_le(b, z) == True{} : Bool}, a, U32.to_nat(U32.from_nat(a)), Equal.sym(Nat, U32.to_nat(U32.from_nat(a)), a, ra), hb))
160  U.injective(U32.sub(U32.from_nat(a), U32.from_nat(b)), U32.from_nat(Nat.sub(a, b)),
161    Equal.trans(Nat, U32.to_nat(U32.sub(U32.from_nat(a), U32.from_nat(b))), Nat.sub(a, b), U32.to_nat(U32.from_nat(Nat.sub(a, b))),
162      Equal.trans(Nat, U32.to_nat(U32.sub(U32.from_nat(a), U32.from_nat(b))), Nat.sub(U32.to_nat(U32.from_nat(a)), U32.to_nat(U32.from_nat(b))), Nat.sub(a, b),
163        U.sub_nat(U32.from_nat(a), U32.from_nat(b), le),
164        Equal.trans(Nat, Nat.sub(U32.to_nat(U32.from_nat(a)), U32.to_nat(U32.from_nat(b))), Nat.sub(a, U32.to_nat(U32.from_nat(b))), Nat.sub(a, b),
165          Equal.cong(Nat, Nat, z => Nat.sub(z, U32.to_nat(U32.from_nat(b))), U32.to_nat(U32.from_nat(a)), a, ra),
166          Equal.cong(Nat, Nat, z => Nat.sub(a, z), U32.to_nat(U32.from_nat(b)), b, rb))),
167      Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.sub(a, b))), Nat.sub(a, b),
168        U.to_nat_from_nat(Nat.sub(a, b), k, hk, N.le_lt_trans(Nat.sub(a, b), a, SC.pow2(k), sub_le(a, b), ha)))))