LAWS.bend

lawful-fields@0.1.1.0 · 175 lines · 19 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
5
6# lawful-fields: cutting a line of packed bytes into fields, and reading a
7# decimal number, stated on the list of bytes a buffer holds (D.view).
8
9# cut answers the end offsets of the first n pieces of from .. to-1, split at
10# sep: the pieces those ends delimit are the first n of F.split.
11law cut_view:
12  for b: D.Bytes
13  for d: Nat
14  for from: U32
15  for to: U32
16  for sep: U32
17  for n: Nat
18  for h: {D.ok(b, d) == True{} : Bool}
19  for hft: {U32.is_le(from, to) == True{} : Bool}
20  for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
21  for hs: {U32.is_lt(sep, 256) == True{} : Bool}
22  {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>>}
23
24# The ends are exactly where split's pieces end, counted from from (so they
25# increase, and each next piece starts just after the previous end).
26law cut_ends:
27  for b: D.Bytes
28  for d: Nat
29  for from: U32
30  for to: U32
31  for sep: U32
32  for n: Nat
33  for h: {D.ok(b, d) == True{} : Bool}
34  for hft: {U32.is_le(from, to) == True{} : Bool}
35  for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
36  for hs: {U32.is_lt(sep, 256) == True{} : Bool}
37  {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>}
38
39# Every end lies in from .. to.
40law cut_bounds:
41  for b: D.Bytes
42  for d: Nat
43  for from: U32
44  for to: U32
45  for sep: U32
46  for n: Nat
47  for h: {D.ok(b, d) == True{} : Bool}
48  for hft: {U32.is_le(from, to) == True{} : Bool}
49  for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
50  for hs: {U32.is_lt(sep, 256) == True{} : Bool}
51  {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}
52
53law cut_pair:
54  for b: D.Bytes
55  for from: U32
56  for to: U32
57  for sep: U32
58  for n: Nat
59  {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>}
60
61# num reads the decimal number in from .. to-1 when it is one and fits a U32.
62law num_view:
63  for b: D.Bytes
64  for d: Nat
65  for from: U32
66  for to: U32
67  for h: {D.ok(b, d) == True{} : Bool}
68  for hft: {U32.is_le(from, to) == True{} : Bool}
69  for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
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
72law num_pair:
73  for b: D.Bytes
74  for from: U32
75  for to: U32
76  {C.num(b, from, to) == (b, Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(b, from, to))) : D.Bytes & Maybe<&2, U32>}
77
78# The number of pieces split gives is one more than the number of separators.
79law split_length:
80  for xs: List<&2, U32>
81  for sep: U32
82  {List.length(&2, List<&2, U32>, F.split(xs, sep)) == Nat.add(F.count(xs, sep), 1n) : Nat}
83
84# Joining the pieces with the separator gives xs back.
85law split_join:
86  for xs: List<&2, U32>
87  for sep: U32
88  {F.join(F.split(xs, sep), sep) == xs : List<&2, U32>}
89
90# digits says the bytes are one or more decimal digits, a number of any size
91# (num answers None both for non-numbers and for numbers of 2^32 or more).
92law digits_view:
93  for b: D.Bytes
94  for d: Nat
95  for from: U32
96  for to: U32
97  for h: {D.ok(b, d) == True{} : Bool}
98  for hft: {U32.is_le(from, to) == True{} : Bool}
99  for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
100  {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}
101
102law digits_pair:
103  for b: D.Bytes
104  for from: U32
105  for to: U32
106  {C.digits(b, from, to) == (b, Pair.snd(D.Bytes, Bool, C.digits(b, from, to))) : D.Bytes & Bool}
107
108# put_dec writes n in decimal at the end (room for 10 more bytes needed).
109law put_dec_view:
110  for b: D.Bytes
111  for d: Nat
112  for n: U32
113  for h: {D.ok(b, d) == True{} : Bool}
114  for hc: {Nat.is_le(Nat.add(D.size(b), 10n), D.cap(b)) == True{} : Bool}
115  {D.view(C.put_dec(b, n)) == List.append(&2, U32, D.view(b), F.show(n)) : List<&2, U32>}
116
117law put_dec_ok:
118  for b: D.Bytes
119  for d: Nat
120  for n: U32
121  for h: {D.ok(b, d) == True{} : Bool}
122  for hc: {Nat.is_le(Nat.add(D.size(b), 10n), D.cap(b)) == True{} : Bool}
123  {D.ok(C.put_dec(b, n), d) == True{} : Bool}
124
125# ==========================================================================
126# Text (one Char per byte): what the bytes mean to a String-based spec
127# ==========================================================================
128
129# Splitting bytes is splitting their text.
130law split_text:
131  for xs: List<&2, U32>
132  for sep: U32
133  {String.split(F.text(xs), Chr{sep}) == F.texts(F.split(xs, sep)) : List<&2, String>}
134
135# Joining bytes is joining their text.
136law join_text:
137  for ps: List<&2, List<&2, U32>>
138  for sep: U32
139  {F.text(F.join(ps, sep)) == String.join(F.texts(ps), F.text([sep])) : String}
140
141law text_codes:
142  for s: String
143  {F.text(F.codes(s)) == s : String}
144
145# Joining a list of pieces splits at piece k: the first k+1 pieces, the
146# separator, the rest.
147law join_at:
148  for ps: List<&2, List<&2, U32>>
149  for sep: U32
150  for k: Nat
151  for h: {Nat.is_lt(Nat.add(k, 1n), List.length(&2, List<&2, U32>, ps)) == True{} : Bool}
152  {F.join(ps, sep) == List.append(&2, U32, F.join(List.take(&2, List<&2, U32>, ps, Nat.add(k, 1n)), sep), Con{sep, F.join(List.drop(&2, List<&2, U32>, ps, Nat.add(k, 1n)), sep)}) : List<&2, U32>}
153
154# Piece k ends at the k-th end: the first k+1 pieces joined, from from.
155law ends_join:
156  for ps: List<&2, List<&2, U32>>
157  for sep: U32
158  for from: Nat
159  for k: Nat
160  for h: {Nat.is_lt(k, List.length(&2, List<&2, U32>, ps)) == True{} : Bool}
161  {List.get(&2, Nat, F.ends(ps, from), k) == Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, ps, Nat.add(k, 1n)), sep)))} : Maybe<&2, Nat>}
162
163law pieces_length:
164  for es: List<&2, U32>
165  for xs: List<&2, U32>
166  for from: Nat
167  {List.length(&2, List<&2, U32>, F.pieces(es, xs, from)) == List.length(&2, U32, es) : Nat}
168
169# decb (with bound 2^32) is dec when the number fits.
170law decb_fits:
171  for xs: List<&2, U32>
172  for n: Nat
173  for h: {F.dec(xs) == Some{n} : Maybe<&2, Nat>}
174  for hn: {Nat.is_lt(n, Nat.pow(2n, 32n)) == True{} : Bool}
175  {F.decb(xs, Nat.pow(2n, 32n)) == Some{n} : Maybe<&2, Nat>}