1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../../spec/lib/common.bend as SC
5	import ../../../spec/containers/lru.bend as SP
6	import ../hash_table/buckets.bend as B
7	import ../hash_table/insa.bend as IA
8	import ./state.bend as ST
9	import ./lists.bend as LS
10	import ./dll.bend as DL
11	import ../../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	
16	type Tr is Data:
17	  TNil{}
18	  TW{y: Nat, o: Nat, v: U32, t: Tr}
19	
20	# t's writes first, then this one
21	def 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
29	def 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
37	def 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	
44	def 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
52	def 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	
59	def 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	
67	def 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	
74	def 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	
81	def 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	
86	def 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	
93	def 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	
101	def 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	
109	def 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	
117	def 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	
126	def 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
136	def 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
146	def 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	
154	def 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
163	def 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	
176	def 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	
183	def 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	
190	def 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
198	def 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
206	def 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	
213	def 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)))