proofs/containers/lru/trace.bend
bend-collections-laws-containers@1.0.0.0 · 219 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as SP
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insa.bend as IA
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/lists.bend as LS
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/dll.bend as DL
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
12
13# Traces of writes to link words (words 0 and 1 of a slot): what a recency
14# or free-list operation does to lk, and what it leaves.
15
16type Tr is Data:
17 TNil{}
18 TW{y: Nat, o: Nat, v: U32, t: Tr}
19
20# t's writes first, then this one
21def app(+ll: List<&2, U32>, tr: Tr) -> List<&2, U32>:
22 match tr:
23 case TNil{}:
24 ll
25 case TW{+y, +o, +v, +t}:
26 SC.update(U32, app(ll, t), ST.off(y, o), v)
27
28# every write is to a link word
29def trlo(tr: Tr) -> Bool:
30 match tr:
31 case TNil{}:
32 True{}
33 case TW{y, +o, v, +t}:
34 Bool.and(Nat.is_lt(o, 2n), trlo(t))
35
36# every written slot is in xs / none is
37def trin(tr: Tr, +xs: List<&2, Nat>) -> Bool:
38 match tr:
39 case TNil{}:
40 True{}
41 case TW{+y, o, v, +t}:
42 Bool.and(NL.memn(y, xs), trin(t, xs))
43
44def trout(tr: Tr, +xs: List<&2, Nat>) -> Bool:
45 match tr:
46 case TNil{}:
47 True{}
48 case TW{+y, o, v, +t}:
49 Bool.and(Bool.not(NL.memn(y, xs)), trout(t, xs))
50
51# b's writes, then a's
52def tcat(a: Tr, b: Tr) -> Tr:
53 match a:
54 case TNil{}:
55 b
56 case TW{+y, +o, +v, +t}:
57 TW{y, o, v, tcat(t, b)}
58
59def app_cat(+ll: List<&2, U32>, +a: Tr, +b: Tr) -> {app(ll, tcat(a, b)) == app(app(ll, b), a) : List<&2, U32>}:
60 match a:
61 case TNil{}:
62 {==}
63 case TW{+y, +o, +v, +t}:
64 Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, ST.off(y, o), v), app(ll, tcat(t, b)), app(app(ll, b), t), app_cat(ll, t, b))
65
66
67def lo_cat(+a: Tr, +b: Tr, +ha: {trlo(a) == True{} : Bool}, +hb: {trlo(b) == True{} : Bool}) -> {trlo(tcat(a, b)) == True{} : Bool}:
68 match a:
69 case TNil{}:
70 hb
71 case TW{+y, +o, +v, +t}:
72 L.and_intro(Nat.is_lt(o, 2n), trlo(tcat(t, b)), L.and_left(Nat.is_lt(o, 2n), trlo(t), ha), lo_cat(t, b, L.and_right(Nat.is_lt(o, 2n), trlo(t), ha), hb))
73
74def in_cat(+a: Tr, +b: Tr, +xs: List<&2, Nat>, +ha: {trin(a, xs) == True{} : Bool}, +hb: {trin(b, xs) == True{} : Bool}) -> {trin(tcat(a, b), xs) == True{} : Bool}:
75 match a:
76 case TNil{}:
77 hb
78 case TW{+y, +o, +v, +t}:
79 L.and_intro(NL.memn(y, xs), trin(tcat(t, b), xs), L.and_left(NL.memn(y, xs), trin(t, xs), ha), in_cat(t, b, xs, L.and_right(NL.memn(y, xs), trin(t, xs), ha), hb))
80
81def lt8(+o: Nat, +h: {Nat.is_lt(o, 2n) == True{} : Bool}) -> {Nat.is_lt(o, 8n) == True{} : Bool}:
82 N.lt_le_trans(o, 2n, 8n, h, {==})
83
84# ---- what a trace leaves ----
85
86def len_tr(+ll: List<&2, U32>, +tr: Tr) -> {SC.length(U32, app(ll, tr)) == SC.length(U32, ll) : Nat}:
87 match tr:
88 case TNil{}:
89 {==}
90 case TW{+y, +o, +v, +t}:
91 Equal.trans(Nat, SC.length(U32, SC.update(U32, app(ll, t), ST.off(y, o), v)), SC.length(U32, app(ll, t)), SC.length(U32, ll), IA.len_upd(app(ll, t), ST.off(y, o), v), len_tr(ll, t))
92
93def es_tr(~V: Data, +ll: List<&2, U32>, +tr: Tr, +h: {trlo(tr) == True{} : Bool}, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +sl: List<&2, Nat>) -> {ST.es(~V, app(ll, tr), kl, el, sl) == ST.es(~V, ll, kl, el, sl) : List<&2, SP.Ent<V>>}:
94 match tr:
95 case TNil{}:
96 {==}
97 case TW{+y, +o, +v, +t}:
98 +h01 = L.and_left(Nat.is_lt(o, 2n), trlo(t), h)
99 Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, SC.update(U32, app(ll, t), ST.off(y, o), v), kl, el, sl), ST.es(~V, app(ll, t), kl, el, sl), ST.es(~V, ll, kl, el, sl), DL.es_fr(~V, app(ll, t), y, o, v, lt8(o, h01), h01, kl, el, sl), es_tr(~V, ll, t, L.and_right(Nat.is_lt(o, 2n), trlo(t), h), kl, el, sl))
100
101def has_tr(~V: Data, +ll: List<&2, U32>, +tr: Tr, +h: {trlo(tr) == True{} : Bool}, +bs: List<&2, B.Bk>, +m: Nat, +sl: List<&2, Nat>) -> {ST.hasall(~V, bs, m, app(ll, tr), sl) == ST.hasall(~V, bs, m, ll, sl) : Bool}:
102 match tr:
103 case TNil{}:
104 {==}
105 case TW{+y, +o, +v, +t}:
106 +h01 = L.and_left(Nat.is_lt(o, 2n), trlo(t), h)
107 Equal.trans(Bool, ST.hasall(~V, bs, m, SC.update(U32, app(ll, t), ST.off(y, o), v), sl), ST.hasall(~V, bs, m, app(ll, t), sl), ST.hasall(~V, bs, m, ll, sl), DL.has_fr(~V, app(ll, t), y, o, v, lt8(o, h01), h01, bs, m, sl), has_tr(~V, ll, t, L.and_right(Nat.is_lt(o, 2n), trlo(t), h), bs, m, sl))
108
109def bsl_tr(+ll: List<&2, U32>, +tr: Tr, +h: {trlo(tr) == True{} : Bool}, +bs: List<&2, B.Bk>, +sl: List<&2, Nat>, +m: Nat) -> {ST.bsl(bs, sl, app(ll, tr), m) == ST.bsl(bs, sl, ll, m) : Bool}:
110 match tr:
111 case TNil{}:
112 {==}
113 case TW{+y, +o, +v, +t}:
114 +h01 = L.and_left(Nat.is_lt(o, 2n), trlo(t), h)
115 Equal.trans(Bool, ST.bsl(bs, sl, SC.update(U32, app(ll, t), ST.off(y, o), v), m), ST.bsl(bs, sl, app(ll, t), m), ST.bsl(bs, sl, ll, m), DL.bsl_fr(app(ll, t), y, o, v, lt8(o, h01), h01, bs, sl, m), bsl_tr(ll, t, L.and_right(Nat.is_lt(o, 2n), trlo(t), h), bs, sl, m))
116
117def fll_tr(+ll: List<&2, U32>, +tr: Tr, +h: {trlo(tr) == True{} : Bool}, +fl: List<&2, Nat>, +hout: {trout(tr, fl) == True{} : Bool}) -> {ST.fll(app(ll, tr), fl) == ST.fll(ll, fl) : Bool}:
118 match tr:
119 case TNil{}:
120 {==}
121 case TW{+y, +o, +v, +t}:
122 +h01 = L.and_left(Nat.is_lt(o, 2n), trlo(t), h)
123 +hy = L.not_true(NL.memn(y, fl), L.and_left(Bool.not(NL.memn(y, fl)), trout(t, fl), hout))
124 Equal.trans(Bool, ST.fll(SC.update(U32, app(ll, t), ST.off(y, o), v), fl), ST.fll(app(ll, t), fl), ST.fll(ll, fl), DL.fll_fs(app(ll, t), y, o, v, lt8(o, h01), fl, hy), fll_tr(ll, t, L.and_right(Nat.is_lt(o, 2n), trlo(t), h), fl, L.and_right(Bool.not(NL.memn(y, fl)), trout(t, fl), hout)))
125
126def seg_tr(+ll: List<&2, U32>, +tr: Tr, +h: {trlo(tr) == True{} : Bool}, +sl: List<&2, Nat>, +p: U32, +q: U32, +hout: {trout(tr, sl) == True{} : Bool}) -> {ST.seg(app(ll, tr), sl, p, q) == ST.seg(ll, sl, p, q) : Bool}:
127 match tr:
128 case TNil{}:
129 {==}
130 case TW{+y, +o, +v, +t}:
131 +h01 = L.and_left(Nat.is_lt(o, 2n), trlo(t), h)
132 +hy = L.not_true(NL.memn(y, sl), L.and_left(Bool.not(NL.memn(y, sl)), trout(t, sl), hout))
133 Equal.trans(Bool, ST.seg(SC.update(U32, app(ll, t), ST.off(y, o), v), sl, p, q), ST.seg(app(ll, t), sl, p, q), ST.seg(ll, sl, p, q), DL.seg_fs(app(ll, t), y, o, v, lt8(o, h01), sl, p, q, hy), seg_tr(ll, t, L.and_right(Nat.is_lt(o, 2n), trlo(t), h), sl, p, q, L.and_right(Bool.not(NL.memn(y, sl)), trout(t, sl), hout)))
134
135# a word of a slot the trace does not write
136def lw_tr(+ll: List<&2, U32>, +tr: Tr, +h: {trlo(tr) == True{} : Bool}, +x: Nat, +o2: Nat, +ho2: {Nat.is_lt(o2, 8n) == True{} : Bool}, +hout: {trout(tr, Con{x, Nil{}}) == True{} : Bool}) -> {ST.lw(app(ll, tr), x, o2) == ST.lw(ll, x, o2) : U32}:
137 match tr:
138 case TNil{}:
139 {==}
140 case TW{+y, +o, +v, +t}:
141 +h01 = L.and_left(Nat.is_lt(o, 2n), trlo(t), h)
142 +hy = NL.or_ff_l(Nat.is_eq(x, y), False{}, L.not_true(NL.memn(y, Con{x, Nil{}}), L.and_left(Bool.not(NL.memn(y, Con{x, Nil{}})), trout(t, Con{x, Nil{}}), hout)))
143 Equal.trans(U32, ST.lw(SC.update(U32, app(ll, t), ST.off(y, o), v), x, o2), ST.lw(app(ll, t), x, o2), ST.lw(ll, x, o2), DL.lw_other(app(ll, t), y, o, v, lt8(o, h01), x, o2, ho2, DL.ne_slot(y, x, o, o2, NL.ne_sym(x, y, hy))), lw_tr(ll, t, L.and_right(Nat.is_lt(o, 2n), trlo(t), h), x, o2, ho2, L.and_right(Bool.not(NL.memn(y, Con{x, Nil{}})), trout(t, Con{x, Nil{}}), hout)))
144
145# a data word (2 <= o2) of any slot
146def lw_tr_hi(+ll: List<&2, U32>, +tr: Tr, +h: {trlo(tr) == True{} : Bool}, +x: Nat, +o2: Nat, +ho2: {Nat.is_lt(o2, 8n) == True{} : Bool}, +h2: {Nat.is_le(2n, o2) == True{} : Bool}) -> {ST.lw(app(ll, tr), x, o2) == ST.lw(ll, x, o2) : U32}:
147 match tr:
148 case TNil{}:
149 {==}
150 case TW{+y, +o, +v, +t}:
151 +h01 = L.and_left(Nat.is_lt(o, 2n), trlo(t), h)
152 Equal.trans(U32, ST.lw(SC.update(U32, app(ll, t), ST.off(y, o), v), x, o2), ST.lw(app(ll, t), x, o2), ST.lw(ll, x, o2), DL.lw_hi(app(ll, t), y, o, v, lt8(o, h01), h01, x, o2, ho2, h2), lw_tr_hi(ll, t, L.and_right(Nat.is_lt(o, 2n), trlo(t), h), x, o2, ho2, h2))
153
154def not_vac(~V: Data, +y: Nat, +fl: List<&2, Nat>, +fr: Nat, +el: List<&2, Maybe<&2, V>>, +hl: {ST.live(~V, el, y) == True{} : Bool}, +hf: {ST.flok(~V, fl, fr, el) == True{} : Bool}, +c: Bool, +hc: {NL.memn(y, fl) == c : Bool}) -> {Bool.not(c) == True{} : Bool}:
155 match c:
156 case False{}:
157 {==}
158 case True{}:
159 +hv = L.and_right(Nat.is_lt(y, fr), Bool.not(ST.live(~V, el, y)), LS.sall_mem(~V, ST.PVac{fr, el}, y, fl, hf, hc))
160 Empty.absurd({Bool.not(True{}) == True{} : Bool}, L.false_true(L.subst(Bool, z => {Bool.not(z) == True{} : Bool}, ST.live(~V, el, y), True{}, hl, hv)))
161
162# written slots are live, fl's are vacant: fl is untouched
163def out_of_in(~V: Data, +tr: Tr, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +fr: Nat, +el: List<&2, Maybe<&2, V>>, +hin: {trin(tr, sl) == True{} : Bool}, +hs: {ST.slok(~V, sl, fr, el) == True{} : Bool}, +hf: {ST.flok(~V, fl, fr, el) == True{} : Bool}) -> {trout(tr, fl) == True{} : Bool}:
164 match tr:
165 case TNil{}:
166 {==}
167 case TW{+y, +o, +v, +t}:
168 +hy = L.and_left(NL.memn(y, sl), trin(t, sl), hin)
169 +hl = L.and_right(Nat.is_lt(y, fr), ST.live(~V, el, y), LS.sall_mem(~V, ST.PLive{fr, el}, y, sl, hs, hy))
170 L.and_intro(Bool.not(NL.memn(y, fl)), trout(t, fl), not_vac(~V, y, fl, fr, el, hl, hf, NL.memn(y, fl), {==}), out_of_in(~V, t, sl, fl, fr, el, L.and_right(NL.memn(y, sl), trin(t, sl), hin), hs, hf))
171
172
173# ---- where a trace writes ----
174
175
176def trin_r(+tr: Tr, +a: List<&2, Nat>, +x: List<&2, Nat>, +h: {trin(tr, x) == True{} : Bool}) -> {trin(tr, SC.append(Nat, a, x)) == True{} : Bool}:
177 match tr:
178 case TNil{}:
179 {==}
180 case TW{+y, +o, +v, +t}:
181 L.and_intro(NL.memn(y, SC.append(Nat, a, x)), trin(t, SC.append(Nat, a, x)), NL.mem_app_r(y, a, x, L.and_left(NL.memn(y, x), trin(t, x), h)), trin_r(t, a, x, L.and_right(NL.memn(y, x), trin(t, x), h)))
182
183def trin_l(+tr: Tr, +a: List<&2, Nat>, +x: List<&2, Nat>, +h: {trin(tr, a) == True{} : Bool}) -> {trin(tr, SC.append(Nat, a, x)) == True{} : Bool}:
184 match tr:
185 case TNil{}:
186 {==}
187 case TW{+y, +o, +v, +t}:
188 L.and_intro(NL.memn(y, SC.append(Nat, a, x)), trin(t, SC.append(Nat, a, x)), NL.mem_app_l(y, a, x, L.and_left(NL.memn(y, a), trin(t, a), h)), trin_l(t, a, x, L.and_right(NL.memn(y, a), trin(t, a), h)))
189
190def trin_cons(+tr: Tr, +s: Nat, +x: List<&2, Nat>, +h: {trin(tr, x) == True{} : Bool}) -> {trin(tr, Con{s, x}) == True{} : Bool}:
191 match tr:
192 case TNil{}:
193 {==}
194 case TW{+y, +o, +v, +t}:
195 L.and_intro(NL.memn(y, Con{s, x}), trin(t, Con{s, x}), NL.or_tr(Nat.is_eq(s, y), NL.memn(y, x), L.and_left(NL.memn(y, x), trin(t, x), h)), trin_cons(t, s, x, L.and_right(NL.memn(y, x), trin(t, x), h)))
196
197# written slots all in a: none in x
198def trout_r(+tr: Tr, +a: List<&2, Nat>, +x: List<&2, Nat>, +hin: {trin(tr, a) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, a, x)) == True{} : Bool}) -> {trout(tr, x) == True{} : Bool}:
199 match tr:
200 case TNil{}:
201 {==}
202 case TW{+y, +o, +v, +t}:
203 L.and_intro(Bool.not(NL.memn(y, x)), trout(t, x), NL.not_f(NL.memn(y, x), NL.nd_dj2(a, x, hnd, y, L.and_left(NL.memn(y, a), trin(t, a), hin))), trout_r(t, a, x, L.and_right(NL.memn(y, a), trin(t, a), hin), hnd))
204
205# written slots all in x: none in a
206def trout_l(+tr: Tr, +a: List<&2, Nat>, +x: List<&2, Nat>, +hin: {trin(tr, x) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, a, x)) == True{} : Bool}) -> {trout(tr, a) == True{} : Bool}:
207 match tr:
208 case TNil{}:
209 {==}
210 case TW{+y, +o, +v, +t}:
211 L.and_intro(Bool.not(NL.memn(y, a)), trout(t, a), NL.not_f(NL.memn(y, a), NL.nd_dj(a, x, hnd, y, L.and_left(NL.memn(y, x), trin(t, x), hin))), trout_l(t, a, x, L.and_right(NL.memn(y, x), trin(t, x), hin), hnd))
212
213def trout_tail(+tr: Tr, +s: Nat, +x: List<&2, Nat>, +h: {trout(tr, Con{s, x}) == True{} : Bool}) -> {trout(tr, x) == True{} : Bool}:
214 match tr:
215 case TNil{}:
216 {==}
217 case TW{+y, +o, +v, +t}:
218 +h0 = L.not_true(NL.memn(y, Con{s, x}), L.and_left(Bool.not(NL.memn(y, Con{s, x})), trout(t, Con{s, x}), h))
219 L.and_intro(Bool.not(NL.memn(y, x)), trout(t, x), NL.not_f(NL.memn(y, x), NL.or_ff_r(Nat.is_eq(s, y), NL.memn(y, x), h0)), trout_tail(t, s, x, L.and_right(Bool.not(NL.memn(y, Con{s, x})), trout(t, Con{s, x}), h)))