proofs/containers/bitlist/bits.bend
bend-collections-laws-containers@1.0.0.0 · 281 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/arith.bend as AT
7import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as B
8import bend-collections-laws-containers@1.0.0.0/src/containers/bitlist.bend as BLI
9import bend-collections-laws-containers@1.0.0.0/src/containers/types/bitlist.bend as E
10import bend-collections-laws-containers@1.0.0.0/spec/containers/bitset.bend as BS
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/lists.bend as BL
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/listx.bend as LX
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/word.bend as W
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/model.bend as MD
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/state.bend as ST
16import bend-collections-laws-containers@1.0.0.0/spec/containers/bitlist.bend as S
17
18# List-level facts about the stored bits: F = ST.flat(ws) is every stored
19# bit, the bitlist is its first n bits, and ST.invf(n, F) says n <= |F| and
20# every stored bit from position n on is zero. These are the effects of
21# push (in place or with a new word), pop, to_list and count on F, stated
22# like the Lean 4 List lemmas they correspond to (List.take_succ,
23# List.getElem_set, List.take_append_of_le_length, List.drop_append).
24# (source: proofs/containers/bitlist/bits.src)
25
26
27# ---- the zero tail ----
28
29def nth_false(+xs: List<&2, Bool>, +n: Nat, +h: {Nat.is_lt(n, SC.length(Bool, xs)) == True{} : Bool}, +ht: {BL.allf(SC.drop(Bool, xs, n)) == True{} : Bool}) -> {SC.nth(Bool, xs, n) == Some{False{}} : Maybe<&2, Bool>}:
30 match xs n:
31 case Nil{} 0n:
32 Empty.absurd({SC.nth(Bool, Nil{}, 0n) == Some{False{}} : Maybe<&2, Bool>}, L.false_true(h))
33 case Nil{} 1n+p:
34 Empty.absurd({SC.nth(Bool, Nil{}, 1n+p) == Some{False{}} : Maybe<&2, Bool>}, L.false_true(h))
35 case Con{False{}, t} 0n:
36 {==}
37 case Con{True{}, t} 0n:
38 Empty.absurd({SC.nth(Bool, Con{True{}, t}, 0n) == Some{False{}} : Maybe<&2, Bool>}, L.false_true(ht))
39 case Con{False{}, +t} 1n+ +p:
40 nth_false(t, p, h, ht)
41 case Con{True{}, +t} 1n+ +p:
42 nth_false(t, p, h, ht)
43
44def allf_succ(+xs: List<&2, Bool>, +n: Nat, +ht: {BL.allf(SC.drop(Bool, xs, n)) == True{} : Bool}) -> {BL.allf(SC.drop(Bool, xs, 1n+n)) == True{} : Bool}:
45 match xs n:
46 case Nil{} 0n:
47 {==}
48 case Nil{} 1n+p:
49 {==}
50 case Con{False{}, +t} 0n:
51 %Equal.sym(List<&2, Bool>, SC.drop(Bool, t, 0n), t, LX.drop_zero(Bool, t)) : {BL.allf(_) == True{} : Bool}
52 ht
53 case Con{True{}, t} 0n:
54 Empty.absurd({BL.allf(SC.drop(Bool, Con{True{}, t}, 1n)) == True{} : Bool}, L.false_true(ht))
55 case Con{False{}, +t} 1n+ +p:
56 allf_succ(t, p, ht)
57 case Con{True{}, +t} 1n+ +p:
58 allf_succ(t, p, ht)
59
60def invf_succ(+n: Nat, +xs: List<&2, Bool>, +h: {Nat.is_lt(n, SC.length(Bool, xs)) == True{} : Bool}, +g: {ST.invf(n, xs) == True{} : Bool}) -> {ST.invf(1n+n, xs) == True{} : Bool}:
61 L.and_intro(Nat.is_le(1n+n, SC.length(Bool, xs)), BL.allf(SC.drop(Bool, xs, 1n+n)), N.lt_succ_le_succ(n, SC.length(Bool, xs), h), allf_succ(xs, n, ST.inv_tail(n, xs, g)))
62
63# push of a zero bit into stored space: nothing is written
64def push_zero(+n: Nat, +xs: List<&2, Bool>, +h: {Nat.is_lt(n, SC.length(Bool, xs)) == True{} : Bool}, +g: {ST.invf(n, xs) == True{} : Bool}) -> {SC.take(Bool, xs, 1n+n) == SC.snoc(Bool, SC.take(Bool, xs, n), False{}) : List<&2, Bool>}:
65 LX.take_succ(Bool, xs, n, False{}, nth_false(xs, n, h, ST.inv_tail(n, xs, g)))
66
67# push of any bit into stored space: bit n is written
68def push_put(+n: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {Nat.is_lt(n, SC.length(Bool, xs)) == True{} : Bool}) -> {SC.take(Bool, SC.update(Bool, xs, n, v), 1n+n) == SC.snoc(Bool, SC.take(Bool, xs, n), v) : List<&2, Bool>}:
69 LX.take_update_succ(Bool, xs, n, v, h)
70
71def push_put_inv(+n: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {Nat.is_lt(n, SC.length(Bool, xs)) == True{} : Bool}, +g: {ST.invf(n, xs) == True{} : Bool}) -> {ST.invf(1n+n, SC.update(Bool, xs, n, v)) == True{} : Bool}:
72 %Equal.sym(Nat, SC.length(Bool, SC.update(Bool, xs, n, v)), SC.length(Bool, xs), LL.length_update(Bool, xs, n, v)) : {Bool.and(Nat.is_le(1n+n, _), BL.allf(SC.drop(Bool, SC.update(Bool, xs, n, v), 1n+n))) == True{} : Bool}
73 %Equal.sym(List<&2, Bool>, SC.drop(Bool, SC.update(Bool, xs, n, v), 1n+n), SC.drop(Bool, xs, 1n+n), LX.drop_update(Bool, xs, n, v)) : {Bool.and(Nat.is_le(1n+n, SC.length(Bool, xs)), BL.allf(_)) == True{} : Bool}
74 invf_succ(n, xs, h, g)
75
76# ---- push into a new word ----
77
78
79def flat_snoc(+ws: List<&2, U32>, +x: U32) -> {ST.flat(SC.snoc(U32, ws, x)) == SC.append(Bool, ST.flat(ws), W.ubits(x)) : List<&2, Bool>}:
80 match ws:
81 case Nil{}:
82 LL.append_nil(Bool, W.ubits(x))
83 case Con{+w, +t}:
84 %Equal.sym(List<&2, Bool>, ST.flat(SC.snoc(U32, t, x)), SC.append(Bool, ST.flat(t), W.ubits(x)), flat_snoc(t, x)) : {SC.append(Bool, W.ubits(w), _) == SC.append(Bool, SC.append(Bool, W.ubits(w), ST.flat(t)), W.ubits(x)) : List<&2, Bool>}
85 Equal.sym(List<&2, Bool>, SC.append(Bool, SC.append(Bool, W.ubits(w), ST.flat(t)), W.ubits(x)), SC.append(Bool, W.ubits(w), SC.append(Bool, ST.flat(t), W.ubits(x))), LL.append_assoc(Bool, W.ubits(w), ST.flat(t), W.ubits(x)))
86
87def sub_succ_self(+n: Nat) -> {Nat.sub(1n+n, n) == 1n : Nat}:
88 match n:
89 case 0n:
90 {==}
91 case 1n+ +p:
92 sub_succ_self(p)
93
94def first_bit(+v: Bool) -> {SC.take(Bool, W.ubits(B.word_put(v, 0, 0n)), 1n) == Con{v, Nil{}} : List<&2, Bool>}:
95 match v:
96 case True{}:
97 {==}
98 case False{}:
99 {==}
100
101def rest_zero(+v: Bool) -> {BL.allf(SC.drop(Bool, W.ubits(B.word_put(v, 0, 0n)), 1n)) == True{} : Bool}:
102 match v:
103 case True{}:
104 {==}
105 case False{}:
106 {==}
107
108def drop_append_succ(+xs: List<&2, Bool>, +ys: List<&2, Bool>) -> {SC.drop(Bool, SC.append(Bool, xs, ys), 1n+SC.length(Bool, xs)) == SC.drop(Bool, ys, 1n) : List<&2, Bool>}:
109 match xs:
110 case Nil{}:
111 {==}
112 case Con{+h, +t}:
113 drop_append_succ(t, ys)
114
115# the new word holds bit |F| = v in its low position, zeros above
116def push_new_abs(+ws: List<&2, U32>, +v: Bool) -> {SC.take(Bool, ST.flat(SC.snoc(U32, ws, B.word_put(v, 0, 0n))), 1n+SC.length(Bool, ST.flat(ws))) == SC.snoc(Bool, SC.take(Bool, ST.flat(ws), SC.length(Bool, ST.flat(ws))), v) : List<&2, Bool>}:
117 %Equal.sym(List<&2, Bool>, ST.flat(SC.snoc(U32, ws, B.word_put(v, 0, 0n))), SC.append(Bool, ST.flat(ws), W.ubits(B.word_put(v, 0, 0n))), flat_snoc(ws, B.word_put(v, 0, 0n))) : {SC.take(Bool, _, 1n+SC.length(Bool, ST.flat(ws))) == SC.snoc(Bool, SC.take(Bool, ST.flat(ws), SC.length(Bool, ST.flat(ws))), v) : List<&2, Bool>}
118 %Equal.sym(List<&2, Bool>, SC.take(Bool, SC.append(Bool, ST.flat(ws), W.ubits(B.word_put(v, 0, 0n))), 1n+SC.length(Bool, ST.flat(ws))), SC.append(Bool, ST.flat(ws), SC.take(Bool, W.ubits(B.word_put(v, 0, 0n)), Nat.sub(1n+SC.length(Bool, ST.flat(ws)), SC.length(Bool, ST.flat(ws))))), LL.sc_take_append_right(Bool, ST.flat(ws), W.ubits(B.word_put(v, 0, 0n)), 1n+SC.length(Bool, ST.flat(ws)), N.le_succ(SC.length(Bool, ST.flat(ws))))) : {_ == SC.snoc(Bool, SC.take(Bool, ST.flat(ws), SC.length(Bool, ST.flat(ws))), v) : List<&2, Bool>}
119 %Equal.sym(Nat, Nat.sub(1n+SC.length(Bool, ST.flat(ws)), SC.length(Bool, ST.flat(ws))), 1n, sub_succ_self(SC.length(Bool, ST.flat(ws)))) : {SC.append(Bool, ST.flat(ws), SC.take(Bool, W.ubits(B.word_put(v, 0, 0n)), _)) == SC.snoc(Bool, SC.take(Bool, ST.flat(ws), SC.length(Bool, ST.flat(ws))), v) : List<&2, Bool>}
120 %Equal.sym(List<&2, Bool>, SC.take(Bool, W.ubits(B.word_put(v, 0, 0n)), 1n), Con{v, Nil{}}, first_bit(v)) : {SC.append(Bool, ST.flat(ws), _) == SC.snoc(Bool, SC.take(Bool, ST.flat(ws), SC.length(Bool, ST.flat(ws))), v) : List<&2, Bool>}
121 %Equal.sym(List<&2, Bool>, SC.take(Bool, ST.flat(ws), SC.length(Bool, ST.flat(ws))), ST.flat(ws), LX.take_all(Bool, ST.flat(ws))) : {SC.append(Bool, ST.flat(ws), Con{v, Nil{}}) == SC.snoc(Bool, _, v) : List<&2, Bool>}
122 Equal.sym(List<&2, Bool>, SC.snoc(Bool, ST.flat(ws), v), SC.append(Bool, ST.flat(ws), Con{v, Nil{}}), LL.snoc_append(Bool, ST.flat(ws), v))
123
124def push_new_inv(+ws: List<&2, U32>, +v: Bool) -> {ST.invf(1n+SC.length(Bool, ST.flat(ws)), ST.flat(SC.snoc(U32, ws, B.word_put(v, 0, 0n)))) == True{} : Bool}:
125 %Equal.sym(List<&2, Bool>, ST.flat(SC.snoc(U32, ws, B.word_put(v, 0, 0n))), SC.append(Bool, ST.flat(ws), W.ubits(B.word_put(v, 0, 0n))), flat_snoc(ws, B.word_put(v, 0, 0n))) : {ST.invf(1n+SC.length(Bool, ST.flat(ws)), _) == True{} : Bool}
126 %Equal.sym(Nat, SC.length(Bool, SC.append(Bool, ST.flat(ws), W.ubits(B.word_put(v, 0, 0n)))), Nat.add(SC.length(Bool, ST.flat(ws)), SC.length(Bool, W.ubits(B.word_put(v, 0, 0n)))), LL.length_append(Bool, ST.flat(ws), W.ubits(B.word_put(v, 0, 0n)))) : {Bool.and(Nat.is_le(1n+SC.length(Bool, ST.flat(ws)), _), BL.allf(SC.drop(Bool, SC.append(Bool, ST.flat(ws), W.ubits(B.word_put(v, 0, 0n))), 1n+SC.length(Bool, ST.flat(ws))))) == True{} : Bool}
127 %Equal.sym(Nat, SC.length(Bool, W.ubits(B.word_put(v, 0, 0n))), 32n, W.ulen(B.word_put(v, 0, 0n))) : {Bool.and(Nat.is_le(1n+SC.length(Bool, ST.flat(ws)), Nat.add(SC.length(Bool, ST.flat(ws)), _)), BL.allf(SC.drop(Bool, SC.append(Bool, ST.flat(ws), W.ubits(B.word_put(v, 0, 0n))), 1n+SC.length(Bool, ST.flat(ws))))) == True{} : Bool}
128 %Equal.sym(Nat, Nat.add(SC.length(Bool, ST.flat(ws)), 32n), 1n+Nat.add(SC.length(Bool, ST.flat(ws)), 31n), N.add_succ(SC.length(Bool, ST.flat(ws)), 31n)) : {Bool.and(Nat.is_le(1n+SC.length(Bool, ST.flat(ws)), _), BL.allf(SC.drop(Bool, SC.append(Bool, ST.flat(ws), W.ubits(B.word_put(v, 0, 0n))), 1n+SC.length(Bool, ST.flat(ws))))) == True{} : Bool}
129 %Equal.sym(List<&2, Bool>, SC.drop(Bool, SC.append(Bool, ST.flat(ws), W.ubits(B.word_put(v, 0, 0n))), 1n+SC.length(Bool, ST.flat(ws))), SC.drop(Bool, W.ubits(B.word_put(v, 0, 0n)), 1n), drop_append_succ(ST.flat(ws), W.ubits(B.word_put(v, 0, 0n)))) : {Bool.and(Nat.is_le(1n+SC.length(Bool, ST.flat(ws)), 1n+Nat.add(SC.length(Bool, ST.flat(ws)), 31n)), BL.allf(_)) == True{} : Bool}
130 L.and_intro(Nat.is_le(1n+SC.length(Bool, ST.flat(ws)), 1n+Nat.add(SC.length(Bool, ST.flat(ws)), 31n)), BL.allf(SC.drop(Bool, W.ubits(B.word_put(v, 0, 0n)), 1n)), N.le_add_right(SC.length(Bool, ST.flat(ws)), 31n), rest_zero(v))
131
132# ---- pop ----
133
134def pop_spec(+l: Maybe<&2, Nat>, +c: Nat, +ys: List<&2, Bool>, +b: Bool) -> {S.pop(l, c, SC.snoc(Bool, ys, b)) == (S.M{l, c, ys}, E.OBit{Done{b}}) : S.Model & E.Obs}:
135 match ys:
136 case Nil{}:
137 {==}
138 case Con{+h, +t}:
139 %Equal.sym(List<&2, Bool>, SC.init(Bool, SC.snoc(Bool, Con{h, t}, b)), Con{h, t}, LL.init_snoc(Bool, Con{h, t}, b)) : {(S.M{l, c, _}, E.OBit{S.last_bit(SC.last(Bool, SC.snoc(Bool, Con{h, t}, b)))}) == (S.M{l, c, Con{h, t}}, E.OBit{Done{b}}) : S.Model & E.Obs}
140 %Equal.sym(Maybe<&2, Bool>, SC.last(Bool, SC.snoc(Bool, Con{h, t}, b)), Some{b}, LL.last_snoc(Bool, Con{h, t}, b)) : {(S.M{l, c, Con{h, t}}, E.OBit{S.last_bit(_)}) == (S.M{l, c, Con{h, t}}, E.OBit{Done{b}}) : S.Model & E.Obs}
141 {==}
142
143def lt_of_inv(+m: Nat, +xs: List<&2, Bool>, +g: {ST.invf(1n+m, xs) == True{} : Bool}) -> {Nat.is_lt(m, SC.length(Bool, xs)) == True{} : Bool}:
144 N.succ_le_lt(m, SC.length(Bool, xs), ST.inv_le(1n+m, xs, g))
145
146# a zero last bit: the stored bits stay as they are
147def pop_keep_inv(+m: Nat, +xs: List<&2, Bool>, +g: {ST.invf(1n+m, xs) == True{} : Bool}, +hb: {SC.nth(Bool, xs, m) == Some{False{}} : Maybe<&2, Bool>}) -> {ST.invf(m, xs) == True{} : Bool}:
148 %Equal.sym(List<&2, Bool>, SC.drop(Bool, xs, m), Con{False{}, SC.drop(Bool, xs, 1n+m)}, LX.drop_cons(Bool, xs, m, False{}, hb)) : {Bool.and(Nat.is_le(m, SC.length(Bool, xs)), BL.allf(_)) == True{} : Bool}
149 L.and_intro(Nat.is_le(m, SC.length(Bool, xs)), BL.allf(SC.drop(Bool, xs, 1n+m)), N.lt_le(m, SC.length(Bool, xs), lt_of_inv(m, xs, g)), ST.inv_tail(1n+m, xs, g))
150
151# a one last bit is cleared
152def pop_clear_inv(+m: Nat, +xs: List<&2, Bool>, +g: {ST.invf(1n+m, xs) == True{} : Bool}) -> {ST.invf(m, SC.update(Bool, xs, m, False{})) == True{} : Bool}:
153 +hz = LL.nth_update_same(Bool, xs, m, False{}, lt_of_inv(m, xs, g))
154 %Equal.sym(List<&2, Bool>, SC.drop(Bool, SC.update(Bool, xs, m, False{}), m), Con{False{}, SC.drop(Bool, SC.update(Bool, xs, m, False{}), 1n+m)}, LX.drop_cons(Bool, SC.update(Bool, xs, m, False{}), m, False{}, hz)) : {Bool.and(Nat.is_le(m, SC.length(Bool, SC.update(Bool, xs, m, False{}))), BL.allf(_)) == True{} : Bool}
155 %Equal.sym(List<&2, Bool>, SC.drop(Bool, SC.update(Bool, xs, m, False{}), 1n+m), SC.drop(Bool, xs, 1n+m), LX.drop_update(Bool, xs, m, False{})) : {Bool.and(Nat.is_le(m, SC.length(Bool, SC.update(Bool, xs, m, False{}))), BL.allf(_)) == True{} : Bool}
156 %Equal.sym(Nat, SC.length(Bool, SC.update(Bool, xs, m, False{})), SC.length(Bool, xs), LL.length_update(Bool, xs, m, False{})) : {Bool.and(Nat.is_le(m, _), BL.allf(SC.drop(Bool, xs, 1n+m))) == True{} : Bool}
157 L.and_intro(Nat.is_le(m, SC.length(Bool, xs)), BL.allf(SC.drop(Bool, xs, 1n+m)), N.lt_le(m, SC.length(Bool, xs), lt_of_inv(m, xs, g)), ST.inv_tail(1n+m, xs, g))
158
159# ---- to_list: one word of the first n bits ----
160
161def word_bits(+m: Nat, +x: U32, +rest: List<&2, Bool>, +h: {Nat.is_le(m, 32n) == True{} : Bool}) -> {BLI.word_bits(m, x, rest) == SC.append(Bool, SC.take(Bool, W.ubits(x), m), rest) : List<&2, Bool>}:
162 match m x:
163 case 0n U32{w}:
164 match w:
165 case WCon{b, t}:
166 {==}
167 case 1n+ +p U32{w}:
168 match w:
169 case WCon{+b, +t}:
170 %Equal.sym(Bool, B.low(U32{WCon{b, t}}), b, W.low_word(b, t)) : {Con{_, BLI.word_bits(p, U32.shr(U32{WCon{b, t}}), rest)} == Con{b, SC.append(Bool, SC.take(Bool, W.wbits(31n, t), p), rest)} : List<&2, Bool>}
171 %Equal.sym(List<&2, Bool>, BLI.word_bits(p, U32.shr(U32{WCon{b, t}}), rest), SC.append(Bool, SC.take(Bool, W.ubits(U32.shr(U32{WCon{b, t}})), p), rest), word_bits(p, U32.shr(U32{WCon{b, t}}), rest, N.le_trans(p, 1n+p, 32n, N.le_succ(p), h))) : {Con{b, _} == Con{b, SC.append(Bool, SC.take(Bool, W.wbits(31n, t), p), rest)} : List<&2, Bool>}
172 %Equal.sym(List<&2, Bool>, W.ubits(U32.shr(U32{WCon{b, t}})), SC.snoc(Bool, W.wbits(31n, t), False{}), W.u_shr(b, t)) : {Con{b, SC.append(Bool, SC.take(Bool, _, p), rest)} == Con{b, SC.append(Bool, SC.take(Bool, W.wbits(31n, t), p), rest)} : List<&2, Bool>}
173 %Equal.sym(List<&2, Bool>, SC.snoc(Bool, W.wbits(31n, t), False{}), SC.append(Bool, W.wbits(31n, t), Con{False{}, Nil{}}), LL.snoc_append(Bool, W.wbits(31n, t), False{})) : {Con{b, SC.append(Bool, SC.take(Bool, _, p), rest)} == Con{b, SC.append(Bool, SC.take(Bool, W.wbits(31n, t), p), rest)} : List<&2, Bool>}
174 +h31 = L.subst(Nat, z => {Nat.is_le(p, z) == True{} : Bool}, 31n, SC.length(Bool, W.wbits(31n, t)), Equal.sym(Nat, SC.length(Bool, W.wbits(31n, t)), 31n, W.len_wbits(31n, t)), h)
175 %Equal.sym(List<&2, Bool>, SC.take(Bool, SC.append(Bool, W.wbits(31n, t), Con{False{}, Nil{}}), p), SC.take(Bool, W.wbits(31n, t), p), LL.sc_take_append_left(Bool, W.wbits(31n, t), Con{False{}, Nil{}}, p, h31)) : {Con{b, SC.append(Bool, _, rest)} == Con{b, SC.append(Bool, SC.take(Bool, W.wbits(31n, t), p), rest)} : List<&2, Bool>}
176 {==}
177
178def sub_le_zero(+a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.sub(a, b) == 0n : Nat}:
179 match a b:
180 case 0n 0n:
181 {==}
182 case 0n 1n+r:
183 {==}
184 case 1n+p 0n:
185 Empty.absurd({Nat.sub(1n+p, 0n) == 0n : Nat}, L.false_true(h))
186 case 1n+ +p 1n+ +r:
187 sub_le_zero(p, r, h)
188
189def sub_sub(+b: Nat, +a: Nat, +c: Nat) -> {Nat.sub(Nat.sub(a, b), c) == Nat.sub(a, Nat.add(c, b)) : Nat}:
190 match b a:
191 case 0n 0n:
192 %Equal.sym(Nat, Nat.add(c, 0n), c, N.add_zero(c)) : {Nat.sub(0n, c) == Nat.sub(0n, _) : Nat}
193 {==}
194 case 0n 1n+ +q:
195 %Equal.sym(Nat, Nat.add(c, 0n), c, N.add_zero(c)) : {Nat.sub(1n+q, c) == Nat.sub(1n+q, _) : Nat}
196 {==}
197 case 1n+ +p 0n:
198 %Equal.sym(Nat, Nat.add(c, 1n+p), 1n+Nat.add(c, p), N.add_succ(c, p)) : {Nat.sub(0n, c) == Nat.sub(0n, _) : Nat}
199 sub_le_zero(0n, c, N.zero_le(c))
200 case 1n+ +p 1n+ +q:
201 %Equal.sym(Nat, Nat.add(c, 1n+p), 1n+Nat.add(c, p), N.add_succ(c, p)) : {Nat.sub(Nat.sub(q, p), c) == Nat.sub(1n+q, _) : Nat}
202 sub_sub(p, q, c)
203
204# the first s bits of 32 bits then more: a prefix of the word, then of the rest
205def take_word(+a: List<&2, Bool>, +bs: List<&2, Bool>, +s: Nat, +ha: {SC.length(Bool, a) == 32n : Nat}, c: Bool, +ec: {Nat.is_lt(32n, s) == c : Bool}) -> {SC.take(Bool, SC.append(Bool, a, bs), s) == SC.append(Bool, SC.take(Bool, a, Nat.min(32n, s)), SC.take(Bool, bs, Nat.sub(s, 32n))) : List<&2, Bool>}:
206 match c:
207 case True{}:
208 %Equal.sym(Nat, Nat.min(32n, s), 32n, N.min_left(32n, s, ec)) : {SC.take(Bool, SC.append(Bool, a, bs), s) == SC.append(Bool, SC.take(Bool, a, _), SC.take(Bool, bs, Nat.sub(s, 32n))) : List<&2, Bool>}
209 +hle = L.subst(Nat, z => {Nat.is_le(z, s) == True{} : Bool}, 32n, SC.length(Bool, a), Equal.sym(Nat, SC.length(Bool, a), 32n, ha), N.lt_le(32n, s, ec))
210 %Equal.sym(List<&2, Bool>, SC.take(Bool, SC.append(Bool, a, bs), s), SC.append(Bool, a, SC.take(Bool, bs, Nat.sub(s, SC.length(Bool, a)))), LL.sc_take_append_right(Bool, a, bs, s, hle)) : {_ == SC.append(Bool, SC.take(Bool, a, 32n), SC.take(Bool, bs, Nat.sub(s, 32n))) : List<&2, Bool>}
211 %Equal.sym(Nat, SC.length(Bool, a), 32n, ha) : {SC.append(Bool, a, SC.take(Bool, bs, Nat.sub(s, _))) == SC.append(Bool, SC.take(Bool, a, 32n), SC.take(Bool, bs, Nat.sub(s, 32n))) : List<&2, Bool>}
212 +ht = L.subst(Nat, z => {SC.take(Bool, a, z) == a : List<&2, Bool>}, SC.length(Bool, a), 32n, ha, LX.take_all(Bool, a))
213 %Equal.sym(List<&2, Bool>, SC.take(Bool, a, 32n), a, ht) : {SC.append(Bool, a, SC.take(Bool, bs, Nat.sub(s, 32n))) == SC.append(Bool, _, SC.take(Bool, bs, Nat.sub(s, 32n))) : List<&2, Bool>}
214 {==}
215 case False{}:
216 %Equal.sym(Nat, Nat.min(32n, s), s, N.min_right(32n, s, ec)) : {SC.take(Bool, SC.append(Bool, a, bs), s) == SC.append(Bool, SC.take(Bool, a, _), SC.take(Bool, bs, Nat.sub(s, 32n))) : List<&2, Bool>}
217 +hs = N.not_lt_le(32n, s, ec)
218 %Equal.sym(Nat, Nat.sub(s, 32n), 0n, sub_le_zero(s, 32n, hs)) : {SC.take(Bool, SC.append(Bool, a, bs), s) == SC.append(Bool, SC.take(Bool, a, s), SC.take(Bool, bs, _)) : List<&2, Bool>}
219 %Equal.sym(List<&2, Bool>, SC.take(Bool, bs, 0n), Nil{}, LL.sc_take_zero(Bool, bs)) : {SC.take(Bool, SC.append(Bool, a, bs), s) == SC.append(Bool, SC.take(Bool, a, s), _) : List<&2, Bool>}
220 %Equal.sym(List<&2, Bool>, SC.append(Bool, SC.take(Bool, a, s), Nil{}), SC.take(Bool, a, s), LL.append_nil(Bool, SC.take(Bool, a, s))) : {SC.take(Bool, SC.append(Bool, a, bs), s) == _ : List<&2, Bool>}
221 LL.sc_take_append_left(Bool, a, bs, s, L.subst(Nat, z => {Nat.is_le(s, z) == True{} : Bool}, 32n, SC.length(Bool, a), Equal.sym(Nat, SC.length(Bool, a), 32n, ha), hs))
222
223def min_le(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.min(a, b), a) == True{} : Bool}:
224 match a b:
225 case 0n 0n:
226 {==}
227 case 0n 1n+r:
228 {==}
229 case 1n+p 0n:
230 {==}
231 case 1n+ +p 1n+ +r:
232 min_le(p, r)
233
234
235# word q of the first n bits: words q.. restricted to bits below n
236def bits_step(+ws: List<&2, U32>, +n: Nat, +q: Nat, +x: U32, +hx: {SC.nth(U32, ws, q) == Some{x} : Maybe<&2, U32>}) -> {SC.take(Bool, ST.flat(SC.drop(U32, ws, q)), Nat.sub(n, Nat.mul(q, 32n))) == BLI.word_bits(Nat.min(32n, Nat.sub(n, Nat.mul(q, 32n))), x, SC.take(Bool, ST.flat(SC.drop(U32, ws, 1n+q)), Nat.sub(n, Nat.mul(1n+q, 32n)))) : List<&2, Bool>}:
237 %Equal.sym(List<&2, U32>, SC.drop(U32, ws, q), Con{x, SC.drop(U32, ws, 1n+q)}, LX.drop_cons(U32, ws, q, x, hx)) : {SC.take(Bool, ST.flat(_), Nat.sub(n, Nat.mul(q, 32n))) == BLI.word_bits(Nat.min(32n, Nat.sub(n, Nat.mul(q, 32n))), x, SC.take(Bool, ST.flat(SC.drop(U32, ws, 1n+q)), Nat.sub(n, Nat.mul(1n+q, 32n)))) : List<&2, Bool>}
238 %sub_sub(Nat.mul(q, 32n), n, 32n) : {SC.take(Bool, SC.append(Bool, W.ubits(x), ST.flat(SC.drop(U32, ws, 1n+q))), Nat.sub(n, Nat.mul(q, 32n))) == BLI.word_bits(Nat.min(32n, Nat.sub(n, Nat.mul(q, 32n))), x, SC.take(Bool, ST.flat(SC.drop(U32, ws, 1n+q)), _)) : List<&2, Bool>}
239 %Equal.sym(List<&2, Bool>, SC.take(Bool, SC.append(Bool, W.ubits(x), ST.flat(SC.drop(U32, ws, 1n+q))), Nat.sub(n, Nat.mul(q, 32n))), SC.append(Bool, SC.take(Bool, W.ubits(x), Nat.min(32n, Nat.sub(n, Nat.mul(q, 32n)))), SC.take(Bool, ST.flat(SC.drop(U32, ws, 1n+q)), Nat.sub(Nat.sub(n, Nat.mul(q, 32n)), 32n))), take_word(W.ubits(x), ST.flat(SC.drop(U32, ws, 1n+q)), Nat.sub(n, Nat.mul(q, 32n)), W.ulen(x), Nat.is_lt(32n, Nat.sub(n, Nat.mul(q, 32n))), {==})) : {_ == BLI.word_bits(Nat.min(32n, Nat.sub(n, Nat.mul(q, 32n))), x, SC.take(Bool, ST.flat(SC.drop(U32, ws, 1n+q)), Nat.sub(Nat.sub(n, Nat.mul(q, 32n)), 32n))) : List<&2, Bool>}
240 Equal.sym(List<&2, Bool>, BLI.word_bits(Nat.min(32n, Nat.sub(n, Nat.mul(q, 32n))), x, SC.take(Bool, ST.flat(SC.drop(U32, ws, 1n+q)), Nat.sub(Nat.sub(n, Nat.mul(q, 32n)), 32n))), SC.append(Bool, SC.take(Bool, W.ubits(x), Nat.min(32n, Nat.sub(n, Nat.mul(q, 32n)))), SC.take(Bool, ST.flat(SC.drop(U32, ws, 1n+q)), Nat.sub(Nat.sub(n, Nat.mul(q, 32n)), 32n))), word_bits(Nat.min(32n, Nat.sub(n, Nat.mul(q, 32n))), x, SC.take(Bool, ST.flat(SC.drop(U32, ws, 1n+q)), Nat.sub(Nat.sub(n, Nat.mul(q, 32n)), 32n)), min_le(32n, Nat.sub(n, Nat.mul(q, 32n)))))
241
242# ---- push helpers ----
243
244def below_eq(+l: Maybe<&2, Nat>, +n: Nat) -> {BLI.below(l, n) == S.below(l, n) : Bool}:
245 match l:
246 case None{}:
247 {==}
248 case Some{k}:
249 {==}
250
251def upd_snoc_end(+p: List<&2, Bool>, +x: Bool, +v: Bool) -> {SC.update(Bool, SC.snoc(Bool, p, x), SC.length(Bool, p), v) == SC.snoc(Bool, p, v) : List<&2, Bool>}:
252 match p:
253 case Nil{}:
254 {==}
255 case Con{+h, +t}:
256 LL.cons_cong(Bool, h, SC.update(Bool, SC.snoc(Bool, t, x), SC.length(Bool, t), v), SC.snoc(Bool, t, v), upd_snoc_end(t, x, v))
257
258def lt_plus(+k: Nat, +x: Nat) -> {Nat.is_lt(x, Nat.add(1n+k, x)) == True{} : Bool}:
259 match k:
260 case 0n:
261 N.lt_succ(x)
262 case 1n+ +p:
263 N.lt_le_trans(x, Nat.add(1n+p, x), 1n+Nat.add(1n+p, x), lt_plus(p, x), N.le_succ(Nat.add(1n+p, x)))
264
265def lt_mul32(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(a, 32n), Nat.mul(b, 32n)) == True{} : Bool}:
266 +h1 = AT.mul_le(1n+a, b, 32n, N.lt_succ_le_succ(a, b, h))
267 N.lt_le_trans(Nat.mul(a, 32n), Nat.mul(1n+a, 32n), Nat.mul(b, 32n), lt_plus(31n, Nat.mul(a, 32n)), h1)
268
269def mul32_lt(+a: Nat, +b: Nat, c: Bool, +ec: {Nat.is_lt(a, b) == c : Bool}, +h: {Nat.is_lt(Nat.mul(a, 32n), Nat.mul(b, 32n)) == True{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
270 match c:
271 case True{}:
272 ec
273 case False{}:
274 Empty.absurd({Nat.is_lt(a, b) == True{} : Bool}, L.true_not_false(Nat.is_lt(Nat.mul(a, 32n), Nat.mul(b, 32n)), h, N.le_not_lt(Nat.mul(a, 32n), Nat.mul(b, 32n), AT.mul_le(b, a, 32n, N.not_lt_le(a, b, ec)))))
275
276def mul32_nlt(+a: Nat, +b: Nat, c: Bool, +ec: {Nat.is_lt(a, b) == c : Bool}, +h: {Nat.is_lt(Nat.mul(a, 32n), Nat.mul(b, 32n)) == False{} : Bool}) -> {Nat.is_lt(a, b) == False{} : Bool}:
277 match c:
278 case False{}:
279 ec
280 case True{}:
281 Empty.absurd({Nat.is_lt(a, b) == False{} : Bool}, L.true_not_false(Nat.is_lt(Nat.mul(a, 32n), Nat.mul(b, 32n)), lt_mul32(a, b, ec), h))