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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ⟨p := gs.p; PSCPERSIST_FO(l; p); gs.p := p⟩ (gs0 = gs), ctrok(gs.ctr, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∃ n. isPersistFO(n, gs.p(l)) ⊦ ∀ t0. relyws(t0, gs.readers, gs0.readers) ∧ relyws(t0, gs.writers, gs0.writers) ∧ rely(t0, gs.p, gs0.p)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ⟨p := gs.p; PSCPERSIST_FO(l; p); gs.p := p⟩ (gs0 = gs), ctrok(gs.ctr, gs.writers), isPersistFO(n, gs.p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ relyws(t0, gs.readers, gs0.readers) ∧ relyws(t0, gs.writers, gs0.writers) ∧ rely(t0, gs.p, gs0.p)

Rule argument

Additional information

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

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 4:

  ⟨PSCPERSIST_FO(l; p); gs.p := p⟩ (gs0 = gs), p = gs.p, ctrok(gs.ctr, gs.writers), isPersistFO(n, gs.p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ relyws(t0, gs.readers, gs0.readers) ∧ relyws(t0, gs.writers, gs0.writers) ∧ rely(t0, gs.p, gs0.p)

Rule argument

Additional information

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

Heuristic split applied rule split left

And obtained the following new goals

• Proof step 5:

  ⟨gs.p := p0⟩ (gs0 = gs), ⟨PSCPERSIST_FO(l; p)⟩ (p = p0), p = gs.p, ctrok(gs.ctr, gs.writers), isPersistFO(n, gs.p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ relyws(t0, gs.readers, gs0.readers) ∧ relyws(t0, gs.writers, gs0.writers) ∧ rely(t0, gs.p, gs0.p)

Rule argument

Additional information

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

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 6:

  ⟨PSCPERSIST_FO(l; p)⟩ (p = p0), gs0 = gs.p:= p0, p = gs.p, ctrok(gs.ctr, gs.writers), isPersistFO(n, gs.p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers) ⊦ relyws(t0, gs.readers, gs0.readers) ∧ relyws(t0, gs.writers, gs0.writers) ∧ rely(t0, gs.p, gs0.p)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ⟨PSCPERSIST_FO(l; p)⟩ (p = p0), p = gs.p, ctrok(gs.ctr, gs.writers), isPersistFO(n, gs.p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ rely(t0, gs.p, p0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.p:= p).p = p; (s) ⊦ relyws(t, tsf, tsf); (s) ⊦ (gs.p:= p).writers = gs.writers; (s) ⊦ (gs.p:= p).readers = gs.readers; (s)

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

Heuristic unfold applied rule call left

And obtained the following new goals

• Proof step 8:

  ⟨choose n with isPersistFO(n, p(l)) in p(l) := p(l) -p n ifnone skip⟩ (p = p0), p = gs.p, ctrok(gs.ctr, gs.writers), isPersistFO(n, gs.p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ rely(t0, gs.p, p0) ⊦

Rule argument

Additional information

Used simplifier rules: decl: PSCPERSIST_FO(l; p){choose n with isPersistFO(n, p(l)) in p(l) := p(l) -p n ifnone skip};

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

Heuristic symbolic execution applied rule choose left

And obtained the following new goals

• Proof step 9:

  ⟨p(l) := p(l) -p n⟩ (p = p0), p = gs.p, ctrok(gs.ctr, gs.writers), isPersistFO(n0, gs.p(l)), isPersistFO(n, p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ rely(t0, gs.p, p0) ⊦

• Proof step 10:

  ⟨skip⟩ (p = p0), p = gs.p, ctrok(gs.ctr, gs.writers), isPersistFO(n, gs.p(l)), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ rely(t0, gs.p, p0), ∀ n. ¬ isPersistFO(n, p(l)) ⊦

Rule argument

Additional information

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

Heuristic symbolic execution applied rule assign left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ isPersistFO(n, p(l)) → rely(t, p, p(l := p(l) -p n)); (ss)

Proof step 10 from proof rely-PSCPERSIST_FO (previous step) (back to tree)

Heuristic symbolic execution applied rule skip left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ rely(t, p, p); (s)