subred.aux.art
notation syntax rsyntax rels runtime rstatics conforms ; import syntax rsyntax runtime0 wf wfenv rstatics1 statics1 rsubst cstatics subred.aux conforms ;// Frame allocation preserves conformance, if all the conditions are right...
proof of // frame-allocation-lemma if TE wf_tyenv TE_wf !j. j < LEN(argvals) --> ?varty. (TE,heap) |- EL(j)(argvals) rval_hastype varty & TE |- varty varty_widens_to EL(j)(AT) args_fit (TE,heap) |- thisval rval_hastype objty addr_types TE |- objty varty_widens_to thisty this_fits frames1 = sAddFrame(frames0,frame1) frame1 = PGRAPH gframe1 <+ (this, thisval) gframe1 = { (x,z) | ?j. j < LEN(Xord) & x = EL(j)(Xord) & z = EL(j)(argvals) } gframe1 LEN(Xord) = LEN(argvals) [elim,auto] TE |- heap heap_conforms heap_conforms (TE,heap) |- frames0 frames_conform_to FT0 frames0_conform FT1 = FT0 ×! (Xtys <+ (this, thisty)) AT = MAP(PAPPLY(Xtys))(Xord) AT ELS(Xord) = PDOM(Xtys) no_repeats ORDERING(Xord) ordered_args then (TE,heap) |- frames1 frames_conform_to FT1 g; have IS_GRAPH gframe1 graph_frame1 by GRAPH_FROM_LISTS [Xord/l1,argvals/l2],gframe1,ordered_args; have (TE,heap) |- thisval val_conforms_to thisty this_fits2 by conforms-from-typing [TE,heap,thisval], val_conforms-trans [TE,heap,thisval], this_fits,heap_conforms,TE_wf,addr_types; have !j. j < LEN(argvals) --> (TE,heap) |- EL(j)(argvals) val_conforms_to EL(j)(AT) args_fit2 by conforms-from-typing [TE,heap], val_conforms-trans [TE,heap], args_fit,heap_conforms,TE_wf; // needs unification up to records/tuples given our aggressive untupling of quantifiers have LEN(frames0) = LEN(FT0) [rw,auto] by FRAMES_CONFORM_TO,frames0_conform; have LEN(frames1) = LEN(FT1) by sAddFrame; then consider fidx,FS,id,vt st + fidx < LEN(frames1) fidx + FS = EL(fidx)(FT1) + id :: PDOM(FS) id_in_FS + PLOOKUP(FS)(id) = SOME(vt) [rw,auto] - ?val. sGetStackVar(frames1,fidx,id) = SOME(val) & (TE,heap) |- val val_conforms_to vt g2 by FRAMES_CONFORM_TO,g; per cases case fidx = LEN(frames0) ; have FS = Xtys <+ (this, thisty) ; consider j st j < LEN(Xord) id <> this id = EL(j)(Xord) by ELS_ELIM,FUN_EQ,IN_ELIM,id_in_FS,no_repeats,GSPEC_ELIM, sGetStackVar,sAddFrame,this_fits2,g2 [thisval]; have (id,EL(j)(argvals)) :: gframe1 [auto,rw] by gframe1; have frame1 id = SOME(EL(j)(argvals)) [auto,rw] by IN_ELIM,PGRAPH_SOME [gframe1/R],graph_frame1; have PAPPLY(FS)(id) = vt [auto,rw] by PAPPLY_ELIM; qed by g2 [EL(j)(argvals)],args_fit2 [j],sGetStackVar,sAddFrame,AT,PAPPLY_ELIM; case fidx < LEN(frames0) ; qed by FRAMES_CONFORM_TO__stackvar [frames0,TE,heap,FT0,fidx,id,vt], frames0_conform,sGetStackVar,sAddFrame,id_in_FS; end by BOUNDED_CASES [fidx/m,LEN(frames0)/n],fidx,sAddFrame;
// Prove that translating from compiled source expressions preserves types // // One of those cool proofs where simplification and meson do all the work. // (Actually the last two cases are not proved automatically, though // they almost are! I've left them as future challenges as they are // good examples of how mixing equality reasoning and first order reasoning // is kind of difficult.)
proof of // mk_exp-preserves-types if TE wf_tyenv TE_wf fidx < LEN(FT:ftyenv) fidx_OK !id. PLOOKUP(EL(fidx)(FT))(id) = PLOOKUP(VE)(id) wf_FT then { if (TE,VE) |- var cvar_hastype var_ty var_types then (TE,FT,heap) |- (mk_rvar fidx var) rvar_hastype var_ty } and { if (TE,VE) |- exp cexp_hastype exp_ty exp_types then (TE,FT,heap) |- (mk_rexp fidx exp) rexp_hastype exp_ty }; proceed by rule induction on var_types with var,var_ty variable, exp_types with exp,exp_ty variable; case Id; qed by fidx_OK,wf_FT,rstatics__StackVar [TE],PDOM,IN_ELIM,mk_rexp; case Access; then qed by mk_rexp,rstatics__Access [TE,FT]; case FieldA; then qed by mk_rexp,rstatics__Field [TE,FT]; case Var; then qed by mk_rexp,rstatics__Var [TE,FT]; case Void; then qed by mk_rexp,rstatics__Void [TE,FT]; case Prim; then qed by mk_rexp,rval_hastype__Prim,rstatics__Value [TE,FT]; case NewClassA; then qed by mk_rexp,rstatics__NewClass [TE,FT,heap]; case NewArray; then qed by hard mk_rexp,rstatics__NewArray [TE,FT,heap],ALL_ELIM; // both of these fail - good examples of how equality reasoning and first order are hard to mix. Work on this case CallA; then qed by hard mk_rexp,rstatics__Call [TE,FT,heap],ALL_ELIM; // both of these fail - good examples of how equality reasoning and first order are hard to mix. Work on this end;
// And the same for statements...
proof of // mk_stmt-preserves-types if TE wf_tyenv fidx < LEN(FT:ftyenv) !id. PLOOKUP(EL(fidx)(FT))(id) = PLOOKUP(VE)(id) (TE,VE) |- stmt cstmt_hastype stmt_types then (TE,FT,heap) |- (mk_rstmt fidx stmt) rstmt_hastype; proceed by rule induction on stmt_types with stmt variable; case Assign stmt = AssignA(l,r) (TE,VE) |- l cvar_hastype lty l_types (TE,VE) |- r cexp_hastype SOME(rty) TE |- rty varty_widens_to lty; then qed by structural cases on l,mk_rexp, rstatics__AssignToField [TE,FT,heap], rstatics__AssignToArray [TE,FT,heap], rstatics__AssignToStackVar [TE,FT,heap], mk_exp-preserves-types [TE,FT,VE,heap,fidx,r], mk_var-preserves-types [TE,FT,VE,heap,fidx,l]; case If; then qed by mk_rexp,rstatics__If [TE,FT,heap],mk_exp-preserves-types [TE,FT,VE,heap,fidx]; case Block stmt = BlockA(stmts) !j. j < LEN stmts --> (TE,FT,heap) |- mk_rstmt fidx (EL j stmts) rstmt_hastype & (TE,VE) |- EL j stmts cstmt_hastype; then qed by mk_rexp,rstatics__Block [TE,FT,heap,MAP (mk_rstmt fidx) stmts],ALL_ELIM; case Expr; then qed by mk_rexp,rstatics__Expr [TE,FT,heap],mk_exp-preserves-types [TE,FT,VE,heap,fidx]; end;
// And thus the same for method bodies...
proof of // mk_body-preserves-types if TE wf_tyenv fidx < LEN(FT:ftyenv) !id. PLOOKUP(EL(fidx)(FT))(id) = PLOOKUP(VE)(id) (TE,VE) |- body cbody_hastype rt body_types then (TE,FT,heap) |- RBody(mk_rbody fidx body) rexp_hastype rt; qed by rule cases on body_types,mk_rbody, rstatics__Body [TE,FT], mk_exp-preserves-types [TE,FT,VE,heap,fidx], mk_stmt-preserves-types [TE,FT,VE,heap,fidx];
