Specification persistence-io-inv

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

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,
enrich
   encoding-superblock
, 
   encoding-lpt, 
   encoding-log, 
   encoding-orphans
, 
   ebm-vol-inv

with
   

   
   constants  SB_LOG : nat;
              SB_ORPH : nat;
              SB_LPT : nat;
   functions  lebs : avolume × nat × nat → buffer;
   predicates  persistence-io-inv : superblock × nat × avolume × lp-array × nat-list × nat-set;
               disk-layout : superblock × nat;
               mapped-full? : avolume × nat × nat;
   
   variables  main : nat;
              logoff : nat;
              log : nat-list;
              orphans : nat-set;
   
   

   

   axioms persistence-io-inv
          : ⊦   persistence-io-inv(sb, logoff, avol, lpt, log, orphans)
              ↔ (∃ mainareasize. 
                     disk-layout(sb, mainareasize) ∧ sb.main + mainareasize = # avol ∧ avol[0].mapped? ∧ is-encoded(sb, avol[0].data)
                   ∧ avol[sb.orph].mapped? ∧ is-encoded-pad(orphans, sb.orphsize, avol[sb.orph].data) ∧ avol[sb.log].mapped?
                   ∧ (logoff ≠ LEB_SIZE → # avol[sb.log].data = logoff) ∧ is-encoded(log, avol[sb.log].data)
                   ∧ mapped-full?(avol, sb.lpt, lptlebs(mainareasize, LEB_SIZE)) ∧ # lpt = mainareasize
                   ∧ is-encoded(lpt, lebs(avol, sb.lpt, lptlebs(mainareasize, LEB_SIZE))));
          used for: s, ls;
          disk-layout
          : ⊦   disk-layout(sb, mainareasize)
              ↔   (  sb.log = SB_LOG ∧ sb.orph = SB_ORPH ∧ sb.lpt = SB_LPT
                   ∨ sb.log = SB_LOG + 1 ∧ sb.orph = SB_ORPH + 1 ∧ sb.lpt = SB_LPT + lptlebs(mainareasize, LEB_SIZE))
                ∧ sb.main = SB_LPT + 2 * lptlebs(mainareasize, LEB_SIZE);
          used for: ls;
          sb-log :  ⊦ SB_LOG = 1;
          used for: s, ls;
          sb-orph :  ⊦ SB_ORPH = 3;
          used for: s, ls;
          sb-lpt :  ⊦ SB_LPT = 5;
          used for: s, ls;
          lebs-base :  ⊦ lebs(avol, n, 0) = mkbuf(0);
          used for: s, ls;
          lebs-rec
          : ⊦   n + m < # avol
              →   lebs(avol, n, m + 1)
                = lebs(avol, n, m) + (avol[n + m].mapped? ⊃ avol[n + m].data + mkempbuf(LEB_SIZE - # avol[n + m].data);mkempbuf(LEB_SIZE));
          used for: ls;
          mapped-full
          :  ⊦ mapped-full?(avol, n, m) ↔ (∀ n0. n ≤ n0 ∧ n0 < n + m ∧ n0 < # avol → avol[n0].mapped? ∧ # avol[n0].data = LEB_SIZE);
          used for: ls;

   

   
end enrich