proof_seq.bend

lawful-bytes@0.1.1.0 · 199 lines · 11 definitions

1import Base
2import lawful-bytes@0.1.1.0/defs.bend as D
3import lawful-words@0.1.0.0/defs.bend as W
4import lawful-words@0.1.0.0/proof_nat.bend as N
5import lawful-words@0.1.0.0/proof_bytes.bend as Y
6import lawful-arrays@0.1.0.0/proof_base.bend as AB
7
8# List facts the Bytes proofs need (take, set, append, unpack), for lists of
9# U32. Every variable is reusable.
10
11law take_zero:
12  for +xs: List<&2, U32>
13  {List.take(&2, U32, xs, 0n) == Nil{} : List<&2, U32>}
14
15def take_zero(xs):
16  match xs:
17    case Nil{}:
18      {==}
19    case Con{x, t}:
20      {==}
21
22law take_length:
23  for +xs: List<&2, U32>
24  for +n: Nat
25  for +h: {Nat.is_le(n, List.length(&2, U32, xs)) == True{} : Bool}
26  {List.length(&2, U32, List.take(&2, U32, xs, n)) == n : Nat}
27
28def take_length(xs, n, h):
29  match xs n:
30    case Nil{} 0n:
31      {==}
32    case Nil{} 1n+p:
33      Empty.absurd({0n == 1n+p : Nat}, AB.false_ne_true(h))
34    case Con{x, t} 0n:
35      {==}
36    case Con{x, t} 1n+p:
37      %take_length(t, p, h) : {1n+List.length(&2, U32, List.take(&2, U32, t, p)) == 1n+_ : Nat}
38      {==}
39
40law take_take:
41  for +xs: List<&2, U32>
42  for +m: Nat
43  for +n: Nat
44  for +h: {Nat.is_le(n, m) == True{} : Bool}
45  {List.take(&2, U32, List.take(&2, U32, xs, m), n) == List.take(&2, U32, xs, n) : List<&2, U32>}
46
47def take_take(xs, m, n, h):
48  match xs m n:
49    case Nil{} _ _:
50      {==}
51    case Con{x, t} 0n 0n:
52      {==}
53    case Con{x, t} 0n 1n+q:
54      Empty.absurd({Nil{} == x <> List.take(&2, U32, t, q) : List<&2, U32>}, AB.false_ne_true(h))
55    case Con{x, t} 1n+p 0n:
56      {==}
57    case Con{x, t} 1n+p 1n+q:
58      %take_take(t, p, q, h) : {x <> List.take(&2, U32, List.take(&2, U32, t, p), q) == x <> _ : List<&2, U32>}
59      {==}
60
61law take_set:
62  for +xs: List<&2, U32>
63  for +m: Nat
64  for +i: Nat
65  for +v: U32
66  {List.take(&2, U32, List.set(&2, U32, xs, i, v), m) == List.set(&2, U32, List.take(&2, U32, xs, m), i, v) : List<&2, U32>}
67
68def take_set(xs, m, i, v):
69  match xs m i:
70    case Nil{} _ _:
71      {==}
72    case Con{x, t} 0n 0n:
73      {==}
74    case Con{x, t} 0n 1n+j:
75      {==}
76    case Con{x, t} 1n+p 0n:
77      {==}
78    case Con{x, t} 1n+p 1n+j:
79      %take_set(t, p, j, v) : {x <> List.take(&2, U32, List.set(&2, U32, t, j, v), p) == x <> _ : List<&2, U32>}
80      {==}
81
82# Setting index n and keeping n + 1 elements: the first n, then v.
83law take_set_succ:
84  for +xs: List<&2, U32>
85  for +n: Nat
86  for +v: U32
87  for +h: {Nat.is_lt(n, List.length(&2, U32, xs)) == True{} : Bool}
88  {List.take(&2, U32, List.set(&2, U32, xs, n, v), Nat.add(n, 1n)) == List.append(&2, U32, List.take(&2, U32, xs, n), [v]) : List<&2, U32>}
89
90def take_set_succ(xs, n, v, h):
91  match xs n:
92    case Nil{} _:
93      Empty.absurd({List.take(&2, U32, Nil{}, Nat.add(n, 1n)) == List.append(&2, U32, Nil{}, [v]) : List<&2, U32>},
94        AB.lt_zero_absurd(n, h))
95    case Con{x, t} 0n:
96      %Equal.sym(List<&2, U32>, List.take(&2, U32, t, 0n), Nil{}, take_zero(t)) : {v <> _ == [v] : List<&2, U32>}
97      {==}
98    case Con{x, t} 1n+p:
99      %take_set_succ(t, p, v, h) : {x <> List.take(&2, U32, List.set(&2, U32, t, p, v), Nat.add(p, 1n)) == x <> _ : List<&2, U32>}
100      {==}
101
102law take_append_l:
103  for +xs: List<&2, U32>
104  for +ys: List<&2, U32>
105  for +n: Nat
106  for +h: {Nat.is_le(n, List.length(&2, U32, xs)) == True{} : Bool}
107  {List.take(&2, U32, List.append(&2, U32, xs, ys), n) == List.take(&2, U32, xs, n) : List<&2, U32>}
108
109def take_append_l(xs, ys, n, h):
110  match xs n:
111    case Nil{} 0n:
112      take_zero(ys)
113    case Nil{} 1n+p:
114      Empty.absurd({List.take(&2, U32, ys, 1n+p) == Nil{} : List<&2, U32>}, AB.false_ne_true(h))
115    case Con{x, t} 0n:
116      {==}
117    case Con{x, t} 1n+p:
118      %take_append_l(t, ys, p, h) : {x <> List.take(&2, U32, List.append(&2, U32, t, ys), p) == x <> _ : List<&2, U32>}
119      {==}
120
121# Unpacking
122# =========
123
124law unpack_length4:
125  for +ws: List<&2, U32>
126  {List.length(&2, U32, D.unpack(ws)) == Nat.mul(List.length(&2, U32, ws), 4n) : Nat}
127
128def unpack_length4(ws):
129  match ws:
130    case Nil{}:
131      {==}
132    case Con{w, t}:
133      %unpack_length4(t) : {4n+List.length(&2, U32, D.unpack(t)) == 4n+_ : Nat}
134      {==}
135
136law unpack_length:
137  for +ws: List<&2, U32>
138  {List.length(&2, U32, D.unpack(ws)) == Nat.mul(4n, List.length(&2, U32, ws)) : Nat}
139
140def unpack_length(ws):
141  Equal.trans(Nat, List.length(&2, U32, D.unpack(ws)), Nat.mul(List.length(&2, U32, ws), 4n),
142    Nat.mul(4n, List.length(&2, U32, ws)), unpack_length4(ws), N.mul_comm(List.length(&2, U32, ws), 4n))
143
144law unpack_append:
145  for +xs: List<&2, U32>
146  for +ys: List<&2, U32>
147  {D.unpack(List.append(&2, U32, xs, ys)) == List.append(&2, U32, D.unpack(xs), D.unpack(ys)) : List<&2, U32>}
148
149def unpack_append(xs, ys):
150  match xs:
151    case Nil{}:
152      {==}
153    case Con{+w, t}:
154      %unpack_append(t, ys) :
155        {W.byte(w, 0n) <> W.byte(w, 1n) <> W.byte(w, 2n) <> W.byte(w, 3n) <> D.unpack(List.append(&2, U32, t, ys)) ==
156          W.byte(w, 0n) <> W.byte(w, 1n) <> W.byte(w, 2n) <> W.byte(w, 3n) <> _ : List<&2, U32>}
157      {==}
158
159law all_bytes_unpack:
160  for +ws: List<&2, U32>
161  {D.all_bytes(D.unpack(ws)) == True{} : Bool}
162
163def all_bytes_unpack(ws):
164  match ws:
165    case Nil{}:
166      {==}
167    case Con{+w, t}:
168      %Equal.sym(Bool, U32.is_lt(W.byte(w, 0n), 256), True{}, Y.byte_lt(w, 0n)) :
169        {Bool.and(_, Bool.and(U32.is_lt(W.byte(w, 1n), 256), Bool.and(U32.is_lt(W.byte(w, 2n), 256),
170          Bool.and(U32.is_lt(W.byte(w, 3n), 256), D.all_bytes(D.unpack(t)))))) == True{} : Bool}
171      %Equal.sym(Bool, U32.is_lt(W.byte(w, 1n), 256), True{}, Y.byte_lt(w, 1n)) :
172        {Bool.and(True{}, Bool.and(_, Bool.and(U32.is_lt(W.byte(w, 2n), 256),
173          Bool.and(U32.is_lt(W.byte(w, 3n), 256), D.all_bytes(D.unpack(t)))))) == True{} : Bool}
174      %Equal.sym(Bool, U32.is_lt(W.byte(w, 2n), 256), True{}, Y.byte_lt(w, 2n)) :
175        {Bool.and(True{}, Bool.and(True{}, Bool.and(_,
176          Bool.and(U32.is_lt(W.byte(w, 3n), 256), D.all_bytes(D.unpack(t)))))) == True{} : Bool}
177      %Equal.sym(Bool, U32.is_lt(W.byte(w, 3n), 256), True{}, Y.byte_lt(w, 3n)) :
178        {Bool.and(True{}, Bool.and(True{}, Bool.and(True{},
179          Bool.and(_, D.all_bytes(D.unpack(t)))))) == True{} : Bool}
180      %Equal.sym(Bool, D.all_bytes(D.unpack(t)), True{}, all_bytes_unpack(t)) :
181        {Bool.and(True{}, Bool.and(True{}, Bool.and(True{}, Bool.and(True{}, _)))) == True{} : Bool}
182      {==}
183
184law all_bytes_take:
185  for +xs: List<&2, U32>
186  for +n: Nat
187  for +h: {D.all_bytes(xs) == True{} : Bool}
188  {D.all_bytes(List.take(&2, U32, xs, n)) == True{} : Bool}
189
190def all_bytes_take(xs, n, h):
191  match xs n:
192    case Nil{} _:
193      {==}
194    case Con{x, t} 0n:
195      {==}
196    case Con{+x, t} 1n+p:
197      %Equal.sym(Bool, U32.is_lt(x, 256), True{}, AB.and_true_l(U32.is_lt(x, 256), D.all_bytes(t), h)) :
198        {Bool.and(_, D.all_bytes(List.take(&2, U32, t, p))) == True{} : Bool}
199      all_bytes_take(t, p, AB.and_true_r(U32.is_lt(x, 256), D.all_bytes(t), h))