enrich
   gjournal-base

with
   

   
   
   functions  valid-group-nodes : group-node-list → nat;
              refsize0-addresses : group-store → address-set;
              nodes : group-store × nat-set → node-store;
              nodes : nat × group-block → node-store;
              abs-log : nat-list × group-store → address-list;
              . ↓ : group-block → group-block;
              . ↓ : group-store → group-store;
   predicates  remove-nonend-inv : address-list × address-list × address-list × group-node-list × group-node-list × bool;
               restore-log-inv : nat-list × nat-list × group-store × nat-set × address-list × error;
   
   variables  lnum : nat;
              validhead : bool;
   
   

   

   axioms down-block
          : ⊦   gblock ↓
              = groupblock
                (prefixn(valid-group-nodes(gblock.gndlist), gblock.gndlist), prefixn(valid-group-nodes(gblock.gndlist), gblock.ladrlist), 
                 gblock.ref-size);
          down-store-in :  ⊦ n ∈ gstore ↓ ↔ n ∈ gstore;
          used for: s, ls;
          down-store-at :  ⊦ n ∈ gstore → gstore ↓[n] = gstore[n] ↓;
          used for: s, ls;
          valid-group-nodes-base :  ⊦ valid-group-nodes([]) = 0;
          used for: s, ls;
          valid-group-nodes-rec :  ⊦ valid-group-nodes(gndx + gnd ') = (gnd.end ⊃ # gndx + 1;valid-group-nodes(gndx));
          used for: s, ls;
          abs-log-base :  ⊦ abs-log([], gstore) = [];
          used for: s, ls;
          abs-log-rec :  ⊦ abs-log(n ' + nx, gstore) = gstore[n].ladrlist.to-adr(n) + abs-log(nx, gstore);
          used for: s, ls;
          nodes-gstore-in :  ⊦ adr ∈ nodes(gstore, ginval) ↔ ¬ ¬(adr ∈ gstore ∧ ¬ adr.lnum ∈ ginval);
          used for: ls;
          nodes-gstore-at :  ⊦ adr ∈ nodes(gstore, ginval) → nodes(gstore, ginval)[adr] = gstore[adr].nd;
          used for: s, ls;
          nodes-block-in :  ⊦ adr ∈ nodes(n, gblock) ↔ ¬ ¬(adr.lnum = n ∧ @(adr.pos, adr.size) ∈ gblock.ladrlist);
          used for: ls;
          nodes-block-at :  ⊦ adr ∈ nodes(n, gblock) → nodes(n, gblock)[adr] = gblock.gndlist[pos(@(adr.pos, adr.size), gblock.ladrlist)].nd;
          used for: s, ls;
          refsize0-addresses :  ⊦ adr ∈ refsize0-addresses(gstore) ↔ ¬ ¬(adr ∈ gstore ∧ gstore[adr.lnum].ref-size = 0);
          used for: ls;
          remove-nonend-inv
          : ⊦   remove-nonend-inv(log, log0, ax, gndx, gndx0, boolvar)
              ↔ (∃ gndx1. 
                     # ax = # gndx ∧ gndx = gndx0 + gndx1 ∧ log = log0 + prefixn(# gndx0, ax)
                   ∧ valid-group-nodes(gndx0) = valid-group-nodes(gndx) ∧ (boolvar → # gndx0 = valid-group-nodes(gndx)));
          used for: s, ls;
          restore-log-inv
          : ⊦   restore-log-inv(nx, nx1, gstore, ginval, log, err)
              ↔ (∃ nx0. 
                     nx = nx0 + nx1 ∧ inv(gstore \ ginval) ∧ (err = ESUCCESS ∨ ⌊err⌋ )
                   ∧ (err = ESUCCESS → log = abs-log(nx0, gstore ↓) ∧ elems nx ⊆ dom gstore ∧ elems nx ∩ ginval = ∅));
          used for: s, ls;

   

   
end enrich