subred.artnotation syntax rsyntax rels runtime rstatics conforms ; import syntax rsyntax statics1 cstatics runtime0 wf runtime1 ; wfenv link2_0 rstatics1 conforms exceptional subred.aux rsubst; //theorem subject_reduction proof of // What follows is the statement of four facts that get proved by // mutual recursion using rule induct'n if TE wf_tyenv TE_wf // TE |- FT0 wf_ftyenv FT0_wf (TE,heap0) |- frames0 frames_conform_to FT0 frames0_conform TE |- heap0 heap_conforms heap0_conforms TE |- p cprog_hastype p_types s0 = (frames0,heap0) s1 = (frames1:frames,(heap1:heap)) then { if (var0,s0) var_reduce(TE,p) (var1,s1) var0_reduces (TE,FT0,heap0) |- var0 rvar_hastype var0_ty var0_welltyped then var_types (TE,FT0,heap0) var0 var0_ty (var1,s1) or exceptional_var(var1) var1_exceptional } and { if (exp0,s0) exp_reduce(TE,p) (exp1,s1) exp0_reduces (TE,FT0,heap0) |- exp0 rexp_hastype exp0_ty exp0_welltyped then exp_types (TE,FT0,heap0) exp0_ty (exp1,s1) or exceptional_exp(exp1) exp1_exceptional } and { if (stmt0,s0) stmt_reduce(TE,p) (stmtB,s1) stmt0_reduces (TE,FT0,heap0) |- stmt0 rstmt_hastype stmt0_welltyped then stmt_types (TE,FT0,heap0) (stmtB,s1) or exceptional_stmt(stmtB) stmtB_exceptional } ; // We prove all three goals by mutual induct'n over the derivation // of the typing judgments. proceed by rule induction on var0_welltyped with var0, var0_ty, var1 variable, exp0_welltyped with exp0, exp0_ty, exp1 variable, stmt0_welltyped with stmt0, stmtB variable; (* i.e. with TE,FT0,s0,rp,p,decs,s1 etc. constant *) case StackVar var0 = RStackVar(frame,id) frame < LEN(FT0) EL(frame)(FT0) = FS PLOOKUP(FS)(id) = SOME(var0_ty); contradiction by rule cases on var0_reduces; case Access var0 = RAccess(arr0,idx0) var0_ty = VT(simpty0,ndim) !arr1. (arr0,s0) exp_reduce(TE,p) (arr1,s1) --> exp_types (TE,FT0,heap0) (SOME (VT (simpty0,dim))) (arr1,s1) | exceptional_exp arr1 arr0_ihyp (TE,FT0,heap0) |- arr0 rexp_hastype SOME(VT(simpty0,dim)) arr0_ty 0 < dim !idx1. (idx0,s0) exp_reduce(TE,p) (idx1,s1) --> exp_types (TE,FT0,heap0) (SOME (VT (PrimT intT,0))) (idx1,s1) | exceptional_exp idx1 idx0_ihyp (TE,FT0,heap0) |- idx0 rexp_hastype SOME(VT(PrimT(intT),0)) idx0_ty ndim = dim - 1 ; let arr0_ty = SOME(VT(simpty0,dim)) ; let int = SOME(VT(PrimT(intT),0)) ; per cases // case where arr0 reduces to something case var1 = RAccess(arr1,idx0) (arr0,s0) exp_reduce(TE,p) (arr1,s1) arr0_reduces; // This case is quite complex because there are two subexpressions. // did arr0 give an exception. per cases case exceptional_exp(arr1) ; qed by exceptional,not var1_exceptional; // arr0 reduces conformantly, to some narrower array. case TE |- heap0 heap_leq heap1 heap1_larger FT0 ftyenv_leq FT1 FT1_larger (TE,heap1) |- frames1 frames_conform_to FT1 frames1_conform TE |- heap1 heap_conforms heap1_conforms (TE,FT1,heap1) |- arr1 rexp_hastype arr1_ty arr1_ty TE |- arr1_ty expty_widens_to arr0_ty arr1_narrower ; // the thing it reduces to is indeed an aray, of the same dimension consider simpty1 st arr1_ty = SOME(VT(simpty1,dim)) TE |- simpty1 simpty_widens_to simpty0 simpty0_narrower by array-widens-lemma,arr1_narrower; // we now know the type for the new var1 let var1_ty = VT(simpty1,dim-1) ; // idx0 might have a narrower type because // of side effects on the state. However, there is no type narrower // than int. have (TE,FT1,heap1) |- idx0 rexp_hastype int idx0_types_in_s1 by exp-mono-lemma [TE,heap0/heap0,heap1/heap1,FT0/FT0, FT1/FT1,idx0,int],idx0_ty, FT1_larger,TE_wf,heap0_conforms, heap1_larger,prim-widens-lemma; // demonstrate var1_ty is indeed the type for the new overall expression have (TE,FT1,heap1) |- var1 rvar_hastype var1_ty var1_types by rstatics__Access [dim/dim],arr1_ty,idx0_types_in_s1; // demonstrate that this overall type is indeed narrower have TE |- var1_ty varty_widens_to var0_ty var1_narrower by varty_widens_to__Simple,simpty0_narrower; qed by FT1_larger,frames1_conform,heap1_conforms,var1_types,var1_narrower,heap1_larger,var_types; end by arr0_ihyp [arr1],arr0_reduces, exp_types; case var1 = RAccess(arr0,idx1) (idx0,s0) exp_reduce(TE,p) (idx1,s1) idx0_reduces; // did idx0 give an exception? per cases case exceptional_exp(idx1) ; qed by exceptional, not var1_exceptional; // idx0 reduces conformantly, to something wider. case TE |- heap0 heap_leq heap1 heap1_larger FT0 ftyenv_leq FT1 FT1_larger (TE,heap1) |- frames1 frames_conform_to FT1 frames1_conform TE |- heap1 heap_conforms heap1_conforms (TE,FT1,heap1) |- idx1 rexp_hastype idx1_ty idx1_ty TE |- idx1_ty expty_widens_to int idx1_narrower; // However, there is no type narrower // then int. have idx1_ty = int by idx1_narrower,prim-widens-lemma; // idx0 might have a narrower type because // of side effects on the state, so arr0 might have narrowed! consider arr0_ty2 st (TE,FT1,heap1) |- arr0 rexp_hastype arr0_ty2 arr0_ty2 TE |- arr0_ty2 expty_widens_to arr0_ty arr0_ty2_narrower by exp-mono-lemma [TE,heap0/heap0,heap1/heap1,FT0/FT0, FT1/FT1,arr0,arr0_ty] ,arr0_ty, FT1_larger,TE_wf,heap0_conforms, heap1_larger; // and the only thing it could have narrowed to is an array type: consider simpty1 st arr0_ty2 = SOME(VT(simpty1,dim)) TE |- simpty1 simpty_widens_to simpty0 simpty1_narrower by array-widens-lemma,arr0_ty2_narrower; // we now know the type for the new var1 let var1_ty = VT(simpty1,dim-1) ; // etc. have (TE,FT1,heap1) |- var1 rvar_hastype var1_ty var1_types by rstatics__Access [dim/dim] ,idx1_ty,arr0_ty2; have TE |- var1_ty varty_widens_to var0_ty var1_narrower by varty_widens_to__Simple,simpty1_narrower; qed by FT1_larger,frames1_conform,heap1_conforms, var1_types,var1_narrower,heap1_larger,var_types; end by idx0_reduces,idx0_ihyp [idx1],exp_types; end by rule cases on var0_reduces case Field var0 = RField(obj0,C',fld) !obj1. (obj0,s0) exp_reduce(TE,p) (obj1,s1) --> exp_types (TE,FT0,heap0) (SOME (VT (Class(C0),0))) (obj1,s1) | exceptional_exp obj1 ihyp0 (TE,FT0,heap0) |- obj0 rexp_hastype SOME(VT(Class(C0),0)) obj0_types ((C',fld),var0_ty) :: FDecs(TE,C0) fld_visible; let obj0_ty = SOME(VT(Class(C0),0)) ; consider obj1 st var1 = RField(obj1,C',fld) (obj0,s0) exp_reduce(TE,p) (obj1,s1) obj0_reduces by rule cases on var0_reduces; // but did obj0 --> obj1 give an exception? per cases case exceptional_exp(obj1) ; qed by exceptional , not var1_exceptional; // obj0 reduces conformantly, to something narrower. case TE |- heap0 heap_leq heap1 heap1_larger FT0 ftyenv_leq FT1 FT1_larger (TE,heap1) |- frames1 frames_conform_to FT1 frames1_conform TE |- heap1 heap_conforms heap1_conforms (TE,FT1,heap1) |- obj1 rexp_hastype obj1_ty obj1_types TE |- obj1_ty expty_widens_to obj0_ty obj1_narrower; // C can't be Object, 'cos its got a field 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 obj1_ty = SOME(VT(Class(C1),0)) by TE_wf,class-widens-lemma [TE,C0,obj1_ty],obj1_narrower // fix wf condition! have ((C',fld),var0_ty) :: FDecs(TE,C1) by inherited-fields-exist [TE],C1_subclass,fld_visible,TE_wf; then have (TE,FT1,heap1) |- var1 rvar_hastype var0_ty var1_types by rstatics__Field [C1/C],obj1_types; qed by FT1_larger,frames1_conform,heap1_conforms,var1_types,heap1_larger,var_types,PEXISTS_SPLIT; end; end by ihyp0 [obj1],obj0_reduces,exp_types; // case Value // contradiction by exp0_reduces; case Var exp0 = RVar(svar0) exp0_ty = SOME(svar0_ty) !var1. (svar0,s0) var_reduce(TE,p) (var1,s1) --> var_types (TE,FT0,heap0) svar0 svar0_ty (var1,s1) | exceptional_var var1 ihyp0 (TE,FT0,heap0) |- svar0 rvar_hastype svar0_ty svar0_types; // All the complexity of the Array, StackVar and Field access // cases gets covered here, because these are ground variables // but unground expressions. // if svar0 is var_ground, then by case analysis of the // various possible forms of welltyped var_ground terms, // svar0 must take one of the following forms: // Notes on the analysis: // -- the only welltyped values that type to a class are // RValue(RAddr(NONE)) and RValue(RAddr(addr)). // -- similarly for arrays. // In all these cases a reduction or an exception happens. per cases case FPLOOKUP(heap0)(addr) = cell cell cell = SOME(OBJECT(fldvals,C)) lookup PLOOKUP(fldvals)(Cf,f) = SOME(fldval) fldval_in_object svar0 = RField(RValue(RAddr(SOME(addr))),Cf,f) exp1 = RValue(fldval) s1 = s0 ; // Now the case where we're resolving a field reference. No // ihyps are used. // // All of the following follow by case analysis on the typing rules! consider Caddr st (TE,FT0,heap0) |- RValue(RAddr(SOME(addr))) rexp_hastype SOME(VT(Class(Caddr),0)) addr_types ((Cf,f),svar0_ty) :: FDecs(TE,Caddr) f_visible by rule cases on svar0_types; // C is the runtime type of the object being accessed // Caddr is the type of the address as given by the type system, which we prove to be the same as C // Cf is the class where the field being accessed in found have (TE,heap0) |- RAddr(SOME(addr)) rval_hastype VT(Class(Caddr),0) addr_types2 by rule cases on addr_types; // by typing the cell is either an object or an array consider fldvals' st cell = SOME(OBJECT(fldvals',Caddr)) by rule cases on addr_types2,cell; then have C = Caddr by lookup; // requires some non-trivial equality reasoning // exp0/svar0 is the entire field access expression // we look up the field, which is well typed because // of conformance. // We have TE |- s0 conforms to FT0, thus addr conforms to C, // Thus the field conforms to the type of the field. // // Hence we have: then have ((Cf,f),svar0_ty) :: FDecs(TE,C) f_in_C by inherited-fields-exist,TE_wf,f_visible; have (TE,heap0) |- fldval wconforms_to svar0_ty fldval_conforms by object-fields-conform,heap0_conforms,lookup,cell,f_in_C,fldval_in_object; // Because fldval weakly conforms, we have some type // exp1_ty narrower than svar0_ty (this is an important lemma!). consider exp1_ty st (TE,FT0,heap0) |- RValue(fldval) rexp_hastype exp1_ty exp1_types TE |- exp1_ty expty_widens_to SOME(svar0_ty) exp1_narrower by exp_typing-from-weak,fldval_conforms,TE_wf; qed by exp1_types,frames0_conform,heap0_conforms,exp1_narrower,exp_types; // The array access case: case dest_int32(k32) >>= 0 n = int_to_nat(dest_int32(k32)) FPLOOKUP(heap0)(addr) = cell cell cell = SOME(ARRAY(varty,vec)) lookup n < LEN(vec) svar0 = RAccess(RValue(RAddr(SOME(addr))),RValue(RPrim(Int(k32)))) exp1 = RValue(EL(n)(vec)) s1 = s0 ; // Now the case where we're resolving an array reference. No // ihyps are used. consider simpty,dim st (TE,FT0,heap0) |- RValue(RAddr(SOME(addr))) rexp_hastype SOME(VT(simpty,dim)) addr_types 0 < dim svar0_ty = VT(simpty,dim-1) // (TE,FT,s) |- RValue(RPrim(Int(k32))) rexp_hastype SOME(VT(PrimT(intT),0)) k32_types by rule cases on svar0_types; have (TE,heap0) |- RAddr(SOME(addr)) rval_hastype VT(simpty,dim) addr_types2 by rule cases on addr_types; consider dim',vec' st dim = dim'+1 cell = SOME(ARRAY(VT(simpty,dim'),vec')) by rule cases on addr_types2,cell; then have varty = VT(simpty,dim') by lookup; have (TE,heap0) |- EL(n)(vec) wconforms_to varty val1_conforms by array-elements-conform,heap0_conforms,lookup,cell; // Because val1 weakly conforms, we have some type // exp1_ty narrower than svar0_ty (this is an important lemma!). consider exp1_ty st (TE,FT0,heap0) |- RValue(EL(n)(vec)) rexp_hastype exp1_ty exp1_types TE |- exp1_ty expty_widens_to SOME varty exp1_narrower by exp_typing-from-weak,val1_conforms,TE_wf; qed by exp1_types,frames0_conform,heap0_conforms,exp1_narrower,exp_types; case sGetStackVar(frames0,fidx,id) = fcell fcell fcell = SOME(val) fetch svar0 = RStackVar(fidx,id) exp1 = RValue(val) s1 = s0 ; consider FS st fidx < LEN(FT0) EL(fidx)(FT0) = FS FS id = exp0_ty id by rule cases on svar0_types; have LEN frames0 = LEN FT0 [rw,auto] by frames0_conform,FRAMES_CONFORM_TO; consider val' st fcell = SOME(val') fetch2 (TE,heap0) |- val' val_conforms_to svar0_ty by FRAMES_CONFORM_TO__stackvar [FT0,fidx,TE,heap0,frames0,id,svar0_ty], IN_ELIM,PDOM,frames0_conform, fcell,id,TE_wf; then consider exp1_ty st (TE,FT0,heap0) |- RValue(val') rexp_hastype exp1_ty exp1_types TE |- exp1_ty expty_widens_to exp0_ty exp1_narrower by weak-from-val [TE,svar0_ty,heap0], exp_typing-from-weak [FT0,TE,heap0,svar0_ty], TE_wf; have val = val' by fetch2,fetch; qed by exp1_narrower,frames0_conform,heap0_conforms,exp1_types,exp_types; case (svar0,s0) var_reduce(TE,p) (svar1,s1) svar0_reduces exp0 = RVar(svar0) exp1 = RVar(svar1) ; // did svar0 give an exception? per cases case exceptional_var(svar1) ; qed by exceptional, not exp1_exceptional; // svar0 reduces conformantly, to something narrower. case TE |- heap0 heap_leq heap1 heap1_larger FT0 ftyenv_leq FT1 FT1_larger (TE,heap1) |- frames1 frames_conform_to FT1 frames1_conform TE |- heap1 heap_conforms heap1_conforms (TE,FT1,heap1) |- svar1 rvar_hastype svar1_ty svar1_ty TE |- svar1_ty varty_widens_to svar0_ty svar1_narrower; let exp1_ty = SOME(svar1_ty) ; have (TE,FT1,heap1) |- exp1 rexp_hastype exp1_ty exp1_types by rstatics__Var,svar1_ty have TE |- exp1_ty expty_widens_to exp0_ty exp1_narrower by expty_widens_to__Some,svar1_narrower; qed by FT1_larger,frames1_conform,heap1_conforms,exp1_types,exp1_narrower,heap1_larger,exp_types; end by ihyp0 [svar1],svar0_reduces,var_types ; // NEEDS HIGH TIME LIMIT end by rule cases on exp0_reduces, not exp1_exceptional, exceptional; // cases // CHECKED case Void exp0 = RVoid exp0_ty = NONE; contradiction by rule cases on exp0_reduces // CHECKED, apart from important state conformance lemma case NewClass // Determine the obvious reduction, prove that the new state conforms. // No exception possible, no narrowing occurs. exp0 = RNewClass(C,flds) exp0_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)} flds ; consider fldvals,addr1,heapobj,val1 st fldvals = initial o_p flds fldvals heapobj = OBJECT(fldvals,C) sAlloc(heap0,heapobj) = (heap1,addr1) alloc val1 = RAddr(SOME(addr1)) exp1 = RValue(val1) frames1 = frames0 by rule cases on exp0_reduces; have FPLOOKUP heap1 addr1 = SOME(heapobj) [rw,auto] by sAlloc,alloc; then have (TE,FT0,heap1) |- exp1 rexp_hastype exp0_ty exp1_types by rval_hastype__AddrToClass [heap1,addr1,fldvals],rstatics__Value; have TE |- heap1 heap_conforms heap1_conforms TE |- heap0 heap_leq heap1 heap1_larger by object-alloc-conforms-lemma [TE,heap0/heap0,heap1/heap1,C/C,heapobj,fldvals], heap0_conforms,TE_wf,fields_wf,flds,fldvals,alloc; have (TE,heap1) |- frames0 frames_conform_to FT0 frames0_conform_in_s1 by frames_conform-mono-lemma [TE,heap0/heap0,heap1/heap1,FT0,frames0], frames0_conform,heap1_larger,heap0_conforms,TE_wf; then qed by exp1_types,heap1_larger,frames0_conform_in_s1,heap1_conforms,exp_types; case NewArray exp0 = RNewArray(st,dims0,ext) exp0_ty = SOME(VT(st,dim)) dim = LEN(dims0)+ext 0 < dim dims0_size TE |- st wf_simptype st_wf !j. j < LEN(dims0) --> (!exp1. (EL(j)(dims0),s0) exp_reduce(TE,p) (exp1,s1) --> exp_types (TE,FT0,heap0) (SOME(VT(PrimT(intT),0))) (exp1,s1) | exceptional_exp exp1) & (TE,FT0,heap0) |- (EL(j)(dims0)) rexp_hastype (SOME(VT(PrimT(intT),0))) ihyp ; have !j exp1. j < LEN(dims0) & (EL(j)(dims0),s0) exp_reduce(TE,p) (exp1,s1) --> exp_types (TE,FT0,heap0) (SOME(VT(PrimT(intT),0))) (exp1,s1) | exceptional_exp exp1 ihyp2 by ihyp; // there are different cases, depending on how ground the expressions are, // and whether the ground expressions are +ve integers. let ndims = LEN(dims0) [rw,auto]; let intty = SOME(VT(PrimT(intT),0)) ; per cases case // some dimension is not ground k < ndims dimk0 = EL(k)(dims0) (dimk0,s0) exp_reduce(TE,p) (dimk1,s1) dimk0_reduces dims1 = REPLACE(k)(dims0)(dimk1) exp1 = RNewArray(st,dims1,ext) ; // did dimk0 give an exception? per cases case exceptional_exp(dimk1) ; qed by exceptional,EXISTSL_REPLACE, not exp1_exceptional; // dimk0 reduces conformantly, to something narrower. However, there is no type narrower // than int. case TE |- heap0 heap_leq heap1 heap1_larger FT0 ftyenv_leq FT1 FT1_larger (TE,heap1) |- frames1 frames_conform_to FT1 frames1_conform TE |- heap1 heap_conforms heap1_conforms (TE,FT1,heap1) |- dimk1 rexp_hastype dimk1_ty dimk1_types TE |- dimk1_ty expty_widens_to intty dimk1_narrower; have dimk1_ty = intty by dimk1_narrower,prim-widens-lemma; // all the other dimensions might have narrower types because // of side effects on the state. However, there is no type narrower // than int. have !j. j < ndims --> (TE,FT1,heap1) |- EL(j)(dims1) rexp_hastype intty dims1_type proof then consider j st + j < ndims - (TE,FT1,heap1) |- EL(j)(dims1) rexp_hastype intty; let e = EL(j)(dims1) ; per cases case k = j ; qed by dimk1_types; case k <> j ; have (TE,FT0,heap0) |- e rexp_hastype intty init_typing by ihyp; consider ty2 st (TE,FT1,heap1) |- e rexp_hastype ty2 e_types_in_s1 TE |- ty2 expty_widens_to intty ty2_narrower by exp-mono-lemma [FT0/FT0,TE,FT1/FT1,heap0/heap0,heap1/heap1,e,intty],init_typing,FT1_larger,TE_wf,heap0_conforms,heap1_larger; have ty2 = intty by ty2_narrower,prim-widens-lemma; qed by e_types_in_s1; end; ; have 0 < LEN(dims1)+ext dims1_size by LEN_REPLACE,dims0_size; have (TE,FT1,heap1) |- exp1 rexp_hastype exp0_ty exp1_types by rstatics__NewArray [TE,heap1,FT1,st,dims1], dims1_type,dims1_size,st_wf qed by FT1_larger,frames1_conform,heap1_conforms,exp1_types,heap1_larger,exp_types; end by ihyp2 [k,dimk1],dimk0_reduces,exp_types ; case // all dimensions are ground. The groundedness assumptions are irrelevant, as long as we magically come up with the right number of array dimensions LEN(dimns: nat list) = ndims [rw,auto] // this one isn't val_alloc(heap0,st,dimns,ext) = (val1,heap1) exp1 = RValue(val1) frames0 = frames1 ; // s1 is conformant to FT1 = FT0 by a lengthy argument that at each // stage of the bottom up allocation of an array conformance // is preserved. have TE |- heap1 heap_conforms heap1_conforms TE |- heap0 heap_leq heap1 heap1_larger by array-alloc-conforms-lemma,TE_wf,heap0_conforms; have (TE,FT0,heap1) |- exp1 rexp_hastype exp0_ty exp1_types by array-alloc-types-lemma [ext/ext,dimns,heap0/heap0,heap1/heap1,TE,FT0,st],TE_wf, heap1_conforms,frames0_conform,heap0_conforms; // requires trivial use of arithmetic dproc. or and/or congruence closure have (TE,heap1) |- frames0 frames_conform_to FT0 frames0_conform_in_s1 by frames_conform-mono-lemma [TE,heap0/heap0,heap1/heap1,frames0,FT0], frames0_conform,heap1_larger,heap0_conforms,TE_wf; then qed by exp_types,exp1_types,heap1_larger, frames0_conform_in_s1,heap1_conforms; // the second case is proved end by rule cases on exp0_reduces, not exp1_exceptional, exceptional; 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. exp0 = RCall(obj0,AT,m,args0) exp0_ty = rt0 LEN(args0) = nargs [rw,auto] LEN(AT) = nargs [rw,auto] !exp1. (obj0,s0) exp_reduce(TE,p) (exp1,s1) --> exp_types (TE,FT0,heap0) (SOME(vt0)) (exp1,s1) | exceptional_exp exp1 ihyp_for_obj0 (TE,FT0,heap0) |- obj0 rexp_hastype SOME(vt0) obj0_types_in_s0 MSigs(TE,vt0)(m,MT(AT,rt0)) m_visible_from_vt0 !j. j < nargs --> ?varty. ((!exp1. (EL(j)(args0),s0) exp_reduce(TE,p) (exp1,s1)--> exp_types (TE,FT0,heap0) (SOME(varty)) (exp1,s1) | exceptional_exp exp1) & (TE,FT0,heap0) |- EL(j)(args0) rexp_hastype SOME(varty)) & TE |- varty varty_widens_to EL(j)(AT) ihyp_for_args0 ; // tool failure ? // Extract the simple typing condition from the ihyp (used when the ihyp is // irrelevant and we just want to use the fact that the args0 are well typed) have !j. j < nargs --> ?varty. (TE,FT0,heap0) |- EL(j)(args0) rexp_hastype SOME(varty) & TE |- varty varty_widens_to EL(j)(AT) args0_type_in_s0 by ihyp_for_args0 let obj0_ty = SOME(vt0) ; // now do case analysis on the various combinations of groundedness per cases case (obj0,s0) exp_reduce(TE,p) (obj1,s1) obj0_reduces exp1 = RCall(obj1,AT,m,args0) ; per cases case exceptional_exp(obj1) ; qed by exceptional, not exp1_exceptional; // obj0 reduces conformantly, to something narrower. case TE |- heap0 heap_leq heap1 heap1_larger FT0 ftyenv_leq FT1 FT1_larger (TE,heap1) |- frames1 frames_conform_to FT1 frames1_conform TE |- heap1 heap_conforms heap1_conforms (TE,FT1,heap1) |- obj1 rexp_hastype obj1_ty obj1_types TE |- obj1_ty expty_widens_to obj0_ty obj1_narrower; // now we have to establish the types for the arguments in the new world... // Argument types might narrow because of side effects. sheesh... have !j. j < nargs --> ?varty. (TE,FT1,heap1) |- EL(j)(args0) rexp_hastype SOME(varty) & TE |- varty varty_widens_to EL(j)(AT) args0_type_in_s1 proof hard; qed; ; // unfinished - tedious... // by args0_type_in_s0,exp-mono-lemma,FT1_larger,frames0_conform,frames1_conform; // case analysis on the differnt things C0 might have become consider vt1 st obj1_ty = SOME(vt1) TE |- vt1 varty_widens_to vt0 vt1_narrower by rule cases on obj1_narrower,PEXISTS_SPLIT; 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,AT,rt0/rt0,vt1/vt1,vt0/vt0,m],m_visible_from_vt0,TE_wf,vt1_narrower have (TE,FT1,heap1) |- exp1 rexp_hastype rt1 exp1_types by rstatics__Call [TE,heap1,FT1,obj1,AT,rt1,vt1,m/m], args0_type_in_s1,obj1_types,m_visible_from_vt1; qed by heap1_larger,FT1_larger,frames1_conform,heap1_conforms,exp1_types,rt1_narrower,exp_types; end by ihyp_for_obj0 [obj1],obj0_reduces,exp_types ; case // some dimension is not ground k < nargs argk0 = EL(k)(args0) (argk0,s0) exp_reduce(TE,p) (argk1,s1) argk0_reduces args1 = REPLACE(k)(args0)(argk1) exp1 = RCall(obj0,AT,m,args1) ; // use the induction hypothesis, which gives us a type for argk0 and a // reduction for it as well. (nb. here argk0_ty is a vartype, not an exptype) consider argk0_ty st (TE,FT0,heap0) |- EL(k)(args0) rexp_hastype SOME(argk0_ty) argk0_types TE |- argk0_ty varty_widens_to EL(k)(AT) argk0_narrower_than_arg exp_types (TE,FT0,heap0) (SOME(argk0_ty)) (argk1,s1) | exceptional_exp argk1 argk1_types_or_fails by ihyp_for_args0 [k],argk0_reduces ; // did argk0 give an exception? per cases case exceptional_exp(argk1) ; qed by exceptional, not exp1_exceptional, EXISTSL_REPLACE; // argk0 reduces conformantly, to something narrower. case TE |- heap0 heap_leq heap1 heap1_larger FT0 ftyenv_leq FT1 FT1_larger (TE,heap1) |- frames1 frames_conform_to FT1 frames1_conform TE |- heap1 heap_conforms heap1_conforms (TE,FT1,heap1) |- argk1 rexp_hastype argk1_ty argk1_types TE |- argk1_ty expty_widens_to SOME(argk0_ty) argk1_narrower; // We prove that all the arguments have some type in s1 that is narrower // than their corresponding argument. // // This is easy for the case where j = k, but requires more // work for the other cases. // The other dimensions might have narrower types because // of side effects on the state. have !j. j < nargs --> ?varty. (TE,FT1,heap1) |- EL(j)(args1) rexp_hastype SOME(varty) & TE |- varty varty_widens_to EL(j)(AT) args1_type proof then consider j st + j < nargs - ?varty. (TE,FT1,heap1) |- EL(j)(args1) rexp_hastype SOME(varty) & TE |- varty varty_widens_to EL(j)(AT) ; let e = EL(j)(args1) ; per cases case k = j ; qed by argk1_types, rule cases on argk1_narrower, varty_widens_to-trans [TE,EL(j)(AT)/vt3], argk0_narrower_than_arg,TE_wf; // bug with transitivity rule makes this harder than it should be - now fixed case k <> j ; consider argj0_ty st (TE,FT0,heap0) |- e rexp_hastype SOME(argj0_ty) init_typing TE |- argj0_ty varty_widens_to EL(j)(AT) argj0_narrower_than_arg by args0_type_in_s0; consider argj1_ty st (TE,FT1,heap1) |- e rexp_hastype argj1_ty e_types_in_s1 TE |- argj1_ty expty_widens_to SOME(argj0_ty) ty2_narrower by exp-mono-lemma [TE,heap0/heap0,heap1/heap1,FT0/FT0,FT1/FT1,e,SOME(argj0_ty)], TE_wf,heap0_conforms,init_typing,FT1_larger,heap1_larger; // argj1_ty is a SOME(varty) and not void, because it is narrower than SOME(argj0_ty) consider argj1_vty st argj1_ty = SOME(argj1_vty) TE |- argj1_vty varty_widens_to argj0_ty vty2_narrower by rule cases on ty2_narrower,e_types_in_s1,PEXISTS_SPLIT have TE |- argj1_vty varty_widens_to EL(j)(AT) by varty_widens_to-trans [TE,EL(j)(AT)/vt3,argj1_vty/vt1,argj0_ty/vt2], argj0_narrower_than_arg,vty2_narrower,TE_wf; // meson not working properly for some reason - hence instantiations then qed by e_types_in_s1; end; ; // FIX ME - double semicolon! // Now consider obj0 - it's type might have become narrower due to // side effects consider obj1_ty st (TE,FT1,heap1) |- obj0 rexp_hastype obj1_ty obj0_types_in_s1 TE |- obj1_ty expty_widens_to obj0_ty obj0_narrower by exp-mono-lemma [TE,heap0/heap0,heap1/heap1,FT0/FT0,FT1/FT1], TE_wf,heap0_conforms,obj0_types_in_s0,FT1_larger,heap1_larger; consider vt1 st obj1_ty = SOME(vt1) TE |- vt1 varty_widens_to vt0 vt1_narrower by rule cases on obj0_narrower,PEXISTS_SPLIT; 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,m_visible_from_vt0,TE_wf,vt1_narrower have (TE,FT1,heap1) |- exp1 rexp_hastype rt1 exp1_types by rstatics__Call [TE,heap1,FT1,AT,rt1,obj0,vt1,args1], args1_type,obj0_types_in_s1,m_visible_from_vt1; qed by FT1_larger,frames1_conform,heap1_conforms,exp1_types,rt1_narrower,heap1_larger,exp_types; end by argk1_types_or_fails,exp_types; case // The most interesting case: the object and all arguments are ground. obj0 = RValue(thisval) FPLOOKUP heap0 addr = SOME(heapobj) [rw,auto] MethBody(m,AT,hoType(heapobj),p)(Xord,body) fetch !j. j < nargs --> EL(j)(args0) = RValue(EL(j)(argvals)) [rw,auto] LEN(argvals) = nargs [rw,auto] fidx = sNextFrame(frames0) [rw,auto] rbody = mk_rbody fidx body [rw,auto] gframe1 = { (x,z) | ?j. j < LEN(Xord) & x = EL(j)(Xord) & z = EL(j)(argvals) } [rw,auto] thisval = RAddr(SOME(addr)) [rw,auto] frames1 = sAddFrame(frames0,PGRAPH gframe1 <+ (this, thisval) ) [rw,auto] exp1 = RBody(rbody) [rw,auto] heap0 = heap1 [rw,auto]; // Crun is the runtime type of the object being accessed // C0 is the type of the address as given by the type system, which we prove to be the same as C have LEN(FT0) = LEN(frames0) [rw,auto] by FRAMES_CONFORM_TO,frames0_conform; // by typing the cell is either an object or an array have (TE,heap0) |- RAddr(SOME(addr)) rval_hastype vt0 addr_types by rule cases on obj0_types_in_s0; // Get the method body from the original program. // We know it is well-typed in the original source language. consider Xtys,mbody,Cmeth,thisty st vt0 = hoType(heapobj) thisty = VT(Class(Cmeth),0) TE |- vt0 varty_widens_to thisty this_fits (Cmeth,TE) |- mbody cmethod_hastype MT(AT,rt0) mbody_types mbody = ((Xord,Xtys),body) by fetch, implemented-inheritance-is-welltyped [TE,p,AT,rt0,body,Xord], TE_wf,p_types,m_visible_from_vt0,rule cases on addr_types,hoType,PEXISTS_SPLIT; // Look at the details of the method body. // Nb. The return type can narrow. consider rt1,VE st ELS(Xord) = PDOM(Xtys) ORDERING(Xord) VE = Xtys <+ (this, thisty) (TE,VE) |- body cbody_hastype rt1 body_types TE |- rt1 expty_widens_to rt0 exp1_narrower AT = MAP(PAPPLY(Xtys))(Xord) by rule cases on mbody_types; // this is the typing for the frame of variables. let FT1 = FT0 ×! VE ; have FT0 ftyenv_leq FT1 FT1_larger by ftyenv_leq; // now show that all the arguments are actually well-typed values have !j. j < nargs --> ?varty. (TE,heap0) |- EL(j)(argvals) rval_hastype varty & TE |- varty varty_widens_to EL(j)(AT) args_fit proof then consider j st + j < nargs - ?varty. (TE,heap0) |- EL(j)(argvals) rval_hastype varty & TE |- varty varty_widens_to EL(j)(AT) g; consider varty st (TE,FT0,heap0) |- EL(j)(args0) rexp_hastype SOME(varty) t1 TE |- varty varty_widens_to EL(j)(AT) t2 by args0_type_in_s0 qed by rule cases on t1,t2,g [varty]; ; // now use the lemma that the new set of frames conform have (TE,heap0) |- frames1 frames_conform_to FT1 frames1_conform by frame-allocation-lemma [TE,argvals,AT,frames1/frames1,frames0/frames0,Xtys,Xord,FT0/FT0,FT1/FT1,thisval/thisval,thisty/thisty,vt0/objty,heap0], frames0_conform,heap0_conforms,TE_wf,args_fit,this_fits,addr_types; // now show that the the types in FT match the types in VE have fidx < LEN(FT1) good_fidx by sNextFrame; have !id. PLOOKUP(EL(fidx)(FT1))(id) = PLOOKUP(VE)(id) good_VE by sNextFrame; // now invoke the lemma that says that translated methods start off // well-typed in the runtime world. have (TE,FT1,heap0) |- exp1 rexp_hastype rt1 exp1_types by good_VE,good_fidx, mk_body-preserves-types [FT1,TE,VE,heap0,body,rt1,fidx], body_types,TE_wf; qed by exp1_types,exp1_narrower,frames1_conform,heap0_conforms,FT1_larger,exp_types; end by hard rule cases on exp0_reduces, not exp1_exceptional, exceptional; // too hard for naive meson!! case Body exp0 = RBody(rstmt0,rexp0) !stmtB. (rstmt0,s0) stmt_reduce(TE,p) (stmtB,s1) --> stmt_types (TE,FT0,heap0) (stmtB,s1) | exceptional_stmt stmtB ihyp_for_rstmt0 (TE,FT0,heap0) |- rstmt0 rstmt_hastype rstmt0_types !exp1. (rexp0,s0) exp_reduce(TE,p) (exp1,s1) --> exp_types (TE,FT0,heap0) exp0_ty (exp1,s1) | exceptional_exp exp1 ihyp_for_rexp0 (TE,FT0,heap0) |- rexp0 rexp_hastype exp0_ty rexp0_types_in_s0; per cases case (rstmt0,s0) stmt_reduce(TE,p) (rstmtB,s1) rstmt0_reduces exp1 = RBody(rstmtB,rexp0) ; // did rstmt0 give an exception? per cases case exceptional_stmt(rstmtB) ; qed by exceptional, not exp1_exceptional; // rstmt0 reduces conformantly, to some narrower stmt. case TE |- heap0 heap_leq heap1 heap1_larger FT0 ftyenv_leq FT1 FT1_larger (TE,heap1) |- frames1 frames_conform_to FT1 frames1_conform TE |- heap1 heap_conforms heap1_conforms (TE,FT1,heap1) |- rstmtB rstmt_hastype rstmtB_ty; // rexp0 might have a narrower type because // of side effects on the state. However, there is no type narrower // than int. consider rexp1_ty st (TE,FT1,heap1) |- rexp0 rexp_hastype rexp1_ty rexp0_types_in_s1 TE |- rexp1_ty expty_widens_to exp0_ty rexp1_narrower by exp-mono-lemma,TE_wf,heap0_conforms,rexp0_types_in_s0, FT1_larger,heap1_larger; have (TE,FT1,heap1) |- exp1 rexp_hastype rexp1_ty exp1_types by rstatics__Body,rstmtB_ty,rexp0_types_in_s1; qed by FT1_larger,frames1_conform,heap1_conforms,exp1_types,rexp1_narrower,heap1_larger,exp_types; end by ihyp_for_rstmt0 [rstmtB],rstmt0_reduces,stmt_types ; case exp1 = rexp0 s1 = s0 ; qed by frames0_conform,heap0_conforms,rexp0_types_in_s0,exp_types; end by rule cases on exp0_reduces; // ASSIGNMENTS // Note that addr := val is not well typed. case AssignToStackVar stmt0 = RAssign(RStackVar(fidx,id),rexp0) !exp1. (rexp0,s0) exp_reduce(TE,p) (exp1,s1) --> exp_types (TE,FT0,heap0) (SOME(rexp0_vty)) (exp1,s1) | exceptional_exp exp1 ihyp_for_rexp0 (TE,FT0,heap0) |- rexp0 rexp_hastype SOME(rexp0_vty) rexp0_types !var1. (RStackVar(fidx,id),s0) var_reduce(TE,p) (var1,s1) --> var_types (TE,FT0,heap0) (RStackVar(fidx,id)) lval0_ty (var1,s1) | exceptional_var var1 unused (TE,FT0,heap0) |- RStackVar(fidx,id) rvar_hastype lval0_ty lval0_types_in_s0 TE |- rexp0_vty varty_widens_to lval0_ty rexp0_fits; let lval0 = RStackVar(fidx,id) ; per cases case (lval0,s0) var_reduce(TE,p) (lval1,s1) lval0_reduces stmtB = RAssign(lval1,rexp0) ; contradiction by rule cases on lval0_reduces; case (rexp0,s0) exp_reduce(TE,p) (rexp1,s1) rexp0_reduces stmtB = RAssign(lval0,rexp1) ; per cases case exceptional_exp(rexp1) ; qed by exceptional, not stmtB_exceptional; // rexp0 reduces conformantly, to something narrower. case TE |- heap0 heap_leq heap1 heap1_larger FT0 ftyenv_leq FT1 FT1_larger (TE,heap1) |- frames1 frames_conform_to FT1 frames1_conform TE |- heap1 heap_conforms heap1_conforms (TE,FT1,heap1) |- rexp1 rexp_hastype rexp1_ty rexp1_types TE |- rexp1_ty expty_widens_to SOME(rexp0_vty) rexp1_narrower; consider rexp1_vty st rexp1_ty = SOME(rexp1_vty) by rule cases on rexp1_narrower,PEXISTS_SPLIT; have TE |- rexp1_vty varty_widens_to lval0_ty rexp1_fits by varty_widens_to-trans,rule cases on rexp1_narrower,rexp0_fits,TE_wf; // types of stack variables do not alter in conformant states have (TE,FT1,heap1) |- lval0 rvar_hastype lval0_ty lval0_types_in_s1 by StackVar-mono [TE,FT0/FT0,FT1/FT1,heap0/heap0,heap1/heap1,lval0_ty],lval0_types_in_s0, FT1_larger,frames1_conform,heap1_conforms, frames0_conform,heap0_conforms,TE_wf,heap1_larger; have (TE,FT1,heap1) |- stmtB rstmt_hastype stmtB_types by rstatics__AssignToStackVar,lval0_types_in_s1,rexp1_types,rexp1_fits; qed by FT1_larger,frames1_conform,heap1_conforms,stmtB_types,heap1_larger,stmt_types; end by ihyp_for_rexp0 [rexp1],rexp0_reduces,exp_types; case rexp0 = RValue(val) frames1 = sSetStackVar(frames0,fidx,id,val) stmtB = RExpr(RVoid) heap0 = heap1 ; consider FS st fidx < LEN(FT0) EL(fidx)(FT0) = FS FS id = SOME(lval0_ty) by rule cases on lval0_types_in_s0; have (TE,heap0) |- frames1 frames_conform_to FT0 frames1_conform by stack-assign-conforms-lemma [val,id,fidx,lval0_ty/vty,rexp0_vty/ety,heap0/heap,frames0/frames0,frames1/frames1],frames0_conform,rexp0_fits,rexp0_types,TE_wf; have (TE,FT0,heap1) |- stmtB rstmt_hastype by rstatics__Expr [NONE:varType option],rstatics__Void; then qed by frames1_conform,heap0_conforms,stmt_types; end by rule cases on stmt0_reduces; case AssignToField stmt0 = RAssign(RField(obj0,C,fld),rexp0) !exp1. (rexp0,s0) exp_reduce(TE,p) (exp1,s1) --> exp_types (TE,FT0,heap0) (SOME(rexp0_vty)) (exp1,s1) | exceptional_exp exp1 ihyp_for_rexp0 (TE,FT0,heap0) |- rexp0 rexp_hastype SOME(rexp0_vty) rexp0_types_in_s0 !var1. (RField(obj0,C,fld),s0) var_reduce(TE,p) (var1,s1) --> var_types (TE,FT0,heap0) (RField(obj0,C,fld)) lval0_ty (var1,s1) | exceptional_var var1 ihyp_for_lval0 (TE,FT0,heap0) |- RField(obj0,C,fld) rvar_hastype lval0_ty lval0_types_in_s0 TE |- rexp0_vty varty_widens_to lval0_ty rexp0_fits; let lval0 = RField(obj0,C,fld) ; per cases case (lval0,s0) var_reduce(TE,p) (lval1,s1) lval0_reduces stmtB = RAssign(lval1,rexp0) ; per cases case exceptional_var(lval1) ; qed by exceptional, not stmtB_exceptional; // lval0 reduces conformantly, to something of the *same* type (this is part of the induction invariant) case TE |- heap0 heap_leq heap1 heap1_larger FT0 ftyenv_leq FT1 FT1_larger (TE,heap1) |- frames1 frames_conform_to FT1 frames1_conform TE |- heap1 heap_conforms heap1_conforms (TE,FT1,heap1) |- lval1 rvar_hastype lval0_ty lval1_types lval1 = RField(obj1,C,fld) ; consider rexp1_ty st (TE,FT1,heap1) |- rexp0 rexp_hastype rexp1_ty rexp0_types_in_s1 TE |- rexp1_ty expty_widens_to (SOME(rexp0_vty)) rexp1_narrower by exp-mono-lemma [FT0/FT0,FT1/FT1,TE,rexp0], rexp0_types_in_s0, TE_wf,heap0_conforms,FT1_larger,heap1_larger; consider rexp1_vty st rexp1_ty = SOME(rexp1_vty) by rule cases on rexp1_narrower,PEXISTS_SPLIT; have TE |- rexp1_vty varty_widens_to lval0_ty rexp1_fits by varty_widens_to-trans,rule cases on rexp1_narrower,rexp0_fits,TE_wf; have (TE,FT1,heap1) |- stmtB rstmt_hastype stmtB_types by rstatics__AssignToField,rexp0_types_in_s1,lval1_types,rexp1_fits; qed by FT1_larger,frames1_conform,heap1_conforms,stmtB_types,heap1_larger,stmt_types; end by ihyp_for_lval0 [lval1],lval0_reduces,var_types ; case (rexp0,s0) exp_reduce(TE,p) (rexp1,s1) rexp0_reduces stmtB = RAssign(lval0,rexp1) ; per cases case exceptional_exp(rexp1) ; qed by exceptional, not stmtB_exceptional; // rexp0 reduces conformantly, to something narrower. case TE |- heap0 heap_leq heap1 heap1_larger FT0 ftyenv_leq FT1 FT1_larger (TE,heap1) |- frames1 frames_conform_to FT1 frames1_conform TE |- heap1 heap_conforms heap1_conforms (TE,FT1,heap1) |- rexp1 rexp_hastype rexp1_ty rexp1_types TE |- rexp1_ty expty_widens_to SOME(rexp0_vty) rexp1_narrower; consider rexp1_vty st rexp1_ty = SOME(rexp1_vty) by rule cases on rexp1_narrower,PEXISTS_SPLIT; have TE |- rexp1_vty varty_widens_to lval0_ty rexp1_fits by varty_widens_to-trans,rule cases on rexp1_narrower,rexp0_fits,TE_wf; // types of fields do not alter in conformant states have (TE,FT1,heap1) |- lval0 rvar_hastype lval0_ty lval0_types_in_s1 by Field-mono [TE,FT0/FT0,FT1/FT1,heap0/heap0,heap1/heap1],lval0_types_in_s0, FT1_larger,heap1_larger,heap1_conforms,heap0_conforms; have (TE,FT1,heap1) |- stmtB rstmt_hastype stmtB_types by rstatics__AssignToField,lval0_types_in_s1,rexp1_types,rexp1_fits,TE_wf; qed by FT1_larger,frames1_conform,heap1_conforms,stmtB_types,heap1_larger,stmt_types; end by ihyp_for_rexp0 [rexp1],rexp0_reduces,exp_types ; case obj0 = RValue(RAddr(SOME(addr))) rexp0 = RValue(val) heap1 = sFieldSet(heap0,addr,C,fld,val) stmtB = RExpr(RVoid) frames1 = frames0 ; consider Caddr st (TE,FT0,heap0) |- obj0 rexp_hastype SOME(VT(Class(Caddr),0)) obj0_types ((C,fld),lval0_ty) :: FDecs(TE,Caddr) field_types by rule cases on lval0_types_in_s0; // C' is the runtime type of the object being accessed, as found in the state // Caddr is the type of the address as given by the type system, which we prove to be the same as C have (TE,heap0) |- RAddr(SOME(addr)) rval_hastype VT(Class(Caddr),0) addr_types by rule cases on obj0_types; consider fldvals st FPLOOKUP heap0 addr = SOME(OBJECT(fldvals,Caddr)) old_lookup by rule cases on addr_types; have (TE,heap0) |- val rval_hastype rexp0_vty val_types by rule cases on rexp0_types_in_s0; have TE |- heap1 heap_conforms heap1_conforms TE |- heap0 heap_leq heap1 heap1_larger by field-assign-conforms-lemma [fldvals,lval0_ty/vty,rexp0_vty/ety, Caddr/C',heap0/heap0,heap1/heap1,TE,val,addr,C/C], heap0_conforms, rexp0_fits,val_types,TE_wf, old_lookup,field_types; have (TE,heap1) |- frames0 frames_conform_to FT0 frames0_conform_in_s1 by frames_conform-mono-lemma [TE,heap0/heap0,heap1/heap1],TE_wf,frames0_conform,heap1_larger,heap0_conforms; have (TE,FT0,heap1) |- stmtB rstmt_hastype by rstatics__Expr [NONE:varType option],rstatics__Void; then qed by heap1_larger,frames0_conform_in_s1,heap1_conforms,stmt_types; end by rule cases on stmt0_reduces, not stmtB_exceptional, exceptional; case AssignToArray stmt0 = RAssign(RAccess(arr0,idx0),rexp0) !exp1. (rexp0,s0) exp_reduce(TE,p) (exp1,s1) --> exp_types (TE,FT0,heap0) rexp0_ty (exp1,s1) | exceptional_exp exp1 ihyp_for_rexp0 (TE,FT0,heap0) |- rexp0 rexp_hastype rexp0_ty rexp0_types_in_s0 !var1. (RAccess(arr0,idx0),s0) var_reduce(TE,p) (var1,s1) --> var_types (TE,FT0,heap0) (RAccess(arr0,idx0)) lval0_ty (var1,s1) | exceptional_var var1 ihyp_for_lval0 (TE,FT0,heap0) |- RAccess(arr0,idx0) rvar_hastype lval0_ty lval0_types_in_s0; let lval0 = RAccess(arr0,idx0) ; per cases case (lval0,s0) var_reduce(TE,p) (lval1,s1) lval0_reduces stmtB = RAssign(lval1,rexp0) ; per cases case exceptional_var(lval1) ; qed by exceptional, not stmtB_exceptional; // lval0 reduces conformantly, to something narrower (all praise be to for runtime type checking) case TE |- heap0 heap_leq heap1 heap1_larger FT0 ftyenv_leq FT1 FT1_larger (TE,heap1) |- frames1 frames_conform_to FT1 frames1_conform TE |- heap1 heap_conforms heap1_conforms (TE,FT1,heap1) |- lval1 rvar_hastype lval1_ty lval1_types lval1 = RAccess(arr1,idx1) ; // rexp1 also gets narrower (but narrowness doesn't matter for array assignments) consider rexp1_ty st (TE,FT1,heap1) |- rexp0 rexp_hastype rexp1_ty rexp0_types_in_s1 by exp-mono-lemma [heap0/heap0,heap1/heap1,FT0/FT0,FT1/FT1,TE,rexp0], rexp0_types_in_s0, TE_wf,heap0_conforms,FT1_larger,heap1_larger; have (TE,FT1,heap1) |- stmtB rstmt_hastype stmtB_types by rstatics__AssignToArray [rexp1_ty/ety, lval1_ty/varty],rexp0_types_in_s1,lval1_types; qed by FT1_larger,frames1_conform,heap1_conforms,stmtB_types,heap1_larger,stmt_types; end by ihyp_for_lval0 [lval1],lval0_reduces,var_types; case (rexp0,s0) exp_reduce(TE,p) (rexp1,s1) rexp0_reduces stmtB = RAssign(lval0,rexp1) ; per cases case exceptional_exp(rexp1) ; qed by exceptional, not stmtB_exceptional; // rexp0 reduces conformantly (no need to worry about narrowing for array assignments, except to ensure rexp1 does not become void!) case TE |- heap0 heap_leq heap1 heap1_larger FT0 ftyenv_leq FT1 FT1_larger (TE,heap1) |- frames1 frames_conform_to FT1 frames1_conform TE |- heap1 heap_conforms heap1_conforms (TE,FT1,heap1) |- rexp1 rexp_hastype rexp1_ty rexp1_types TE |- rexp1_ty expty_widens_to rexp0_ty rexp1_narrower; consider lval1_ty st (TE,FT1,heap1) |- lval0 rvar_hastype lval1_ty lval0_types_in_s1 by var-mono-lemma [heap0/heap0,heap1/heap1,FT0/FT0,FT1/FT1,TE,lval0], lval0_types_in_s0, FT1_larger,heap1_larger,heap0_conforms,TE_wf; have (TE,FT1,heap1) |- stmtB rstmt_hastype stmtB_types by rstatics__AssignToArray,lval0_types_in_s1,rexp1_types,TE_wf; qed by FT1_larger,frames1_conform,heap1_conforms,stmtB_types,heap1_larger,stmt_types; end by ihyp_for_rexp0 [rexp1],rexp0_reduces,exp_types; case arr0 = RValue(RAddr(SOME(taddr))) idx0 = RValue(RPrim(Int(k32))) rexp0 = RValue(val) FPLOOKUP heap0 taddr = cell cell cell = SOME(ARRAY(arrty,vec)) lookup dest_int32(k32) >>= 0 idx = int_to_nat(dest_int32(k32)) idx < LEN(vec) typecheck((TE,heap0),val,arrty) val_fits heap1 = heap0 <++ (taddr,ARRAY(arrty,REPLACE(idx)(vec)(val))) stmtB = RExpr(RVoid) frames1 = frames0 ; consider simpty,dim,ndim st (TE,FT0,heap0) |- arr0 rexp_hastype SOME(VT(simpty,dim)) arr0_types 0 < dim (TE,FT0,heap0) |- idx0 rexp_hastype SOME(VT(PrimT(intT),0)) idx0_types ndim = dim-1 lval0_ty = VT(simpty,ndim) by rule cases on lval0_types_in_s0; // prove that the type of the expression correlates with the type of the // vector in the state. Not very hard have (TE,heap0) |- RAddr(SOME(taddr)) rval_hastype VT(simpty,dim) taddr_types by rule cases on arr0_types; consider dim',vec' st dim = dim'+1 cell = SOME(ARRAY(VT(simpty,dim'),vec')) by rule cases on taddr_types,cell; then have arrty = VT(simpty,dim') vec = vec' by lookup; // why is s1 conformant? // - have to show new object at taddr conforms // - i.e. this is true because sval weakly conforms to tvt // slightly tricky: sval w.c. in s0, not. // The problem might be at the conflicting address taddr when // sval = RAddr(SOME(taddr)). However, weak conformance does // not depend on the values at taddr, just the *type* at taddr, // which is still tvt in. Thus sval is still conformant at. consider rexp0_vty st rexp0_ty = SOME(rexp0_vty) (TE,heap0) |- val rval_hastype rexp0_vty val_types by rule cases on rexp0_types_in_s0,PEXISTS_SPLIT; have TE |- heap1 heap_conforms heap1_conforms TE |- heap0 heap_leq heap1 heap1_larger by array-assign-conforms-lemma [TE,arrty/arrty,rexp0_vty/ety,heap1/heap1,heap0/heap0,val,i |