proofs/containers/lru/pre.bend source

proofs/containers/lru/pre.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/array.bend as ARimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/lru.bend as SPimport ../../lib/u32div.bend as UDimport ../../../src/math/u64.bend as Wimport ../../../src/containers/hash_table.bend as Himport ../../../src/containers/lru.bend as LRimport ../hash_table/buckets.bend as Bimport ../hash_table/state.bend as HTimport ../hash_table/table.bend as TBimport ../hash_table/arena.bend as ANimport ./state.bend as STimport ./dll.bend as DLimport ./idx.bend as IDimport ../hash_table/keys.bend as Kimport ../../lib/nat_list.bend as NLimport ../../lib/links.bend as LKimport ../../lib/words32.bend as W32# The grown arena: every array gains a blank second half; the invariant and# the model read the first half only.def nth0_app(+xs: List<&2, U32>, +r: List<&2, U32>, +t: Nat, +h: {Nat.is_lt(t, SC.length(U32, xs)) == True{} : Bool}) -> {W32.nth0(SC.append(U32, xs, r), t) == W32.nth0(xs, t) : U32}:  match xs t:    case Nil{} _:      Empty.absurd({W32.nth0(SC.append(U32, Nil{}, r), t) == W32.nth0(Nil{}, t) : U32}, N.lt_zero_absurd(t, h))    case Con{x, u} 0n:      {==}    case Con{x, u} 1n+p:      nth0_app(u, r, p, h)def lw_app(+ll: List<&2, U32>, +rl: List<&2, U32>, +sd: Nat, +hl: {SC.length(U32, ll) == SC.pow2(3n+sd) : Nat}, +x: Nat, +hx: {Nat.is_lt(x, SC.pow2(sd)) == True{} : Bool}, +o: Nat, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}) -> {ST.lw(SC.append(U32, ll, rl), x, o) == ST.lw(ll, x, o) : U32}:  nth0_app(ll, rl, ST.off(x, o), AN.len_eq_lt(U32, ll, 3n+sd, hl, ST.off(x, o), ID.off_lt(x, sd, hx, o, ho)))def skey_app(+ll: List<&2, U32>, +rl: List<&2, U32>, +sd: Nat, +hl: {SC.length(U32, ll) == SC.pow2(3n+sd) : Nat}, +kl: List<&2, String>, +rk: List<&2, String>, +hk: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +x: Nat, +hx: {Nat.is_lt(x, SC.pow2(sd)) == True{} : Bool}) -> {ST.skey(SC.append(U32, ll, rl), SC.append(String, kl, rk), x) == ST.skey(ll, kl, x) : String}:  Equal.trans(String, TB.keyof(ST.lw(SC.append(U32, ll, rl), x, 2n), TB.nths(SC.append(String, kl, rk), x)), TB.keyof(ST.lw(ll, x, 2n), TB.nths(SC.append(String, kl, rk), x)), TB.keyof(ST.lw(ll, x, 2n), TB.nths(kl, x)), Equal.cong(U32, String, z => TB.keyof(z, TB.nths(SC.append(String, kl, rk), x)), ST.lw(SC.append(U32, ll, rl), x, 2n), ST.lw(ll, x, 2n), lw_app(ll, rl, sd, hl, x, hx, 2n, {==})), Equal.cong(String, String, z => TB.keyof(ST.lw(ll, x, 2n), z), TB.nths(SC.append(String, kl, rk), x), TB.nths(kl, x), AN.nths_app(kl, rk, x, AN.len_eq_lt(String, kl, sd, hk, x, hx))))def sent_app(~V: Data, +ll: List<&2, U32>, +rl: List<&2, U32>, +sd: Nat, +hl: {SC.length(U32, ll) == SC.pow2(3n+sd) : Nat}, +kl: List<&2, String>, +rk: List<&2, String>, +hk: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +x: Nat, +hx: {Nat.is_lt(x, SC.pow2(sd)) == True{} : Bool}, +m: Maybe<&2, V>) -> {ST.sent_m(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), x, m) == ST.sent_m(~V, ll, kl, x, m) : List<&2, SP.Ent<V>>}:  match m:    case None{}:      {==}    case Some{+w}:      +r1 = L.subst(String, z => {Con{SP.LE{z, w, ST.lw(SC.append(U32, ll, rl), x, 3n), W.U64{ST.lw(SC.append(U32, ll, rl), x, 4n), ST.lw(SC.append(U32, ll, rl), x, 5n)}}, Nil{}} == ST.sent_m(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), x, Some{w}) : List<&2, SP.Ent<V>>}, ST.skey(SC.append(U32, ll, rl), SC.append(String, kl, rk), x), ST.skey(ll, kl, x), skey_app(ll, rl, sd, hl, kl, rk, hk, x, hx), {==})      +r2 = L.subst(U32, z => {Con{SP.LE{ST.skey(ll, kl, x), w, z, W.U64{ST.lw(SC.append(U32, ll, rl), x, 4n), ST.lw(SC.append(U32, ll, rl), x, 5n)}}, Nil{}} == ST.sent_m(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), x, Some{w}) : List<&2, SP.Ent<V>>}, ST.lw(SC.append(U32, ll, rl), x, 3n), ST.lw(ll, x, 3n), lw_app(ll, rl, sd, hl, x, hx, 3n, {==}), r1)      +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.append(U32, ll, rl), x, 5n)}}, Nil{}} == ST.sent_m(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), x, Some{w}) : List<&2, SP.Ent<V>>}, ST.lw(SC.append(U32, ll, rl), x, 4n), ST.lw(ll, x, 4n), lw_app(ll, rl, sd, hl, x, hx, 4n, {==}), r2)      +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.append(U32, ll, rl), SC.append(String, kl, rk), x, Some{w}) : List<&2, SP.Ent<V>>}, ST.lw(SC.append(U32, ll, rl), x, 5n), ST.lw(ll, x, 5n), lw_app(ll, rl, sd, hl, x, hx, 5n, {==}), r3)      Equal.sym(List<&2, SP.Ent<V>>, ST.sent_m(~V, ll, kl, x, Some{w}), ST.sent_m(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), x, Some{w}), r4)def es_pre(~V: Data, +ll: List<&2, U32>, +rl: List<&2, U32>, +sd: Nat, +hl: {SC.length(U32, ll) == SC.pow2(3n+sd) : Nat}, +kl: List<&2, String>, +rk: List<&2, String>, +hk: {SC.length(String, kl) == SC.pow2(sd) : Nat}, +el: List<&2, Maybe<&2, V>>, +re: List<&2, Maybe<&2, V>>, +he: {SC.length(Maybe<&2, V>, el) == SC.pow2(sd) : Nat}, +fr: Nat, +hfr: {Nat.is_le(fr, SC.pow2(sd)) == True{} : Bool}, +xs: List<&2, Nat>, +h: {ST.slok(~V, xs, fr, el) == True{} : Bool}) -> {ST.es(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), SC.append(Maybe<&2, V>, el, re), xs) == ST.es(~V, ll, kl, el, xs) : List<&2, SP.Ent<V>>}:  match xs:    case Nil{}:      {==}    case Con{+x, +t}:      +hx = N.lt_le_trans(x, fr, SC.pow2(sd), L.and_left(Nat.is_lt(x, fr), ST.live(~V, el, x), L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h)), hfr)      +em = AN.nthm_app(~V, el, re, x, AN.len_eq_lt(Maybe<&2, V>, el, sd, he, x, hx))      +a = Equal.cong(Maybe<&2, V>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, ST.sent_m(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), x, z), ST.es(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), SC.append(Maybe<&2, V>, el, re), t)), HT.nthm(~V, SC.append(Maybe<&2, V>, el, re), x), HT.nthm(~V, el, x), em)      +b = Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, z, ST.es(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), SC.append(Maybe<&2, V>, el, re), t)), ST.sent_m(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), x, HT.nthm(~V, el, x)), ST.sent_m(~V, ll, kl, x, HT.nthm(~V, el, x)), sent_app(~V, ll, rl, sd, hl, kl, rk, hk, x, hx, HT.nthm(~V, el, x)))      +c = Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, x, HT.nthm(~V, el, x)), z), ST.es(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), SC.append(Maybe<&2, V>, el, re), t), ST.es(~V, ll, kl, el, t), es_pre(~V, ll, rl, sd, hl, kl, rk, hk, el, re, he, fr, hfr, t, L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h)))      Equal.trans(List<&2, SP.Ent<V>>, SC.append(SP.Ent<V>, ST.sent_m(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), x, HT.nthm(~V, SC.append(Maybe<&2, V>, el, re), x)), ST.es(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), SC.append(Maybe<&2, V>, el, re), t)), SC.append(SP.Ent<V>, ST.sent_m(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), x, HT.nthm(~V, el, x)), ST.es(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), SC.append(Maybe<&2, V>, el, re), t)), SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, x, HT.nthm(~V, el, x)), ST.es(~V, ll, kl, el, t)), a, Equal.trans(List<&2, SP.Ent<V>>, SC.append(SP.Ent<V>, ST.sent_m(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), x, HT.nthm(~V, el, x)), ST.es(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), SC.append(Maybe<&2, V>, el, re), t)), SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, x, HT.nthm(~V, el, x)), ST.es(~V, SC.append(U32, ll, rl), SC.append(String, kl, rk), SC.append(Maybe<&2, V>, el, re), t)), SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, x, HT.nthm(~V, el, x)), ST.es(~V, ll, kl, el, t)), b, c))def seg_pre(~V: Data, +ll: List<&2, U32>, +rl: List<&2, U32>, +sd: Nat, +hl: {SC.length(U32, ll) == SC.pow2(3n+sd) : Nat}, +el: List<&2, Maybe<&2, V>>, +fr: Nat, +hfr: {Nat.is_le(fr, SC.pow2(sd)) == True{} : Bool}, +xs: List<&2, Nat>, +h: {ST.slok(~V, xs, fr, el) == True{} : Bool}, +p: U32, +q: U32) -> {ST.seg(SC.append(U32, ll, rl), xs, p, q) == ST.seg(ll, xs, p, q) : Bool}:  match xs:    case Nil{}:      {==}    case Con{+x, +t}:      +hx = N.lt_le_trans(x, fr, SC.pow2(sd), L.and_left(Nat.is_lt(x, fr), ST.live(~V, el, x), L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h)), hfr)      DL.seg_c(SC.append(U32, ll, rl), ll, x, t, p, q, lw_app(ll, rl, sd, hl, x, hx, 0n, {==}), lw_app(ll, rl, sd, hl, x, hx, 1n, {==}), seg_pre(~V, ll, rl, sd, hl, el, fr, hfr, t, L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h), LK.lnk(x), q))def has_pre(~V: Data, +bs: List<&2, B.Bk>, +m: Nat, +ll: List<&2, U32>, +rl: List<&2, U32>, +sd: Nat, +hl: {SC.length(U32, ll) == SC.pow2(3n+sd) : Nat}, +el: List<&2, Maybe<&2, V>>, +fr: Nat, +hfr: {Nat.is_le(fr, SC.pow2(sd)) == True{} : Bool}, +xs: List<&2, Nat>, +h: {ST.slok(~V, xs, fr, el) == True{} : Bool}) -> {ST.hasall(~V, bs, m, SC.append(U32, ll, rl), xs) == ST.hasall(~V, bs, m, ll, xs) : Bool}:  match xs:    case Nil{}:      {==}    case Con{+x, +t}:      +hx = N.lt_le_trans(x, fr, SC.pow2(sd), L.and_left(Nat.is_lt(x, fr), ST.live(~V, el, x), L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h)), hfr)      +e = Equal.cong(U32, Bool, z => ST.anyb(bs, m, LK.lnk(x), z), ST.lw(SC.append(U32, ll, rl), x, 2n), ST.lw(ll, x, 2n), lw_app(ll, rl, sd, hl, x, hx, 2n, {==}))      Equal.trans(Bool, Bool.and(ST.anyb(bs, m, LK.lnk(x), ST.lw(SC.append(U32, ll, rl), x, 2n)), ST.hasall(~V, bs, m, SC.append(U32, ll, rl), t)), Bool.and(ST.anyb(bs, m, LK.lnk(x), ST.lw(ll, x, 2n)), ST.hasall(~V, bs, m, SC.append(U32, ll, rl), t)), Bool.and(ST.anyb(bs, m, LK.lnk(x), ST.lw(ll, x, 2n)), ST.hasall(~V, bs, m, ll, t)), Equal.cong(Bool, Bool, z => Bool.and(z, ST.hasall(~V, bs, m, SC.append(U32, ll, rl), t)), ST.anyb(bs, m, LK.lnk(x), ST.lw(SC.append(U32, ll, rl), x, 2n)), ST.anyb(bs, m, LK.lnk(x), ST.lw(ll, x, 2n)), e), Equal.cong(Bool, Bool, z => Bool.and(ST.anyb(bs, m, LK.lnk(x), ST.lw(ll, x, 2n)), z), ST.hasall(~V, bs, m, SC.append(U32, ll, rl), t), ST.hasall(~V, bs, m, ll, t), has_pre(~V, bs, m, ll, rl, sd, hl, el, fr, hfr, t, L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h))))def slok_pre(~V: Data, +sd: Nat, +el: List<&2, Maybe<&2, V>>, +re: List<&2, Maybe<&2, V>>, +he: {SC.length(Maybe<&2, V>, el) == SC.pow2(sd) : Nat}, +fr: Nat, +hfr: {Nat.is_le(fr, SC.pow2(sd)) == True{} : Bool}, +xs: List<&2, Nat>, +h: {ST.slok(~V, xs, fr, el) == True{} : Bool}) -> {ST.slok(~V, xs, fr, SC.append(Maybe<&2, V>, el, re)) == True{} : Bool}:  match xs:    case Nil{}:      {==}    case Con{+x, +t}:      +hx = N.lt_le_trans(x, fr, SC.pow2(sd), L.and_left(Nat.is_lt(x, fr), ST.live(~V, el, x), L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h)), hfr)      +hl = L.and_right(Nat.is_lt(x, fr), ST.live(~V, el, x), L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h))      +el2 = Equal.trans(Bool, ST.live(~V, SC.append(Maybe<&2, V>, el, re), x), ST.live(~V, el, x), True{}, Equal.cong(Maybe<&2, V>, Bool, z => HT.some_b(~V, z), HT.nthm(~V, SC.append(Maybe<&2, V>, el, re), x), HT.nthm(~V, el, x), AN.nthm_app(~V, el, re, x, AN.len_eq_lt(Maybe<&2, V>, el, sd, he, x, hx))), hl)      L.and_intro(Bool.and(Nat.is_lt(x, fr), ST.live(~V, SC.append(Maybe<&2, V>, el, re), x)), ST.slok(~V, t, fr, SC.append(Maybe<&2, V>, el, re)), L.and_intro(Nat.is_lt(x, fr), ST.live(~V, SC.append(Maybe<&2, V>, el, re), x), L.and_left(Nat.is_lt(x, fr), ST.live(~V, el, x), L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h)), el2), slok_pre(~V, sd, el, re, he, fr, hfr, t, L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, el), h)))def bslb_pre(+sl: List<&2, Nat>, +ll: List<&2, U32>, +rl: List<&2, U32>, +sd: Nat, +hl: {SC.length(U32, ll) == SC.pow2(3n+sd) : Nat}, +b: B.Bk, +hw: {B.wb(sd, b) == True{} : Bool}) -> {ST.bslb(sl, SC.append(U32, ll, rl), b) == ST.bslb(sl, ll, b) : Bool}:  match b:    case B.BE{}:      {==}    case B.BF{+w, +l, +k}:      +hx = L.and_left(Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)), Bool.and(U32.is_eq(w, K.kword(k)), Bool.not(U32.is_eq(l, 0))), hw)      Equal.cong(U32, Bool, z => Bool.and(NL.memn(UD.v(H.slot(l)), sl), U32.is_eq(z, w)), ST.lw(SC.append(U32, ll, rl), UD.v(H.slot(l)), 2n), ST.lw(ll, UD.v(H.slot(l)), 2n), lw_app(ll, rl, sd, hl, UD.v(H.slot(l)), hx, 2n, {==}))def bsl_pre(+bs: List<&2, B.Bk>, +sl: List<&2, Nat>, +ll: List<&2, U32>, +rl: List<&2, U32>, +sd: Nat, +hl: {SC.length(U32, ll) == SC.pow2(3n+sd) : Nat}, +m: Nat, +hw: {B.all_lt(B.PWell{bs, sd}, m) == True{} : Bool}) -> {ST.bsl(bs, sl, SC.append(U32, ll, rl), m) == ST.bsl(bs, sl, ll, m) : Bool}:  match m:    case 0n:      {==}    case 1n+j:      +h1 = L.and_left(B.wb(sd, B.at(bs, j)), B.all_lt(B.PWell{bs, sd}, j), hw)      +h2 = L.and_right(B.wb(sd, B.at(bs, j)), B.all_lt(B.PWell{bs, sd}, j), hw)      Equal.trans(Bool, Bool.and(ST.bslb(sl, SC.append(U32, ll, rl), B.at(bs, j)), ST.bsl(bs, sl, SC.append(U32, ll, rl), j)), Bool.and(ST.bslb(sl, ll, B.at(bs, j)), ST.bsl(bs, sl, SC.append(U32, ll, rl), 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.append(U32, ll, rl), j)), ST.bslb(sl, SC.append(U32, ll, rl), B.at(bs, j)), ST.bslb(sl, ll, B.at(bs, j)), bslb_pre(sl, ll, rl, sd, hl, B.at(bs, j), h1)), Equal.cong(Bool, Bool, z => Bool.and(ST.bslb(sl, ll, B.at(bs, j)), z), ST.bsl(bs, sl, SC.append(U32, ll, rl), j), ST.bsl(bs, sl, ll, j), bsl_pre(bs, sl, ll, rl, sd, hl, j, h2)))# ---- two writes to different cells commute ----def upd_comm(+xs: List<&2, U32>, +i: Nat, +j: Nat, +x: U32, +y: U32, +h: {Nat.is_eq(i, j) == False{} : Bool}) -> {SC.update(U32, SC.update(U32, xs, i, x), j, y) == SC.update(U32, SC.update(U32, xs, j, y), i, x) : List<&2, U32>}:  match xs i j:    case Nil{} _ _:      {==}    case Con{+a, +t} 0n 0n:      Empty.absurd({SC.update(U32, SC.update(U32, Con{a, t}, 0n, x), 0n, y) == SC.update(U32, SC.update(U32, Con{a, t}, 0n, y), 0n, x) : List<&2, U32>}, L.true_false(h))    case Con{+a, +t} 0n 1n+q:      {==}    case Con{+a, +t} 1n+p 0n:      {==}    case Con{+a, +t} 1n+p 1n+q:      Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{a, z}, SC.update(U32, SC.update(U32, t, p, x), q, y), SC.update(U32, SC.update(U32, t, q, y), p, x), upd_comm(t, p, q, x, y, h))# the blank value halfdef vac_eq(~V: Data, +d: Nat) -> {LR.vac(&2, V, d) == AR.thaw(Maybe<&2, V>, AR.trep(Maybe<&2, V>, d, None{})) : Array<Maybe<&2, V>>}:  match d:    case 0n:      {==}    case 1n+p:      Equal.trans(Array<Maybe<&2, V>>, ANode{LR.vac(&2, V, p), LR.vac(&2, V, p)}, ANode{AR.thaw(Maybe<&2, V>, AR.trep(Maybe<&2, V>, p, None{})), LR.vac(&2, V, p)}, AR.thaw(Maybe<&2, V>, AR.trep(Maybe<&2, V>, 1n+p, None{})), Equal.cong(Array<Maybe<&2, V>>, Array<Maybe<&2, V>>, a => ANode{a, LR.vac(&2, V, p)}, LR.vac(&2, V, p), AR.thaw(Maybe<&2, V>, AR.trep(Maybe<&2, V>, p, None{})), vac_eq(~V, p)), Equal.cong(Array<Maybe<&2, V>>, Array<Maybe<&2, V>>, a => ANode{AR.thaw(Maybe<&2, V>, AR.trep(Maybe<&2, V>, p, None{})), a}, LR.vac(&2, V, p), AR.thaw(Maybe<&2, V>, AR.trep(Maybe<&2, V>, p, None{})), vac_eq(~V, p)))