Module simple_imp:host /*Expressions*/ e ::= num(int) | plus(e, e) | name(string) | greater(e, e) | eq(e, e) | and(e, e) | or(e, e) | true | false | recBuild(recFieldExprs) | recFieldAccess(e, string) Projection e : recFieldExprs ::= endRecFieldExprs | addRecFieldExprs(string, e, recFieldExprs) Projection recFieldExprs : /*Statement Commands*/ c ::= noop | seq(c, c) | declare(string, ty, e) | assign(string, e) | ifThenElse(e, c, c) | while(e, c) | recUpdate(string, recFields, e) /*rec.field = e*/ Projection c : recFields ::= oneField(string) | addField(string, recFields) Projection recFields : /*Types*/ ty ::= intTy | boolTy | recTy([(string, ty)]) Projection ty : /*Evaluation Values*/ value ::= intVal(int) | trueVal | falseVal | recVal([(string, value)]) Projection value :
Module simple_imp:host Judgment vars : e* [string] Judgment vars_rf : recFieldExprs* [string] /*Vars in Expressions*/ -------------- [V-Num] vars num(I) [] vars E1 D1 vars E2 D2 D1 ++ D2 = D ------------------- [V-Plus] vars plus(E1, E2) D ---------------- [V-Name] vars name(X) [X] vars E1 D1 vars E2 D2 D1 ++ D2 = D ---------------------- [V-Greater] vars greater(E1, E2) D vars E1 D1 vars E2 D2 D1 ++ D2 = D ------------------- [V-Eq] vars eq(E1, E2) D vars E1 D1 vars E2 D2 D1 ++ D2 = D ------------------- [V-And] vars and(E1, E2) D vars E1 D1 vars E2 D2 D1 ++ D2 = D ------------------- [V-Or] vars or(E1, E2) D ------------ [V-True] vars true [] ------------- [V-False] vars false [] vars_rf Fields D ----------------------- [V-RecBuild] vars recBuild(Fields) D vars Rec D --------------------------------- [V-RecAccess] vars recFieldAccess(Rec, Field) D /*Vars in Record Fields*/ --------------------------- [VRF-Empty] vars_rf endRecFieldExprs [] vars_rf Rest DRest vars E DE DE ++ DRest = D -------------------------------------- [VRF-Add] vars_rf addRecFieldExprs(X, E, Rest) D
Module simple_imp:host Judgment typeOf : [(string, ty)] e* ty Judgment typeRecFields : [(string, ty)] recFieldExprs* [(string, ty)] Judgment typeOK : [(string, ty)] c* [(string, ty)] /*Expression Typing*/ --------------------- [T-Num] typeOf G num(I) intTy typeOf G E1 intTy typeOf G E2 intTy --------------------------- [T-Plus] typeOf G plus(E1, E2) intTy lookup G X Ty ------------------- [T-Name] typeOf G name(X) Ty typeOf G E1 intTy typeOf G E2 intTy ------------------------------- [T-Greater] typeOf G greater(E1, E2) boolTy typeOf G E1 Ty typeOf G E2 Ty -------------------------- [T-Eq] typeOf G eq(E1, E2) boolTy typeOf G E1 boolTy typeOf G E2 boolTy --------------------------- [T-And] typeOf G and(E1, E2) boolTy typeOf G E1 boolTy typeOf G E2 boolTy -------------------------- [T-Or] typeOf G or(E1, E2) boolTy -------------------- [T-True] typeOf G true boolTy --------------------- [T-False] typeOf G false boolTy typeRecFields G Fields FTys ------------------------------------- [T-RecBuild] typeOf G recBuild(Fields) recTy(FTys) typeOf G Rec recTy(Fields) lookup Fields Field FTy --------------------------------------- [T-RecField] typeOf G recFieldAccess(Rec, Field) FTy /*Record Field Typing*/ ----------------------------------- [TRF-End] typeRecFields G endRecFieldExprs [] typeOf G E Ty typeRecFields G Rest FTys no_lookup FTys L /*each label only occurs once*/ ---------------------------------------------------------- [TRF-Add] typeRecFields G addRecFieldExprs(L, E, Rest) (L, Ty)::FTys /*Statement Typing*/ --------------- [T-Noop] typeOK G noop G typeOK G C1 G1 typeOK G1 C2 G2 ----------------------- [T-Seq] typeOK G seq(C1, C2) G2 no_lookup G X /*can't overwrite existing decls*/ typeOf G E Ty ------------------------------------- [T-Declare] typeOK G declare(X, Ty, E) (X, Ty)::G typeOf G E Ty lookup G X Ty ----------------------- [T-Assign] typeOK G assign(X, E) G typeOf G Cond boolTy typeOK G Then GT typeOK G Else GE --------------------------------------- [T-IfThenElse] typeOK G ifThenElse(Cond, Then, Else) G /*branches open new scopes*/ typeOf G Cond boolTy typeOK G Body GB ---------------------------- [T-While] typeOK G while(Cond, Body) G /*body opens a new scope*/ lookup G Rec recTy(FFields) checkRecUpdate Fields FFields Ty typeOf G E Ty ------------------------------------ [T-RecUpdate] typeOK G recUpdate(Rec, Fields, E) G /*Check whether the update to the nested fields is valid The tyctx is the fields of the record*/ Judgment checkRecUpdate : recFields* [(string, ty)] ty lookup RecFieldTys F Ty ----------------------------------------- [CRU-OneField] checkRecUpdate oneField(F) RecFieldTys Ty lookup RecFieldTys F recTy(FFieldTys) checkRecUpdate Rest FFieldTys Ty ----------------------------------------------- [CRU-AddField] checkRecUpdate addField(F, Rest) RecFieldTys Ty /*Typing for values to allow type soundness*/ Judgment typeOfVal : value* ty ------------------------- [TV-Int] typeOfVal intVal(I) intTy ------------------------ [TV-True] typeOfVal trueVal boolTy ------------------------- [TV-False] typeOfVal falseVal boolTy typeOfEvalctx Fields FTys ------------------------------------ [TV-Rec] typeOfVal recVal(Fields) recTy(FTys) /*Typing for evaluation contexts to allow type soundness and recVal typing*/ Fixed Judgment typeOfEvalctx : [(string, value)] [(string, ty)] =================== [TEC-Empty] typeOfEvalctx [] [] typeOfVal V Ty typeOfEvalctx Rest RestTys =========================================== [TEC-Add] typeOfEvalctx (X, V)::Rest (X, Ty)::RestTys
Module simple_imp:host Judgment eval_e : [(string, value)] e* value Judgment eval_rf : [(string, value)] recFieldExprs* [(string, value)] Judgment eval_c : [(string, value)] c* [(string, value)] /*Expression Evaluation*/ ------------------------- [E-Num] eval_e G num(I) intVal(I) eval_e G E1 intVal(I1) eval_e G E2 intVal(I2) I1 + I2 = I ------------------------------- [E-Plus] eval_e G plus(E1, E2) intVal(I) lookup G X V ------------------ [E-Name] eval_e G name(X) V eval_e G E1 intVal(I1) eval_e G E2 intVal(I2) I1 > I2 -------------------------------- [E-GreaterTrue] eval_e G greater(E1, E2) trueVal eval_e G E1 intVal(I1) eval_e G E2 intVal(I2) I1 <= I2 --------------------------------- [E-GreaterFalse] eval_e G greater(E1, E2) falseVal eval_e G E1 V1 eval_e G E2 V2 val_eq V1 V2 --------------------------- [E-EqTrue] eval_e G eq(E1, E2) trueVal eval_e G E1 V1 eval_e G E2 V2 ! val_eq V1 V2 ---------------------------- [E-EqFalse] eval_e G eq(E1, E2) falseVal eval_e G E1 trueVal eval_e G E2 trueVal ---------------------------- [E-AndTrue] eval_e G and(E1, E2) trueVal eval_e G E1 falseVal ----------------------------- [E-AndFalse1] eval_e G and(E1, E2) falseVal eval_e G E1 trueVal eval_e G E2 falseVal ----------------------------- [E-AndFalse2] eval_e G and(E1, E2) falseVal eval_e G E1 trueVal --------------------------- [E-OrTrue1] eval_e G or(E1, E2) trueVal eval_e G E1 falseVal eval_e G E2 trueVal --------------------------- [E-OrTrue2] eval_e G or(E1, E2) trueVal eval_e G E1 falseVal eval_e G E2 falseVal ---------------------------- [E-OrFalse] eval_e G or(E1, E2) falseVal --------------------- [E-True] eval_e G true trueVal ----------------------- [E-False] eval_e G false falseVal eval_rf G Fields FieldVals ------------------------------------------- [E-RecBuild] eval_e G recBuild(Fields) recVal(FieldVals) eval_e G Rec recVal(Fields) lookup Fields Field V ------------------------------------- [E-RecField] eval_e G recFieldAccess(Rec, Field) V /*Record Field Evaluation*/ ----------------------------- [ERF-End] eval_rf G endRecFieldExprs [] eval_e G E V eval_rf G Rest FVs -------------------------------------------------- [ERF-Add] eval_rf G addRecFieldExprs(L, E, Rest) (L, V)::FVs /*Command Evaluation*/ --------------- [E-Noop] eval_c G noop G eval_c G C1 G1 eval_c G1 C2 G2 ----------------------- [E-Seq] eval_c G seq(C1, C2) G2 eval_e G E V ------------------------------------ [E-Declare] eval_c G declare(X, Ty, E) (X, V)::G eval_e G E V ------------------------------- [E-Assign] eval_c G assign(X, E) (X, V)::G eval_e G Cond trueVal eval_c G Then G1 ---------------------------------------- [E-IfThenElseTrue] eval_c G ifThenElse(Cond, Then, Else) G1 eval_e G Cond falseVal eval_c G Else G1 ---------------------------------------- [E-IfThenElseFalse] eval_c G ifThenElse(Cond, Then, Else) G1 eval_e G Cond falseVal ---------------------------- [E-WhileFalse] eval_c G while(Cond, Body) G eval_e G Cond trueVal eval_c G Body G1 eval_c G1 while(Cond, Body) G2 ------------------------------ [E-WhileTrue] eval_c G while(Cond, Body) G2 eval_e G E V lookup G Rec recVal(Fields) update_rec_fields RecFields Fields V Result ------------------------------------------- [E-RecUpdate] {eval_c G recUpdate(Rec, RecFields, E) (Rec, recVal(Result))::G} Extensibella_Stand_In { |{c}- C ~~> T eval_c G T G1 ------------- [E-Q] eval_c G C G1 } /*Update the associations in the first tyCtx for the fields, descending through it to place the value in the final one, producing the ending tyCtx*/ Judgment update_rec_fields : recFields* [(string, value)] value [(string, value)] ------------------------------------------------- [URF-One] update_rec_fields oneField(F) Init V (F, V)::Init lookup Init F recVal(FFields) update_rec_fields Rest FFields V UpdatedFFields ----------------------------------------------- [URF-Step] {update_rec_fields addField(F, Rest) Init V (F, recVal(UpdatedFFields))::Init} /*Check equality in a way appropriate to each value type*/ Judgment val_eq : value* value -------------------------- [VE-Int] val_eq intVal(I) intVal(I) ---------------------- [VE-True] val_eq trueVal trueVal ------------------------ [VE-False] val_eq falseVal falseVal evalctx_eq Fields1 Fields2 -------------------------------------- [VE-Rec] val_eq recVal(Fields1) recVal(Fields2) Fixed Judgment evalctx_eq : [(string, value)] [(string, value)] ================ [ECEq-Empty] evalctx_eq [] [] select (X, V2) EC2 Rest2 val_eq V1 V2 evalctx_eq Rest1 Rest2 ============================= [ECEq-Add] evalctx_eq (X, V1)::Rest1 EC2
Click on a command or tactic to see a detailed view of its use.
Module simple_imp:host. Projection_Constraint proj_e_unique : forall E E1 E2, |{e}- E ~~> E1 -> |{e}- E ~~> E2 -> E1 = E2. Projection_Constraint proj_e_is : forall E E', |{e}- E ~~> E' -> is_e E -> is_e E'. Projection_Constraint proj_rf_unique : forall RF RF1 RF2, |{recFieldExprs}- RF ~~> RF1 -> |{recFieldExprs}- RF ~~> RF2 -> RF1 = RF2. Projection_Constraint proj_rf_is : forall RF RF', |{recFieldExprs}- RF ~~> RF' -> is_recFieldExprs RF -> is_recFieldExprs RF'. Projection_Constraint proj_c_unique : forall C C1 C2, |{c}- C ~~> C1 -> |{c}- C ~~> C2 -> C1 = C2. Projection_Constraint proj_c_is : forall C C', |{c}- C ~~> C' -> is_c C -> is_c C'. Projection_Constraint proj_recFields_unique : forall RF RF1 RF2, |{recFields}- RF ~~> RF1 -> |{recFields}- RF ~~> RF2 -> RF1 = RF2. Projection_Constraint proj_recFields_is : forall RF RF', |{recFields}- RF ~~> RF' -> is_recFields RF -> is_recFields RF'. Projection_Constraint proj_ty_unique : forall Ty Ty1 Ty2, |{ty}- Ty ~~> Ty1 -> |{ty}- Ty ~~> Ty2 -> Ty1 = Ty2. Projection_Constraint proj_ty_is : forall Ty Ty', |{ty}- Ty ~~> Ty' -> is_ty Ty -> is_ty Ty'. Projection_Constraint proj_value_unique : forall V V1 V2, |{value}- V ~~> V1 -> |{value}- V ~~> V2 -> V1 = V2. Projection_Constraint proj_value_is : forall V V', |{value}- V ~~> V' -> is_value V -> is_value V'. Extensible_Theorem vars_join : forall E V D, Vars : vars E V -> exists D', V ++ D = D' on Vars, vars_rf_join : forall RF V D, Vars : vars_rf RF V -> exists D', V ++ D = D' on Vars. [Show Proof] Extensible_Theorem vars_unique : forall E V1 V2, Vars1 : vars E V1 -> Vars2 : vars E V2 -> V1 = V2 on Vars1, vars_rf_unique : forall RF V1 V2, Vars1 : vars_rf RF V1 -> Vars2 : vars_rf RF V2 -> V1 = V2 on Vars1. [Show Proof] Projection_Constraint proj_e_vars_exist : forall E E' V, |{e}- E ~~> E' -> vars E V -> exists V', vars E' V'. %Rationale for TC: %Evaluation depends on the variables in an expression. In fact, by %the property vars_eval_same_result below, evaluation is determined %*entirely* by the variables in an expression. Therefore making the %variables in an expression be a subset of those in its projection %gives other extensions a handle on understanding the behavior of an %unknown expression in particular contexts. Projection_Constraint proj_e_vars : forall E E' V V' X, |{e}- E ~~> E' -> vars E V -> vars E' V' -> mem X V -> mem X V'. Projection_Constraint proj_rf_vars_exist : forall RF RF' V, |{recFieldExprs}- RF ~~> RF' -> vars_rf RF V -> exists V', vars_rf RF' V'. Projection_Constraint proj_rf_vars : forall RF RF' V V' X, |{recFieldExprs}- RF ~~> RF' -> vars_rf RF V -> vars_rf RF' V' -> mem X V -> mem X V'. Theorem append__is_list__is_string : forall L1 L2 L, is_list is_string L1 -> is_list is_string L2 -> L1 ++ L2 = L -> is_list is_string L. [Show Proof] Extensible_Theorem vars_is : forall E V, IsE : is_e E -> Vars : vars E V -> is_list is_string V on Vars, vars_rf_is : forall RF V, IsRF : is_recFieldExprs RF -> Vars : vars_rf RF V -> is_list is_string V on Vars. [Show Proof] Theorem append__is_list__is_string__total : forall L1 L2, is_list is_string L1 -> is_list is_string L2 -> exists L, L1 ++ L2 = L. [Show Proof] Extensible_Theorem vars_exist : forall E, IsE : is_e E -> exists V, vars E V on IsE, vars_rf_exist : forall RF, IsRF : is_recFieldExprs RF -> exists V, vars_rf RF V on IsRF. [Show Proof] Extensible_Theorem typeOf_unique : forall G E T1 T2, Ty1: typeOf G E T1 -> Ty2: typeOf G E T2 -> T1 = T2 on Ty1, typeRecFields_unique : forall G RF T1 T2, Ty1: typeRecFields G RF T1 -> Ty2: typeRecFields G RF T2 -> T1 = T2 on Ty1. [Show Proof] Extensible_Theorem typeOK_unique : forall G C G1 G2, Ty1: typeOK G C G1 -> Ty2: typeOK G C G2 -> G1 = G2 on Ty1. [Show Proof] Projection_Constraint proj_eval_e : forall G E E' V, |{e}- E ~~> E' -> eval_e G E V -> exists V', eval_e G E' V'. Extensible_Theorem eval_e_unique : forall G E V1 V2, Ev1: eval_e G E V1 -> Ev2: eval_e G E V2 -> V1 = V2 on Ev1, eval_rf_unique : forall G RF V1 V2, Ev1: eval_rf G RF V1 -> Ev2: eval_rf G RF V2 -> V1 = V2 on Ev1. [Show Proof] Extensible_Theorem update_rec_fields_unique : forall F G V G1 G2, U1: update_rec_fields F G V G1 -> U2: update_rec_fields F G V G2 -> G1 = G2 on U1. [Show Proof] Projection_Constraint proj_c_eval : forall C C' G G2, |{c}- C ~~> C' -> eval_c G C G2 -> exists G', eval_c G C' G'. Ext_Size eval_c G C G1. Proj_Rel eval_c G C G1. Ext_Ind forall G C G1, eval_c G C G1. [Show Proof] Extensible_Theorem eval_c_unique : forall G C G1 G2, Ev1 : eval_c G C G1 -> Ev2 : eval_c G C G2 -> G1 = G2 on Ev1. [Show Proof] Projection_Constraint proj_c_eval_results : forall C C' G G1 G2 X V, |{c}- C ~~> C' -> eval_c G C G1 -> eval_c G C' G2 -> lookup G1 X V -> lookup G2 X V. Projection_Constraint proj_c_eval_results_back : forall C C' G G1 G2 X V, |{c}- C ~~> C' -> eval_c G C G1 -> eval_c G C' G2 -> lookup G2 X V -> lookup G1 X V. Theorem vars_equiv_left : forall (G1 : list (pair string value)) G2 D D1 D2, (forall X U1 U2, mem X D -> lookup G1 X U1 -> lookup G2 X U2 -> U1 = U2) -> D1 ++ D2 = D -> (forall X U1 U2, mem X D1 -> lookup G1 X U1 -> lookup G2 X U2 -> U1 = U2). [Show Proof] Theorem vars_equiv_right : forall (G1 : list (pair string value)) G2 D D1 D2, (forall X U1 U2, mem X D -> lookup G1 X U1 -> lookup G2 X U2 -> U1 = U2) -> D1 ++ D2 = D -> (forall X U1 U2, mem X D2 -> lookup G1 X U1 -> lookup G2 X U2 -> U1 = U2). [Show Proof] Extensible_Theorem vars_eval_same_result : forall G1 G2 E D V1 V2, Equiv : (forall X U1 U2, mem X D -> lookup G1 X U1 -> lookup G2 X U2 -> U1 = U2) -> Vars : vars E D -> Ev1 : eval_e G1 E V1 -> Ev2 : eval_e G2 E V2 -> V1 = V2 on Ev1, vars_equal_rf_same_result : forall G1 G2 RF D V1 V2, Equiv : (forall X U1 U2, mem X D -> lookup G1 X U1 -> lookup G2 X U2 -> U1 = U2) -> Vars : vars_rf RF D -> Ev1 : eval_rf G1 RF V1 -> Ev2 : eval_rf G2 RF V2 -> V1 = V2 on Ev1. [Show Proof]