Proof step 1 from proof step-ACrash (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, PLIBLInv(gs, lsf(t), pcf(t)), allReadsOK(gs.h), allWritesOK(gs.h) ⊦ ⟪pm := gs.pm, vm := gs.vm, h := gs.h; ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟫ ((allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ PLIBLInv(gs, lsf(t), pcf(t)))

Rule argument

Additional information

Proof step 2 from proof step-ACrash (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 3:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, h = gs.h, pm = gs.pm, vm = gs.vm, PLIBLInv(gs, lsf(t), pcf(t)), allReadsOK(gs.h), allWritesOK(gs.h) ⊦ ⟪ACrash(pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟫ ((allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true)) ∧ PLIBLInv(gs, lsf(t), pcf(t)))

Rule argument

Additional information

Proof step 3 from proof step-ACrash (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, h = gs.h, vm = gs.vm, PLIBLInv(gs, lsf(t), pcf(t)), allReadsOK(gs.h), allWritesOK(gs.h) ⊦ ⟪ACrash(gs.pm; vm, h, pcf); gs := (gs.vm:= vm).h:= h⟫ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true) ∧ PLIBLInv(gs, lsf(t), pcf(t)))

Rule argument

Additional information

Proof step 4 from proof step-ACrash (previous step) (back to tree)

Heuristic unfold applied rule call right

And obtained the following new goals

• Proof step 5:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, h = gs.h, pm = gs.pm, vm = gs.vm, PLIBLInv(gs, lsf(t), pcf(t)), allReadsOK(gs.h), allWritesOK(gs.h) ⊦ ⟪pcf := λ t. (pcf(t) = idle ⊃ idle;crashed), vm := pm, h := h | true; gs := (gs.vm:= vm).h:= h⟫ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true) ∧ PLIBLInv(gs, lsf(t), pcf(t)))

Rule argument

Additional information

Used simplifier rules: decl: ACrash(pm; vm, h, pcf) {pcf := λ t. (pcf(t) = idle ⊃ idle;crashed), vm := pm, h := h | true};

Proof step 5 from proof step-ACrash (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 6:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, h = gs.h, pm = gs.pm, vm = gs.vm, PLIBLInv(gs, lsf(t), pcf(t)), allReadsOK(gs.h), allWritesOK(gs.h) ⊦ ⟪gs := (gs.vm:= pm).h:= (h | true)⟫ (allReadsOK(gs.h) ∧ allWritesOK(gs.h) ∧ gs.vm = ∅ ⊕ gs.h ∧ gs.pm = ∅ ⊕ (gs.h | true) ∧ PLIBLInv(gs, lsf(t), (pcf(t) = idle ⊃ idle;crashed)))

Rule argument

Additional information

Proof step 6 from proof step-ACrash (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 7:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, h = gs.h, pm = gs.pm, vm = gs.vm, PLIBLInv(gs, lsf(t), pcf(t)), allReadsOK(gs.h), allWritesOK(gs.h) ⊦ allReadsOK(((gs.vm:= pm).h:= (h | true)).h) ∧ allWritesOK(((gs.vm:= pm).h:= (h | true)).h) ∧ ((gs.vm:= pm).h:= (h | true)).vm = ∅ ⊕ ((gs.vm:= pm).h:= (h | true)).h ∧ ((gs.vm:= pm).h:= (h | true)).pm = ∅ ⊕ (((gs.vm:= pm).h:= (h | true)).h | true) ∧ PLIBLInv((gs.vm:= pm).h:= (h | true), lsf(t), (pcf(t) = idle ⊃ idle;crashed))

Rule argument

Additional information

Proof step 7 from proof step-ACrash (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  gs.pm = ∅ ⊕ (gs.h | true), gs.vm = ∅ ⊕ gs.h, PLIBLInv(gs, lsf(t), pcf(t)), allReadsOK(gs.h), allWritesOK(gs.h), ¬ PLIBLInv((gs.vm:= gs.pm).h:= (gs.h | true), lsf(t), (pcf(t) = idle ⊃ idle;crashed)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h | b | b = h | b; (s) ⊦ (gs.h:= h).h = h; (s) ⊦ (gs.vm:= vm).pm = gs.pm; (s) ⊦ (gs.h:= h).pm = gs.pm; (s) ⊦ (gs.vm:= vm).vm = vm; (s) ⊦ (gs.h:= h).vm = gs.vm; (s) ⊦ allWritesOK(h) → allWritesOK(h | true); (ss) ⊦ allReadsOK(h) → allReadsOK(h | true); (ss)

Proof step 8 from proof step-ACrash (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ PLIBLInv(gs, ls, pc) ↔ pc = resWrite → (gs.h | ls.t) | false = [] ∨ (gs.h | ls.t) | false = (W(ls.t, ls.il, ls.iv), false) '

Rule argument

Additional information

Used simplifier rules: ⊦ idle ≠ resWrite; (s) ⊦ crashed ≠ resWrite; (s) Used terms: (gs.vm:= gs.pm).h:= (gs.h | true), lsf(t), (pcf(t) = idle ⊃ idle;crashed)

Proof step 9 from proof step-ACrash (previous step) (back to tree)

A spec-lemma