1	import Base
2	import ../src/cache.bend as C
3	import ./invariants.bend as Inv
4	import ./recency_membership.bend as Filter
5	import ./recency_update_membership.bend as Move
6	import ./map_routing.bend as R
7	import ./map_delete_prefix.bend as And
8	import ./map_key_membership.bend as Keys
9	
10	def moved(+xs: List<&2, String>, +key: String) -> List<&2, String>:
11	  List.append(&2, String, C.without(xs, key), Con{key, Nil{}})
12	
13	law append_included:
14	  for xs: List<&2, String>
15	  for +ys: List<&2, String>
16	  for +key: String
17	  for +included: {Inv.included(xs, ys) == True{} : Bool}
18	  for +present: {Inv.member(ys, key) == True{} : Bool}
19	  {Inv.included(List.append(&2, String, xs, Con{key, Nil{}}), ys) == True{} : Bool}
20	def append_included(xs, ys, key, included, present):
21	  match xs:
22	    case Nil{}: And.conjunction(Inv.member(ys, key), True{}, present, {==})
23	    case Con{+head, +tail}:
24	      And.conjunction(Inv.member(ys, head), Inv.included(List.append(&2, String, tail, Con{key, Nil{}}), ys), R.and_left(Inv.member(ys, head), Inv.included(tail, ys), included), append_included(tail, ys, key, R.and_right(Inv.member(ys, head), Inv.included(tail, ys), included), present))
25	
26	law forward:
27	  for +xs: List<&2, String>
28	  for +ys: List<&2, String>
29	  for +key: String
30	  for +included: {Inv.included(xs, ys) == True{} : Bool}
31	  for present: {Inv.member(ys, key) == True{} : Bool}
32	  {Inv.included(moved(xs, key), ys) == True{} : Bool}
33	def forward(xs, ys, key, included, present):
34	  append_included(C.without(xs, key), ys, key, Filter.filter_included_left(xs, ys, key, included), present)
35	
36	law retained:
37	  for +xs: List<&2, String>
38	  for +key: String
39	  for +query: String
40	  for present: {Inv.member(xs, query) == True{} : Bool}
41	  {Inv.member(moved(xs, key), query) == True{} : Bool}
42	def retained(xs, key, query, present):
43	  Equal.trans(Bool, Inv.member(moved(xs, key), query), String.eq(query, key) || Inv.member(xs, query), True{}, Move.move(xs, key, query), %Equal.sym(Bool, Inv.member(xs, query), True{}, present) : {String.eq(query, key) || _ == True{} : Bool} Keys.or_true(String.eq(query, key)))
44	
45	law backward:
46	  for xs: List<&2, String>
47	  for +ys: List<&2, String>
48	  for +key: String
49	  for +included: {Inv.included(xs, ys) == True{} : Bool}
50	  {Inv.included(xs, moved(ys, key)) == True{} : Bool}
51	def backward(xs, ys, key, included):
52	  match xs:
53	    case Nil{}: {==}
54	    case Con{+head, +tail}:
55	      And.conjunction(Inv.member(moved(ys, key), head), Inv.included(tail, moved(ys, key)), retained(ys, key, head, R.and_left(Inv.member(ys, head), Inv.included(tail, ys), included)), backward(tail, ys, key, R.and_right(Inv.member(ys, head), Inv.included(tail, ys), included)))