conforms.art

notation syntax rsyntax rels runtime rstatics conforms ;

import syntax rsyntax runtime0 wf wfenv conforms rstatics1 link2_0 statics1 ;


// value conformance implies weak conformance


thm weak-from-val
   if (TE,heap) |- val val_conforms_to vt a
   then (TE,heap) |- val wconforms_to vt

  qed by rule cases on a;

thm typing-from-val
   if (TE,heap) |- val val_conforms_to vt a
   then ?vt'. (TE,heap) |- val rval_hastype vt' & TE |- vt' varty_widens_to vt;

  qed by weak-from-val,WCONFORMS_TO,a;




// transitivity of weak conformance. 


thm wconforms-trans  
if TE wf_tyenv TE_wf
   (TE,heap) |- val wconforms_to val_ty val_conforms
   TE |- val_ty varty_widens_to val_ty' widens1
then (TE,heap) |- val wconforms_to val_ty' goal;

  qed by WCONFORMS_TO,varty_widens_to-trans, val_conforms, widens1,TE_wf;



// value typing implies weak value conformance at the same value.
// It does *not* imply strong value conformance except when the heap conforms!


thm weak-from-typing
if TE wf_tyenv TE_wf
   (TE,heap) |- val rval_hastype val_ty val_types
then (TE,heap) |- val wconforms_to val_ty;

qed by WCONFORMS_TO,varty_widens_to-refl, val_types;



// transitivity of strong value conformance. 


thm val_conforms-trans  
if TE wf_tyenv TE_wf
   (TE,heap) |- val val_conforms_to val_ty val_conforms
   TE |- val_ty varty_widens_to val_ty' widens1
