Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
12 kB · 204 lines
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205# eukhe: the proof of LAW replacement_terminates
import Baseimport ../../bend/replace.bend as Rpimport ../../laws/replace.bend as Replaceimport ../base/logic/logic.bend as LLogicLogicimport ../base/logic/nat.bend as LLogicNatimport ../base/nat.bend as LNatimport ./base.bend as LA
# ---- replace ----
# proof_replace: the replacement laws of LAWS.bend section supervisor (D1), on the# model bend/replace.bend.## - replace_never_downgrades: a start replaces the daemon only with a build# of a higher rank (`pr.replace_older`), and the rank order is transitive# (`pr.lt_trans`), so the daemon after a start is below no daemon before# it (`pr.rising`).# - replacement_terminates: each replacement moves the daemon to a build of# bs of a higher rank, so the count of the builds of bs above the daemon# falls by one at least (`pr.above_strict`); the first daemon has at most# |bs| - 1 builds of bs above it (`pr.above_member`).# - background_never_replaces: the verdict of a background start is always# a keep.
# Logic# -----
def replace.pr.and_l(a: Bool, -b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}: match a: case True{}: {==} case False{}: e
def replace.pr.and_r(a: Bool, -b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}: match a: case True{}: e case False{}: LLogicLogic.supervisor.ps.absurdF({b == True{} : Bool}, e)
def pr.ranks_eq_sound(xs: List<&2, Nat>, ys: List<&2, Nat>, +e: {Rp.ranks_eq(xs, ys) == True{} : Bool}) -> {xs == ys : List<&2, Nat>}: match xs ys: case Nil{} Nil{}: {==} case Nil{} y <> yr: LLogicLogic.supervisor.ps.absurdF({Nil{} == y <> yr : List<&2, Nat>}, e) case x <> xr Nil{}: LLogicLogic.supervisor.ps.absurdF({x <> xr == Nil{} : List<&2, Nat>}, e) case +x <> +xr +y <> +yr: %LLogicNat.supervisor.ps.eq_of_is_eq(x, y, replace.pr.and_l(Nat.is_eq(x, y), Rp.ranks_eq(xr, yr), e)) : {x <> xr == _ <> yr : List<&2, Nat>} %pr.ranks_eq_sound(xr, yr, replace.pr.and_r(Nat.is_eq(x, y), Rp.ranks_eq(xr, yr), e)) : {x <> xr == x <> _ : List<&2, Nat>} {==}
def pr.build_eq_rank(a: Rp.Build, b: Rp.Build, e: {Rp.build_eq(a, b) == True{} : Bool}) -> {Rp.Build.rank(a) == Rp.Build.rank(b) : List<&2, Nat>}: match a b: case Rp.Build{+ra, +ia} Rp.Build{+rb, +ib}: pr.ranks_eq_sound(ra, rb, replace.pr.and_r(String.eq(ia, ib), Rp.ranks_eq(ra, rb), e))
# (D1) replacement_terminates# ---------------------------
def pr.one(b: Bool) -> Nat: match b: case True{}: 1n case False{}: 0n
# the builds of bs above rank rdef pr.above(bs: List<&2, Rp.Build>, +r: List<&2, Nat>) -> Nat: match bs: case Nil{}: 0n case e <> t: Nat.add(pr.one(Rp.lt(r, Rp.Build.rank(e))), pr.above(t, r))
def pr.weak.put(p: Bool, q: Bool, +x: Nat, +y: Nat, rb: List<&2, Nat>, rc: List<&2, Nat>, re: List<&2, Nat>, ep: {Rp.lt(rc, re) == p : Bool}, eq: {Rp.lt(rb, re) == q : Bool}, h: {Rp.lt(rb, rc) == True{} : Bool}, ih: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_le(Nat.add(pr.one(p), x), Nat.add(pr.one(q), y)) == True{} : Bool}: match p q: case True{} True{}: ih case True{} False{}: LA.pr.clash({Nat.is_le(Nat.add(1n, x), Nat.add(0n, y)) == True{} : Bool}, Rp.lt(rb, re), LA.pr.lt_trans(rb, rc, re, h, ep), eq) case False{} True{}: LNat.supervisor.ps.le_trans(x, y, 1n+y, ih, LNat.supervisor.ps.le_succ(y)) case False{} False{}: ih
# rank rc above rank rb: fewer builds above rc than above rbdef pr.above_weak(bs: List<&2, Rp.Build>, +rb: List<&2, Nat>, +rc: List<&2, Nat>, +h: {Rp.lt(rb, rc) == True{} : Bool}) -> {Nat.is_le(pr.above(bs, rc), pr.above(bs, rb)) == True{} : Bool}: match bs: case Nil{}: {==} case +e <> +t: pr.weak.put(Rp.lt(rc, Rp.Build.rank(e)), Rp.lt(rb, Rp.Build.rank(e)), pr.above(t, rc), pr.above(t, rb), rb, rc, Rp.Build.rank(e), {==}, {==}, h, pr.above_weak(t, rb, rc, h))
def pr.strict.put(p: Bool, q: Bool, +x: Nat, +y: Nat, rb: List<&2, Nat>, rc: List<&2, Nat>, re: List<&2, Nat>, ep: {Rp.lt(rc, re) == p : Bool}, eq: {Rp.lt(rb, re) == q : Bool}, h: {Rp.lt(rb, rc) == True{} : Bool}, ih: {Nat.is_le(1n+x, y) == True{} : Bool}) -> {Nat.is_le(1n+Nat.add(pr.one(p), x), Nat.add(pr.one(q), y)) == True{} : Bool}: match p q: case True{} True{}: ih case True{} False{}: LA.pr.clash({Nat.is_le(1n+Nat.add(1n, x), Nat.add(0n, y)) == True{} : Bool}, Rp.lt(rb, re), LA.pr.lt_trans(rb, rc, re, h, ep), eq) case False{} True{}: LNat.supervisor.ps.le_trans(x, 1n+x, y, LNat.supervisor.ps.le_succ(x), ih) case False{} False{}: ih
def pr.member.put(be: Bool, +e: Rp.Build, +t: List<&2, Rp.Build>, +c: Rp.Build, +rb: List<&2, Nat>, ebe: {Rp.build_eq(e, c) == be : Bool}, m: {Bool.or(be, Rp.has(t, c)) == True{} : Bool}, +h: {Rp.lt(rb, Rp.Build.rank(c)) == True{} : Bool}, ih: {Rp.has(t, c) == True{} : Bool} -> {Nat.is_le(1n+pr.above(t, Rp.Build.rank(c)), pr.above(t, rb)) == True{} : Bool}) -> {Nat.is_le(1n+Nat.add(pr.one(Rp.lt(Rp.Build.rank(c), Rp.Build.rank(e))), pr.above(t, Rp.Build.rank(c))), Nat.add(pr.one(Rp.lt(rb, Rp.Build.rank(e))), pr.above(t, rb))) == True{} : Bool}: match be: case True{}: %Equal.sym(List<&2, Nat>, Rp.Build.rank(e), Rp.Build.rank(c), pr.build_eq_rank(e, c, ebe)) : {Nat.is_le(1n+Nat.add(pr.one(Rp.lt(Rp.Build.rank(c), _)), pr.above(t, Rp.Build.rank(c))), Nat.add(pr.one(Rp.lt(rb, _)), pr.above(t, rb))) == True{} : Bool} %Equal.sym(Bool, Rp.lt(Rp.Build.rank(c), Rp.Build.rank(c)), False{}, LA.pr.lt_irrefl(Rp.Build.rank(c))) : {Nat.is_le(1n+Nat.add(pr.one(_), pr.above(t, Rp.Build.rank(c))), Nat.add(pr.one(Rp.lt(rb, Rp.Build.rank(c))), pr.above(t, rb))) == True{} : Bool} %Equal.sym(Bool, Rp.lt(rb, Rp.Build.rank(c)), True{}, h) : {Nat.is_le(1n+Nat.add(pr.one(False{}), pr.above(t, Rp.Build.rank(c))), Nat.add(pr.one(_), pr.above(t, rb))) == True{} : Bool} pr.above_weak(t, rb, Rp.Build.rank(c), h) case False{}: pr.strict.put(Rp.lt(Rp.Build.rank(c), Rp.Build.rank(e)), Rp.lt(rb, Rp.Build.rank(e)), pr.above(t, Rp.Build.rank(c)), pr.above(t, rb), rb, Rp.Build.rank(c), Rp.Build.rank(e), {==}, {==}, h, ih(m))
# a build c of bs above rank rb: c and the builds above it are above rbdef pr.above_strict(bs: List<&2, Rp.Build>, +rb: List<&2, Nat>, +c: Rp.Build, +h: {Rp.lt(rb, Rp.Build.rank(c)) == True{} : Bool}, m: {Rp.has(bs, c) == True{} : Bool}) -> {Nat.is_le(1n+pr.above(bs, Rp.Build.rank(c)), pr.above(bs, rb)) == True{} : Bool}: match bs: case Nil{}: LLogicLogic.supervisor.ps.absurdF({Nat.is_le(1n+pr.above(Nil{}, Rp.Build.rank(c)), pr.above(Nil{}, rb)) == True{} : Bool}, m) case +e <> +t: pr.member.put(Rp.build_eq(e, c), e, t, c, rb, {==}, m, h, i => pr.above_strict(t, rb, c, h, i))
def pr.len.put(p: Bool, +x: Nat, +n: Nat, ih: {Nat.is_le(x, n) == True{} : Bool}) -> {Nat.is_le(Nat.add(pr.one(p), x), 1n+n) == True{} : Bool}: match p: case True{}: ih case False{}: LNat.supervisor.ps.le_trans(x, n, 1n+n, ih, LNat.supervisor.ps.le_succ(n))
def pr.above_le_len(bs: List<&2, Rp.Build>, +r: List<&2, Nat>) -> {Nat.is_le(pr.above(bs, r), List.length(&2, Rp.Build, bs)) == True{} : Bool}: match bs: case Nil{}: {==} case +e <> +t: pr.len.put(Rp.lt(r, Rp.Build.rank(e)), pr.above(t, r), List.length(&2, Rp.Build, t), pr.above_le_len(t, r))
def pr.mlen.put(p: Bool, +x: Nat, +n: Nat, ih: {Nat.is_le(1n+x, n) == True{} : Bool}) -> {Nat.is_le(1n+Nat.add(pr.one(p), x), 1n+n) == True{} : Bool}: match p: case True{}: ih case False{}: LNat.supervisor.ps.le_trans(x, 1n+x, n, LNat.supervisor.ps.le_succ(x), ih)
def pr.member_len.put(be: Bool, +e: Rp.Build, +t: List<&2, Rp.Build>, +c: Rp.Build, ebe: {Rp.build_eq(e, c) == be : Bool}, m: {Bool.or(be, Rp.has(t, c)) == True{} : Bool}, ih: {Rp.has(t, c) == True{} : Bool} -> {Nat.is_le(1n+pr.above(t, Rp.Build.rank(c)), List.length(&2, Rp.Build, t)) == True{} : Bool}) -> {Nat.is_le(1n+Nat.add(pr.one(Rp.lt(Rp.Build.rank(c), Rp.Build.rank(e))), pr.above(t, Rp.Build.rank(c))), 1n+List.length(&2, Rp.Build, t)) == True{} : Bool}: match be: case True{}: %Equal.sym(List<&2, Nat>, Rp.Build.rank(e), Rp.Build.rank(c), pr.build_eq_rank(e, c, ebe)) : {Nat.is_le(1n+Nat.add(pr.one(Rp.lt(Rp.Build.rank(c), _)), pr.above(t, Rp.Build.rank(c))), 1n+List.length(&2, Rp.Build, t)) == True{} : Bool} %Equal.sym(Bool, Rp.lt(Rp.Build.rank(c), Rp.Build.rank(c)), False{}, LA.pr.lt_irrefl(Rp.Build.rank(c))) : {Nat.is_le(1n+Nat.add(pr.one(_), pr.above(t, Rp.Build.rank(c))), 1n+List.length(&2, Rp.Build, t)) == True{} : Bool} pr.above_le_len(t, Rp.Build.rank(c)) case False{}: pr.mlen.put(Rp.lt(Rp.Build.rank(c), Rp.Build.rank(e)), pr.above(t, Rp.Build.rank(c)), List.length(&2, Rp.Build, t), ih(m))
# a build c of bs: at most |bs| - 1 builds of bs above itdef pr.above_member(bs: List<&2, Rp.Build>, +c: Rp.Build, m: {Rp.has(bs, c) == True{} : Bool}) -> {Nat.is_le(1n+pr.above(bs, Rp.Build.rank(c)), List.length(&2, Rp.Build, bs)) == True{} : Bool}: match bs: case Nil{}: LLogicLogic.supervisor.ps.absurdF({Nat.is_le(1n+pr.above(Nil{}, Rp.Build.rank(c)), 0n) == True{} : Bool}, m) case +e <> +t: pr.member_len.put(Rp.build_eq(e, c), e, t, c, {==}, m, i => pr.above_member(t, c, i))
def pr.count.put(v: Rp.Verdict, +c: Rp.Build, +b: Rp.Build, -k: Rp.Caller, +rest: List<&2, Rp.Start>, +bs: List<&2, Rp.Build>, ev: {Rp.verdict(c, b, k) == v : Rp.Verdict}, mc: {Rp.has(bs, c) == True{} : Bool}, ih: @d: Rp.Build -> {Nat.is_le(Rp.replaced.go(rest, Some{d}), pr.above(bs, Rp.Build.rank(d))) == True{} : Bool}) -> {Nat.is_le(Nat.add(Rp.replaces.put(v), Rp.replaced.go(rest, Some{Rp.after.put(v, c, b)})), pr.above(bs, Rp.Build.rank(b))) == True{} : Bool}: match v: case Rp.Replace{}: LNat.supervisor.ps.le_trans(1n+Rp.replaced.go(rest, Some{c}), 1n+pr.above(bs, Rp.Build.rank(c)), pr.above(bs, Rp.Build.rank(b)), ih(c), pr.above_strict(bs, Rp.Build.rank(b), c, LA.pr.replace_older(c, b, k, ev), mc)) case Rp.Keep{r}: ih(b)
# from the daemon b, the replacements are at most the builds of bs above bdef pr.count_le(ss: List<&2, Rp.Start>, +bs: List<&2, Rp.Build>, +b: Rp.Build, +cov: {Rp.covers(bs, ss) == True{} : Bool}) -> {Nat.is_le(Rp.replaced.go(ss, Some{b}), pr.above(bs, Rp.Build.rank(b))) == True{} : Bool}: match ss: case Nil{}: LNat.ps.le_zero(pr.above(bs, Rp.Build.rank(b))) case s <> +rest: match s: case Rp.Start{+c, +k}: pr.count.put(Rp.verdict(c, b, k), c, b, k, rest, bs, {==}, replace.pr.and_l(Rp.has(bs, c), Rp.covers(bs, rest), cov), d => pr.count_le(rest, bs, d, replace.pr.and_r(Rp.has(bs, c), Rp.covers(bs, rest), cov)))
def pr.le_pred(+a: Nat, n: Nat, h: {Nat.is_le(1n+a, n) == True{} : Bool}) -> {Nat.is_le(a, Nat.sub(n, 1n)) == True{} : Bool}: match n: case 0n: LLogicLogic.supervisor.ps.absurdF({Nat.is_le(a, Nat.sub(0n, 1n)) == True{} : Bool}, h) case 1n+m: match m: case 0n: h case 1n+j: h
def pr.replacement_terminates(+bs: List<&2, Rp.Build>, ss: List<&2, Rp.Start>, +cover: {Rp.covers(bs, ss) == True{} : Bool}) -> {Nat.is_le(Rp.replaced(ss), Nat.sub(List.length(&2, Rp.Build, bs), 1n)) == True{} : Bool}: match ss: case Nil{}: LNat.ps.le_zero(Nat.sub(List.length(&2, Rp.Build, bs), 1n)) case s <> +rest: match s: case Rp.Start{+c, k}: pr.le_pred(Rp.replaced.go(rest, Some{c}), List.length(&2, Rp.Build, bs), LNat.supervisor.ps.le_trans(1n+Rp.replaced.go(rest, Some{c}), 1n+pr.above(bs, Rp.Build.rank(c)), List.length(&2, Rp.Build, bs), pr.count_le(rest, bs, c, replace.pr.and_r(Rp.has(bs, c), Rp.covers(bs, rest), cover)), pr.above_member(bs, c, replace.pr.and_l(Rp.has(bs, c), Rp.covers(bs, rest), cover))))
def Replace.replacement_terminates(bs, ss, cover): pr.replacement_terminates(bs, ss, cover)