conforms.abs

notation syntax rsyntax rels runtime rstatics conforms ;
import syntax rsyntax statics1 runtime0 wf wfenv rstatics1 ;

reserve C for :id;
reserve FT0 for :ftyenv
reserve FT for :ftyenv
reserve id for :id;
reserve heap for :heap;
reserve frames for :frames;
reserve s for :frames × heap;
reserve prog for :rprog;
reserve mbody for :rmethodbody;
reserve addr for :int;
reserve val for :rval;

// --------------------------------------------------------------------------
// Weak conformance and Value conformance.
//
// This is not part of the runtime model, but is used to correlate
// the static and runtime models.
// --------------------------------------------------------------------------


def wconforms_to 
  ((TE,heap) |- val wconforms_to val_ty)  <=>
        (?val_ty'. (TE,heap) |- val rval_hastype val_ty' &
                  TE |- val_ty' varty_widens_to val_ty) ;

def fldvals_wconform_to
  ((TE,heap) |- fldvals fldvals_wconform_to C)  <=>
        (!idx vt'. FDecs(TE,C)(idx,vt') --> 
            (?val. PLOOKUP(fldvals)(idx) = SOME(val) & 
              (TE,heap) |- val wconforms_to vt') )


def els_wconform_to
  ((TE,heap) |- vec els_wconform_to vt)  <=>
             (!j. j < LEN(vec) --> 
               (TE,heap) |- EL(j)(vec) wconforms_to vt);



lfp val_conforms_to

Prim 
           (TE,heap) |- RPrim(pval) wconforms_to vt
      // ----------------------------------------------------------
          (TE,heap) |- RPrim(pval) val_conforms_to vt

Null 
           (TE,heap) |- RAddr(NONE) wconforms_to vt
      // ----------------------------------------------------------
          (TE,heap) |- RAddr(NONE) val_conforms_to vt


Object
           (TE,heap) |- RAddr(SOME(addr)) wconforms_to vt &
            FPLOOKUP(heap)(addr) = SOME(OBJECT(fldvals,C)) &
            (TE,heap) |- fldvals fldvals_wconform_to C
      // ----------------------------------------------------------
          (TE,heap) |- RAddr(SOME(addr)) val_conforms_to vt

Array
            (TE,heap) |- RAddr(SOME(addr)) wconforms_to vt &
             FPLOOKUP(heap)(addr) = SOME(ARRAY(vt',vec)) &
             (TE,heap) |- vec els_wconform_to vt'
      // ----------------------------------------------------------
          (TE,heap) |- RAddr(SOME(addr)) val_conforms_to vt





thm weak-from-val 
   (TE,heap) |- val val_conforms_to vt --> 
    (TE,heap) |- val wconforms_to vt

thm typing-from-val
   (TE,heap) |- val val_conforms_to vt --> 
    ?vt'. (TE,heap) |- val rval_hastype vt' & TE |- vt' varty_widens_to vt

thm wconforms-trans
   TE wf_tyenv &
    (TE,heap) |- val wconforms_to val_ty &
    TE |- val_ty varty_widens_to val_ty'
    --> (TE,heap) |- val wconforms_to val_ty';

thm weak-from-typing
   TE wf_tyenv & 
    (TE,heap) |- val rval_hastype val_ty
    --> (TE,heap) |- val wconforms_to val_ty;

thm val_conforms-trans 
   TE wf_tyenv &
    (TE,heap) |- val val_conforms_to val_ty &
    TE |- val_ty varty_widens_to val_ty'
    --> (TE,heap) |- val val_conforms_to val_ty';

thm exp_typing-from-weak
    TE wf_tyenv &
     (TE,heap) |- val wconforms_to valty -->
     ?expty. (TE,FT,heap) |- RValue(val) rexp_hastype expty &
             TE |- expty expty_widens_to SOME(valty)



// Narrowing/enlarging between frames.  There is aconflict of
// terminology here.  One heap conforms, i.e. is bigger (because more elements
// are defined), or narrower (because where the first is defined the
// second is defined and has narrrower type) than another.
// 
// This relation could be defined over a set of active addresses to allow
// a garbage collection rule.  At the moment it constrains heaps to be
// monotonically increasing in size


def heap_leq 
 TE |- heap0 heap_leq heap1 <=>
    !addr. addr ::: FPDOM(heap0) -->
    !val_ty. (TE,heap0) |- RAddr(SOME(addr)) val_conforms_to val_ty
    --> ((TE,heap1) |- RAddr(SOME(addr)) val_conforms_to val_ty) ;


thm heap_leq-refl [simp,auto,prolog] TE |- heap heap_leq heap 




// Heap conformance.  No heap typing is needed.  Again could be
// restricted to a particular set of addresses to allow garbage collection.


def addr_conforms
  (TE,heap) |- addr addr_conforms <=>
    (!fldvals C. 
      FPLOOKUP(heap)(addr) = SOME(OBJECT(fldvals,C)) -->
        ((TE,heap) |- RAddr(SOME(addr)) val_conforms_to VT(Class(C),0)) ) &
    (!st dim vec. 
      FPLOOKUP(heap)(addr) = SOME(ARRAY(VT(st,dim),vec)) -->
        ((TE,heap) |- RAddr(SOME(addr)) val_conforms_to VT(st,dim+1)) );

       
def heap_conforms
   TE |- heap heap_conforms <=>
      !addr. addr ::: FPDOM(heap) --> ((TE,heap) |- addr addr_conforms) 



// Heap conformance is enough to give us typing --> value conformance


thm conforms-from-typing 
    TE wf_tyenv & 
    TE |- heap heap_conforms &
    (TE,heap) |- val rval_hastype val_ty
    --> (TE,heap) |- val val_conforms_to val_ty;


// Facts we derive from heap conformance


// this says that if an object conforms, then all its fields weakly conform.
thm object-fields-conform 
   TE |- heap heap_conforms &
    FPLOOKUP(heap)(addr) = SOME(OBJECT(fldvals,C)) &
    ((C',f),varty) :: FDecs(TE,C) &
    PLOOKUP(fldvals)(C',f) = SOME(val) 
    --> (TE,heap) |- val wconforms_to varty;


// this says that if an array conforms, then all its elements weakly conform.
thm array-elements-conform 
   TE |- heap heap_conforms &
    FPLOOKUP(heap)(addr) = SOME(ARRAY(vt,vec)) &
    j < LEN(vec) -->
    (TE,heap) |- EL(j)(vec) wconforms_to vt



// Define narrowing/enlarging between frame typings.


def ftyenv_leq 
   FT0 ftyenv_leq FT1 <=>
        LEN(FT0) <= LEN(FT1) & (!j. j < LEN(FT0) --> EL(j)(FT0) = EL(j)(FT1))

// a simple one:
thm ftyenv_leq-refl [simp,auto,prolog] 
   FT ftyenv_leq FT;


// Lemmas: as heaps and frame typings get narrower, typing judgemsnts
// get narrower.


thm lemma">val-mono-lemma 
    TE wf_tyenv &
     TE |- heap0 heap_conforms &
     TE |- heap0 heap_leq heap1 &
     (TE,heap0) |- val rval_hastype val_ty
     --> ?val_ty'. (TE,heap1) |- val rval_hastype val_ty' & 
                   TE |- val_ty' varty_widens_to val_ty

thm lemma">exp-mono-lemma 
    TE wf_tyenv &
     TE |- heap0 heap_conforms &
     FT0 ftyenv_leq FT1 & 
     TE |- heap0 heap_leq heap1 &
     (TE,FT0,heap0) |- exp rexp_hastype exp_ty
     --> ?exp_ty'. (TE,FT1,heap1) |- exp rexp_hastype exp_ty' & 
                   TE |- exp_ty' expty_widens_to exp_ty


thm lemma">var-mono-lemma 
    TE wf_tyenv &
     TE |- heap0 heap_conforms &
     FT0 ftyenv_leq FT1 & 
     TE |- heap0 heap_leq heap1 &
     (TE,FT0,heap0) |- var rvar_hastype var_ty
     --> ?var_ty'. (TE,FT1,heap1) |- var rvar_hastype var_ty' & 
                   TE |- var_ty' varty_widens_to var_ty

thm lemma">stmt-mono-lemma
    TE wf_tyenv &
     TE |- heap0 heap_conforms &
     FT0 ftyenv_leq FT1 & 
     TE |- heap0 heap_leq heap1 &
     (TE,FT0,heap0) |- stmt rstmt_hastype
     --> (TE,FT1,heap1) |- stmt rstmt_hastype


// Stack vars and Fields are not just monotonic up to widening - their types
// remain identical
thm StackVar-mono  
    FT0 ftyenv_leq FT1 & 
     TE |- heap0 heap_conforms &
     TE |- heap0 heap_leq heap1 &
     (TE,FT0,heap0) |- RStackVar(fidx,id) rvar_hastype var_ty
     --> (TE,FT1,heap1) |- RStackVar(fidx,id) rvar_hastype var_ty

thm Field-mono  
    FT0 ftyenv_leq FT1 & 
     TE |- heap0 heap_conforms &
     TE |- heap0 heap_leq heap1 &
     (TE,FT0,heap0) |- RField(obj,C,fld) rvar_hastype var_ty
     --> (TE,FT1,heap1) |- RField(obj,C,fld) rvar_hastype var_ty


thm lemma">wconforms-mono-lemma 
    TE wf_tyenv &
     TE |- heap0 heap_conforms &
     TE |- heap0 heap_leq heap1 &
     (TE,heap0) |- val wconforms_to val_ty
     --> (TE,heap1) |- val wconforms_to val_ty

thm lemma">val_conforms-mono-lemma 
    TE wf_tyenv &
     TE |- heap0 heap_conforms &
     TE |- heap0 heap_leq heap1 &
     (TE,heap0) |- val val_conforms_to val_ty
     --> (TE,heap1) |- val val_conforms_to val_ty


// Frames conformance  - connects a frame typing and a state.


def frames_conform_to
  ((TE,heap) |- frames frames_conform_to FT)  <=>
     LEN(frames) = LEN(FT) &  
     !fidx FS. fidx < LEN(frames) & FS = EL(fidx)(FT) -->
     !id vt. id :: PDOM(FS) & PLOOKUP(FS)(id) = SOME(vt) -->
        (?val. sGetStackVar(frames,fidx,id) = SOME(val) &
            (TE,heap) |- val val_conforms_to vt) ;

thm lemma">frames_conform-mono-lemma 
    TE wf_tyenv &
     TE |- heap0 heap_conforms &
     TE |- heap0 heap_leq heap1 &
     (TE,heap0) |- frames frames_conform_to FT
     --> (TE,heap1) |- frames frames_conform_to FT



// Various operations on the state produce a narrower, conformant state.
// Allocation first.


thm initial-values-conform 
   TE |- vt wf_vartype 
    --> (TE,heap) |- initial(vt) wconforms_to vt

// two lemmas about transformations that just add new cells (allocations).
thm lemma">wconforms_preserved-lemma
   TE wf_tyenv &
    TE |- heap0 heap_conforms &
    heap0 FPSUBFUN heap1 &
    (TE,heap0) |- val wconforms_to vt 
    --> (TE,heap1) |- val wconforms_to vt;

thm lemma">heap_leq-lemma
   TE wf_tyenv &
    TE |- heap0 heap_conforms &
    heap0 FPSUBFUN heap1
    --> TE |- heap0 heap_leq heap1;

thm lemma">alloc-conforms-lemma 
   TE wf_tyenv &
    TE |- heap0 heap_conforms &
    heap0 FPSUBFUN heap1 &
    (!addr. addr ::: FPDOM(heap1) & ~(addr ::: FPDOM(heap0)) --> (TE,heap1) |- addr addr_conforms)
    --> TE |- heap1 heap_conforms;


// Allocation preserves conformance, if all the conditions are right.



thm lemma">object-alloc-conforms-lemma 
   TE wf_tyenv &
    TE |- heap0 heap_conforms &  
    (!fld vt. (fld,vt) :: FDecs(TE,C) --> TE |- vt wf_vartype) &
    flds = PGRAPH {fspec | FDecs(TE,C)(fspec)} &
    fldvals = initial o_p flds &
    heapobj = OBJECT(fldvals,C) &
    sAlloc(heap0,heapobj) = (heap1,addr1)
    --> TE |- heap1 heap_conforms &
        TE |- heap0 heap_leq heap1


      // heap1 is conformant because the object rule for conformance for
      // the new address is satisfied.  This is because every field in
      // FDecs(G,C) is given a weakly conforant value by initial.
      //
      // (But how do we know flds is related to FDecs?  The rstatics typing
      //  rules for RNewClass must refer to FDecs!)
      //
      // Note we need the lemmas that FDecs produces a PGRAPH for 
      // a wellformed environment.
 

// similar, but much lengthier
thm lemma">array-alloc-conforms-lemma 
   TE wf_tyenv &
    TE |- heap0 heap_conforms &
    (val1,heap1) = val_alloc(heap0,st,dimns,ext)
    --> TE |- heap1 heap_conforms &
        TE |- heap0 heap_leq heap1

// this is a simple corollary of the general result
thm lemma">array-alloc-types-lemma   
   TE wf_tyenv &
    TE |- heap1 heap_conforms &
    (val1,heap1) = val_alloc(heap0,st,dimns,ext) &
    dim = LEN(dimns)+ext
    --> (TE,FT0,heap1) |- RValue(val1) rexp_hastype SOME(VT(st,dim))



// Assignment to local variables preserves conformance, 
// if all the conditions are right.
//
// Usable as a rewrite if local variables are instantiated explicitly
//
// NOTES ON PROOF:
// the hard part is to establish that heap1 conforms to heap0
// have (FT1,heap1) |- val val_conforms_to var0_ty // by defn. of conformance
// follows because val/exp0 has a type that widens to var0_ty,
// and because TE |- heap0 conforms to FT (this establishes conformance for
// all the addresses that val/exp0 may contain)
//
// Note if we are only using weak conformance the argument would falter
// here.



thm lemma">stack-assign-conforms-lemma 
   TE wf_tyenv &
    (TE,heap) |- frames0 frames_conform_to FT &
    fidx < LEN(FT) &
    PLOOKUP(EL(fidx)(FT))(id) = SOME(vty) &
    (TE,FT,heap) |- RValue(val) rexp_hastype SOME(ety) &
    TE |- ety varty_widens_to vty &
    frames1 = sSetStackVar(frames0,fidx,id,val)
 --> (TE,heap) |- frames1 frames_conform_to FT



// usable as a rewrite if some variables are instantiated explicitly
thm lemma">field-assign-conforms-lemma 
   TE wf_tyenv &
    TE |- heap0 heap_conforms &

    FPLOOKUP(heap0)(addr) = SOME(OBJECT(fldvals,C')) &
    ((C,fld),vty) :: FDecs(TE,C') &

    (TE,heap0) |- val rval_hastype ety &
    TE |- ety varty_widens_to vty &
    heap1 = sFieldSet(heap0,addr,C,fld,val)
 --> TE |- heap1 heap_conforms &
     TE |- heap0 heap_leq heap1


thm typecheck-correct 
  TE wf_tyenv &
  (TE,heap0) |- val rval_hastype ety &
  typecheck((TE,heap0),val,vt)
  --> (TE,heap0) |- val wconforms_to vt
   
// usable as a rewrite if some variables are instantiated explicitly
thm lemma">array-assign-conforms-lemma 
   TE wf_tyenv &
    TE |- heap0 heap_conforms &

    FPLOOKUP(heap0)(addr) = SOME(ARRAY(arrty,vec)) &
    idx < LEN(vec) &

    (TE,heap0) |- val rval_hastype ety &
    typecheck((TE,heap0),val,arrty) &
    heap1 = heap0 <++ (addr,ARRAY(arrty,REPLACE(idx)(vec)(val)))
 --> TE |- heap1 heap_conforms &
     TE |- heap0 heap_leq heap1



// various relations must be undisturbed by a move to a conformant environment
// i.e. monotonic
//
// Note in the long run conformance (increasing the size of an environment) may cause
// much bigger changes, esp. dynamic linking introducing more classes.  These lemmas
// become more complex in that case.

// NOTE: now not needed with static typing environment
//  (will be needed with dynamic linking)


//thm lemma">wf_tyenv-mono-lemma 
//   TE0 wf_tyenv &
//    TE0 tyenv_leq TE1 --> TE1 wf_tyenv

//thm lemma">wf_simptype-mono-lemma 
//   TE0 wf_tyenv &
//    TE0 tyenv_leq TE1 & 
//    TE0 |- st wf_simptype --> 
//    TE1 |- st wf_simptype;

//thm lemma">varty_widens_to-mono-lemma 
//   TE0 wf_tyenv &
//    TE0 tyenv_leq TE1 & 
//    TE0 |- vt1 varty_widens_to vt2 --> 
//    TE1 |- vt1 varty_widens_to vt2;

//thm lemma">subclass_of-mono-lemma 
//   TE0 wf_tyenv &
//    TE0 tyenv_leq TE1 & 
//    TE0 |- C subclass_of C' -->
//    TE1 |- C subclass_of C'

//thm lemma">Cdec-mono-lemma 
//   TE0 wf_tyenv &
//    TE0 tyenv_leq TE1 & 
//    Cdec(TE0,C) = SOME(cdec) -->
//    Cdec(TE1,C) = SOME(cdec)

//thm lemma">MSigsC-mono-lemma 
//   TE0 wf_tyenv &
//    TE0 tyenv_leq TE1 & 
//    MSigsC(TE0,C)(x) -->
//    MSigsC(TE1,C)(x)

//thm lemma">MSigsI-mono-lemma 
//   TE0 wf_tyenv &
//    TE0 tyenv_leq TE1 & 
//    MSigsI(TE0,C)(x) -->
//    MSigsI(TE1,C)(x)