~/bend-docscommunity

proofs/containers/lru/idx.bend source

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

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/u32.bend as Uimport ../../lib/u32alg.bend as Aimport ../../../spec/lib/common.bend as SCimport ../../lib/word.bend as WDimport ../../lib/arith.bend as ATimport ../../lib/u32div.bend as UDimport ../../../src/containers/lru.bend as LRimport ./state.bend as STimport ../../lib/words32.bend as W32# Index arithmetic for lk: word o of slot s is at 8s + o.# ---- offsets are injective ----def lt8_ne(+a: Nat, +b: Nat, +ha: {Nat.is_lt(a, 8n) == True{} : Bool}) -> {Nat.is_eq(a, 8n+b) == False{} : Bool}:  N.is_eq_lt(a, 8n+b, N.lt_le_trans(a, 8n, 8n+b, ha, N.le_add_right(8n, b)))def off_ne(+x: Nat, +y: Nat, +o: Nat, +o2: Nat, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +ho2: {Nat.is_lt(o2, 8n) == True{} : Bool}, +h: {Bool.or(Bool.not(Nat.is_eq(x, y)), Bool.not(Nat.is_eq(o, o2))) == True{} : Bool}) -> {Nat.is_eq(ST.off(x, o), ST.off(y, o2)) == False{} : Bool}:  match x y:    case 0n 0n:      L.not_true(Nat.is_eq(o, o2), h)    case 0n 1n+q:      lt8_ne(o, ST.off(q, o2), ho)    case 1n+p 0n:      N.is_eq_sym_false(o2, 8n+ST.off(p, o), lt8_ne(o2, ST.off(p, o), ho2))    case 1n+p 1n+q:      off_ne(p, q, o, o2, ho, ho2, h)# ---- U32 addition without overflow ----def av_z(+u: Nat, +s: Nat, +e: {Nat.add(u, WD.sc(32n, 0n)) == s : Nat}) -> {u == s : Nat}:  Equal.trans(Nat, u, Nat.add(u, 0n), s, Equal.sym(Nat, Nat.add(u, 0n), u, N.add_zero(u)), L.subst(Nat, z => {Nat.add(u, z) == s : Nat}, WD.sc(32n, 0n), 0n, A.sc_zero(32n), e))def av_b(+one: Nat, +h1: {one == 1n : Nat}, +u: Nat, +s: Nat, +c: Nat, +e: {Nat.add(u, WD.sc(32n, c)) == s : Nat}, +h: {Nat.is_lt(s, WD.sc(32n, one)) == True{} : Bool}, +b: Bool, +hb: {Nat.is_eq(c, 0n) == b : Bool}) -> {u == s : Nat}:  match b:    case True{}:      av_z(u, s, L.subst(Nat, z => {Nat.add(u, WD.sc(32n, z)) == s : Nat}, c, 0n, N.eq_from_is_eq(c, 0n, hb), e))    case False{}:      +h0 = N.lt_or_eq(0n, c, N.zero_le(c), N.is_eq_sym_false(c, 0n, hb))      +h1b = L.subst(Nat, z => {Nat.is_le(z, c) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), N.lt_succ_le_succ(0n, c, h0))      +l1 = AT.sc_le(32n, one, c, h1b)      +l2 = N.le_trans(WD.sc(32n, one), WD.sc(32n, c), Nat.add(u, WD.sc(32n, c)), l1, L.subst(Nat, z => {Nat.is_le(WD.sc(32n, c), z) == True{} : Bool}, Nat.add(WD.sc(32n, c), u), Nat.add(u, WD.sc(32n, c)), N.add_comm(WD.sc(32n, c), u), N.le_add_right(WD.sc(32n, c), u)))      +l3 = L.subst(Nat, z => {Nat.is_le(WD.sc(32n, one), z) == True{} : Bool}, Nat.add(u, WD.sc(32n, c)), s, e, l2)      Empty.absurd({u == s : Nat}, L.true_false(Equal.trans(Bool, True{}, Nat.is_lt(s, WD.sc(32n, one)), False{}, Equal.sym(Bool, Nat.is_lt(s, WD.sc(32n, one)), True{}, h), N.le_not_lt(s, WD.sc(32n, one), l3))))def av_c(+one: Nat, +h1: {one == 1n : Nat}, +u: Nat, +s: Nat, +c: Nat, +e: {Nat.add(u, WD.sc(32n, c)) == s : Nat}, +h: {Nat.is_lt(s, WD.sc(32n, one)) == True{} : Bool}) -> {u == s : Nat}:  av_b(one, h1, u, s, c, e, h, Nat.is_eq(c, 0n), {==})def av_w(+one: Nat, +h1: {one == 1n : Nat}, +x: Word(32n), +y: Word(32n), +h: {Nat.is_lt(Nat.add(UD.v(U32{x}), UD.v(U32{y})), WD.sc(32n, one)) == True{} : Bool}) -> {UD.v(U32.add(U32{x}, U32{y})) == Nat.add(UD.v(U32{x}), UD.v(U32{y})) : Nat}:  +e = A.cons(32n, x, y)  +ex = U.to_nat_word(x)  +ey = U.to_nat_word(y)  +es = U.to_nat_word(Word.add(32n, x, y))  +e2 = L.subst(Nat, z => {Nat.add(A.uw(32n, Word.add(32n, x, y)), WD.sc(32n, A.cy(32n, x, y, False{}))) == Nat.add(z, A.uw(32n, y)) : Nat}, A.uw(32n, x), UD.v(U32{x}), Equal.sym(Nat, UD.v(U32{x}), A.uw(32n, x), ex), e)  +e3 = L.subst(Nat, z => {Nat.add(A.uw(32n, Word.add(32n, x, y)), WD.sc(32n, A.cy(32n, x, y, False{}))) == Nat.add(UD.v(U32{x}), z) : Nat}, A.uw(32n, y), UD.v(U32{y}), Equal.sym(Nat, UD.v(U32{y}), A.uw(32n, y), ey), e2)  Equal.trans(Nat, UD.v(U32.add(U32{x}, U32{y})), A.uw(32n, Word.add(32n, x, y)), Nat.add(UD.v(U32{x}), UD.v(U32{y})), es, av_c(one, h1, A.uw(32n, Word.add(32n, x, y)), Nat.add(UD.v(U32{x}), UD.v(U32{y})), A.cy(32n, x, y, False{}), e3, h))# a + b below 2^32 is exactdef add_val(+one: Nat, +h1: {one == 1n : Nat}, +a: U32, +b: U32, +h: {Nat.is_lt(Nat.add(UD.v(a), UD.v(b)), WD.sc(32n, one)) == True{} : Bool}) -> {UD.v(U32.add(a, b)) == Nat.add(UD.v(a), UD.v(b)) : Nat}:  match a b:    case U32{+x} U32{+y}:      av_w(one, h1, x, y, h)# 2^d <= 2^32 for d <= 32def pow_le(+one: Nat, +h1: {one == 1n : Nat}, +d: Nat, +hd: {Nat.is_le(d, 32n) == True{} : Bool}) -> {Nat.is_le(SC.pow2(d), WD.sc(32n, one)) == True{} : Bool}:  +j = Nat.sub(32n, d)  +e = Equal.trans(Nat, WD.sc(32n, one), WD.sc(Nat.add(d, j), one), WD.sc(d, WD.sc(j, one)), Equal.cong(Nat, Nat, z => WD.sc(z, one), 32n, Nat.add(d, j), Equal.sym(Nat, Nat.add(d, j), 32n, N.sub_add(32n, d, hd))), AT.sc_idx(d, j, one))  L.subst(Nat, z => {Nat.is_le(SC.pow2(d), z) == True{} : Bool}, WD.sc(d, WD.sc(j, one)), WD.sc(32n, one), Equal.sym(Nat, WD.sc(32n, one), WD.sc(d, WD.sc(j, one)), e), L.subst(Nat, z => {Nat.is_le(z, WD.sc(d, WD.sc(j, one))) == True{} : Bool}, WD.sc(d, one), SC.pow2(d), Equal.sym(Nat, SC.pow2(d), WD.sc(d, one), W32.pow_one(one, h1, d)), AT.sc_le(d, one, WD.sc(j, one), AT.le_sc(j, one))))# ---- the slot word indices ----def d8(+x: Nat) -> Nat:  Nat.double(Nat.double(Nat.double(x)))# word o < 8 of a slot below 2^sd lies below 2^(3 + sd)def off_lt(+s: Nat, +sd: Nat, +hs: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}, +o: Nat, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}) -> {Nat.is_lt(ST.off(s, o), SC.pow2(3n+sd)) == True{} : Bool}:  +l1 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(8n, d8(s))) == True{} : Bool}, Nat.add(o, d8(s)), ST.off(s, o), N.add_comm(o, d8(s)), N.lt_add_r2(o, 8n, d8(s), ho))  +l2 = N.double_le(Nat.double(1n+s), Nat.double(SC.pow2(sd)), N.double_le(1n+s, SC.pow2(sd), N.lt_succ_le_succ(s, SC.pow2(sd), hs)))  N.lt_le_trans(ST.off(s, o), d8(1n+s), SC.pow2(3n+sd), l1, N.double_le(Nat.double(Nat.double(1n+s)), Nat.double(Nat.double(SC.pow2(sd))), l2))def shl_v(+x: U32, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +v: Nat, +ev: {UD.v(x) == v : Nat}, +h: {Nat.is_lt(Nat.double(v), SC.pow2(k)) == True{} : Bool}) -> {UD.v(U32.shl(x)) == Nat.double(v) : Nat}:  Equal.trans(Nat, UD.v(U32.shl(x)), Nat.double(UD.v(x)), Nat.double(v), U.shl_value(x, k, hk, L.subst(Nat, z => {Nat.is_lt(Nat.double(z), SC.pow2(k)) == True{} : Bool}, v, UD.v(x), Equal.sym(Nat, UD.v(x), v, ev), h)), Equal.cong(Nat, Nat, z => Nat.double(z), UD.v(x), v, ev))# pidx s = 8sdef pidx_d8(+s: U32, +sd: Nat, +hsd: {Nat.is_le(3n+sd, 32n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), SC.pow2(sd)) == True{} : Bool}) -> {UD.v(LR.pidx(s)) == d8(UD.v(s)) : Nat}:  +v = UD.v(s)  +h1 = N.double_lt(v, SC.pow2(sd), hs)  +h2 = N.double_lt(Nat.double(v), SC.pow2(1n+sd), h1)  +h3 = N.double_lt(Nat.double(Nat.double(v)), SC.pow2(2n+sd), h2)  +k2 = N.le_trans(2n+sd, 3n+sd, 32n, N.le_succ(2n+sd), hsd)  +k1 = N.le_trans(1n+sd, 2n+sd, 32n, N.le_succ(1n+sd), k2)  +e1 = shl_v(s, 1n+sd, k1, v, {==}, h1)  +e2 = shl_v(U32.shl(s), 2n+sd, k2, Nat.double(v), e1, h2)  shl_v(U32.shl(U32.shl(s)), 3n+sd, hsd, Nat.double(Nat.double(v)), e2, h3)def off_sym(+x: Nat, +o: Nat) -> {Nat.add(o, d8(x)) == ST.off(x, o) : Nat}:  N.add_comm(o, d8(x))def w0(+one: Nat, +h1: {one == 1n : Nat}, +s: U32, +sd: Nat, +hsd: {Nat.is_le(3n+sd, 32n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), SC.pow2(sd)) == True{} : Bool}) -> {UD.v(LR.pidx(s)) == ST.off(UD.v(s), 0n) : Nat}:  Equal.trans(Nat, UD.v(LR.pidx(s)), d8(UD.v(s)), ST.off(UD.v(s), 0n), pidx_d8(s, sd, hsd, hs), off_sym(UD.v(s), 0n))def w1(+one: Nat, +h1: {one == 1n : Nat}, +s: U32, +sd: Nat, +hsd: {Nat.is_le(3n+sd, 32n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), SC.pow2(sd)) == True{} : Bool}) -> {UD.v(LR.nidx(s)) == ST.off(UD.v(s), 1n) : Nat}:  +e0 = pidx_d8(s, sd, hsd, hs)  +hb = L.subst(Nat, z => {Nat.is_lt(1n+z, WD.sc(32n, one)) == True{} : Bool}, d8(UD.v(s)), UD.v(LR.pidx(s)), Equal.sym(Nat, UD.v(LR.pidx(s)), d8(UD.v(s)), e0), L.subst(Nat, z => {Nat.is_lt(z, WD.sc(32n, one)) == True{} : Bool}, ST.off(UD.v(s), 1n), 1n+d8(UD.v(s)), Equal.sym(Nat, 1n+d8(UD.v(s)), ST.off(UD.v(s), 1n), off_sym(UD.v(s), 1n)), N.lt_le_trans(ST.off(UD.v(s), 1n), SC.pow2(3n+sd), WD.sc(32n, one), off_lt(UD.v(s), sd, hs, 1n, {==}), pow_le(one, h1, 3n+sd, hsd))))  Equal.trans(Nat, UD.v(LR.nidx(s)), 1n+d8(UD.v(s)), ST.off(UD.v(s), 1n), Equal.trans(Nat, UD.v(U32.inc(LR.pidx(s))), 1n+UD.v(LR.pidx(s)), 1n+d8(UD.v(s)), W32.inc_val(one, h1, LR.pidx(s), hb), Equal.cong(Nat, Nat, z => 1n+z, UD.v(LR.pidx(s)), d8(UD.v(s)), e0)), off_sym(UD.v(s), 1n))# pidx s + o for a small odef wo(+one: Nat, +h1: {one == 1n : Nat}, +s: U32, +sd: Nat, +hsd: {Nat.is_le(3n+sd, 32n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), SC.pow2(sd)) == True{} : Bool}, +o: U32, +ho: {Nat.is_lt(UD.v(o), 8n) == True{} : Bool}) -> {UD.v(U32.add(LR.pidx(s), o)) == ST.off(UD.v(s), UD.v(o)) : Nat}:  +e0 = pidx_d8(s, sd, hsd, hs)  +hb0 = N.lt_le_trans(ST.off(UD.v(s), UD.v(o)), SC.pow2(3n+sd), WD.sc(32n, one), off_lt(UD.v(s), sd, hs, UD.v(o), ho), pow_le(one, h1, 3n+sd, hsd))  +hb = L.subst(Nat, z => {Nat.is_lt(Nat.add(z, UD.v(o)), WD.sc(32n, one)) == True{} : Bool}, d8(UD.v(s)), UD.v(LR.pidx(s)), Equal.sym(Nat, UD.v(LR.pidx(s)), d8(UD.v(s)), e0), hb0)  Equal.trans(Nat, UD.v(U32.add(LR.pidx(s), o)), Nat.add(UD.v(LR.pidx(s)), UD.v(o)), ST.off(UD.v(s), UD.v(o)), add_val(one, h1, LR.pidx(s), o, hb), Equal.cong(Nat, Nat, z => Nat.add(z, UD.v(o)), UD.v(LR.pidx(s)), d8(UD.v(s)), e0))def w2(+one: Nat, +h1: {one == 1n : Nat}, +s: U32, +sd: Nat, +hsd: {Nat.is_le(3n+sd, 32n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), SC.pow2(sd)) == True{} : Bool}) -> {UD.v(LR.hidx(s)) == ST.off(UD.v(s), 2n) : Nat}:  wo(one, h1, s, sd, hsd, hs, 2, {==})def w3(+one: Nat, +h1: {one == 1n : Nat}, +s: U32, +sd: Nat, +hsd: {Nat.is_le(3n+sd, 32n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), SC.pow2(sd)) == True{} : Bool}) -> {UD.v(LR.tidx(s)) == ST.off(UD.v(s), 3n) : Nat}:  wo(one, h1, s, sd, hsd, hs, 3, {==})def w4(+one: Nat, +h1: {one == 1n : Nat}, +s: U32, +sd: Nat, +hsd: {Nat.is_le(3n+sd, 32n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), SC.pow2(sd)) == True{} : Bool}) -> {UD.v(LR.dlo_idx(s)) == ST.off(UD.v(s), 4n) : Nat}:  wo(one, h1, s, sd, hsd, hs, 4, {==})def w5(+one: Nat, +h1: {one == 1n : Nat}, +s: U32, +sd: Nat, +hsd: {Nat.is_le(3n+sd, 32n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(s), SC.pow2(sd)) == True{} : Bool}) -> {UD.v(LR.dhi_idx(s)) == ST.off(UD.v(s), 5n) : Nat}:  wo(one, h1, s, sd, hsd, hs, 5, {==})