1	import Base
2	import lawful-bytes@0.1.0.0/defs.bend as D
3	import ./defs.bend as F
4	import ./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.
11	law 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).
26	law 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.
40	law 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	
53	law 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.
62	law 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	
72	law 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.
79	law 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.
85	law 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).
92	law 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	
102	law 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).
109	law 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	
117	law 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.
130	law 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.
136	law 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	
141	law 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.
147	law 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.
155	law 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	
163	law 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.
170	law 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>}