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 ../../lib/u32div.bend as UD 7 import ../../../src/math/u64.bend as W 8 import ../../../src/containers/hash_table.bend as H 9 import ../hash_table/buckets.bend as B 10 import ../hash_table/state.bend as HT 11 import ../hash_table/table.bend as TB 12 import ../hash_table/tools.bend as TL 13 import ./state.bend as ST 14 import ./dll.bend as DL 15 import ./elfr.bend as EF 16 import ./walk.bend as WL 17 import ../../lib/nat_list.bend as NL 18 import ../../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 24 def 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 27 def 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 30 def 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 37 def 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 47 def 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 50 def 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 58 def 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 65 def 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 72 def 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 83 def 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 86 def 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 102 def 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 112 def 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>}: 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>}, 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>}, 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>}, 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>}, 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>, 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 125 def 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>}: 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>, List<&2, SP.Ent>, z => SC.append(SP.Ent, 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>, SC.append(SP.Ent, 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, 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, ST.sent_m(~V, ll, kl, s, m), ST.es(~V, ll, kl, el, t)), a, Equal.cong(List<&2, SP.Ent>, List<&2, SP.Ent>, z => SC.append(SP.Ent, 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))))