enrich gen-execute , 
       gen-value , 
       gen-names , 
       gen-command-list
 with
   functions 
      contents : systemstate × name → value;
      comment: Rushby Def. 5;
       
      observe : secdomain → names;
      comment: Rushby Def. 5;
       
      alter : secdomain → names;
      comment: Rushby Def. 5;
       
      run : systemstate × commandlist → systemstate;
      execl : commandlist → systemstate;
      step : systemstate × command → systemstate;
      test : commandlist × command → output;
      purge : systemstate × commandlist × secdomain → commandlist;
   predicates 
       . ⇒ . : secdomain × secdomain;
      comment: security policy, interference relation;
       
      eqd : systemstate × secdomain × systemstate;
      comment: Rushby Reference Monitor Assumption.;
       
   
   axioms 
      eqd-def :  ⊦ eqd(sys, d, sys0) ↔ (∀ nam. nam ∈ observe(d) → contents(sys, nam) = contents(sys0, nam));
      RMA-1 :  ⊦ eqd(sys, cdom(co), sys0) → exec(sys, co) .2 = exec(sys0, co) .2;
      RMA-2
      : ⊦ 
          eqd(sys, cdom(co), sys0) ∧ (contents(exec(sys, co) .1, nam) ≠ contents(sys, nam) ∨ contents(exec(sys0, co) .1, nam) ≠ contents(sys0, nam))
        → contents(exec(sys, co) .1, nam) = contents(exec(sys0, co) .1, nam);
      RMA-2-weaker
      : ⊦ 
          eqd(sys, cdom(co), sys0) ∧ contents(sys, nam) = contents(sys0, nam) ∧ nam ∈ alter(cdom(co))
        → contents(exec(sys, co) .1, nam) = contents(exec(sys0, co) .1, nam);
      RMA-3 :  ⊦ contents(exec(sys, co) .1, nam) ≠ contents(sys, nam) → nam ∈ alter(cdom(co));
      policy-respects-observe :  ⊦ d ⇒ d0 → observe(d) ⊆ observe(d0);
      alter-observe-respects-policy :  ⊦ nam ∈ alter(d) ∧ nam ∈ observe(d0) → d ⇒ d0;
      test :  ⊦ test(cl, co) = exec(execl(cl), co) .2;
      step :  ⊦ step(sys, co) = exec(sys, co) .1;
      run-base :  ⊦ run(sys, []) = sys;
      used for : s, ls;
       
      run-rec :  ⊦ run(sys, co ' + cl) = run(exec(sys, co) .1, cl);
      used for : s, ls;
       
      execl :  ⊦ execl(cl) = run(initialstate, cl);
      purge-base :  ⊦ purge(sys, [], d) = [];
      used for : s, ls;
       
      purge-rec :  ⊦ purge(sys, co ' + cl, d) = ((cdom(co) ⇒ d ⊃ co + purge(exec(sys, co) .1, cl, d); purge(sys, cl, d)));
end enrich