then (TE,heap) |- val val_conforms_to val_ty' goal;

  have (TE,heap) |- val wconforms_to val_ty' 
            by rule cases on val_conforms, wconforms-trans,widens1,TE_wf;
  then qed by rule cases on val_conforms, 
          val_conforms_to__Prim [TE,heap,val_ty'],
          val_conforms_to__Object [TE,heap,val_ty'/vt],
          val_conforms_to__Array [TE,heap,val_ty'/vt],
          val_conforms_to__Null [TE,heap,val_ty'];  // true - meson would get this but tab won't!



// value typing implies weak value conformance at the same value.
// It does *not* imply strong value conformance except when the heap conforms!


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

then qed by expty_widens_to__Some, rstatics__Value, WCONFORMS_TO__rule


// Simple facts about heap conformance


thm heap_leq-refl 
  TE |- heap0 heap_leq heap0;
 qed by  [heap0/heap1]






// And here is the case where the heap conforms, and so typing
// implies strong value conformance.


thm conforms-from-typing 
if TE wf_tyenv TE_wf
   (TE,heap) |- val rval_hastype val_ty val_types
   TE |- heap heap_conforms heap_conforms
then (TE,heap) |- val val_conforms_to val_ty g;

  have (TE,heap) |- val wconforms_to val_ty by weak-from-typing,wconforms-trans,val_types,TE_wf;
  per cases 
   case val = RAddr(SOME(addr)) 
        FPLOOKUP heap addr = SOME(OBJECT(fldvals,C)) lookup
        val_ty = VT(Class(C),0) ;

     qed by HEAP_CONFORMS__rule [TE,heap,addr],ADDR_CONFORMS__object [TE,heap,addr],lookup,heap_conforms,IN_FPDOM;

   case val = RAddr(SOME(addr)) 
        FPLOOKUP heap addr = SOME(ARRAY(VT(simpty,dim),vec)) lookup
        val_ty = VT(simpty,ndim) 
        ndim = dim + 1 ;

     qed by HEAP_CONFORMS__rule [TE,heap,addr],ADDR_CONFORMS__array [TE,heap,addr],lookup,heap_conforms,IN_FPDOM;

  end by rule cases on val_types,g,
          heap_conforms, TE_wf,weak-from-typing, val_types,
          val_conforms_to__Prim [TE,heap],
          val_conforms_to__Null [TE,heap];


//


thm object-fields-conform
  if TE |- heap heap_conforms heap_conforms
     FPLOOKUP heap addr = SOME(OBJECT(fldvals,C)) [rw,auto]
     (idx,varty) :: FDecs(TE,C) is_field
     fldvals idx = SOME(val) [rw,auto]
  then (TE,heap) |- val wconforms_to varty;

  have addr ::: FPDOM(heap) by IN_FPDOM;
  then have (TE,heap) |- RAddr(SOME(addr)) val_conforms_to VT(Class(C),0) addr_conforms
        by HEAP_CONFORMS,ADDR_CONFORMS__object [heap,TE,addr,fldvals],heap_conforms;

  have (TE,heap) |- fldvals fldvals_wconform_to C
    by rule cases on addr_conforms;

  then have
    !idx vt'. FDecs(TE,C)(idx,vt') --> 
           ?val. fldvals idx = SOME(val) & 
                 (TE,heap) |- val wconforms_to vt' fields_conform
    by FLDVALS_WCONFORM_TO;

  qed by hard is_field,IN_ELIM,fields_conform [idx,varty]




// this says that if an array conforms, then all its elements weakly conform.


thm array-elements-conform
  if TE |- heap heap_conforms heap_conforms
     FPLOOKUP heap addr = cell cell
     cell = SOME(ARRAY(vt,vec)) lookup
     j < LEN(vec) is_in_vec
  then (TE,heap) |- EL(j)(vec) wconforms_to vt;

  let vt = VT(simpty,dim) ;
  have addr ::: FPDOM(heap) by IN_FPDOM,lookup,cell;
  then have (TE,heap) |- RAddr(SOME(addr)) val_conforms_to VT(simpty,dim+1) addr_conforms
        by HEAP_CONFORMS,ADDR_CONFORMS__array [heap,TE,addr],lookup,cell,heap_conforms;
  consider fldvals',C'',vt',vec' st
    (cell = SOME(OBJECT(fldvals',C''))) |
     (cell = SOME(ARRAY(vt',vec')) & (TE,heap) |- vec' els_wconform_to vt')
    by rule cases on addr_conforms,cell;

  then qed by lookup, is_in_vec,IN_ELIM,ELS_WCONFORM_TO



// Simple facts about frame typing conformance


thm ftyenv_leq-refl 
  FT ftyenv_leq FT;
 qed by ftyenv_leq [FT/FT1]


// Monotonicity of value typing under stack/heap widening, up to widening



thm val-mono-lemma
if TE wf_tyenv TE_wf
   TE |- heap0 heap_conforms heap0_conforms
   TE |- heap0 heap_leq heap1 heap1_bigger
   (TE,heap0) |- val rval_hastype val_ty val_types_in_heap0
then ?val_ty'. (TE,heap1) |- val rval_hastype val_ty' & 
                TE |- val_ty' varty_widens_to val_ty valgoal;

  // most the cases are trivial because the state is not used. We 
  // only have to consider the two heap object cases,
  // where the result follows easily by the definition of heap_leq.

 per cases
   case val = RAddr(SOME(addr)) 
        FPLOOKUP heap0 addr = SOME(OBJECT(fldvals,C)) lookup
        val_ty = VT(Class(C),0) ;
     have addr ::: FPDOM(heap0) in_heap by IN_ELIM,PDOM,lookup;
     then have (TE,heap0) |- val val_conforms_to val_ty by HEAP_CONFORMS,ADDR_CONFORMS__object,lookup,heap0_conforms;
     then have (TE,heap1) |- val val_conforms_to val_ty by HEAP_LEQ__rule [addr,heap0/heap0,heap1/heap1],val_types_in_heap0,heap1_bigger,in_heap;
     then qed by weak-from-val,typing-from-val;

   case val = RAddr(SOME(addr)) 
        FPLOOKUP heap0 addr = SOME(ARRAY(VT(simpty,dim),vec)) lookup
        val_ty = VT(simpty,ndim) 
        ndim = dim + 1 ;
     have addr ::: FPDOM(heap0) in_heap by IN_ELIM,PDOM,lookup;
     then have (TE,heap0) |- val val_conforms_to val_ty by HEAP_CONFORMS,ADDR_CONFORMS__array,lookup,heap0_conforms;
     then have (TE,heap1) |- val val_conforms_to val_ty by HEAP_LEQ__rule [addr,heap0/heap0,heap1/heap1],val_types_in_heap0,heap1_bigger,in_heap;
     then qed by weak-from-val,typing-from-val;
  end by rule cases on val_types_in_heap0, 
          valgoal [val_ty], varty_widens_to-refl,
          rval_hastype__NullToClass [TE,heap1],
          rval_hastype__NullToInterface [TE,heap1],
          rval_hastype__NullToArray [TE,heap1],
          rval_hastype__Prim [TE,heap1];



// Monotonicity of typing under stack/heap widening, up to widening
//
// This proof subsumes several of the theorems in the abstract.



thm exp-mono-lemma // and , var-mono-lemma, stmt-mono-lemma, StackVar-mono-lemma, Field-mono-lemma
if TE wf_tyenv TE_wf
   TE |- heap0 heap_conforms heap0_conforms
   FT0 ftyenv_leq FT1 FT1_bigger
   TE |- heap0 heap_leq heap1 heap1_bigger
then {
  if (TE,FT0,heap0) |- var rvar_hastype var_ty var_types_in_heap0
  then ?var_ty'. (TE,FT1,heap1) |- var rvar_hastype var_ty' & 
                  TE |- var_ty' varty_widens_to var_ty &
                  (!obj' C' f'. var = RField(obj',C',f') --> var_ty' = var_ty) &
                  (!fidx' id'. var = RStackVar(fidx',id') --> var_ty' = var_ty) vargoal
} and {
  if (TE,FT0,heap0) |- exp rexp_hastype exp_ty exp_types_in_heap0
  then ?exp_ty'. (TE,FT1,heap1) |- exp rexp_hastype exp_ty' & 
                   TE |- exp_ty' expty_widens_to exp_ty expgoal
} and {
  if (TE,FT0,heap0) |- stmt rstmt_hastype stmt_types_in_heap0
  then (TE,FT1,heap1) |- stmt rstmt_hastype
}


proceed by rule induction on 
    var_types_in_heap0 with var,var_ty variable,
    exp_types_in_heap0 with exp,exp_ty variable,
    stmt_types_in_heap0 with stmt variable;

  case StackVar
    var = RStackVar(frame,id)  
    frame < LEN(FT0) 
    EL(frame)(FT0) = FS FS
    PLOOKUP(FS)(id) = SOME(var_ty) ;

    have FS = EL(frame)(FT1) 
         frame < LEN(FT1) by hard FT1_bigger,ftyenv_leq,FS,arith12; 
    then qed by rstatics__StackVar, vargoal [var_ty], varty_widens_to-refl

  case Access
    var = RAccess(arr,idx) 
    var_ty = VT(simpty,ndim) 
    ?exp_ty'. (TE,FT1,heap1) |- arr rexp_hastype exp_ty' & 
               TE |- exp_ty' expty_widens_to SOME(VT(simpty,dim)) arr_ihyp
    (TE,FT0,heap0) |- arr rexp_hastype SOME(VT(simpty,dim)) arr_ty
    0 < dim 
    ?exp_ty'. (TE,FT1,heap1) |- idx rexp_hastype exp_ty' & 
               TE |- exp_ty' expty_widens_to SOME(VT(PrimT(intT),0)) idx_ihyp
    (TE,FT0,heap0) |- idx rexp_hastype SOME(VT(PrimT(intT),0)) idx_ty 
    ndim = dim - 1 ;

    let int = SOME(VT(PrimT(intT),0)) ;

   // tool failure: rigid specification of induction specs mean we have to repeat these to
   // introduce names.
    consider arr_ty1 st
       (TE,FT1,heap1) |- arr rexp_hastype arr_ty1 arr_types_in_s1
       TE |- arr_ty1 expty_widens_to SOME(VT(simpty,dim)) arr_ty1_narrower by arr_ihyp;

    consider simpty1 st
         arr_ty1 = SOME(VT(simpty1,dim)) 
         TE |- simpty1 simpty_widens_to simpty simpty1_narrower
             by array-widens-lemma [TE,arr_ty1,simpty,dim],arr_ty1_narrower;

    consider idx_ty1 st
       (TE,FT1,heap1) |- idx rexp_hastype idx_ty1 idx_types_in_s1
       TE |- idx_ty1 expty_widens_to int idx_ty1_narrower by idx_ihyp;

    have idx_ty1 = int  by idx_ty1_narrower,prim-widens-lemma;

    have TE |- VT(simpty1,ndim) varty_widens_to VT(simpty,ndim) by varty_widens_to__Simple,simpty1_narrower;

    then qed by rstatics__Access [dim/dim], vargoal [VT(simpty1,ndim)], arr_types_in_s1, idx_types_in_s1

  case Field
     var = RField(obj,C',fld)  
     ?exp_ty'. (TE,FT1,heap1) |- obj rexp_hastype exp_ty' & 
                TE |- exp_ty' expty_widens_to SOME(VT(Class(C0),0)) obj_ihyp
     (TE,FT0,heap0) |- obj rexp_hastype SOME(VT(Class(C0),0)) obj_types
     ((C',fld),var_ty) :: FDecs(TE,C0) fld_visible;

   // tool failure: rigid specification of induction specs mean we have to repeat these to
   // introduce names.
    consider obj_ty1 st
       (TE,FT1,heap1) |- obj rexp_hastype obj_ty1 obj_types_in_s1
       TE |- obj_ty1 expty_widens_to SOME(VT(Class(C0),0)) obj_ty1_narrower by obj_ihyp;

        // C can't be Object, 'cos its got an entry in the env.
    per cases 
      case C0 = Object ;
        contradiction by TE_wf,FDecs-Object [TE],fld_visible;

      case C0 <> Object ;
        consider C1 st
           TE |- C1 subclass_of C0 C1_subclass
           obj_ty1 = SOME(VT(Class(C1),0))  
             by class-widens-lemma [C0,TE,obj_ty1],TE_wf,obj_ty1_narrower

        have ((C',fld),var_ty) :: FDecs(TE,C1)
           by inherited-fields-exist [TE],C1_subclass,fld_visible,TE_wf;

        then qed by rstatics__Field [C'/C',C1/C], 
                vargoal [var_ty], obj_types_in_s1
    end;


  case Var
     exp = RVar(svar) 
     exp_ty = SOME(svar_ty) 
     ?var_ty'. (TE,FT1,heap1) |- svar rvar_hastype var_ty' & 
                TE |- var_ty' varty_widens_to svar_ty &
                (!obj' C' f'. svar = RField(obj',C',f') --> var_ty' = svar_ty) &
                (!fidx' id'. svar = RStackVar(fidx',id') --> var_ty' = svar_ty) svar_ihyp
     (TE,FT0,heap0) |- svar rvar_hastype svar_ty svar_types;

   // tool failure: rigid specification of induction specs mean we have to repeat these to
   // introduce names.
    consider svar_ty1 st
       (TE,FT1,heap1) |- svar rvar_hastype svar_ty1 svar_types_in_s1
       TE |- svar_ty1 varty_widens_to svar_ty svar_ty1_narrower by svar_ihyp;

    then have TE |- SOME(svar_ty1) expty_widens_to exp_ty wider by expty_widens_to__Some;

    qed by rstatics__Var, expgoal [SOME(svar_ty1)], svar_types_in_s1, wider;

  case Void
     exp = RVoid  
     exp_ty = NONE ;

     qed by rstatics__Void, expgoal [NONE:varType option]

  case NewClass

    exp = RNewClass(C,flds) 
    exp_ty = SOME(VT(Class(C),0)) 
    !fld vt. (fld,vt) :: FDecs(TE,C) --> TE |- vt wf_vartype fields_wf
    flds = PGRAPH {fspec | FDecs(TE,C)(fspec)}  ;

   qed by rstatics__NewClass [TE,heap1,FT1], expgoal [exp_ty], expty_widens_to-refl,fields_wf

  case NewArray 
    exp = RNewArray(st,dims,ext) 
    exp_ty = SOME(VT(st,dim)) 
    dim = LEN(dims)+ext  
    0 < dim 
    TE |- st wf_simptype 
    !j. j < LEN(dims) --> 
         (?exp_ty'. (TE,FT1,heap1) |- EL(j)(dims) rexp_hastype exp_ty' & 
                    TE |- exp_ty' expty_widens_to (SOME(VT(PrimT(intT),0)))) &
         (TE,FT0,heap0) |- (EL(j)(dims)) rexp_hastype (SOME(VT(PrimT(intT),0))) ihyp;

    let int = SOME(VT(PrimT(intT),0)) ;
    have !j. j < LEN(dims) --> (TE,FT1,heap1) |- EL(j)(dims) rexp_hastype int 
       proof 
        then consider j st
          + j < LEN(dims) 
          - (TE,FT1,heap1) |- EL(j)(dims) rexp_hastype int ;
        consider exp_ty' st 
            (TE,FT1,heap1) |- EL(j)(dims) rexp_hastype exp_ty'
            TE |- exp_ty' expty_widens_to int by ihyp [j];
        then qed by prim-widens-lemma [TE,intT,exp_ty']; ;

    then qed by rstatics__NewArray [heap1,TE,FT1,ext/ext,LEN(dims)+ext/dim,dims,st], 
                expgoal [exp_ty], expty_widens_to-refl;



  case Call
    // Consider the case where all the arguments are ground.
    // A Null excpeption may occur, otherwise get the program body
    // and use lemmas that demonstrate that this has the right type.


    exp = RCall(obj,AT,m,args) 
    exp_ty = rt0 
    LEN(args) = nargs [rw,auto]
    LEN(AT) = nargs [rw,auto]
    ?exp_ty'. (TE,FT1,heap1) |- obj rexp_hastype exp_ty' & 
               TE |- exp_ty' expty_widens_to SOME(vt0) obj_ihyp
    (TE,FT0,heap0) |- obj rexp_hastype SOME(vt0) obj0_types_in_heap0

    MSigs(TE,vt0)(m,MT(AT,rt0)) m_visible_from_vt0

    !j. j < nargs --> 
          ?varty.((?exp_ty'. (TE,FT1,heap1) |- EL(j)(args) rexp_hastype exp_ty' &          
                             TE |- exp_ty' expty_widens_to SOME(varty)) &
                   (TE,FT0,heap0) |- EL(j)(args) rexp_hastype SOME(varty)) &
                  TE |- varty varty_widens_to EL(j)(AT) ihyp_for_args ;


   // tool failure: rigid specification of induction specs mean we have to repeat these to
   // introduce names.
    let obj_ty0 = SOME(vt0) ;
    consider obj_ty1 st
       (TE,FT1,heap1) |- obj rexp_hastype obj_ty1 obj_types_in_s1
       TE |- obj_ty1 expty_widens_to obj_ty0 obj_ty1_narrower by obj_ihyp;

    consider vt1 st
       obj_ty1 = SOME(vt1) 
       TE |- vt1 varty_widens_to vt0 vt1_narrower by rule cases on obj_ty1_narrower,PEXISTS_SPLIT;

   // now establish new types for each argument
    have !j. j < LEN(args) --> 
          ?varty. (TE,FT1,heap1) |- EL(j)(args) rexp_hastype SOME(varty) &
                  TE |- varty varty_widens_to EL(j)(AT) args_type_in_s1
       proof 
        then consider j st
          + j < LEN(args) 
          - ?varty. 
                (TE,FT1,heap1) |- EL(j)(args) rexp_hastype SOME(varty) &
                TE |- varty varty_widens_to EL(j)(AT);
        consider varty0, expty1 st
           (TE,FT1,heap1) |- EL(j)(args) rexp_hastype expty1 argj_types_in_s1
           TE |- expty1 expty_widens_to SOME(varty0) expty1_narrower
           TE |- varty0 varty_widens_to EL(j)(AT) varty0_fits by ihyp_for_args [j];
        consider varty1 st
           expty1 = SOME(varty1) 
           TE |- varty1 varty_widens_to varty0 varty1_narrower by rule cases on expty1_narrower,PEXISTS_SPLIT;
        have TE |- varty1 varty_widens_to EL(j)(AT) varty1_fits 
           by varty0_fits,
              varty_widens_to-trans [TE,varty1/vt1,EL(j)(AT)/vt3,varty0/vt2],
              varty1_narrower,TE_wf; 
                         // BUG: this should not not need explicit instantiation.
        qed by varty1_fits,argj_types_in_s1; ;

   consider rt1 st
     MSigs(TE,vt1)(m,MT(AT,rt1)) m_visible_from_vt1
     TE |- rt1 expty_widens_to rt0 rt1_narrower 
            by inherited-methods-exist [TE],m_visible_from_vt0,TE_wf,vt1_narrower

   qed by rstatics__Call [TE,rt1,heap1,FT1,vt1,args,AT,obj], expgoal [rt1], 
              args_type_in_s1,obj_types_in_s1,m_visible_from_vt1, rt1_narrower;

  case Body
    exp = RBody(rstmt,rexp) 
    (TE,FT1,heap1) |- rstmt rstmt_hastype rstmt_types_in_s1
    (TE,FT0,heap0) |- rstmt rstmt_hastype rstmt_types_in_heap0
    ?exp_ty'. (TE,FT1,heap1) |- rexp rexp_hastype exp_ty' & 
               TE |- exp_ty' expty_widens_to exp_ty rexp_ihyp
    (TE,FT0,heap0) |- rexp rexp_hastype exp_ty rexp0_types_in_heap0;

   // tool failure: rigid specification of induction specs mean we have to repeat these to
   // introduce names.
    consider exp_ty1 st
       (TE,FT1,heap1) |- rexp rexp_hastype exp_ty1 rexp_types_in_s1
       TE |- exp_ty1 expty_widens_to exp_ty exp_ty1_narrower by rexp_ihyp;

   qed by rstatics__Body, expgoal [exp_ty1], exp_ty1_narrower, rexp_types_in_s1, rstmt_types_in_s1;

// ASSIGNMENTS
//  Note that addr := val is not well typed.

  case AssignToStackVar

     stmt = RAssign(RStackVar(fidx,id),rexp) 
     ?exp_ty'. (TE,FT1,heap1) |- rexp rexp_hastype exp_ty' & 
                TE |- exp_ty' expty_widens_to SOME(rexp_vty) rexp_ihyp
     (TE,FT0,heap0) |- rexp rexp_hastype SOME(rexp_vty) rexp0_types
     ?var_ty'. (TE,FT1,heap1) |- RStackVar(fidx,id) rvar_hastype var_ty' & 
                TE |- var_ty' varty_widens_to lval_vty0 &
                (!obj' C' f'. RStackVar(fidx,id) = RField(obj',C',f') --> var_ty' = lval_vty0) &
                (!fidx' id'. RStackVar(fidx,id) = RStackVar(fidx',id') --> var_ty' = lval_vty0) lval_ihyp
     (TE,FT0,heap0) |- RStackVar(fidx,id) rvar_hastype lval_vty0 lval_types_in_heap0
     TE |- rexp_vty varty_widens_to lval_vty0          rexp0_fits;

   // tool failure: rigid specification of induction specs mean we have to repeat these to
   // introduce names.
    consider exp_ty1 st
       (TE,FT1,heap1) |- rexp rexp_hastype exp_ty1 rexp_types_in_s1
       TE |- exp_ty1 expty_widens_to SOME(rexp_vty) exp_ty1_narrower by rexp_ihyp;

    consider exp_vty1 st
       exp_ty1 = SOME(exp_vty1) 
       TE |- exp_vty1 varty_widens_to rexp_vty exp_vty1_narrower by rule cases on exp_ty1_narrower,PEXISTS_SPLIT;

    have TE |- exp_vty1 varty_widens_to lval_vty0 rexp1_fits by varty_widens_to-trans,exp_vty1_narrower,rexp0_fits,TE_wf;
   // tool failure: rigid specification of induction specs mean we have to repeat these to
   // introduce names.
    have (TE,FT1,heap1) |- RStackVar(fidx,id) rvar_hastype lval_vty0 lval_types_in_s1
         TE |- lval_vty0 varty_widens_to lval_vty0 lval_vty0_narrower by lval_ihyp;

    qed by rstatics__AssignToStackVar [exp_vty1/varty', lval_vty0/varty], lval_vty0_narrower, lval_types_in_s1, rexp_types_in_s1, rexp1_fits;


  case AssignToField

     stmt = RAssign(RField(obj,C,fld),rexp) 
     ?exp_ty'. (TE,FT1,heap1) |- rexp rexp_hastype exp_ty' & 
                TE |- exp_ty' expty_widens_to SOME(rexp_vty) rexp_ihyp
     (TE,FT0,heap0) |- rexp rexp_hastype SOME(rexp_vty) rexp_types_in_heap0
     ?var_ty'. (TE,FT1,heap1) |- RField(obj,C,fld) rvar_hastype var_ty' & 
                TE |- var_ty' varty_widens_to lval_vty0 &
                (!obj' C' f'. RField(obj,C,fld) = RField(obj',C',f') --> var_ty' = lval_vty0) &
                (!fidx' id'. RField(obj,C,fld) = RStackVar(fidx',id') --> var_ty' = lval_vty0) lval_ihyp
     (TE,FT0,heap0) |- RField(obj,C,fld) rvar_hastype lval_vty0 lval0_types_in_heap0
     TE |- rexp_vty varty_widens_to lval_vty0          rexp0_fits;

   // tool failure: rigid specification of induction specs mean we have to repeat these to
   // introduce names.
    consider exp_ty1 st
       (TE,FT1,heap1) |- rexp rexp_hastype exp_ty1 rexp_types_in_s1
       TE |- exp_ty1 expty_widens_to SOME(rexp_vty) exp_ty1_narrower by rexp_ihyp;

    consider exp_vty1 st
       exp_ty1 = SOME(exp_vty1) 
       TE |- exp_vty1 varty_widens_to rexp_vty exp_vty1_narrower by rule cases on exp_ty1_narrower,PEXISTS_SPLIT;

    have TE |- exp_vty1 varty_widens_to lval_vty0 rexp1_fits by varty_widens_to-trans,exp_vty1_narrower,rexp0_fits,TE_wf;

   // tool failure: rigid specification of induction specs mean we have to repeat these to
   // introduce names.
    have (TE,FT1,heap1) |- RField(obj,C,fld) rvar_hastype lval_vty0 lval_types_in_s1
         TE |- lval_vty0 varty_widens_to lval_vty0 lval_vty0_narrower by lval_ihyp;

    qed by rstatics__AssignToField [exp_vty1/varty', lval_vty0/varty], lval_vty0_narrower, lval_types_in_s1, rexp_types_in_s1, rexp1_fits;


  case AssignToArray

     stmt = RAssign(RAccess(arr,idx),rexp) 
     ?exp_ty'. (TE,FT1,heap1) |- rexp rexp_hastype exp_ty' & 
                TE |- exp_ty' expty_widens_to rexp_ty rexp_ihyp
     (TE,FT0,heap0) |- rexp rexp_hastype rexp_ty rexp_types_in_heap0
     ?var_ty'. (TE,FT1,heap1) |- RAccess(arr,idx) rvar_hastype var_ty' & 
                TE |- var_ty' varty_widens_to lval_vty0 &
                (!obj' C' f'. RAccess(arr,idx) = RField(obj',C',f') --> var_ty' = lval_vty0) &
                (!fidx' id'. RAccess(arr,idx) = RStackVar(fidx',id') --> var_ty' = lval_vty0) lval_ihyp
     (TE,FT0,heap0) |- RAccess(arr,idx) rvar_hastype lval_vty0 lval0_types_in_heap0;


   // tool failure: rigid specification of induction specs mean we have to repeat these to
   // introduce names.
    consider exp_ty1 st
       (TE,FT1,heap1) |- rexp rexp_hastype exp_ty1 rexp_types_in_s1
       TE |- exp_ty1 expty_widens_to rexp_ty exp_ty1_narrower by rexp_ihyp;

   // tool failure: rigid specification of induction specs mean we have to repeat these to
   // introduce names.
    consider lval_vty1 st
       (TE,FT1,heap1) |- RAccess(arr,idx) rvar_hastype lval_vty1 lval_types_in_s1 by lval_ihyp;

    qed by rstatics__AssignToArray,lval_types_in_s1, rexp_types_in_s1;

// My dumb prover makes this case seem harder than it should!!
  case Value
     exp = RValue(val) 
     exp_ty = SOME(val_ty0) 
     (TE,heap0) |- val rval_hastype val_ty0 val_types_in_heap0;

    consider val_ty1 st
       (TE,heap1) |- val rval_hastype val_ty1  
       TE |- val_ty1 varty_widens_to val_ty0 
            by val-mono-lemma [TE,heap0/heap0,heap1/heap1],TE_wf,heap1_bigger,val_types_in_heap0,heap0_conforms;
    qed by rstatics__Value,expty_widens_to__Some;


   // this should be auotmatic - it isn't hard.  Tab would get it - meson can't handle the
   // simple equality reasoning.
  case If; qed by prim-widens-lemma [TE,boolT],rstatics__If [TE,heap1,FT1];
//     stmt = RIf(bexp,stmt1,stmt2) 
//     (TE,FT1,heap1) |- stmt1 rstmt_hastype 
//     (TE,FT0,heap0) |- stmt1 rstmt_hastype 
//     (TE,FT1,heap1) |- stmt2 rstmt_hastype 
//     (TE,FT0,heap0) |- stmt2 rstmt_hastype 
//     ?exp_ty'. (TE,FT1,heap1) |- bexp rexp_hastype exp_ty' & 
//                TE |- exp_ty' expty_widens_to SOME(VT(PrimT(boolT),0)) 
//     (TE,FT0,heap0) |- bexp rexp_hastype SOME(VT(PrimT(boolT),0));

//   consider exp_ty' (TE,FT1,heap1) |- bexp rexp_hastype exp_ty' & 
//                TE |- exp_ty' expty_widens_to SOME(VT(PrimT(boolT),0)) ;

//   qed by prim-widens-lemma [TE,boolT,exp_ty'],rstatics__If [TE,heap1,FT1];

  case Expr;  qed by rstatics__Expr;
  case Block;  qed by rstatics__Block;


end;








// Monotonicity of weak value conformance under stack/heap widening



thm wconforms-mono-lemma
if TE wf_tyenv TE_wf
   TE |- heap0 heap_conforms heap0_conforms
   TE |- heap0 heap_leq heap1 heap1_bigger
   (TE,heap0) |- val wconforms_to val_ty val_conforms_in_heap0
then (TE,heap1) |- val wconforms_to val_ty goal;

 qed by WCONFORMS_TO,TE_wf,val-mono-lemma [TE,heap0/heap0,heap1/heap1,val], 
        val_conforms_in_heap0,heap1_bigger,  heap0_conforms, varty_widens_to-trans;




// Monotonicity of value conformance under stack/heap widening



thm val_conforms-mono-lemma
if TE wf_tyenv TE_wf
   TE |- heap0 heap_conforms heap0_conforms
   TE |- heap0 heap_leq heap1 heap1_bigger
   (TE,heap0) |- val val_conforms_to val_ty val_conforms_in_heap0
then (TE,heap1) |- val val_conforms_to val_ty goal;

  // most the cases are trivial because the state is not used. We 
  // only have to consider the two heap object cases,
  // where the result follows easily by the definition of heap_leq.

  per cases
    case val = RAddr(SOME(addr)) 
         FPLOOKUP heap0 addr = SOME(heapobj) ;
      have addr ::: FPDOM(heap0) by IN_FPDOM;
      then qed by HEAP_LEQ__rule [heap0/heap0, heap1/heap1, addr],heap1_bigger,val_conforms_in_heap0;
  end by rule cases on val_conforms_in_heap0, 
          goal, heap0_conforms,heap1_bigger, TE_wf,
          val_conforms_to__Prim [TE,heap1],
          val_conforms_to__Null [TE,heap1],
          wconforms-mono-lemma [TE,heap0/heap0,heap1/heap1]



// Monotonicity of addr_conforms.  NO!! Self-consistency is not implied by 
// heap0 heap_leq heap1.


//proof of // addr_conforms-mono-lemma
//if TE wf_tyenv 
//   TE |- heap0 heap_conforms 
//   TE |- heap0 heap_leq heap1 
//   addr ::: FPDOM(heap0) 
//   (TE,heap0) |- addr addr_conforms 
//then (TE,heap1) |- addr addr_conforms;




// Monotonicity of frames conformance under stack/heap widening


thm frames_conform-mono-lemma
if TE wf_tyenv TE_wf
   TE |- heap0 heap_conforms heap0_conforms
   TE |- heap0 heap_leq heap1 heap1_bigger
   (TE,heap0) |- frames frames_conform_to FT frames_conform_in_heap0
then (TE,heap1) |- frames frames_conform_to FT;

  qed by FRAMES_CONFORM_TO,TE_wf,heap0_conforms,heap1_bigger,
         frames_conform_in_heap0,val_conforms-mono-lemma [TE,heap0/heap0,heap1/heap1];  // needs long search



// this says that object allocation preserves heap conformance
//
// A nasty but interesting proof.



// first prove initial creates values that conform
thm  initial-values-conform
  if TE |- vt wf_vartype vt_wf
  then (TE,heap) |- initial(vt) wconforms_to vt goal;
  consider st',dim st 
      + vt = VT(st',dim) 
      - (TE,heap) |- initial(vt) rval_hastype vt g by WCONFORMS_TO,varty_widens_to-refl [vt,TE],goal;
  have TE |- st' wf_simptype st_wf by vt_wf,WF_VARTYPE;
  consider pt st vt = VT(PrimT(pt),0)  
     by g,initial,
            rule cases on st_wf,st_wf,
            rval_hastype__NullToClass [TE,heap],
            rval_hastype__NullToInterface [TE,heap],
            rval_hastype__NullToArray [TE,heap], ZERO_CASES [dim];  // case split helps determine when dim is zero - silly arith stuff!
  qed by structural cases on pt,initial,
            g,rval_hastype__Prim [TE,heap];




// allocation preserves weak conformance


thm wconforms_preserved-lemma
  if TE wf_tyenv TE_wf
     TE |- heap0 heap_conforms heap0_conforms
     heap0 FPSUBFUN heap1 heap0_preserved
     (TE,heap0) |- val wconforms_to vt val_wconforms_in_heap0
  then (TE,heap1) |- val wconforms_to vt goal;

  consider vt' st
      + (TE,heap0) |- val rval_hastype vt' val_types_in_heap0
      + TE |- vt' varty_widens_to vt  widens
      - ?vt''. (TE,heap1) |- val rval_hastype vt'' & TE |- vt'' varty_widens_to vt valgoal
           by val_wconforms_in_heap0,goal,WCONFORMS_TO;
  per cases
       case val = RAddr(SOME(addr)) 
          FPLOOKUP heap0 addr = SOME(OBJECT(fldvals,C)) lookup
          vt' = VT(Class(C),0) ;
         have FPLOOKUP heap1 addr = SOME(OBJECT(fldvals,C)) by heap0_preserved,lookup,FPSUBFUN [heap0/f1]
         then qed by rval_hastype__AddrToClass [TE,heap1,fldvals,C,addr], valgoal [vt'], val_types_in_heap0, widens;

       case val = RAddr(SOME(addr)) 
         FPLOOKUP heap0 addr = SOME(ARRAY(VT(simpty,dim'),vec)) lookup
         vt' = VT(simpty,ndim) 
         ndim = dim' + 1 ;
         have FPLOOKUP heap1 addr = SOME(ARRAY(VT(simpty,dim'),vec)) by heap0_preserved,lookup,FPSUBFUN [heap0/f1];
         then qed by rval_hastype__AddrToArray [TE,heap1,dim'/dim,vec,ndim/ndim,addr,simpty], valgoal [vt'], val_types_in_heap0, widens;

  end by rule cases on  val_types_in_heap0, 
          valgoal [vt'], widens, 
          rval_hastype__NullToClass [TE,heap1],
          rval_hastype__NullToInterface [TE,heap1],
          rval_hastype__NullToArray [TE,heap1],
          rval_hastype__Prim [TE,heap1];





// allocation preserves value conformance


thm heap_leq-lemma
  if TE wf_tyenv TE_wf
     TE |- heap0 heap_conforms heap0_conforms
     heap0 FPSUBFUN heap1 heap0_preserved
  then TE |- heap0 heap_leq heap1 goal;

  have !val vt. (TE,heap0) |- val wconforms_to vt --> 
               (TE,heap1) |- val wconforms_to vt wconforms_preserved
         by wconforms_preserved-lemma [TE,heap0/heap0,heap1/heap1],TE_wf,
            heap0_conforms,heap0_preserved,FPSUBFUN [heap0/f1];

  consider addr,val_ty st
    + addr ::: FPDOM(heap0)  addr_in_heap0
    + (TE,heap0) |- RAddr(SOME(addr)) val_conforms_to val_ty addr_conforms_in_heap0
    - (TE,heap1) |- RAddr(SOME(addr)) val_conforms_to val_ty
         by goal,;
     
  per cases
      case
       (TE,heap0) |- RAddr(SOME(addr)) wconforms_to val_ty addr_wconforms_in_heap0
       FPLOOKUP heap0 addr = SOME(OBJECT(fldvals,C)) lookup
       (TE,heap0) |- fldvals fldvals_wconform_to C  fields_wconform_in_heap0;

         have FPLOOKUP heap1 addr = SOME(OBJECT(fldvals,C)) lookup_in_heap1  by heap0_preserved,lookup,FPSUBFUN [heap0/f1];
         have  (TE,heap1) |- RAddr(SOME(addr)) wconforms_to val_ty  addr_wconforms_in_heap1
                  by wconforms_preserved,TE_wf, addr_wconforms_in_heap0;

         have (TE,heap1) |- fldvals fldvals_wconform_to C  fields_wconform_in_heap1
           by wconforms_preserved, fields_wconform_in_heap0,FLDVALS_WCONFORM_TO;

         qed by addr_wconforms_in_heap1,lookup_in_heap1,
                val_conforms_to__Object [TE,heap1,addr,C,val_ty,fldvals],
                fields_wconform_in_heap1;

     case
       (TE,heap0) |- RAddr(SOME(addr)) wconforms_to val_ty addr_wconforms_in_heap0
       FPLOOKUP heap0 addr = SOME(ARRAY(vt',vec)) lookup
       (TE,heap0) |- vec els_wconform_to vt' els_wconform_in_heap0;

         have FPLOOKUP heap1 addr = SOME(ARRAY(vt',vec)) lookup_in_heap1 by heap0_preserved,lookup,FPSUBFUN [heap0/f1];
         have  (TE,heap1) |- RAddr(SOME(addr)) wconforms_to val_ty  addr_wconforms_in_heap1
                  by wconforms_preserved,TE_wf, addr_wconforms_in_heap0;
         have (TE,heap1) |- vec els_wconform_to vt' els_wconform_in_heap1
             by wconforms_preserved [vt'], els_wconform_in_heap0, ELS_WCONFORM_TO

         qed by addr_wconforms_in_heap1,lookup_in_heap1,
                val_conforms_to__Array [TE,heap1,addr,vec],
                els_wconform_in_heap1;

  end by hard rule cases on addr_conforms_in_heap0;


// if conformance is valid at all new addresses, then
// allocation results in a conformant heap.




thm alloc-conforms-lemma
  if TE wf_tyenv TE_wf
     TE |- heap0 heap_conforms heap0_conforms
     heap0 FPSUBFUN heap1 
     !addr. addr ::: FPDOM(heap1) & ~(addr ::: FPDOM(heap0)) --> (TE,heap1) |- addr addr_conforms alloced_conform
  then TE |- heap1 heap_conforms goal;

   // now show the new heap is narrower, in the sense that it preserves value conformance
 have TE |- heap0 heap_leq heap1 heap1_larger 
    by heap_leq-lemma [TE,heap0/heap0,heap1/heap1],
       TE_wf,heap0_conforms;

  // now show that the new heap conforms at every address.  Only need to consider old
  // addresses in detail because we know newly allocated things conform.
 per cases 

   // The object case.  Old objects conform because they are identical in the new heap.    
   case
     + addr ::: FPDOM(heap0) addr_in_heap0
     + FPLOOKUP heap1 addr = SOME(OBJECT(fldvals,C)) lookup 
     - (TE,heap1) |- RAddr(SOME(addr)) val_conforms_to VT(Class(C),0);

     have FPLOOKUP heap0 addr = SOME(OBJECT(fldvals,C)) lookup_in_heap0  
          by FPSUBFUN_REVERSE [addr,heap0/f1,heap1/f2,OBJECT(fldvals,C)/y'], lookup,  addr_in_heap0,IN_FPDOM;

     have (TE,heap0) |- RAddr(SOME(addr)) val_conforms_to VT(Class(C),0) addr_conforms_in_heap0
             by HEAP_CONFORMS__rule [heap0,addr,TE],ADDR_CONFORMS__object [heap0,addr,C], addr_in_heap0, lookup_in_heap0, heap0_conforms;
     then qed by addr_in_heap0,val_conforms-mono-lemma [heap0/heap0,heap1/heap1],TE_wf,heap1_larger,heap0_conforms;

   // The array case.  Old Arrays conform because they are identical in the new heap.    
   case 
     + addr ::: FPDOM(heap0) addr_in_heap0
     + FPLOOKUP heap1 addr = SOME(ARRAY(VT(st,dim),vec)) lookup
     - (TE,heap1) |- RAddr(SOME(addr)) val_conforms_to VT(st,dim+1);

     have FPLOOKUP heap0 addr =  SOME(ARRAY(VT(st,dim),vec)) lookup_in_heap0  
             by FPSUBFUN_REVERSE [addr,heap0/f1,heap1/f2,ARRAY(VT(st,dim),vec)/y'], lookup, addr_in_heap0,IN_FPDOM;
     have (TE,heap0) |- RAddr(SOME(addr)) val_conforms_to VT(st,dim+1) addr_conforms_in_heap0
             by HEAP_CONFORMS__rule [heap0,addr,TE],ADDR_CONFORMS__array [heap0,addr,st,dim,vec,TE], addr_in_heap0, lookup_in_heap0, heap0_conforms;
     then qed by addr_in_heap0,val_conforms-mono-lemma,TE_wf,heap1_larger,heap0_conforms;

 end by hard goal,HEAP_CONFORMS,ADDR_CONFORMS,heap1_larger,alloced_conform;


// object allocation preserves conformance.


thm object-alloc-conforms-lemma
  if TE wf_tyenv TE_wf
     flds = PGRAPH {fspec | FDecs(TE,C1)(fspec)}  flds
     !fld vt. (fld,vt) :: FDecs(TE,C1) --> TE |- vt wf_vartype fields_wf
     fldvals1 = initial o_p flds fldvals1
     heapobj1 = OBJECT(fldvals1,C1)  heapobj
     sAlloc(heap0,heapobj1) = (heap1,addr1) alloc
     TE |- heap0 heap_conforms heap0_conforms
  then TE |- heap1 heap_conforms &
        TE |- heap0 heap_leq heap1 goal;

 // show all original addresses are preserved
 have heap0 FPSUBFUN heap1 heap0_preserved
    by hard FPSUBFUN_ELIM,alloc,sAlloc,freshi [FPDOM heap0],IN_FPDOM;  // actually easy - I just need to fix higher-order case splitting

   // now show the new heap is narrower, in the sense that it preserves value conformance
 have TE |- heap0 heap_leq heap1 heap1_larger 
    by heap_leq-lemma [TE,heap0/heap0,heap1/heap1],heap0_preserved,TE_wf,heap0_conforms;

 // the new address conforms
 have !addr. addr ::: FPDOM(heap1) & ~(addr ::: FPDOM(heap0)) --> (TE,heap1) |- addr addr_conforms alloced_conform
    proof then sts (TE,heap1) |- addr1 addr_conforms
            by EXCLUDED_MIDDLE [addr = addr1], IN_ELIM,PDOM,alloc,sAlloc,freshi [FPDOM heap0];  // easy with splitting
      have FPLOOKUP heap1 addr1 = SOME(heapobj1) [rw,auto] by heapobj,sAlloc,alloc;
      have (TE,heap1) |- RAddr(SOME(addr1)) rval_hastype VT(Class(C1),0) weak
                     by rval_hastype__AddrToClass [fldvals1,heap1,TE,addr1,C1],heapobj;
      then have (TE,heap1) |- RAddr(SOME(addr1)) wconforms_to VT(Class(C1),0) weak
                 by WCONFORMS_TO,varty_widens_to-refl;
      have (TE,heap1) |- fldvals1 fldvals_wconform_to C1 
         proof then consider idx,vt' st
             + FDecs(TE,C1)(idx,vt') idx_is_field
             - ?val. fldvals1 idx = SOME(val) & 
                      (TE,heap1) |- val wconforms_to vt' by FLDVALS_WCONFORM_TO;
             have TE |- vt' wf_vartype vt_wf by fields_wf,idx_is_field,IN_ELIM;
             have flds(idx) = SOME(vt') 
                 by object-fields-form-graph [TE],TE_wf,
                         PGRAPH_SOME [{fspec | FDecs(TE,C1)(fspec)}/R],flds,idx_is_field,GSPEC_ELIM;
             then have fldvals1(idx) = SOME(initial vt') [rw,auto] by fldvals1; 
             qed by initial-values-conform,vt_wf; ;
       then qed by val_conforms_to__Object [fldvals1,C1,heap1,TE,VT(Class(C1),0),addr1],
                   weak,ADDR_CONFORMS,heapobj; ;
   
 qed by heap1_larger,alloc-conforms-lemma [heap1/heap1,heap0/heap0,TE],
        alloced_conform,heap0_conforms,heap0_preserved,TE_wf;




// this says that array allocation preserves heap conformance
//
// A nasty but interesting proof.  



// allocation is a doubly recursive process - once for the number of dimensions
// and once for each dimension.  Hence we have a double induction.  We prove
// that the key properties are preserved throughout this process.

thm array-alloc-conforms-lemma // subsumes array-alloc-types-lemma
  if TE wf_tyenv TE_wf
     TE |- VT(st,ext) wf_vartype st_wf
     (val1,heap1) = val_alloc(heap0,st,dims,ext) alloc
     TE |- heap0 heap_conforms heap0_conforms

  then heap0 FPSUBFUN heap1 &
        TE |- heap1 heap_conforms &
        (TE,heap1) |- val1 wconforms_to VT(st,LEN(dims)+ext) goal;

 proceed by structural induction on dims with dims,heap0,heap1,val1 variable;

  case NIL dims = [] ;
    qed by heap_leq-refl,heap0_conforms,alloc,val_alloc,initial-values-conform [TE,VT(st,ext)],st_wf; 

  case CONS 
    dims = dim × dims'  dims
    !heap0 heap1 val1. 
        (val1,heap1) = val_alloc(heap0,st,dims',ext) &
        TE |- heap0 heap_conforms -->
        heap0 FPSUBFUN heap1 &
        TE |- heap1 heap_conforms &
        (TE,heap1) |- val1 wconforms_to VT(st,LEN(dims')+ext) ihyp;

    let arr_ty = VT(st,LEN(dims)+ext)  arr_ty;

    let alloc_step = LAM(vec,heap). let (val,heap') = val_alloc(heap,st,dims',ext) in (val×vec,heap')  alloc_step;

    consider heapB,heapobjB,vecB,addrB st
      (vecB,heapB) = REPEATN dim ([],heap0) alloc_step repeat_alloc_step
      heapobjB = ARRAY(VT(st,LEN(dims')+ext),vecB) heapobj
      (heap1,addrB) = sAlloc(heapB,heapobjB) alloc2
      val1 = RAddr(SOME(addrB)) val1 by val_alloc,alloc,alloc_step;

    have heap0 FPSUBFUN heapB heap0_preservedB
         TE |- heapB heap_conforms heapB_conforms
         (TE,heapB) |- vecB els_wconform_to VT(st,LEN(dims')+ext) vecB_wconforms


      proof proceed by structural induction on dim with dim,vecB,heapB variable
                 discarding alloc,goal,alloc2,heapobj,val1,arr_ty,dims;
                    // Discussion about nested inductions:
                    // val1, heap1, dims and addrB are irrelevant for the inner induction, but
                    // are not logically held constant.  They appear in 
                    // the induction condition below in the conditions as equalities, but that's all.
                    // These conditions are automatically eliminated.  Without rigid induction
                    // case specs these would not be needed.
                    //
                    // The situation is actually worse than I thought - the whole original goal appears
                    // all over again in the induction hypothesis.  Blah.
                    //
                    // Problem solved!  Allow explicit mention of goals/facts to discard/include

        case 0 dim = 0 ;
          have (vecB,heapB) = ([],heap0)  by repeat_alloc_step;
          qed by heap_leq-refl,heap0_conforms,ELS_WCONFORM_TO;

        case SUC 
          dim = SUC k  
          !vecB heapB.
           (vecB,heapB) = REPEATN k ([],heap0) alloc_step
         -->
           heap0 FPSUBFUN heapB &
           TE |- heapB heap_conforms &
           (TE,heapB) |- vecB els_wconform_to VT(st,LEN(dims')+ext) repeat-ihyp;

          let elem_ty = VT(st,LEN(dims')+ext) ;
          consider heapA,vecA,valB st
            (vecA,heapA) = REPEATN k ([],heap0) alloc_step inductive-computation
            (valB,heapB) = val_alloc(heapA,st,dims',ext) step-computation
            vecB = valB × vecA  by alloc_step,repeat_alloc_step;


          have heap0 FPSUBFUN heapA t1
               TE |- heapA heap_conforms heapA_conforms 
               (TE,heapA) |- vecA els_wconform_to elem_ty  t6
            by repeat-ihyp [heapA/heapB,vecA/vecB],inductive-computation;

          have heapA FPSUBFUN heapB u1
               TE |- heapB heap_conforms heapB_conforms
               (TE,heapB) |- valB wconforms_to elem_ty u6
                   by ihyp [heapA/heap0,heapB/heap1,valB/val1],step-computation,heapA_conforms;

          
          have heap0 FPSUBFUN heapB  v1
             by u1,t1,FPSUBFUN_ELIM;

          have (TE,heapB) |- vecB els_wconform_to elem_ty v2
             by t6,u6,EL_CONS_ELIM,ELS_WCONFORM_TO,
                wconforms_preserved-lemma [TE,heapA/heap0,heapB/heap1,elem_ty],
                TE_wf,heapA_conforms,u1,arith11; // needs arith - yuck
   
          qed by v1,v2,heapB_conforms;
          
      end; ;

   let elem_ty = VT(st,LEN(dims')+ext) ;
   have heapB FPSUBFUN heap1  heapB_preserved
     by hard alloc2,sAlloc,freshi [FPDOM heapB],IN_FPDOM,FPSUBFUN_ELIM;  // actually easy - I just need to fix higher-order case splitting
   then have heap0 FPSUBFUN heap1  heap0_preserved
     by heap0_preservedB,FPSUBFUN_ELIM;  // actually easy - I just need to fix higher-order case splitting

   // now show the new heap is narrower, in the sense that it preserves value conformance
   have TE |- heap0 heap_leq heap1 heap1_larger 
       by heap_leq-lemma [TE,heap0/heap0,heap1/heap1],heap0_preserved,TE_wf,heap0_conforms;

   // now show the new heap is narrower, in the sense that it preserves value conformance
   have TE |- heapB heap_leq heap1 heap1_largerB 
       by heap_leq-lemma [TE,heapB/heap0,heap1/heap1],heapB_preserved,TE_wf,heapB_conforms;

   have FPLOOKUP heap1 addrB = SOME(heapobjB) [rw,auto] by heapobj,sAlloc,alloc2;

   // this is needed for the induction invariant
   have (TE,heap1) |- val1 wconforms_to arr_ty  val1_wconforms
       by val1,WCONFORMS_TO__derive [val1,TE,heap1,arr_ty/val_ty],
          rval_hastype__AddrToArray [TE,LEN(dims)+ext/ndim,LEN(dims')+ext/dim,vecB,heap1,addrB,st],heapobj;

   have !addr. addr ::: FPDOM(heap1) & ~(addr ::: FPDOM(heap0)) --> (TE,heap1) |- addr addr_conforms alloced_conform
       proof then consider addr st
          + addr ::: FPDOM(heap1) a1
          + ~(addr ::: FPDOM(heap0)) a0
          - (TE,heap1) |- addr addr_conforms g;
       then per cases 
          case + addr ::: FPDOM(heapB) addr_in_B;
          per cases
            case + FPLOOKUP heap1 addr = SOME(OBJECT(fldvals,C)) lookup
                 - (TE,heap1) |- RAddr(SOME(addr)) val_conforms_to VT(Class(C),0) goal;

              have FPLOOKUP heapB addr = SOME(OBJECT(fldvals,C)) 
                    by addr_in_B,IN_FPDOM,heapB_preserved,
                       FPSUBFUN_REVERSE [OBJECT(fldvals,C)/y',addr,heapB/f1,heap1/f2],lookup;
              then have (TE,heapB) |- RAddr(SOME(addr)) val_conforms_to VT(Class(C),0) 
                  by heapB_conforms,HEAP_CONFORMS__rule [heapB,TE,addr],
                   ADDR_CONFORMS__object [heapB,TE,addr],addr_in_B;
              then qed by val_conforms-mono-lemma [heapB/heap0,heap1/heap1],TE_wf,heap1_largerB,heapB_conforms;

            case + FPLOOKUP heap1 addr = SOME(ARRAY(VT(stD,dimD),vec)) lookup
                 - (TE,heap1) |- RAddr(SOME(addr)) val_conforms_to VT(stD,dimD+1);

              have FPLOOKUP heapB addr = SOME(ARRAY(VT(stD,dimD),vec))
                    by lookup,addr_in_B,IN_FPDOM,heapB_preserved,
                       FPSUBFUN_REVERSE [ARRAY(VT(stD,dimD),vec)/y',addr,heapB/f1,heap1/f2];

              then have (TE,heapB) |- RAddr(SOME(addr)) val_conforms_to VT(stD,dimD+1) 
                  by heapB_conforms,HEAP_CONFORMS__rule [heapB,TE],
                     ADDR_CONFORMS__array [TE,addr,heapB],addr_in_B;
              then qed by val_conforms-mono-lemma [heapB/heap0,heap1/heap1,TE],TE_wf,heap1_largerB,heapB_conforms;
          end by ADDR_CONFORMS,g;

          case addr = addrB ;
            have !val vt. (TE,heapB) |- val wconforms_to vt --> 
                           (TE,heap1) |- val wconforms_to vt wconforms_preserved
                    by wconforms_preserved-lemma [TE,heapB/heap0,heap1/heap1],
                       TE_wf,heapB_conforms,heapB_preserved,FPSUBFUN [heapB/f1,heap1/f2];
            have (TE,heap1) |- vecB els_wconform_to elem_ty 
                    by vecB_wconforms,wconforms_preserved,ELS_WCONFORM_TO;
            then have (TE,heap1) |- val1 val_conforms_to arr_ty 
               by val_conforms_to__Array [addr,TE,heap1,arr_ty/vt,VT(st,LEN(dims')+ext)/vt',vecB],
                  val1_wconforms,val1,heapobj;
            then qed by heapobj,ADDR_CONFORMS,val1;
       end by IN_FPDOM,alloc2,sAlloc; ;

   have TE |- heap1 heap_conforms heap1_conforms
       by heap1_larger,alloc-conforms-lemma [TE,heap0/heap0,heap1/heap1],
          alloced_conform,heap0_conforms,heap0_preserved,TE_wf;


   qed by heap0_preserved,heap1_conforms,val1_wconforms;

 end;


// this says that stack assignment preserves frames conformance


thm stack-assign-conforms-lemma 
  if TE wf_tyenv TE_wf
     TE |- heap heap_conforms heap_conforms
     (TE,heap) |- frames0 frames_conform_to FT frames0_conform
     fidx < LEN(FT) 
     (EL(fidx)(FT))(id) = SOME(vty)  lookup
     (TE,heap) |- val rval_hastype ety val_types
     TE |- ety varty_widens_to vty widens
     frames1 = sSetStackVar(frames0,fidx,id,val) 
 then (TE,heap) |- frames1 frames_conform_to FT

 have LEN frames0 = LEN FT [rw,auto] by FRAMES_CONFORM_TO,frames0_conform;
 have (TE,heap) |- val val_conforms_to ety 
     by val_types,heap_conforms,TE_wf,conforms-from-typing [TE,heap];
 then have (TE,heap) |- val val_conforms_to vty 
     by val_conforms-trans,TE_wf,widens;
 
 then qed by FRAMES_CONFORM_TO,
             frames0_conform,sGetStackVar,sSetStackVar,lookup,EL_REPLACE_ELIM; // needs long search??

 


// this says that array assignment preserves heap conformance.  The runtime
// check implies that the value assigned into the array weakly conforms,
// which is all we need.



thm field-assign-conforms-lemma 
  if TE wf_tyenv TE_wf
     TE |- heap0 heap_conforms heap0_conforms
     FPLOOKUP heap0 taddr = SOME(OBJECT(fldvals,C'))  lookup
     ((C,fld),vty) :: FDecs(TE,C') visible

     (TE,heap0) |- sval rval_hastype ety sval_types
     TE |- ety varty_widens_to vty sval_fits
     heap1 = sFieldSet(heap0,taddr,C,fld,sval) heap1
 then TE |- heap1 heap_conforms &
       TE |- heap0 heap_leq heap1 g;

 have !val vt. (TE,heap0) |- val wconforms_to vt --> 
                (TE,heap1) |- val wconforms_to vt wconforms_preserved
   proof then consider val,val_ty st
      (TE,heap0) |- val rval_hastype val_ty val_types
    - (TE,heap1) |- val rval_hastype val_ty  g
                   byWCONFORMS_TO
     per cases 
        case FPLOOKUP heap0 addr = SOME(OBJECT(fldvals2,C2)) [rw,auto]
             val = RAddr(SOME(addr)) 
             val_ty = VT(Class(C2),0) ;

           qed by rval_hastype__AddrToClass [TE,heap1,C2,addr],
                   lookup,EXCLUDED_MIDDLE [addr = taddr],heap1,sFieldSet,PAPPLY_ELIM,hoFieldSet;

        case FPLOOKUP heap0 addr = SOME(ARRAY(VT(simpty2,dim2),vec2)) [rw,auto]
             ndim2 = dim2+1 
             val = RAddr(SOME(addr)) 
             val_ty = VT(simpty2,ndim2) ;
             
           qed by rval_hastype__AddrToArray [TE,heap1,addr],
                  rval_hastype__AddrToArray [TE,heap1,taddr],
                       EXCLUDED_MIDDLE [addr = taddr],lookup,COND_RATOR,COND_RAND,heap1,sFieldSet,hoFieldSet,PAPPLY_ELIM;

     end by rule cases on val_types,EXCLUDED_MIDDLE [addr = taddr],g,heap1,sFieldSet,PAPPLY_ELIM,hoFieldSet,
          rval_hastype__NullToClass [TE,heap1],
          rval_hastype__NullToInterface [TE,heap1],
          rval_hastype__NullToArray [TE,heap1],
          rval_hastype__Prim [TE,heap1]; ;

 // the value assigned to the field weakly conforms
 have (TE,heap1) |- sval wconforms_to vty sval_wconforms
    by WCONFORMS_TO,sval_fits,sval_types,TE_wf,wconforms_preserved;

 have TE |- heap0 heap_leq heap1 heap1_larger
   proof then consider addr,val_ty st
      addr ::: FPDOM(heap0)
      (TE,heap0) |- RAddr(SOME(addr)) val_conforms_to val_ty addr_conforms
    - (TE,heap1) |- RAddr(SOME(addr)) val_conforms_to val_ty by ;

    per cases 
      case addr <> taddr 
           (TE,heap0) |- RAddr(SOME(addr)) wconforms_to val_ty addr_wconforms
           FPLOOKUP heap1 addr = SOME(OBJECT(fldvals2,C2)) [rw,auto]
           (TE,heap0) |- fldvals2 fldvals_wconform_to C2 fields_wconform;

        have (TE,heap1) |- fldvals2 fldvals_wconform_to C2 by wconforms_preserved,FLDVALS_WCONFORM_TO,fields_wconform;
        then qed by val_conforms_to__Object [TE,addr,heap1,fldvals2,C2,val_ty],
                   wconforms_preserved,addr_wconforms;

      case addr = taddr 
           (TE,heap0) |- RAddr(SOME(addr)) wconforms_to val_ty addr_wconforms
           vec' = REPLACE(idx)(tvec)(sval) 
           FPLOOKUP heap1 addr = SOME(OBJECT(fldvals',C')) [auto,rw]
           fldvals' = fldvals <+ ((C,fld),sval) fldvals2
           (TE,heap0) |- fldvals fldvals_wconform_to C' fldvals_conform;

        have (TE,heap1) |- fldvals' fldvals_wconform_to C' 
           proof then consider  Cf,f,vt' st
            + FDecs(TE,C')((Cf,f),vt') 
            - ?val. fldvals' (Cf,f) = SOME(val) & 
                    (TE,heap1) |- val wconforms_to vt' by FLDVALS_WCONFORM_TO;
             per cases
                case (Cf,f) = (C,fld) ; 
                    have vty = vt'  by visible,IN_ELIM, object-fields-unique [TE],PFORALL_SPLIT,TE_wf;
                    qed by fldvals_conform,FLDVALS_WCONFORM_TO,wconforms_preserved,
                          sval_wconforms,fldvals2;
               case (Cf,f) <> (C,fld) ;
                    qed by fldvals_conform,FLDVALS_WCONFORM_TO__rule [TE,fldvals,(Cf,f),vt'],
                           wconforms_preserved,fldvals2;
             end; ;


        then qed by val_conforms_to__Object [TE,addr,heap1,fldvals',val_ty/vt],
               addr_wconforms,wconforms_preserved;

      case (TE,heap0) |- RAddr(SOME(addr)) wconforms_to val_ty addr_wconforms
           FPLOOKUP heap0 addr = SOME(ARRAY(VT(simpty',dim'),vec')) [auto,rw]
           (TE,heap0) |- vec' els_wconform_to VT(simpty',dim') vec_wconforms;

        have FPLOOKUP heap1 addr = SOME(ARRAY(VT(simpty',dim'),vec')) [rw,auto] a by lookup,heap1,sFieldSet,hoFieldSet,PAPPLY_ELIM;
        have (TE,heap1) |- vec' els_wconform_to VT(simpty',dim') by wconforms_preserved,ELS_WCONFORM_TO,vec_wconforms;
        then qed by a,val_conforms_to__Array [TE,addr,heap1,VT(simpty',dim')/vt',vec',val_ty/vt],
               addr_wconforms,wconforms_preserved;

    end by rule cases on addr_conforms,lookup,EXCLUDED_MIDDLE [addr = taddr],heap1,sFieldSet,hoFieldSet,PAPPLY_ELIM; ;

 per cases
   case
      FPLOOKUP heap1 addr = SOME(OBJECT(fldvals2,C2))  lookup2
    - (TE,heap1) |- RAddr(SOME(addr)) val_conforms_to VT(Class(C2),0);

      consider fldvals'' st FPLOOKUP heap0 addr = SOME(OBJECT(fldvals'',C2))  in0 by lookup,lookup2,heap1,sFieldSet,hoFieldSet,PAPPLY_ELIM;
      then have (TE,heap0) |- RAddr(SOME(addr)) val_conforms_to VT(Class(C2),0)
        by HEAP_CONFORMS__rule [addr,TE,heap0],heap0_conforms,
           ADDR_CONFORMS__object [TE,addr,heap0,fldvals'',C2],IN_FPDOM;

      then qed by PEXISTS_SPLIT,heap1_larger,HEAP_LEQ__rule [TE,heap0/heap0,heap1/heap1,VT(Class(C2),0),addr],in0,IN_FPDOM;
        
   case 
      FPLOOKUP heap1 addr = SOME(ARRAY(VT(st',dim'),vec')) lookup2
    - (TE,heap1) |- RAddr(SOME(addr)) val_conforms_to VT(st',dim'+1);

      have FPLOOKUP heap0 addr = SOME(ARRAY(VT(st',dim'),vec'))  in0 by lookup,lookup2,heap1,sFieldSet,hoFieldSet,PAPPLY_ELIM;
      then have (TE,heap0) |- RAddr(SOME(addr)) val_conforms_to VT(st',dim'+1)
        by HEAP_CONFORMS__rule [addr,TE,heap0],heap0_conforms,
           ADDR_CONFORMS__array [TE,addr,heap0,st',vec',dim'],IN_FPDOM;

      then qed by heap1_larger,HEAP_LEQ__rule [TE,heap0/heap0,heap1/heap1,VT(st',dim'+1),addr],in0,IN_FPDOM;

 end by g,HEAP_CONFORMS,heap1_larger,ADDR_CONFORMS,