archive-nl.com » NL » R » ROBBERTKREBBERS.NL

Total: 145

Choose link from "Titles, links and description words view":

Or switch to "Titles and links view".
  • Module expression_eval_smallstep
    expr eval subst ehstep Γ ρ m E e1 ν as e2 simplify map equality auto econstructor do cstep apply IH auto rewrite ectx subst size Nat add lt mono l eauto using ehstep size Qed Lemma ehstep expr eval locks Γ ρ m1 m2 e1 e2 ν Γ ρ ₕ e1 m1 e2 m2 e1 Γ ρ m1 Some ν locks e1 empty locks e2 Proof destruct 1 intros simplify option equality esolve elem of Qed Lemma ehstep expr eval Γ ρ m1 m1 m2 e1 e2 ν Γ ρ ₕ e1 m1 e2 m2 e1 Γ ρ m1 Some ν e1 Γ ρ m1 Some ν e2 Γ ρ m1 Some ν Proof destruct 1 intros simplify option equality solve elem of Qed Lemma ehstep expr eval mem Γ ρ m1 m2 e1 e2 ν Γ ρ ₕ e1 m1 e2 m2 e1 Γ ρ m1 Some ν m1 m2 Proof destruct 1 intros simplify option equality eauto rewrite mem unlock empty try destruct val true false dec as solve elem of Qed Hint Extern 0 typed constructor Lemma ehstep expr eval typed Γ Δ ρ m1 m2 e1 e2 ν τ lr Γ Γ ρ ₕ e1 m1 e2 m2 Γ Δ m1 e1 Γ ρ m1 Some ν Δ ρ Γ Δ ρ 2 e1 τ lr Γ Δ ρ 2 e2 τ lr Proof destruct 2 intros simplify option equality typed inversion all decompose Forall hyps repeat match goal with H ρ 2 i Some τ1 H2 ρ Some τ2 rewrite list lookup fmap H2 in H decompose Forall hyps end try typed constructor eauto using val unop typed val binop typed val cast typed addr top typed cmap index typed valid addr top strict lockset empty valid addr elt typed addr elt strict addr

    Original URL path: http://robbertkrebbers.nl/research/ch2o/expression_eval_smallstep.html (2015-08-10)
    Open archived version from archive


  • Module expression_eval_separation
    Δ ρ m1 m2 e ν τ lr Γ Γ Δ m1 Δ ρ Γ Δ ρ 2 e τ lr e Γ ρ m1 Some ν m1 m2 e Γ ρ m2 Some ν Proof intros eapply expr eval

    Original URL path: http://robbertkrebbers.nl/research/ch2o/expression_eval_separation.html (2015-08-10)
    Open archived version from archive

  • Module executable
    throw n State k Stmt n throw n m label l State k Stmt label l m scase mx State k Stmt scase mx m e State CExpr e k Expr e m ret e State CExpr e ret k Expr e m loop s State CStmt loop k Stmt s m s1 s2 State CStmt s2 k Stmt s1 m catch s State CStmt catch k Stmt s m if e s1 else s2 State CExpr e if s1 else s2 k Expr e m switch e s State CExpr e switch s k Expr e m local τ s let o fresh dom indexset m in State CLocal o τ k Stmt s mem alloc Γ o false perm full val new Γ τ m end Stmt s match k with CLocal o τ k State k Stmt local τ s mem free o m CStmt s2 k State CStmt s k Stmt s2 m CStmt s1 k State k Stmt s1 s m CStmt catch k State k Stmt catch s m CStmt loop k State k Stmt loop s m CStmt if e else s2 k State k Stmt if e s else s2 m CStmt if e s1 else k State k Stmt if e s1 else s m CStmt switch e k State k Stmt switch e s m CParams f o τ s k State k Return f voidV foldr mem free m o τ s 1 end Stmt v s match k with CParams f o τ s k State k Return f v foldr mem free m o τ s 1 CLocal o τ k State k Stmt v local τ s mem free o m CStmt E k State k Stmt v subst E s m end Stmt l s if decide l labels s then match s with label l State k Stmt s m local τ s let o fresh dom indexset m in State CLocal o τ k Stmt l s mem alloc Γ o false perm full val new Γ τ m catch s State CStmt catch k Stmt l s m s1 s2 guard l labels s1 State CStmt s2 k Stmt l s1 m guard l labels s2 State CStmt s1 k Stmt l s2 m loop s State CStmt loop k Stmt l s m if e s1 else s2 guard l labels s1 State CStmt if e else s2 k Stmt l s1 m guard l labels s2 State CStmt if e s1 else k Stmt l s2 m switch e s State CStmt switch e k Stmt l s m end else match k with CLocal o τ k State k Stmt l local τ s mem free o m CStmt Es k State k Stmt l subst Es s m end Stmt mx s match s with scase mx guard mx mx State k Stmt s m local τ s guard mx cases s let o fresh dom indexset m

    Original URL path: http://robbertkrebbers.nl/research/ch2o/executable.html (2015-08-10)
    Open archived version from archive

  • Module executable_sound
    e1 repeat match goal with H assign exec Some apply assign exec correct in H progress decompose elem of H ctx lookup rewrite ctx lookup correct in H progress simplify equality case match end do ehstep Qed Lemma ehexec weak complete Γ k e1 m1 e2 m2 ehexec Γ k e1 m1 Γ locals k ₕ e1 m1 e2 m2 Proof destruct 2 repeat match goal with H assign sem apply assign exec correct in H H is Some destruct H as progress decompose empty H locals Some rewrite ctx lookup correct in H H of option o Ho o Some rewrite Ho in H csimpl in H rewrite collection bind singleton in H progress simplify option equality case match end eauto Qed Lemma ehstep dec Γ ρ e1 m1 e2 m2 Γ ρ ₕ e1 m1 e2 m2 e2 m2 Γ ρ ₕ e1 m1 e2 m2 Proof set k λ o τ CLocal o τ 1 o τ 2 ρ replace ρ with locals k by induction ρ as f equal auto destruct collection choose or empty ehexec Γ k e1 m1 as e2 m2 eauto using ehexec sound ehexec weak complete Qed Lemma cexec sound Γ δ S1 S2 Γ δ ₛ S1 ₑ S2 Γ δ ₛ S1 S2 Proof intros assert k ctx K e m ehexec Γ k e m maybe ECall redex e None is redex e Γ locals k ₕ safe e m intros k e m He rewrite eq None not Some intros Hmaybe Hred Hsafe apply Hmaybe destruct Hsafe eexists apply maybe ECall redex Some eauto edestruct ehexec weak complete eauto destruct S1 repeat match goal with H ehexec apply ehexec sound in H H expr redexes apply expr redexes correct in H destruct H H maybe VBase vb is

    Original URL path: http://robbertkrebbers.nl/research/ch2o/executable_sound.html (2015-08-10)
    Open archived version from archive

  • Module executable_complete
    m1 m2 k E e1 e2 τ lr He τ lr simpl in typed inversion He τ lr edestruct ectx subst typed rev Γ m1 locals k 2 E e1 as τ lr eauto edestruct ehexec complete Γ m1 m2 k e1 e2 as f e2 m2 eauto exists f State k Expr subst E e2 m2 split ands auto assert is redex e1 as He1 by eauto using ehstep is redex assert maybe2 EVal subst E e1 None as destruct E as Ei using rev ind by destruct He1 by destruct Ei by rewrite subst app apply elem of bind exists E e1 assert maybe ECall redex e1 None as rewrite eq None not Some intros Ω f τ s σ Ω s vs Hcall rewrite maybe ECall redex Some in Hcall destruct Hcall as inv ehstep rewrite decide False by esolve elem of split eauto using expr redexes complete apply elem of bind eexists split eauto esolve elem of eleft split ands repeat refine constructor eauto eapply ectx subst refine eauto 10 using ectx refine weaken ectx refine id ehstep forward ehexec sound eauto 10 using ctx refine weaken ctx refine id ehstep forward ehexec sound intros m k Ω f τ s τ E Ω s vs simpl eexists meminj id split ands eauto using state refine id assert maybe2 EVal subst E e None as by destruct E as E using rev ind rewrite subst app apply elem of bind exists E e E split unfold e simpl rewrite maybe ECall redex Some 2 by done by left apply expr redexes complete repeat constructor apply EVals nf intros m k E e He Hsafe simpl in eexists meminj id split ands eauto using state refine id assert maybe2 EVal subst E e None as destruct E as Ei using rev ind by destruct He by destruct Ei by rewrite subst app apply elem of bind exists E e split by apply expr redexes complete destruct collection choose or empty ehexec Γ k e m as e2 m2 destruct Hsafe econstructor eauto using ehexec sound rewrite decide True by done destruct maybe ECall redex e as Ω g σ s σ Ω s vs eqn Hcall eauto apply maybe ECall redex Some in Hcall destruct Hcall as by destruct Hsafe constructor intros m k h s os vs τ f simpl in typed inversion all set os fresh list length vs dom indexset m in assert Forall fresh dom indexset m os by by apply Forall fresh list assert length os length vs by by apply fresh list length edestruct funenv lookup Γ m δ h as eauto simplify equality edestruct mem alloc list refine Γ false meminj id m m os os vs vs as f eauto using cmap refine id vals refine id exists f State CParams h zip os type of vs k Stmt s mem alloc list Γ os vs m split ands auto unfold of option simplify option equality esolve elem of

    Original URL path: http://robbertkrebbers.nl/research/ch2o/executable_complete.html (2015-08-10)
    Open archived version from archive

  • Module frontend
    Γ o false γ v m Δ g mret o Definition update object o index γ perm v val K M modify λ S frontend state K let Γ n Γ m Δ g S in FState Γ n Γ mem alloc Γ o false γ v m Δ g Definition insert global decl x string d global decl K M modify λ S frontend state K let Γ n Γ m Δ g S in FState Γ n Γ m x d Δ g Definition insert fun f funname sto cstorage τ s list type K σ type K ms option stmt K M modify λ S frontend state K let Γ n Γ m Δ g S in FState Γ n f τ s σ Γ m f string Fun sto τ s σ ms Δ g Definition insert compound c compound kind t tag x τ s list string type K M modify λ S frontend state K let Γ n Γ m Δ g S in FState t Compound c x τ s Γ n t x τ s 2 Γ m Δ g Definition insert enum t tag τ i int type K M modify λ S frontend state K let Γ n Γ m Δ g S in FState t Enum τ i Γ n Γ m Δ g Definition first init ref Γ env K τ type K option ref K type K match τ with τ n Some RArray 0 τ n τ structT t τ Γ t 0 Some RStruct 0 t τ unionT t τ Γ t 0 Some RUnion 0 t false τ None end Fixpoint next init ref Γ env K r ref K option ref K type K match r with RArray i τ n r if decide S i n then Some RArray S i τ n r τ else next init ref Γ r RStruct i t r match Γ t S i with Some τ Some RStruct S i t r τ None next init ref Γ r end RUnion r next init ref Γ r None end Definition to ref to expr cexpr M expr K lrtype K ref K type K list string cexpr M ref K type K fix go r τ type K xces struct xces match xces with mret r τ inl x xces c t error of option maybe2 TCompound τ struct union initializer used for non compound type i τ lookup compound t x let rs match c with Struct kind RStruct i t Union kind RUnion i t false end in go rs r τ xces inr ce xces σ n error of option maybe2 TArray τ array initializer used for non array type e to expr ce guard is pure e with array initializer with non constant index Γ gets to env m gets to mem v error of option e Γ m maybe inr array initializer with undefined index x error of option maybe VBase v maybe2 VInt array initializer with non integer index let i Z to nat x in guard i n with array initializer with index out of bounds go RArray i σ n r σ xces end Definition to compound init to expr cexpr M expr K lrtype K to init expr type K cinit M expr K τ type K expr K list ref K list list string cexpr cinit M expr K fix go e seen inits struct inits match inits with mret e xces ci inits Γ gets to env r σ if decide xces then error of option match seen with first init ref Γ τ r next init ref Γ r end excess elements in compound initializer else to ref to expr τ xces guard Forall r seen with element initialized before e1 to init expr σ ci go r e1 e r seen inits end Definition to call fun e expr K τ lr lrtype K option expr K list type K type K match τ lr with inl τ s σ Some e τ s σ inl TType τ τ s σ maybe TBase TPtr τ maybe2 TFun Some load e τ s σ inl TAny None inr τ τ s σ maybe TBase TPtr τ maybe2 TFun Some e τ s σ end Definition to call args to expr cexpr M expr K lrtype K list cexpr list type K M list expr K fix go ces τ s match ces τ s with mret ce ces τ τ s e σ to expr ce curry to R NULL τ Γ gets to env guard cast typed σ τ with function applied to arguments of incorrect type cast τ e go ces τ s fail function applied to the wrong number of arguments end Definition convert fun arg type τ p ptr type K option type K match τ p with TType τ Some TType τ TType τ Some τ τ s τ Some τ s τ TAny None end Definition convert fun ret type τ p ptr type K option type K match τ p with TType τ Some τ TAny Some voidT None end Definition to fun type args to ptr type ctype M ptr type K list option string ctype M list option string type K fix go c τ s match c τ s with mret mx c τ c τ s τ p to ptr type c τ τ error of option convert fun arg type τ p function type with argument of void type mx τ go c τ s end Definition fun empty args x τ s list option string ctype bool match x τ s with None CTVoid true false end Definition to fun type to ptr type ctype M ptr type K c τ s list option string ctype c τ ctype M list option string type K type K τ p to ptr type c τ τ error of option convert fun ret type τ p function type returning function or array if fun empty args c τ s then mret τ else x τ s to fun type args to ptr type c τ s guard NoDup omap fst x τ s with function type with duplicate argument names mret x τ s τ Definition rhs 6 5 16 1p3 safe expr K bool fix go e match e with load var true load true load false true e true true call true abort true e RArray RStruct go e e RUnion false alloc true free e true e go e e1 e2 go e1 go e2 if e2 else e3 go e2 go e3 e2 go e2 cast e go e true false end Definition to field ref seg c compound kind i nat t tag ref seg K match c with Struct kind RStruct i t Union kind RUnion i t false end Inductive to type kind to Type to Ptr Definition to type type K k to type kind match k with to Type type K to Ptr ptr type K end Definition to type ret k τ type K M to type type k match k with to Type mret τ to Ptr mret TType τ end End frontend Fixpoint to expr Env K Δ l local env K ce cexpr M expr K lrtype K match ce return M expr K lrtype K with CEVar x lookup var Δ l x CEConst c τ i z τ i error of option to int const z int const types c τ i integer constant pretty z too large mret intV τ i z inr intT τ i CEConstString zs v n error of option to string const zs char of string constant out of range o insert object perm readonly v mret Ptr addr top o charT n inl TType charT n CELimit c τ li τ to type to Type Δ l c τ z τ i to limit const τ li mret intV τ i z inr intT τ i CEDeref ce e τ to expr Δ l ce curry to R τ p error of option maybe TBase TPtr τ dereferencing non pointer type mret e inl τ p CEAddrOf ce e τ lr to expr Δ l ce τ p error of option maybe inl τ lr taking address of r value mret e inr τ p CEAssign ass ce1 ce2 e1 τ lr1 to expr Δ l ce1 τ1 error of option maybe inl TType τ lr1 assigning to r value e2 τ2 to expr Δ l ce2 curry to R NULL τ1 Γ gets to env guard assign typed τ1 τ2 ass with assignment cannot be typed let e1 if decide ass Assign rhs 6 5 16 1p3 safe e2 then freeze true e1 else e1 in mret e1 ass e2 inr τ1 CECall ce ces e τ lr to expr Δ l ce e τ s σ error of option to call fun e τ lr called object is not a function Γ gets to env guard type complete Γ σ with function called with incomplete type es to call args to expr Δ l ces τ s mret call e es inr σ CEAbort mret abort voidT inr voidT CEAlloc c τ ce τ to type to Type Δ l c τ guard τ voidT with alloc of void type e τ sz to expr Δ l ce curry to R error of option maybe TBase TInt τ sz alloc applied to argument of non integer type mret alloc τ e inr TType τ CEFree ce e τ to expr Δ l ce curry to R τ p error of option maybe TBase TPtr TType τ free applied to argument of non pointer type Γ gets to env guard type complete Γ τ p with free applied to argument of incomplete pointer type mret free e inr voidT CEUnOp op ce e τ to expr Δ l ce curry to R σ error of option unop type of op τ unary operator cannot be typed mret op e inr σ CEBinOp op ce1 ce2 e τ1 to expr Δ l ce1 curry to R e τ2 to expr Δ l ce2 curry to R error of option to binop expr op e τ1 e τ2 binary operator cannot be typed CEIf ce1 ce2 ce3 e1 τ1 to expr Δ l ce1 curry to R τ b error of option maybe TBase τ1 conditional argument of if expression of non base type guard τ b TVoid with conditional argument of if expression of void type e τ2 to expr Δ l ce2 curry to R e τ3 to expr Δ l ce3 curry to R error of option to if expr e1 e τ2 e τ3 if expression cannot be typed CEComma ce1 ce2 e1 τ1 to expr Δ l ce1 curry to R e2 τ2 to expr Δ l ce2 curry to R mret cast voidT e1 e2 inr τ2 CEAnd ce1 ce2 e1 τ1 to expr Δ l ce1 curry to R τ b1 error of option maybe TBase τ1 first argument of of non base type guard τ b1 TVoid with first argument of of void type e2 τ2 to expr Δ l ce2 curry to R τ b2 error of option maybe TBase τ2 second argument of of non base type guard τ b2 TVoid with second argument of of void type mret if e1 if e2 intV sintT 1 else intV sintT 0 else intV sintT 0 inr sintT CEOr ce1 ce2 e1 τ1 to expr Δ l ce1 curry to R τ b1 error of option maybe TBase τ1 first argument of of non base type guard τ b1 TVoid with first argument of of void type e2 τ2 to expr Δ l ce2 curry to R τ b2 error of option maybe TBase τ2 second argument of of non base type guard τ b2 TVoid with second argument of of void type mret if e1 intV sintT 0 else if e2 intV sintT 1 else intV sintT 0 inr sintT CECast c σ ci σ to type to Type Δ l c σ guard maybe2 TArray σ None with array compound literal not supported guard maybe CSingleInit ci None maybe2 TCompound σ None with cast to struct union not allowed e to init expr Δ l σ ci mret e inr σ CEField ce x e τ lr to expr Δ l ce match τ lr with inl τ p c t error of option maybe TType τ p maybe2 TCompound field operator applied to argument of non compound type i σ lookup compound t x mret e to field ref seg c i t inl TType σ inr τ c t error of option maybe2 TCompound τ field operator applied to argument of non compound type i σ lookup compound t x guard maybe2 TArray σ None with indexing array field of r value struct union not supported mret e to field ref seg c i t inr σ end end with to init expr Env K Δ l local env K σ type K ci cinit M expr K match ci with CSingleInit ce match maybe CEConstString ce with Some zs v n error of option to string const zs char of string initializer out of range if decide σ type of v then mret v else if decide σ charT then o insert object perm readonly v mret Ptr addr top o charT n RArray 0 charT n else fail string initializer of wrong type or size None e τ to expr Δ l ce curry to R NULL σ Γ gets to env guard cast typed τ σ with cast or initializer cannot be typed mret cast σ e end CCompoundInit inits Γ gets to env to compound init to expr Δ l to init expr Δ l σ val 0 Γ σ inits end with to type Env K k to type kind Δ l local env K c τ ctype M to type type k match c τ with CTVoid match k with to Type mret voidT to Ptr mret TAny end CTDef x τ p lookup typedef Δ l x match k return M to type type k with to Ptr mret τ p to Type match τ p with TType τ Γ gets to env guard type complete Γ τ with complete typedef expected mret τ TAny mret voidT fail complete typedef expected end end CTEnum x let t tag x in Γ n gets to compounds τ i error of option Γ n t maybe Enum enum x not found to type ret intT τ i CTInt c τ i to type ret intT to inttype c τ i CTPtr c τ τ p to type to Ptr Δ l c τ to type ret τ p CTArray c τ ce τ to type to Type Δ l c τ guard τ voidT with array with elements of void type e to expr Δ l ce guard is pure e with array with non constant size expression Γ gets to env m gets to mem v error of option e Γ m maybe inr array with undefined size expression x error of option maybe VBase v maybe2 VInt array with non integer size expression let n Z to nat x in guard n 0 with array with negative or zero size expression to type ret τ n CTCompound c x let t tag x in match k with to Ptr mret compoundT c t PT to Type Γ gets to env guard is Some Γ t with complete compound type expected mret compoundT c t end CTFun c τ s c τ match k with to Type fail complete type expected to Ptr x τ s τ to fun type to type to Ptr Δ l c τ s c τ mret x τ s 2 τ end CTTypeOf ce τ lr to expr Δ l ce match τ lr with inl TType τ Γ gets to env guard type complete Γ τ with complete typeof expected to type ret τ inr τ to type ret τ fail typeof of function end end Section frontend more Context Env K Definition to init val Δ l local env K τ type K ci cinit M val K e to init expr Δ l τ ci Γ gets to env m gets to mem guard is pure e with initializer with non constant expression error of option e Γ m maybe inr initializer with undefined expression Definition alloc global Δ l local env K x string sto cstorage c τ ctype mci option cinit M index type K list type K type K τ p to type to Ptr Δ l c τ Δ g gets to globals match Δ g x with Some Global sto o τ init guard τ p TType τ with global x previously declared with different type guard sto ExternStorage sto sto sto AutoStorage sto ExternStorage with global x previously declared with different linkage match mci with Some ci guard sto ExternStorage with global x initialized and declared extern guard init false with global x already initialized insert global decl x Global sto o τ true v to init val Δ l τ ci update object o perm full v mret inl o τ None mret inl o τ end Some Fun sto τ s σ ms guard τ p τ s σ with function previously x declared with different type guard sto ExternStorage sto sto sto AutoStorage sto ExternStorage with function x previously declared with different linkage guard mci None with function x with initializer insert fun x sto τ s σ ms mret inr τ s σ Some GlobalTypeDef fail global x previously declared as typedef Some EnumVal fail global x previously declared as enum tag None match τ

    Original URL path: http://robbertkrebbers.nl/research/ch2o/frontend.html (2015-08-10)
    Open archived version from archive

  • Module frontend_sound
    expr inl typed type valid Qed Lemma to R NULL typed S S τ s σ e τ lr e τ to R NULL σ e τ lr S mret e τ S S to env S to mem S τ s e τ lr locks e to env S τ s to env S TType σ to env S to mem S τ s e inr τ locks e S S Proof unfold to R NULL intros H σ error proceed e τ as S destruct to R typed S S τ s e τ lr e τ as auto inversion H σ as σ b intros repeat case match simplify error equality eauto 10 Qed Lemma convert ptrs typed Γ m τ s e1 τ1 e2 τ2 e1 e2 τ convert ptrs e1 τ1 e2 τ2 Some e1 e2 τ Γ m τ s e1 inr τ1 locks e1 Γ m τ s e2 inr τ2 locks e2 Γ Γ τ s Γ m τ s e1 inr τ Γ m τ s e2 inr τ locks e1 locks e2 Proof unfold convert ptrs destruct τ1 as τ2 as intros simplify option equality split repeat typed constructor eauto 12 using TPtr valid inv TBase valid inv expr inr typed type valid Qed Lemma to if expr typed Γ m τ s e1 τ b e2 τ2 e3 τ3 e τ lr to if expr e1 e2 τ2 e3 τ3 Some e τ lr Γ m τ s e1 inr baseT τ b τ b TVoid locks e1 Γ m τ s e2 inr τ2 locks e2 Γ m τ s e3 inr τ3 locks e3 Γ Γ τ s Γ m τ s e τ lr locks e Proof unfold to if expr intros repeat match goal with progress simplify option equality case match x type destruct x H convert ptrs Some eapply convert ptrs typed in H eauto destruct H as end eauto 10 Qed Lemma to binop expr typed Γ m τ s op e1 τ1 e2 τ2 e τ lr to binop expr op e1 τ1 e2 τ2 Some e τ lr Γ m τ s e1 inr τ1 locks e1 Γ m τ s e2 inr τ2 locks e2 Γ Γ τ s Γ m τ s e τ lr locks e Proof unfold to binop expr intros repeat match goal with progress simplify option equality x type destruct x H binop type of Some apply binop type of sound in H H convert ptrs Some eapply convert ptrs typed in H eauto destruct H as end eauto 10 Qed CoInductive seen A x A Seen seen x Ltac weaken repeat match goal with H local env valid S Δ l H2 S S assert local env valid S Δ l by eauto using local env valid subseteq clear H H to env S1 τ p H2 S1 S2 assert to env S2 τ p by eauto using ptr type valid weaken clear H H to env S1 τ ps H2 S1 S2 assert to env S2 τ ps by eauto using ptr types valid weaken clear H H to env S1 τ H2 S1 S2 assert to env S2 τ by eauto using type valid weaken clear H H to env S1 τ s H2 S1 S2 assert to env S2 τ s by eauto using types valid weaken clear H H type complete to env S1 τ H2 S1 S2 assert type complete to env S2 τ by eauto using type complete weaken clear H H Forall type complete to env S1 τ s H2 S1 S2 assert Forall type complete to env S2 τ s by eauto using types complete weaken clear H H to env S1 τ s e τ lr H2 S1 S2 assert to env S2 to mem S2 τ s e τ lr by eapply expr typed weaken to env S1 eauto clear H H to env S1 τ s s cm τ H2 S1 S2 assert to env S2 to mem S2 τ s s cm τ by eapply stmt typed weaken to env S1 eauto clear H H to mem S1 o τ H2 S1 S2 assert to mem S2 o τ by eauto using memenv forward typed clear H H index alive to mem S1 o H2 S1 S2 assert index alive to mem S2 o by eauto using memenv subseteq alive clear H H to env S1 f Some τ s τ H2 S1 S2 assert to env S2 f funname Some τ s τ by eauto using lookup fun weaken clear H H to env S1 r τ σ H2 S1 S2 assert to env S2 r τ σ by eauto using ref typed weaken clear H H to env S1 v τ H2 S1 S2 assert to env S2 to mem S2 v τ by eapply val typed weaken to env S1 eauto clear H H inl apply ltype valid inv in H H inr apply rtype valid inv in H H baseT apply TBase valid inv in H H BT apply TPtr valid inv in H H apply TFun valid inv in H destruct H Γ Δ τ s τ lr unless seen τ lr by assumption assert Γ τ lr by eauto using expr typed type valid Γ Δ τ s assert seen τ lr by constructor progress simplify equality end Lemma insert object valid S S o v γ τ insert object γ v S mret o S S to env S to mem S v τ sep valid γ sep unmapped γ to mem S o τ index alive to mem S o to globals S to globals S S S S Proof destruct S as Γ n Γ m Δ g unfold insert object intros error proceed simplify type equality assert m fresh dom indexset m τ false m eapply insert subseteq mem allocable memenv of is fresh split ands eauto using mem alloc index typed mem alloc index alive split simpl erewrite mem alloc memenv of by eauto eauto using map Forall impl global decl valid weaken eapply mem alloc valid eauto using val typed weaken mem alloc forward Qed Lemma update object valid S S o γ v τ update object o γ v S mret S S to mem S o τ index alive to mem S o to env S to mem S v τ sep valid γ sep unmapped γ S S S Proof destruct S unfold update object intros error proceed do 2 split simpl erewrite mem alloc alive memenv of by eauto eauto using mem alloc alive valid Qed Lemma insert global decl valid S S x d insert global decl x d S mret S S global decl valid to env S to mem S x d maybe4 Fun d None d to globals S x Some d global decl forward d d to globals S x Some d S S S Proof destruct S as Γ n Γ m Δ g unfold insert global decl intros H Γ Hm H Δ g H Γ n H Γ error proceed simplify map equality split ands split simpl auto using map Forall insert 2 intros f τ s τ destruct decide rel f x simplify map equality auto destruct H Γ x τ s τ as sto auto exfalso destruct d naive solver by apply insert included Qed Lemma insert fun None valid S S f sto τ s τ insert fun f sto τ s τ None S mret S S to globals S f string None to env S TType τ s to env S TType τ to env S f Some τ s τ S S S Proof destruct S as Γ n Γ m Δ g unfold insert fun intros H Γ Hm H Δ g H Γ n H Γ error proceed destruct Γ f as τ s τ eqn Hf simplify map equality destruct H Γ f τ s τ naive solver assert Γ f τ s τ Γ by by apply insert fun subseteq split ands split simpl eauto using cmap valid weaken by constructor apply map Forall insert 2 simplify map equality eauto using sizes of weaken map Forall impl global decl valid weaken apply map Forall insert 2 simplify map equality eauto unfold lookup env lookup fun in Hf intros f destruct decide f f simplify map equality eauto apply insert included congruence Qed Lemma insert fun valid S S f sto τ s τ ms insert fun f sto τ s τ ms S mret S S to env S f Some τ s τ fun stmt valid to env S to mem S τ s τ ms S S S Proof destruct S as Γ n Γ m Δ g unfold insert fun intros H Γ Hm H Δ g H Γ n H Γ Hf error proceed rewrite insert fun id by done destruct H Γ f τ s τ as ms auto do 2 split simpl auto using map Forall insert 2 intros f τ s τ unfold lookup env lookup fun in Hf destruct decide f f simplify map equality eauto apply insert included intros naive solver Qed Lemma insert compound valid S S c t x τ s insert compound c t x τ s S mret S S to env S t None to env S x τ s 2 x τ s to env S t Some x τ s 2 S S S Proof destruct S as Γ n Γ m Δ g unfold insert compound intros H Γ Hm H Δ g H Γ n H Γ error proceed simplify map equality split ands split simpl eauto using env insert compound valid fmap nil inv eauto using cmap valid weaken insert compound subseteq eauto using map Forall impl global decl valid weaken insert compound subseteq intros t d destruct decide t t simplify map equality auto rewrite lookup insert compound ne by done by apply H Γ n eauto using insert compound subseteq Qed Lemma insert enum valid S S t τ i insert enum t τ i S mret S S to compounds S t None S S S Proof destruct S as Γ n Γ m Δ g unfold insert enum intros H Γ Hm H Δ g H Γ n H Γ error proceed do 2 split simpl auto using map Forall insert 2 Qed Lemma first init ref typed Γ τ r σ first init ref Γ τ Some r σ Γ τ Γ r τ σ Proof destruct 2 as simplify option equality repeat econstructor eauto with lia Qed Fixpoint next init ref typed Γ τ r σ r σ next init ref Γ r Some r σ Γ r τ σ Γ r τ σ Proof induction 2 as repeat case match simplify option equality repeat econstructor eauto Qed Lemma to ref typed S S Δ l r τ xces σ r σ Forall sum rect λ True λ ce S S e τ lr to expr Δ l ce S mret e τ lr M S S local env valid S Δ l to env S to mem S to local types Δ l e τ lr locks e S S S xces to ref to expr Δ l r σ xces S mret r σ S S local env valid S Δ l to env S r τ σ to env S r τ σ S S S Proof intros IHxces revert S r σ induction IHxces as x ce xces IH IHxces generalize errors intros S r σ simplify equality auto error proceed c s as error proceed i τ as S2 destruct lookup compound typed S S2 s x i τ as τ s auto destruct c error proceed eauto error proceed τ n as error proceed e τ e as S2 error proceed τ i x as destruct IH S S2 e τ e as weaken auto destruct IHxces S2 RArray Z to nat x τ n r τ as eauto Qed Lemma to call fun typed Γ Δ τ s e τ lr e σ s σ to call fun e τ lr Some e σ s σ Γ Δ τ s e τ lr locks e Γ Δ τ s e inl σ s σ locks e Proof destruct τ lr as intros simplify option equality eauto using TBase complete Qed Lemma to call args typed S S Δ l ces τ s es Forall λ ce S S e τ lr to expr Δ l ce S mret e τ lr S S local env valid S Δ l to env S to mem S to local types Δ l e τ lr locks e S S S ces to call args to expr Δ l ces τ s S mret es S S local env valid S Δ l to env S TType τ s to env S to mem S to local types Δ l es inr τ s locks es S S S Proof intros Hces revert S S es τ s induction Hces as ce ces IH IHces intros S S es τ τ s error proceed eauto error proceed e τ lr as S2 error proceed e τ as S3 error proceed es as decompose Forall hyps destruct IH S S2 e τ lr as auto weaken destruct to R NULL typed S2 S3 to local types Δ l τ e τ lr e τ as eauto destruct IHces S2 S es τ s as auto weaken eauto 10 using cast typed type valid Qed Lemma to compound init typed S S Δ l e τ rs inits e Forall λ i Forall sum rect λ True λ ce S S e τ lr to expr Δ l ce S mret e τ lr M S S local env valid S Δ l to env S to mem S to local types Δ l e τ lr locks e S S S i 1 S S τ e to init expr Δ l τ i 2 S mret e S S local env valid S Δ l to env S τ to env S to mem S to local types Δ l e inr τ locks e S S S inits to compound init to expr Δ l to init expr Δ l τ e rs inits S mret e S S local env valid S Δ l Forall λ r σ to env S r τ σ rs to env S to mem S to local types Δ l e inr τ locks e to env S to mem S to local types Δ l e inr τ locks e S S S Proof intros Hinits revert S S rs e e assert Γ1 Γ2 rs Forall λ r σ Γ1 r τ σ rs Γ1 Γ2 Forall λ r σ Γ2 r τ σ rs induction 1 as constructor eauto using ref typed weaken induction Hinits as xces ci inits IHe IHi IH intros S S rs e e Hrs error proceed eauto destruct decide xces error proceed decompose Forall hyps weaken destruct Hrs as r rs σ error proceed decompose Forall hyps error proceed r σ as error proceed e as S2 assert to env S r τ σ by auto using first init ref typed destruct IHi S S2 σ e as eauto using ref typed type valid weaken destruct IH S2 S r r e e e as eauto error proceed r σ as error proceed e as S2 assert to env S r τ σ by eauto using next init ref typed destruct IHi S S2 σ e as eauto using ref typed type valid weaken destruct IH S2 S r r rs r e e e as eauto 10 error proceed r σ as S2 error proceed e as S3 destruct to ref typed S S2 Δ l τ xces τ r σ as auto weaken destruct IHi S2 S3 σ e as eauto using ref typed type valid weaken destruct IH S3 S r rs r e e e as eauto 10 Qed Definition to type type valid k Γ env K to type type k Prop match k with to Type Γ to Ptr Γ end Lemma convert fun arg type valid Γ τ p τ convert fun arg type τ p Some τ Γ τ p Γ TType τ Proof inversion 2 simplify option equality repeat constructor auto by apply type valid ptr type valid Qed Lemma convert fun ret valid Γ τ p τ convert fun ret type τ p Some τ Γ τ p Γ TType τ Proof inversion 2 simplify option equality repeat constructor auto Qed Lemma to fun type valid S S Δ l c τ s c τ x τ s τ Forall λ xc τ S S k τ k to type k Δ l xc τ 2 S mret τ k S S local env valid S Δ l to type type valid to env S τ k S S S c τ s S S k τ k to type k Δ l c τ S mret τ k S S local env valid S Δ l to type type valid to env S τ k S S S to fun type to type to Ptr Δ l c τ s c τ S mret x τ s τ S S local env valid S Δ l to env S TType x τ s 2 to env S TType τ S S S Proof intros IHc τ s revert S c τ τ assert S to fun type args to type to Ptr Δ l c τ s S mret x τ s S S local env valid S Δ l to env S TType x τ s 2 S S S as

    Original URL path: http://robbertkrebbers.nl/research/ch2o/frontend_sound.html (2015-08-10)
    Open archived version from archive

  • Module interpreter
    list type K args list list Z M list val K if decide σ s then mret else if decide σ s sintT charT K T then vs interpreter args go args o insert object perm full VArray charT K vs mret intV sintT length vs ptrV Ptr addr top array o charT K length vs else fail function main should have argument types int and char Definition interpreter initial Θ list string decl args list list Z M istate K E alloc program Θ Δ g gets to globals σ s σ error of option Δ g main maybe4 Fun function main undeclared guard σ sintT T σ uintT T with function main should have return type int vs interpreter args σ s args m gets to mem mret IState initial state m main vs Definition interpreter initial eval Θ list string decl args list list Z string istate K E error eval interpreter initial Θ args Definition cexec Γ env K δ funenv K iS istate K E listset istate K E let ε s S iS in λ S new let ε s new e Γ S new in IState ε s new ε s ε s new S new cexec Γ δ S Context hash istate K E Z Definition cexec all Γ env K δ funenv K iS istate K E listset istate K E listset istate K E let nexts cexec Γ δ iS in if decide nexts then iS else nexts Definition csteps exec all Γ env K δ funenv K listset istate K E stream listset istate K E listset istate K E cofix go iSs let nexts cexec all Γ δ iSs in let reds listset normalize hash nexts fst in let nfs listset normalize hash nexts snd in reds nfs

    Original URL path: http://robbertkrebbers.nl/research/ch2o/interpreter.html (2015-08-10)
    Open archived version from archive