LAWS.bend
lawful-fields@0.1.0.0 · 175 lines · 0 definitions
1import Base
2import lawful-bytes@0.1.0.0/defs.bend as D
3import lawful-fields@0.1.0.0/defs.bend as F
4import lawful-fields@0.1.0.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>}