proofs/containers/lru/hw.bend
bend-collections-laws-containers@1.0.0.0 · 133 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/lib/u32div.bend as UD
7import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as W
8import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
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/hash_table/table.bend as TB
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/tools.bend as TL
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/dll.bend as DL
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/elfr.bend as EF
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/walk.bend as WL
17import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
18import bend-collections-laws-containers@1.0.0.0/proofs/lib/links.bend as LK
19
20# Writes to a slot's data words (o >= 3: the lifetime and deadline) keep its
21# links and its stored hash word; a value written to a slot keeps it live.
22
23
24def ne_hi(+o2: Nat, +o: Nat, +h: {Nat.is_lt(o2, 3n) == True{} : Bool}, +h3: {Nat.is_le(3n, o) == True{} : Bool}) -> {Nat.is_eq(o, o2) == False{} : Bool}:
25 NL.ne_sym(o2, o, N.is_eq_lt(o2, o, N.lt_le_trans(o2, 3n, o, h, h3)))
26
27def lw_lo3(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h3: {Nat.is_le(3n, o) == True{} : Bool}, +x: Nat, +o2: Nat, +ho2: {Nat.is_lt(o2, 8n) == True{} : Bool}, +h: {Nat.is_lt(o2, 3n) == True{} : Bool}) -> {ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, o2) == ST.lw(ll, x, o2) : U32}:
28 DL.lw_other(ll, y, o, v, ho, x, o2, ho2, DL.ne_word(y, x, o, o2, ne_hi(o2, o, h, h3)))
29
30def seg_hw(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h3: {Nat.is_le(3n, o) == True{} : Bool}, +sl: List<&2, Nat>, +p: U32, +q: U32) -> {ST.seg(SC.update(U32, ll, ST.off(y, o), v), sl, p, q) == ST.seg(ll, sl, p, q) : Bool}:
31 match sl:
32 case Nil{}:
33 {==}
34 case Con{+s, +t}:
35 DL.seg_c(SC.update(U32, ll, ST.off(y, o), v), ll, s, t, p, q, lw_lo3(ll, y, o, v, ho, h3, s, 0n, {==}, {==}), lw_lo3(ll, y, o, v, ho, h3, s, 1n, {==}, {==}), seg_hw(ll, y, o, v, ho, h3, t, LK.lnk(s), q))
36
37def fll_hw(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h3: {Nat.is_le(3n, o) == True{} : Bool}, +fl: List<&2, Nat>) -> {ST.fll(SC.update(U32, ll, ST.off(y, o), v), fl) == ST.fll(ll, fl) : Bool}:
38 match fl:
39 case Nil{}:
40 {==}
41 case Con{+s, +t}:
42 +e1 = lw_lo3(ll, y, o, v, ho, h3, s, 1n, {==}, {==})
43 +ih = fll_hw(ll, y, o, v, ho, h3, t)
44 +r1 = L.subst(U32, z => {Bool.and(U32.is_eq(z, LK.fst_or(t, 0)), ST.fll(ll, t)) == ST.fll(ll, Con{s, t}) : Bool}, ST.lw(ll, s, 1n), ST.lw(SC.update(U32, ll, ST.off(y, o), v), s, 1n), Equal.sym(U32, ST.lw(SC.update(U32, ll, ST.off(y, o), v), s, 1n), ST.lw(ll, s, 1n), e1), {==})
45 L.subst(Bool, z => {Bool.and(U32.is_eq(ST.lw(SC.update(U32, ll, ST.off(y, o), v), s, 1n), LK.fst_or(t, 0)), z) == ST.fll(ll, Con{s, t}) : Bool}, ST.fll(ll, t), ST.fll(SC.update(U32, ll, ST.off(y, o), v), t), Equal.sym(Bool, ST.fll(SC.update(U32, ll, ST.off(y, o), v), t), ST.fll(ll, t), ih), r1)
46
47def skey_hw(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h3: {Nat.is_le(3n, o) == True{} : Bool}, +kl: List<&2, String>, +x: Nat) -> {ST.skey(SC.update(U32, ll, ST.off(y, o), v), kl, x) == ST.skey(ll, kl, x) : String}:
48 Equal.cong(U32, String, z => TB.keyof(z, TB.nths(kl, x)), ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 2n), ST.lw(ll, x, 2n), lw_lo3(ll, y, o, v, ho, h3, x, 2n, {==}, {==}))
49
50def has_hw(~V: Data, +ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h3: {Nat.is_le(3n, o) == True{} : Bool}, +bs: List<&2, B.Bk>, +m: Nat, +sl: List<&2, Nat>) -> {ST.hasall(~V, bs, m, SC.update(U32, ll, ST.off(y, o), v), sl) == ST.hasall(~V, bs, m, ll, sl) : Bool}:
51 match sl:
52 case Nil{}:
53 {==}
54 case Con{+s, +t}:
55 +e = Equal.cong(U32, Bool, z => ST.anyb(bs, m, LK.lnk(s), z), ST.lw(SC.update(U32, ll, ST.off(y, o), v), s, 2n), ST.lw(ll, s, 2n), lw_lo3(ll, y, o, v, ho, h3, s, 2n, {==}, {==}))
56 Equal.trans(Bool, Bool.and(ST.anyb(bs, m, LK.lnk(s), ST.lw(SC.update(U32, ll, ST.off(y, o), v), s, 2n)), ST.hasall(~V, bs, m, SC.update(U32, ll, ST.off(y, o), v), t)), Bool.and(ST.anyb(bs, m, LK.lnk(s), ST.lw(ll, s, 2n)), ST.hasall(~V, bs, m, SC.update(U32, ll, ST.off(y, o), v), t)), Bool.and(ST.anyb(bs, m, LK.lnk(s), ST.lw(ll, s, 2n)), ST.hasall(~V, bs, m, ll, t)), Equal.cong(Bool, Bool, z => Bool.and(z, ST.hasall(~V, bs, m, SC.update(U32, ll, ST.off(y, o), v), t)), ST.anyb(bs, m, LK.lnk(s), ST.lw(SC.update(U32, ll, ST.off(y, o), v), s, 2n)), ST.anyb(bs, m, LK.lnk(s), ST.lw(ll, s, 2n)), e), Equal.cong(Bool, Bool, z => Bool.and(ST.anyb(bs, m, LK.lnk(s), ST.lw(ll, s, 2n)), z), ST.hasall(~V, bs, m, SC.update(U32, ll, ST.off(y, o), v), t), ST.hasall(~V, bs, m, ll, t), has_hw(~V, ll, y, o, v, ho, h3, bs, m, t)))
57
58def bslb_hw(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h3: {Nat.is_le(3n, o) == True{} : Bool}, +sl: List<&2, Nat>, +b: B.Bk) -> {ST.bslb(sl, SC.update(U32, ll, ST.off(y, o), v), b) == ST.bslb(sl, ll, b) : Bool}:
59 match b:
60 case B.BE{}:
61 {==}
62 case B.BF{+w, +l, +k}:
63 Equal.cong(U32, Bool, z => Bool.and(NL.memn(UD.v(H.slot(l)), sl), U32.is_eq(z, w)), ST.lw(SC.update(U32, ll, ST.off(y, o), v), UD.v(H.slot(l)), 2n), ST.lw(ll, UD.v(H.slot(l)), 2n), lw_lo3(ll, y, o, v, ho, h3, UD.v(H.slot(l)), 2n, {==}, {==}))
64
65def bsl_hw(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h3: {Nat.is_le(3n, o) == True{} : Bool}, +bs: List<&2, B.Bk>, +sl: List<&2, Nat>, +m: Nat) -> {ST.bsl(bs, sl, SC.update(U32, ll, ST.off(y, o), v), m) == ST.bsl(bs, sl, ll, m) : Bool}:
66 match m:
67 case 0n:
68 {==}
69 case 1n+j:
70 Equal.trans(Bool, Bool.and(ST.bslb(sl, SC.update(U32, ll, ST.off(y, o), v), B.at(bs, j)), ST.bsl(bs, sl, SC.update(U32, ll, ST.off(y, o), v), j)), Bool.and(ST.bslb(sl, ll, B.at(bs, j)), ST.bsl(bs, sl, SC.update(U32, ll, ST.off(y, o), v), j)), Bool.and(ST.bslb(sl, ll, B.at(bs, j)), ST.bsl(bs, sl, ll, j)), Equal.cong(Bool, Bool, z => Bool.and(z, ST.bsl(bs, sl, SC.update(U32, ll, ST.off(y, o), v), j)), ST.bslb(sl, SC.update(U32, ll, ST.off(y, o), v), B.at(bs, j)), ST.bslb(sl, ll, B.at(bs, j)), bslb_hw(ll, y, o, v, ho, h3, sl, B.at(bs, j))), Equal.cong(Bool, Bool, z => Bool.and(ST.bslb(sl, ll, B.at(bs, j)), z), ST.bsl(bs, sl, SC.update(U32, ll, ST.off(y, o), v), j), ST.bsl(bs, sl, ll, j), bsl_hw(ll, y, o, v, ho, h3, bs, sl, j)))
71
72def mapk_hw(+ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +h3: {Nat.is_le(3n, o) == True{} : Bool}, +kl: List<&2, String>, +xs: List<&2, Nat>) -> {WL.mapk(SC.update(U32, ll, ST.off(y, o), v), kl, xs) == WL.mapk(ll, kl, xs) : List<&2, String>}:
73 match xs:
74 case Nil{}:
75 {==}
76 case Con{+x, +t}:
77 Equal.trans(List<&2, String>, Con{ST.skey(SC.update(U32, ll, ST.off(y, o), v), kl, x), WL.mapk(SC.update(U32, ll, ST.off(y, o), v), kl, t)}, Con{ST.skey(ll, kl, x), WL.mapk(SC.update(U32, ll, ST.off(y, o), v), kl, t)}, Con{ST.skey(ll, kl, x), WL.mapk(ll, kl, t)}, Equal.cong(String, List<&2, String>, z => Con{z, WL.mapk(SC.update(U32, ll, ST.off(y, o), v), kl, t)}, ST.skey(SC.update(U32, ll, ST.off(y, o), v), kl, x), ST.skey(ll, kl, x), skey_hw(ll, y, o, v, ho, h3, kl, x)), Equal.cong(List<&2, String>, List<&2, String>, z => Con{ST.skey(ll, kl, x), z}, WL.mapk(SC.update(U32, ll, ST.off(y, o), v), kl, t), WL.mapk(ll, kl, t), mapk_hw(ll, y, o, v, ho, h3, kl, t)))
78
79# ---- a value written to a slot ----
80
81
82# the written slot is live
83def live_same(~V: Data, +el: List<&2, Maybe<&2, V>>, +y: Nat, +w: V, +hlen: {Nat.is_lt(y, SC.length(Maybe<&2, V>, el)) == True{} : Bool}) -> {ST.live(~V, SC.update(Maybe<&2, V>, el, y, Some{w}), y) == True{} : Bool}:
84 Equal.cong(Maybe<&2, V>, Bool, z => HT.some_b(~V, z), HT.nthm(~V, SC.update(Maybe<&2, V>, el, y, Some{w}), y), Some{w}, TL.nthm_upd_same(~V, el, y, Some{w}, hlen))
85
86def sl_c(~V: Data, +el: List<&2, Maybe<&2, V>>, +y: Nat, +w: V, +fr: Nat, +x: Nat, +t: List<&2, Nat>, +hlen: {Nat.is_lt(y, SC.length(Maybe<&2, V>, el)) == True{} : Bool}, +h: {ST.slok(~V, Con{x, t}, fr, el) == True{} : Bool}, +ih: {ST.slok(~V, t, fr, SC.update(Maybe<&2, V>, el, y, Some{w})) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(y, x) == c : Bool}) -> {ST.slok(~V, Con{x, t}, fr, SC.update(Maybe<&2, V>, el, y, Some{w})) == True{} : Bool}:
87 match c:
88 case True{}:
89 +h0 = L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h)
90 +hx = L.and_left(Nat.is_lt(x, fr), ST.live(~V, el, x), h0)
91 +hl = L.and_right(Nat.is_lt(x, fr), ST.live(~V, el, x), h0)
92 +lv = L.subst(Nat, z => {ST.live(~V, SC.update(Maybe<&2, V>, el, y, Some{w}), z) == True{} : Bool}, y, x, N.eq_from_is_eq(y, x, hc), live_same(~V, el, y, w, hlen))
93 L.and_intro(Bool.and(Nat.is_lt(x, fr), ST.live(~V, SC.update(Maybe<&2, V>, el, y, Some{w}), x)), ST.slok(~V, t, fr, SC.update(Maybe<&2, V>, el, y, Some{w})), L.and_intro(Nat.is_lt(x, fr), ST.live(~V, SC.update(Maybe<&2, V>, el, y, Some{w}), x), hx, lv), ih)
94 case False{}:
95 +h0 = L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h)
96 +hx = L.and_left(Nat.is_lt(x, fr), ST.live(~V, el, x), h0)
97 +hl = L.and_right(Nat.is_lt(x, fr), ST.live(~V, el, x), h0)
98 +lv = Equal.trans(Bool, ST.live(~V, SC.update(Maybe<&2, V>, el, y, Some{w}), x), ST.live(~V, el, x), True{}, EF.live_el(~V, el, y, Some{w}, x, hc), hl)
99 L.and_intro(Bool.and(Nat.is_lt(x, fr), ST.live(~V, SC.update(Maybe<&2, V>, el, y, Some{w}), x)), ST.slok(~V, t, fr, SC.update(Maybe<&2, V>, el, y, Some{w})), L.and_intro(Nat.is_lt(x, fr), ST.live(~V, SC.update(Maybe<&2, V>, el, y, Some{w}), x), hx, lv), ih)
100
101# a value written anywhere keeps every listed slot live
102def slok_live(~V: Data, +el: List<&2, Maybe<&2, V>>, +y: Nat, +w: V, +fr: Nat, +xs: List<&2, Nat>, +hlen: {Nat.is_lt(y, SC.length(Maybe<&2, V>, el)) == True{} : Bool}, +h: {ST.slok(~V, xs, fr, el) == True{} : Bool}) -> {ST.slok(~V, xs, fr, SC.update(Maybe<&2, V>, el, y, Some{w})) == True{} : Bool}:
103 match xs:
104 case Nil{}:
105 {==}
106 case Con{+x, +t}:
107 sl_c(~V, el, y, w, fr, x, t, hlen, h, slok_live(~V, el, y, w, fr, t, hlen, L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h)), Nat.is_eq(y, x), {==})
108
109# ---- writes to a slot off the list ----
110
111
112def sent_fs(~V: Data, +ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +kl: List<&2, String>, +x: Nat, +hyx: {Nat.is_eq(y, x) == False{} : Bool}, +m: Maybe<&2, V>) -> {ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, x, m) == ST.sent_m(~V, ll, kl, x, m) : List<&2, SP.Ent<V>>}:
113 match m:
114 case None{}:
115 {==}
116 case Some{+w}:
117 +ek = Equal.cong(U32, String, z => TB.keyof(z, TB.nths(kl, x)), ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 2n), ST.lw(ll, x, 2n), DL.lw_other(ll, y, o, v, ho, x, 2n, {==}, DL.ne_slot(y, x, o, 2n, hyx)))
118 +r1 = L.subst(String, z => {Con{SP.LE{z, w, ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 3n), W.U64{ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 4n), ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 5n)}}, Nil{}} == ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, x, Some{w}) : List<&2, SP.Ent<V>>}, ST.skey(SC.update(U32, ll, ST.off(y, o), v), kl, x), ST.skey(ll, kl, x), ek, {==})
119 +r2 = L.subst(U32, z => {Con{SP.LE{ST.skey(ll, kl, x), w, z, W.U64{ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 4n), ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 5n)}}, Nil{}} == ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, x, Some{w}) : List<&2, SP.Ent<V>>}, ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 3n), ST.lw(ll, x, 3n), DL.lw_other(ll, y, o, v, ho, x, 3n, {==}, DL.ne_slot(y, x, o, 3n, hyx)), r1)
120 +r3 = L.subst(U32, z => {Con{SP.LE{ST.skey(ll, kl, x), w, ST.lw(ll, x, 3n), W.U64{z, ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 5n)}}, Nil{}} == ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, x, Some{w}) : List<&2, SP.Ent<V>>}, ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 4n), ST.lw(ll, x, 4n), DL.lw_other(ll, y, o, v, ho, x, 4n, {==}, DL.ne_slot(y, x, o, 4n, hyx)), r2)
121 +r4 = L.subst(U32, z => {Con{SP.LE{ST.skey(ll, kl, x), w, ST.lw(ll, x, 3n), W.U64{ST.lw(ll, x, 4n), z}}, Nil{}} == ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, x, Some{w}) : List<&2, SP.Ent<V>>}, ST.lw(SC.update(U32, ll, ST.off(y, o), v), x, 5n), ST.lw(ll, x, 5n), DL.lw_other(ll, y, o, v, ho, x, 5n, {==}, DL.ne_slot(y, x, o, 5n, hyx)), r3)
122 Equal.sym(List<&2, SP.Ent<V>>, ST.sent_m(~V, ll, kl, x, Some{w}), ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, x, Some{w}), r4)
123
124# a write to a slot off xs leaves the entries of xs
125def es_fs(~V: Data, +ll: List<&2, U32>, +y: Nat, +o: Nat, +v: U32, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +xs: List<&2, Nat>, +hy: {NL.memn(y, xs) == False{} : Bool}) -> {ST.es(~V, SC.update(U32, ll, ST.off(y, o), v), kl, el, xs) == ST.es(~V, ll, kl, el, xs) : List<&2, SP.Ent<V>>}:
126 match xs:
127 case Nil{}:
128 {==}
129 case Con{+s, +t}:
130 +hyx = NL.ne_sym(s, y, NL.or_ff_l(Nat.is_eq(s, y), NL.memn(y, t), hy))
131 +m = HT.nthm(~V, el, s)
132 +a = Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, z, ST.es(~V, SC.update(U32, ll, ST.off(y, o), v), kl, el, t)), ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, s, m), ST.sent_m(~V, ll, kl, s, m), sent_fs(~V, ll, y, o, v, ho, kl, s, hyx, m))
133 Equal.trans(List<&2, SP.Ent<V>>, SC.append(SP.Ent<V>, ST.sent_m(~V, SC.update(U32, ll, ST.off(y, o), v), kl, s, m), ST.es(~V, SC.update(U32, ll, ST.off(y, o), v), kl, el, t)), SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, m), ST.es(~V, SC.update(U32, ll, ST.off(y, o), v), kl, el, t)), SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, m), ST.es(~V, ll, kl, el, t)), a, Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, m), z), ST.es(~V, SC.update(U32, ll, ST.off(y, o), v), kl, el, t), ST.es(~V, ll, kl, el, t), es_fs(~V, ll, y, o, v, ho, kl, el, t, NL.or_ff_r(Nat.is_eq(s, y), NL.memn(y, t), hy))))