[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 97 from proof inv-format (previous step)

# buf = lptlebs(# lpt, LEB_SIZE) * LEB_SIZE, # buf = lptsize(# lpt, LEB_SIZE), # avol0 = # lpt + 5 + 2 * lptlebs(# lpt, LEB_SIZE), avol0[4] = fill(mkavolume(# avol0), unmapped)[4], avol0[3] = mapped(mkbuf(0)), avol0[2] = fill(mkavolume(# avol0), unmapped)[2], avol0[1] = mapped(mkbuf(0)), avol0[0] = fill(mkavolume(# avol0), unmapped)[0], err = ESUCCESS, m = LEB_SIZE, m0 = EB_PAGE_SIZE, sb = ((((((sb0.indexaddr:= adr).maxino:= m1).log:= 1).orph:= 3).orphsize:= 0).lpt:= 5).main:= (5 + 2 * lptlebs(# lpt, LEB_SIZE)), ebm-vol-inv(fill(mkavolume(# avol0), unmapped)[1, mapped(mkbuf(0))][3, mapped(mkbuf(0))]), ebm-vol-inv(fill(mkavolume(# avol0), unmapped)), ebm-vol-inv(fill(mkavolume(# avol0), unmapped)[1, mapped(mkbuf(0))]), ebm-vol-inv(avol0), is-encoded(lpt, buf), range= (avol0, 5 + lptlebs(# lpt, LEB_SIZE), fill(mkavolume(# avol0), unmapped), 5 + lptlebs(# lpt, LEB_SIZE), # avol0 - 5 + lptlebs(# lpt, LEB_SIZE)), 5 ≤ # avol0, err = ESUCCESS → lebs(avol0, 5, lptlebs(# lpt, LEB_SIZE)) = buf ∧ mapped-full?(avol0, 5, lptlebs(# lpt, LEB_SIZE)), err = ESUCCESS ∨ ⌊err⌋ ⊦ ⟪persistence_io_write_superblock#(sb, m0, m; avol0; err); logoff := m⟫ ( ( err = ESUCCESS → (∃ lpt0, log, orphans. disk-layout(sb, # lpt0) ∧ sb.main + # lpt0 = # avol0 ∧ avol0[0].mapped? ∧ is-encoded(sb, avol0[0].data) ∧ avol0[sb.orph].mapped? ∧ is-encoded-pad(orphans, sb.orphsize, avol0[sb.orph].data) ∧ avol0[sb.log].mapped? ∧ (logoff ≠ LEB_SIZE → # avol0[sb.log].data = logoff) ∧ is-encoded(log, avol0[sb.log].data) ∧ mapped-full?(avol0, sb.lpt, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol0, sb.lpt, lptlebs(# lpt0, LEB_SIZE)))) ∧ m0 = EB_PAGE_SIZE ∧ m = LEB_SIZE ∧ ebm-vol-inv(avol0)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → sb.indexaddr = adr ∧ sb.maxino = m1 ∧ subarray(avol0, sb.main, # avol0 - sb.main) = fill(mkavolume(# lpt), unmapped) ∧ is-encoded(lpt, lebs(avol0, sb.lpt, lptlebs(# avol0 - sb.main, LEB_SIZE))) ∧ avol0[sb.log].data = mkbuf(0) ∧ avol0[sb.orph].data = mkbuf(0)))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 98:
# avol0 = # lpt + 5 + 2 * lptlebs(# lpt, LEB_SIZE), # lebs(avol0, 5, lptlebs(# lpt, LEB_SIZE)) = lptsize(# lpt, LEB_SIZE), avol0[0] = fill(mkavolume(# avol0), unmapped)[0], avol0[1] = mapped(mkbuf(0)), avol0[2] = fill(mkavolume(# avol0), unmapped)[2], avol0[3] = mapped(mkbuf(0)), avol0[4] = fill(mkavolume(# avol0), unmapped)[4], ebm-vol-inv(avol0), ebm-vol-inv(fill(mkavolume(# avol0), unmapped)[1, mapped(mkbuf(0))]), ebm-vol-inv(fill(mkavolume(# avol0), unmapped)), ebm-vol-inv(fill(mkavolume(# avol0), unmapped)[1, mapped(mkbuf(0))][3, mapped(mkbuf(0))]), is-encoded(lpt, lebs(avol0, 5, lptlebs(# lpt, LEB_SIZE))), mapped-full?(avol0, 5, lptlebs(# lpt, LEB_SIZE)), range= (avol0, 5 + lptlebs(# lpt, LEB_SIZE), fill(mkavolume(# avol0), unmapped), 5 + lptlebs(# lpt, LEB_SIZE), # avol0 - 5 + lptlebs(# lpt, LEB_SIZE)), 5 ≤ # avol0 ⊦ ⟪persistence_io_write_superblock# (((((((sb0.indexaddr:= adr).maxino:= m1).log:= 1).orph:= 3).orphsize:= 0).lpt:= 5).main:= (5 + 2 * lptlebs(# lpt, LEB_SIZE)), EB_PAGE_SIZE, LEB_SIZE ; avol0 ; err); logoff := LEB_SIZE⟫ ( ( err = ESUCCESS → (∃ lpt0, log, orphans. disk-layout (((((((sb0.indexaddr:= adr).maxino:= m1).log:= 1).orph:= 3).orphsize:= 0).lpt:= 5).main:= (5 + 2 * lptlebs(# lpt, LEB_SIZE)), # lpt0) ∧ (5 + 2 * lptlebs(# lpt, LEB_SIZE)) + # lpt0 = # avol0 ∧ avol0[0].mapped? ∧ is-encoded (((((((sb0.indexaddr:= adr).maxino:= m1).log:= 1).orph:= 3).orphsize:= 0).lpt:= 5).main:= (5 + 2 * lptlebs(# lpt, LEB_SIZE)), avol0[0].data) ∧ avol0[3].mapped? ∧ is-encoded-pad(orphans, 0, avol0[3].data) ∧ avol0[1].mapped? ∧ (logoff ≠ LEB_SIZE → # avol0[1].data = logoff) ∧ is-encoded(log, avol0[1].data) ∧ mapped-full?(avol0, 5, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol0, 5, lptlebs(# lpt0, LEB_SIZE)))) ∧ ebm-vol-inv(avol0)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → subarray(avol0, 5 + 2 * lptlebs(# lpt, LEB_SIZE), # avol0 - 5 + 2 * lptlebs(# lpt, LEB_SIZE)) = fill(mkavolume(# lpt), unmapped) ∧ is-encoded(lpt, lebs(avol0, 5, lptlebs(# avol0 - 5 + 2 * lptlebs(# lpt, LEB_SIZE), LEB_SIZE))) ∧ avol0[1].data = mkbuf(0) ∧ avol0[3].data = mkbuf(0)))

Rule argument

Additional information

Used simplifier rules: mult-c: ⊦ m * n = n * m; from specification nat-mult%mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult% ⊦ lptlebs(n, LEB_SIZE) * LEB_SIZE = lptsize(n, LEB_SIZE) ↔ true; (s)% ⊦ (sb.maxino:= m).maxino = m; (s)% ⊦ (sb.log:= m0).maxino = sb.maxino; (s)% ⊦ (sb.orph:= m1).maxino = sb.maxino; (s)% ⊦ (sb.orphsize:= m2).maxino = sb.maxino; (s)% ⊦ (sb.lpt:= m3).maxino = sb.maxino; (s)% ⊦ (sb.main:= m4).maxino = sb.maxino; (s)% ⊦ (sb.indexaddr:= adr).indexaddr = adr; (s)% ⊦ (sb.maxino:= m).indexaddr = sb.indexaddr; (s)% ⊦ (sb.log:= m0).indexaddr = sb.indexaddr; (s)% ⊦ (sb.orph:= m1).indexaddr = sb.indexaddr; (s)% ⊦ (sb.orphsize:= m2).indexaddr = sb.indexaddr; (s)% ⊦ (sb.lpt:= m3).indexaddr = sb.indexaddr; (s)% ⊦ (sb.main:= m4).indexaddr = sb.indexaddr; (s)% ⊦ (sb.lpt:= m3).lpt = m3; (s)% ⊦ (sb.main:= m4).lpt = sb.lpt; (s)% ⊦ (sb.log:= m0).log = m0; (s)% ⊦ (sb.orph:= m1).log = sb.log; (s)% ⊦ (sb.orphsize:= m2).log = sb.log; (s)% ⊦ (sb.lpt:= m3).log = sb.log; (s)% ⊦ (sb.main:= m4).log = sb.log; (s)% ⊦ (sb.orphsize:= m2).orphsize = m2; (s)% ⊦ (sb.lpt:= m3).orphsize = sb.orphsize; (s)% ⊦ (sb.main:= m4).orphsize = sb.orphsize; (s)% ⊦ (sb.orph:= m1).orph = m1; (s)% ⊦ (sb.orphsize:= m2).orph = sb.orph; (s)% ⊦ (sb.lpt:= m3).orph = sb.orph; (s)% ⊦ (sb.main:= m4).orph = sb.orph; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ (sb.main:= m4).main = m4; (s)