PROOF.bend

lawful-fields@0.1.1.0 · 166 lines · 10 definitions

1import Base
2import lawful-bytes@0.1.1.0/defs.bend as D
3import lawful-fields@0.1.1.0/defs.bend as F
4import lawful-fields@0.1.1.0/fields.bend as C
5import lawful-fields@0.1.1.0/LAWS.bend as L
6import lawful-bytes@0.1.1.0/proof_core.bend as BC
7import lawful-fields@0.1.1.0/proof_list.bend as Q
8import lawful-fields@0.1.1.0/proof_cut.bend as Z
9import lawful-fields@0.1.1.0/proof_num.bend as NU
10import lawful-fields@0.1.1.0/proof_digits.bend as DG
11
12# Proofs of the laws: `def L.name` proves `law name` of LAWS.bend. A Bytes can
13# be used once, so each law about one goes through lawful-bytes' mirror
14# (BC.bmirror): BC.BT(len, t) with a Tree<U32> t.
15
16# Laws about a Bytes
17# ==================
18
19# One wrapper per law (written mechanically from LAWS.bend): it mirrors each
20# Bytes b, rewrites the goal, transports the hypotheses and calls the mirror
21# lemma `name_t`, which is law `name` with b replaced by BC.BT(l_b, t_b).
22
23def cut_view.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +sep: U32, +n: Nat, h: {D.ok(b, d) == True{} : Bool}, hft: {U32.is_le(from, to) == True{} : Bool}, ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}, hs: {U32.is_lt(sep, 256) == True{} : Bool}, m_b: BC.BMirror(b)) ->
24  {F.pieces(Pair.snd(D.Bytes, List<&2, U32>, C.cut(b, from, to, sep, n)), D.view(b), U32.to_nat(from)) == List.take(&2, List<&2, U32>, F.split(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), n) : List<&2, List<&2, U32>>}:
25  (+l_b, m2_b) = m_b
26  (+t_b, +e_b) = m2_b
27  %e_b : {F.pieces(Pair.snd(D.Bytes, List<&2, U32>, C.cut(_, from, to, sep, n)), D.view(_), U32.to_nat(from)) == List.take(&2, List<&2, U32>, F.split(D.slice(D.view(_), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), n) : List<&2, List<&2, U32>>}
28  +h_t = BC.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
29  +ht_t = BC.tr(x => {Nat.is_le(U32.to_nat(to), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, ht)
30  Z.cut_view_t(l_b, t_b, d, from, to, sep, n, h_t, hft, ht_t, hs)
31
32def L.cut_view(b, d, from, to, sep, n, h, hft, ht, hs):
33  cut_view.go(b, d, from, to, sep, n, h, hft, ht, hs, BC.bmirror(b))
34
35def cut_ends.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +sep: U32, +n: Nat, h: {D.ok(b, d) == True{} : Bool}, hft: {U32.is_le(from, to) == True{} : Bool}, ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}, hs: {U32.is_lt(sep, 256) == True{} : Bool}, m_b: BC.BMirror(b)) ->
36  {F.nats(Pair.snd(D.Bytes, List<&2, U32>, C.cut(b, from, to, sep, n))) == List.take(&2, Nat, F.ends(F.split(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), U32.to_nat(from)), n) : List<&2, Nat>}:
37  (+l_b, m2_b) = m_b
38  (+t_b, +e_b) = m2_b
39  %e_b : {F.nats(Pair.snd(D.Bytes, List<&2, U32>, C.cut(_, from, to, sep, n))) == List.take(&2, Nat, F.ends(F.split(D.slice(D.view(_), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), U32.to_nat(from)), n) : List<&2, Nat>}
40  +h_t = BC.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
41  +ht_t = BC.tr(x => {Nat.is_le(U32.to_nat(to), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, ht)
42  Z.cut_ends_t(l_b, t_b, d, from, to, sep, n, h_t, hft, ht_t, hs)
43
44def L.cut_ends(b, d, from, to, sep, n, h, hft, ht, hs):
45  cut_ends.go(b, d, from, to, sep, n, h, hft, ht, hs, BC.bmirror(b))
46
47def cut_bounds.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, +sep: U32, +n: Nat, h: {D.ok(b, d) == True{} : Bool}, hft: {U32.is_le(from, to) == True{} : Bool}, ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}, hs: {U32.is_lt(sep, 256) == True{} : Bool}, m_b: BC.BMirror(b)) ->
48  {F.within(Pair.snd(D.Bytes, List<&2, U32>, C.cut(b, from, to, sep, n)), U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}:
49  (+l_b, m2_b) = m_b
50  (+t_b, +e_b) = m2_b
51  %e_b : {F.within(Pair.snd(D.Bytes, List<&2, U32>, C.cut(_, from, to, sep, n)), U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}
52  +h_t = BC.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
53  +ht_t = BC.tr(x => {Nat.is_le(U32.to_nat(to), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, ht)
54  Z.cut_bounds_t(l_b, t_b, d, from, to, sep, n, h_t, hft, ht_t, hs)
55
56def L.cut_bounds(b, d, from, to, sep, n, h, hft, ht, hs):
57  cut_bounds.go(b, d, from, to, sep, n, h, hft, ht, hs, BC.bmirror(b))
58
59def cut_pair.go(-b: D.Bytes, +from: U32, +to: U32, +sep: U32, +n: Nat, m_b: BC.BMirror(b)) ->
60  {C.cut(b, from, to, sep, n) == (b, Pair.snd(D.Bytes, List<&2, U32>, C.cut(b, from, to, sep, n))) : D.Bytes & List<&2, U32>}:
61  (+l_b, m2_b) = m_b
62  (+t_b, +e_b) = m2_b
63  %e_b : {C.cut(_, from, to, sep, n) == (_, Pair.snd(D.Bytes, List<&2, U32>, C.cut(_, from, to, sep, n))) : D.Bytes & List<&2, U32>}
64  Z.cut_pair_t(l_b, t_b, from, to, sep, n)
65
66def L.cut_pair(b, from, to, sep, n):
67  cut_pair.go(b, from, to, sep, n, BC.bmirror(b))
68
69def num_view.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, h: {D.ok(b, d) == True{} : Bool}, hft: {U32.is_le(from, to) == True{} : Bool}, ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}, m_b: BC.BMirror(b)) ->
70  {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(b, from, to))) == F.decb(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), Nat.pow(2n, 32n)) : Maybe<&2, Nat>}:
71  (+l_b, m2_b) = m_b
72  (+t_b, +e_b) = m2_b
73  %e_b : {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(_, from, to))) == F.decb(D.slice(D.view(_), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), Nat.pow(2n, 32n)) : Maybe<&2, Nat>}
74  +h_t = BC.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
75  +ht_t = BC.tr(x => {Nat.is_le(U32.to_nat(to), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, ht)
76  NU.num_view_t(l_b, t_b, d, from, to, h_t, hft, ht_t)
77
78def L.num_view(b, d, from, to, h, hft, ht):
79  num_view.go(b, d, from, to, h, hft, ht, BC.bmirror(b))
80
81def num_pair.go(-b: D.Bytes, +from: U32, +to: U32, m_b: BC.BMirror(b)) ->
82  {C.num(b, from, to) == (b, Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(b, from, to))) : D.Bytes & Maybe<&2, U32>}:
83  (+l_b, m2_b) = m_b
84  (+t_b, +e_b) = m2_b
85  %e_b : {C.num(_, from, to) == (_, Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(_, from, to))) : D.Bytes & Maybe<&2, U32>}
86  NU.num_pair_t(l_b, t_b, from, to)
87
88def L.num_pair(b, from, to):
89  num_pair.go(b, from, to, BC.bmirror(b))
90
91def digits_view.go(-b: D.Bytes, +d: Nat, +from: U32, +to: U32, h: {D.ok(b, d) == True{} : Bool}, hft: {U32.is_le(from, to) == True{} : Bool}, ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}, m_b: BC.BMirror(b)) ->
92  {Pair.snd(D.Bytes, Bool, C.digits(b, from, to)) == F.all_digits(D.slice(D.view(b), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from)))) : Bool}:
93  (+l_b, m2_b) = m_b
94  (+t_b, +e_b) = m2_b
95  %e_b : {Pair.snd(D.Bytes, Bool, C.digits(_, from, to)) == F.all_digits(D.slice(D.view(_), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from)))) : Bool}
96  +h_t = BC.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
97  +ht_t = BC.tr(x => {Nat.is_le(U32.to_nat(to), D.size(x)) == True{} : Bool}, b, l_b, t_b, e_b, ht)
98  DG.digits_view_t(l_b, t_b, d, from, to, h_t, hft, ht_t)
99
100def L.digits_view(b, d, from, to, h, hft, ht):
101  digits_view.go(b, d, from, to, h, hft, ht, BC.bmirror(b))
102
103def digits_pair.go(-b: D.Bytes, +from: U32, +to: U32, m_b: BC.BMirror(b)) ->
104  {C.digits(b, from, to) == (b, Pair.snd(D.Bytes, Bool, C.digits(b, from, to))) : D.Bytes & Bool}:
105  (+l_b, m2_b) = m_b
106  (+t_b, +e_b) = m2_b
107  %e_b : {C.digits(_, from, to) == (_, Pair.snd(D.Bytes, Bool, C.digits(_, from, to))) : D.Bytes & Bool}
108  DG.digits_pair_t(l_b, t_b, from, to)
109
110def L.digits_pair(b, from, to):
111  digits_pair.go(b, from, to, BC.bmirror(b))
112
113def put_dec_view.go(-b: D.Bytes, +d: Nat, +n: U32, h: {D.ok(b, d) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(b), 10n), D.cap(b)) == True{} : Bool}, m_b: BC.BMirror(b)) ->
114  {D.view(C.put_dec(b, n)) == List.append(&2, U32, D.view(b), F.show(n)) : List<&2, U32>}:
115  (+l_b, m2_b) = m_b
116  (+t_b, +e_b) = m2_b
117  %e_b : {D.view(C.put_dec(_, n)) == List.append(&2, U32, D.view(_), F.show(n)) : List<&2, U32>}
118  +h_t = BC.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
119  +hc_t = BC.tr(x => {Nat.is_le(Nat.add(D.size(x), 10n), D.cap(x)) == True{} : Bool}, b, l_b, t_b, e_b, hc)
120  DG.put_dec_view_t(l_b, t_b, d, n, h_t, hc_t)
121
122def L.put_dec_view(b, d, n, h, hc):
123  put_dec_view.go(b, d, n, h, hc, BC.bmirror(b))
124
125def put_dec_ok.go(-b: D.Bytes, +d: Nat, +n: U32, h: {D.ok(b, d) == True{} : Bool}, hc: {Nat.is_le(Nat.add(D.size(b), 10n), D.cap(b)) == True{} : Bool}, m_b: BC.BMirror(b)) ->
126  {D.ok(C.put_dec(b, n), d) == True{} : Bool}:
127  (+l_b, m2_b) = m_b
128  (+t_b, +e_b) = m2_b
129  %e_b : {D.ok(C.put_dec(_, n), d) == True{} : Bool}
130  +h_t = BC.tr(x => {D.ok(x, d) == True{} : Bool}, b, l_b, t_b, e_b, h)
131  +hc_t = BC.tr(x => {Nat.is_le(Nat.add(D.size(x), 10n), D.cap(x)) == True{} : Bool}, b, l_b, t_b, e_b, hc)
132  DG.put_dec_ok_t(l_b, t_b, d, n, h_t, hc_t)
133
134def L.put_dec_ok(b, d, n, h, hc):
135  put_dec_ok.go(b, d, n, h, hc, BC.bmirror(b))
136
137
138# Lists, text and decimal numbers (no Bytes parameter)
139# ====================================================
140
141def L.split_length(xs, sep):
142  Q.split_length(xs, sep)
143
144def L.split_join(xs, sep):
145  Q.split_join(xs, sep)
146
147def L.split_text(xs, sep):
148  Q.split_text(xs, sep)
149
150def L.join_text(ps, sep):
151  Q.join_text(ps, sep)
152
153def L.text_codes(s):
154  Q.text_codes(s)
155
156def L.join_at(ps, sep, k, h):
157  Q.join_at(ps, sep, k, h)
158
159def L.ends_join(ps, sep, from, k, h):
160  Q.ends_join(ps, sep, from, k, h)
161
162def L.pieces_length(es, xs, from):
163  Q.pieces_length(es, xs, from)
164
165def L.decb_fits(xs, n, h, hn):
166  Q.decb_fits(xs, n, h, hn)