proofs/containers/lru/lists.bend
bend-collections-laws-containers@1.0.0.0 · 148 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/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
7import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as SP
8import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as W
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as K
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as HT
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
13
14# List algebra for the recency list and the model's keys: membership,
15# duplicate-freedom and the per-slot predicates over appends.
16
17
18# ---- Bool algebra ----
19
20
21
22
23
24# not (x or y) and (z and not w) == (not x and z) and not (y or w)
25
26
27# ---- slot lists ----
28
29
30
31
32# ---- key lists ----
33
34
35def mem_app_s(+x: String, +a: List<&2, String>, +b: List<&2, String>) -> {S.mem(x, SC.append(String, a, b)) == Bool.or(S.mem(x, a), S.mem(x, b)) : Bool}:
36 match a:
37 case Nil{}:
38 {==}
39 case Con{+h, +t}:
40 Equal.trans(Bool, Bool.or(S.str_eq(h, x), S.mem(x, SC.append(String, t, b))), Bool.or(S.str_eq(h, x), Bool.or(S.mem(x, t), S.mem(x, b))), Bool.or(Bool.or(S.str_eq(h, x), S.mem(x, t)), S.mem(x, b)), Equal.cong(Bool, Bool, z => Bool.or(S.str_eq(h, x), z), S.mem(x, SC.append(String, t, b)), Bool.or(S.mem(x, t), S.mem(x, b)), mem_app_s(x, t, b)), NL.or_assoc(S.str_eq(h, x), S.mem(x, t), S.mem(x, b)))
41
42def mem_mid_s(+x: String, +a: List<&2, String>, +s: String, +b: List<&2, String>) -> {S.mem(x, SC.append(String, a, Con{s, b})) == Bool.or(S.mem(x, SC.append(String, a, b)), S.str_eq(s, x)) : Bool}:
43 match a:
44 case Nil{}:
45 NL.or_comm(S.str_eq(s, x), S.mem(x, b))
46 case Con{+h, +t}:
47 Equal.trans(Bool, Bool.or(S.str_eq(h, x), S.mem(x, SC.append(String, t, Con{s, b}))), Bool.or(S.str_eq(h, x), Bool.or(S.mem(x, SC.append(String, t, b)), S.str_eq(s, x))), Bool.or(Bool.or(S.str_eq(h, x), S.mem(x, SC.append(String, t, b))), S.str_eq(s, x)), Equal.cong(Bool, Bool, z => Bool.or(S.str_eq(h, x), z), S.mem(x, SC.append(String, t, Con{s, b})), Bool.or(S.mem(x, SC.append(String, t, b)), S.str_eq(s, x)), mem_mid_s(x, t, s, b)), NL.or_assoc(S.str_eq(h, x), S.mem(x, SC.append(String, t, b)), S.str_eq(s, x)))
48
49def nd_mid_s(+a: List<&2, String>, +s: String, +b: List<&2, String>) -> {S.nodup(SC.append(String, a, Con{s, b})) == Bool.and(S.nodup(SC.append(String, a, b)), Bool.not(S.mem(s, SC.append(String, a, b)))) : Bool}:
50 match a:
51 case Nil{}:
52 NL.and_comm(Bool.not(S.mem(s, b)), S.nodup(b))
53 case Con{+h, +t}:
54 +X = S.mem(h, SC.append(String, t, b))
55 +Z = S.nodup(SC.append(String, t, b))
56 +Wm = S.mem(s, SC.append(String, t, b))
57 +e1 = Equal.cong(Bool, Bool, z => Bool.and(Bool.not(z), S.nodup(SC.append(String, t, Con{s, b}))), S.mem(h, SC.append(String, t, Con{s, b})), Bool.or(X, S.str_eq(s, h)), mem_mid_s(h, t, s, b))
58 +e2 = Equal.cong(Bool, Bool, z => Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), z), S.nodup(SC.append(String, t, Con{s, b})), Bool.and(Z, Bool.not(Wm)), nd_mid_s(t, s, b))
59 +e3 = NL.bt_mid(X, S.str_eq(s, h), Z, Wm)
60 +e4 = Equal.cong(Bool, Bool, z => Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(z, Wm))), S.str_eq(s, h), S.str_eq(h, s), K.str_sym(s, h))
61 Equal.trans(Bool, S.nodup(SC.append(String, Con{h, t}, Con{s, b})), Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), S.nodup(SC.append(String, t, Con{s, b}))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(S.str_eq(h, s), Wm))), e1, Equal.trans(Bool, Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), S.nodup(SC.append(String, t, Con{s, b}))), Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), Bool.and(Z, Bool.not(Wm))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(S.str_eq(h, s), Wm))), e2, Equal.trans(Bool, Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), Bool.and(Z, Bool.not(Wm))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(S.str_eq(s, h), Wm))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(S.str_eq(h, s), Wm))), e3, e4)))
62
63# ---- slot predicates ----
64
65def sall_app(~V: Data, +p: ST.SP1<V>, +a: List<&2, Nat>, +b: List<&2, Nat>) -> {ST.sall(~V, p, SC.append(Nat, a, b)) == Bool.and(ST.sall(~V, p, a), ST.sall(~V, p, b)) : Bool}:
66 match a:
67 case Nil{}:
68 {==}
69 case Con{+h, +t}:
70 Equal.trans(Bool, Bool.and(ST.sev(~V, p, h), ST.sall(~V, p, SC.append(Nat, t, b))), Bool.and(ST.sev(~V, p, h), Bool.and(ST.sall(~V, p, t), ST.sall(~V, p, b))), Bool.and(Bool.and(ST.sev(~V, p, h), ST.sall(~V, p, t)), ST.sall(~V, p, b)), Equal.cong(Bool, Bool, z => Bool.and(ST.sev(~V, p, h), z), ST.sall(~V, p, SC.append(Nat, t, b)), Bool.and(ST.sall(~V, p, t), ST.sall(~V, p, b)), sall_app(~V, p, t, b)), NL.and_assoc(ST.sev(~V, p, h), ST.sall(~V, p, t), ST.sall(~V, p, b)))
71
72def sa_c(~V: Data, +p: ST.SP1<V>, +x: Nat, +s0: Nat, +t: List<&2, Nat>, +h: {Bool.and(ST.sev(~V, p, s0), ST.sall(~V, p, t)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(s0, x) == c : Bool}, +hm: {Bool.or(c, NL.memn(x, t)) == True{} : Bool}, rec: @hs: {ST.sall(~V, p, t) == True{} : Bool} -> @hm2: {NL.memn(x, t) == True{} : Bool} -> {ST.sev(~V, p, x) == True{} : Bool}) -> {ST.sev(~V, p, x) == True{} : Bool}:
73 match c:
74 case True{}:
75 L.subst(Nat, z => {ST.sev(~V, p, z) == True{} : Bool}, s0, x, N.eq_from_is_eq(s0, x, hc), L.and_left(ST.sev(~V, p, s0), ST.sall(~V, p, t), h))
76 case False{}:
77 rec(L.and_right(ST.sev(~V, p, s0), ST.sall(~V, p, t), h), hm)
78
79# p holds at a member
80def sall_mem(~V: Data, +p: ST.SP1<V>, +x: Nat, +xs: List<&2, Nat>, +h: {ST.sall(~V, p, xs) == True{} : Bool}, +hm: {NL.memn(x, xs) == True{} : Bool}) -> {ST.sev(~V, p, x) == True{} : Bool}:
81 match xs:
82 case Nil{}:
83 Empty.absurd({ST.sev(~V, p, x) == True{} : Bool}, L.false_true(hm))
84 case Con{+s0, +t}:
85 sa_c(~V, p, x, s0, t, h, Nat.is_eq(s0, x), {==}, hm, hs => hm2 => sall_mem(~V, p, x, t, hs, hm2))
86
87# ---- the model's entries ----
88
89
90def es_app(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +a: List<&2, Nat>, +b: List<&2, Nat>) -> {ST.es(~V, ll, kl, el, SC.append(Nat, a, b)) == SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)) : List<&2, SP.Ent<V>>}:
91 match a:
92 case Nil{}:
93 {==}
94 case Con{+h, +t}:
95 +x = ST.sent_m(~V, ll, kl, h, HT.nthm(~V, el, h))
96 Equal.trans(List<&2, SP.Ent<V>>, SC.append(SP.Ent<V>, x, ST.es(~V, ll, kl, el, SC.append(Nat, t, b))), SC.append(SP.Ent<V>, x, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, t), ST.es(~V, ll, kl, el, b))), SC.append(SP.Ent<V>, SC.append(SP.Ent<V>, x, ST.es(~V, ll, kl, el, t)), ST.es(~V, ll, kl, el, b)), Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, x, z), ST.es(~V, ll, kl, el, SC.append(Nat, t, b)), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, t), ST.es(~V, ll, kl, el, b)), es_app(~V, ll, kl, el, t, b)), Equal.sym(List<&2, SP.Ent<V>>, SC.append(SP.Ent<V>, SC.append(SP.Ent<V>, x, ST.es(~V, ll, kl, el, t)), ST.es(~V, ll, kl, el, b)), SC.append(SP.Ent<V>, x, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, t), ST.es(~V, ll, kl, el, b))), LL.append_assoc(SP.Ent<V>, x, ST.es(~V, ll, kl, el, t), ST.es(~V, ll, kl, el, b))))
97
98def keys_app(~V: Data, +a: List<&2, SP.Ent<V>>, +b: List<&2, SP.Ent<V>>) -> {SP.keys_of(~V, SC.append(SP.Ent<V>, a, b)) == SC.append(String, SP.keys_of(~V, a), SP.keys_of(~V, b)) : List<&2, String>}:
99 match a:
100 case Nil{}:
101 {==}
102 case Con{SP.LE{+k, +v, +t, +d}, +r}:
103 LL.cons_cong(String, k, SP.keys_of(~V, SC.append(SP.Ent<V>, r, b)), SC.append(String, SP.keys_of(~V, r), SP.keys_of(~V, b)), keys_app(~V, r, b))
104
105def snoc_app(~V: Data, +a: List<&2, SP.Ent<V>>, +e: SP.Ent<V>) -> {SP.snoc(~V, a, e) == SC.append(SP.Ent<V>, a, Con{e, Nil{}}) : List<&2, SP.Ent<V>>}:
106 match a:
107 case Nil{}:
108 {==}
109 case Con{+h, +t}:
110 LL.cons_cong(SP.Ent<V>, h, SP.snoc(~V, t, e), SC.append(SP.Ent<V>, t, Con{e, Nil{}}), snoc_app(~V, t, e))
111
112# no entry of a has key
113def enk(~V: Data, a: List<&2, SP.Ent<V>>, +key: String) -> Bool:
114 match a:
115 case Nil{}:
116 True{}
117 case Con{SP.LE{+k, v, t, d}, r}:
118 Bool.and(Bool.not(S.str_eq(k, key)), enk(~V, r, key))
119
120def drop_c(~V: Data, +k: String, +v: V, +t: U32, +d: W.U64, +r: List<&2, SP.Ent<V>>, +b: List<&2, SP.Ent<V>>, +key: String, +c: Bool, +hc: {S.str_eq(k, key) == c : Bool}, +h: {Bool.not(c) == True{} : Bool}, +ih: {SP.drop(~V, SC.append(SP.Ent<V>, r, b), key) == SC.append(SP.Ent<V>, r, SP.drop(~V, b, key)) : List<&2, SP.Ent<V>>}) -> {SP.drop(~V, SC.append(SP.Ent<V>, Con{SP.LE{k, v, t, d}, r}, b), key) == SC.append(SP.Ent<V>, Con{SP.LE{k, v, t, d}, r}, SP.drop(~V, b, key)) : List<&2, SP.Ent<V>>}:
121 match c:
122 case True{}:
123 Empty.absurd({SP.drop(~V, SC.append(SP.Ent<V>, Con{SP.LE{k, v, t, d}, r}, b), key) == SC.append(SP.Ent<V>, Con{SP.LE{k, v, t, d}, r}, SP.drop(~V, b, key)) : List<&2, SP.Ent<V>>}, L.false_true(h))
124 case False{}:
125 L.subst(Bool, z => {Bool.pick(List<&2, SP.Ent<V>>, z, SC.append(SP.Ent<V>, r, b), Con{SP.LE{k, v, t, d}, SP.drop(~V, SC.append(SP.Ent<V>, r, b), key)}) == SC.append(SP.Ent<V>, Con{SP.LE{k, v, t, d}, r}, SP.drop(~V, b, key)) : List<&2, SP.Ent<V>>}, False{}, S.str_eq(k, key), Equal.sym(Bool, S.str_eq(k, key), False{}, hc), LL.cons_cong(SP.Ent<V>, SP.LE{k, v, t, d}, SP.drop(~V, SC.append(SP.Ent<V>, r, b), key), SC.append(SP.Ent<V>, r, SP.drop(~V, b, key)), ih))
126
127# drop skips a prefix without key
128def drop_app(~V: Data, +a: List<&2, SP.Ent<V>>, +b: List<&2, SP.Ent<V>>, +key: String, +h: {enk(~V, a, key) == True{} : Bool}) -> {SP.drop(~V, SC.append(SP.Ent<V>, a, b), key) == SC.append(SP.Ent<V>, a, SP.drop(~V, b, key)) : List<&2, SP.Ent<V>>}:
129 match a:
130 case Nil{}:
131 {==}
132 case Con{SP.LE{+k, +v, +t, +d}, +r}:
133 drop_c(~V, k, v, t, d, r, b, key, S.str_eq(k, key), {==}, L.and_left(Bool.not(S.str_eq(k, key)), enk(~V, r, key), h), drop_app(~V, r, b, key, L.and_right(Bool.not(S.str_eq(k, key)), enk(~V, r, key), h)))
134
135# ---- splitting a duplicate-free list ----
136
137
138
139
140
141
142
143
144
145# a member of x is not in a
146
147
148# a member of a is not in x