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 assignments_separation
    typed τ1 τ2 ass Γ Δ a TType τ1 Γ Δ v τ2 assign sem Γ m1 a v ass va v m1 m2 assign sem Γ m2 a v ass va v Proof destruct 3 inversion 3 econstructor simplify

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

  • Module operations
    Γ1 Γ2 Δ1 m1 m2 c a1 a2 τ p1 τ p2 Γ1 Γ1 Δ1 a1 τ p1 Γ1 Δ1 a2 τ p2 Γ1 Γ2 o index alive m1 o index alive m2 o addr compare ok Γ1 m1 c a1 a2 Γ1 Γ2 addr compare ok Γ2 m2 c a1 a2 Proof unfold addr compare ok intuition eauto using addr strict weaken Qed Lemma addr compare ok erase Γ m c a1 a2 addr compare ok Γ cmap erase m c a1 a2 addr compare ok Γ m c a1 a2 Proof unfold addr compare ok by rewrite index alive erase Qed Lemma addr compare weaken Γ1 Γ2 Δ1 a1 a2 c τ p1 τ p2 Γ1 Γ1 Δ1 a1 τ p1 Γ1 Δ1 a2 τ p2 Γ1 Γ2 addr compare Γ1 c a1 a2 addr compare Γ2 c a1 a2 Proof unfold addr compare intros by erewrite addr object offset weaken Γ1 Γ2 by eauto Qed Lemma addr plus typed Γ Δ m a σ p j Γ Γ Δ a σ p addr plus ok Γ m j a Γ Δ addr plus Γ j a σ p Proof destruct 2 as o r i τ σ σ p intros constructor simpl in split ands auto apply Nat2Z inj le by rewrite Nat2Z inj mul Z2Nat id by done rewrite Nat2Z id ptr size of Γ σ p at 1 rewrite Z2Nat divide by auto with zpos apply Z divide add r by apply Nat2Z divide by apply Z divide mul r Qed Lemma addr plus ok weaken Γ1 Γ2 Δ1 m1 m2 a σ p j Γ1 Γ1 Δ1 a σ p addr plus ok Γ1 m1 j a Γ1 Γ2 o index alive m1 o index alive m2 o addr plus ok Γ2 m2 j a Proof unfold addr plus ok intros simplify type equality erewrite addr size of weaken size of weaken Γ2 by eauto using addr typed type base valid eauto Qed Lemma addr plus ok erase Γ m a j addr plus ok Γ cmap erase m j a addr plus ok Γ m j a Proof unfold addr plus ok by rewrite index alive erase Qed Lemma addr plus weaken Γ1 Γ2 Δ1 a σ p j Γ1 Γ1 Δ1 a σ p Γ1 Γ2 addr plus Γ1 j a addr plus Γ2 j a Proof intros Ha assert ptr size of Γ1 σ p ptr size of Γ2 σ p by eauto using addr size of weaken destruct Ha simplify type equality congruence Qed Lemma addr type of plus Γ a j type of addr plus Γ j a type of a Proof by destruct a Qed Lemma addr type base plus Γ a j addr type base addr plus Γ j a addr type base a Proof by destruct a Qed Lemma addr index plus Γ a j addr index addr plus Γ j a addr index a Proof by destruct a Qed Lemma addr plus 0 Γ a addr plus Γ 0 a a Proof destruct a simpl by rewrite Z mul 0 l Z add 0 r Nat2Z id Qed Lemma addr plus plus Γ a j1 j2 0 addr byte a j2 ptr size of Γ type of a Z addr plus Γ j1 addr plus Γ j2 a addr plus Γ j1 j2 a Proof intros destruct a as o r i σ σ p do 2 f equal by rewrite Z2Nat id Z add comm j1 Z mul add distr r Z add assoc Qed Lemma addr plus plus nat Γ a j1 j2 nat addr plus Γ j1 addr plus Γ j2 a addr plus Γ j1 j2 nat a Proof rewrite Nat2Z inj add apply addr plus plus auto with zpos Qed Lemma addr is obj plus Γ a j addr is obj addr plus Γ j a addr is obj a Proof by destruct a Qed Lemma addr ref base plus Γ a j addr ref base addr plus Γ j a addr ref base a Proof by destruct a Qed Lemma addr minus typed Γ m a1 a2 addr minus ok Γ m a1 a2 int typed addr minus Γ a1 a2 sptrT Proof by intros Qed Lemma addr minus weaken Γ1 Γ2 Δ1 a1 a2 σ p1 Γ1 Γ1 Δ1 a1 σ p1 Γ1 Γ2 addr minus Γ1 a1 a2 addr minus Γ2 a1 a2 Proof intros unfold addr minus simplify type equality by erewrite addr size of weaken Γ1 Γ2 by eauto Qed Lemma addr minus ok weaken Γ1 Γ2 Δ1 m1 m2 a1 a2 σ p1 Γ1 Γ1 Δ1 a1 σ p1 addr minus ok Γ1 m1 a1 a2 Γ1 Γ2 o index alive m1 o index alive m2 o addr minus ok Γ2 m2 a1 a2 Proof intros split erewrite addr minus weaken Γ1 Γ2 by eauto eauto Qed Lemma addr minus ok erase Γ m a1 a2 addr minus ok Γ cmap erase m a1 a2 addr minus ok Γ m a1 a2 Proof unfold addr minus ok by rewrite index alive erase Qed Lemma addr cast typed Γ Δ m a σ p τ p Γ Δ a σ p addr cast ok Γ m τ p a Γ Δ addr cast τ p a τ p Proof intros constructor eauto Qed Lemma addr cast ok weaken Γ1 Γ2 Δ1 m1 m2 a σ p τ p Γ1 Γ1 Δ1 a σ p o index alive m1 o index alive m2 o addr cast ok Γ1 m1 τ p a Γ1 Γ2 addr cast ok Γ2 m2 τ p a Proof intros repeat split auto destruct τ p as τ simpl auto by erewrite size of weaken by eauto using castable type valid addr typed type base valid Qed Lemma addr cast ok erase Γ m a τ p addr cast ok Γ cmap erase m τ p a addr cast ok Γ m τ p a Proof unfold addr cast ok by rewrite index alive erase Qed Lemma addr type cast a σ p type of addr cast σ p a σ p Proof by destruct a Qed Lemma addr index cast a σ p addr index addr cast σ p a addr index a Proof by destruct a Qed Lemma addr ref cast Γ a σ p addr ref Γ addr cast σ p a addr ref Γ a Proof by destruct a Qed Lemma addr ref byte cast Γ a σ p addr ref byte Γ addr cast σ p a addr ref byte Γ a Proof by destruct a Qed Lemma addr cast self Γ Δ a σ p Γ Δ a σ p addr cast σ p a a Proof by destruct 1 Qed Lemma addr is obj cast a σ p addr is obj addr cast σ p a σ p TType addr type base a Proof by destruct a Qed Lemma addr ref plus char cast Γ Δ a σ p j Γ Γ Δ a σ p addr is obj a j ptr size of Γ σ p addr ref Γ addr plus Γ j addr cast TType ucharT a addr ref Γ a Proof destruct 2 as o r i τ σ σ p intros simplify equality f equal rewrite size of char Z mul 1 r Z2Nat inj add Nat2Z id by auto with zpos symmetry apply Nat div unique with i mod size of Γ σ j by rewrite λ x y H proj2 Nat mod divide x y H by eauto using size of ne 0 ref typed type valid by rewrite Nat add assoc Nat div mod by eauto using ref typed type valid size of ne 0 Qed Lemma addr ref byte plus char cast Γ Δ a σ p j Γ Γ Δ a σ p addr is obj a j ptr size of Γ σ p addr ref byte Γ addr plus Γ j addr cast TType ucharT a j Proof destruct 2 as o r i τ σ σ p intros simplify equality rewrite size of char Z mul 1 r Z2Nat inj add Nat2Z id by auto with zpos rewrite Nat add mod idemp l λ y H proj2 Nat mod divide i y H Nat add 0 l by eauto using ref typed type valid size of ne 0 by apply Nat mod small Qed Lemma addr byte lt size char cast Γ Δ a σ p j Γ Γ Δ a σ p addr is obj a j ptr size of Γ σ p addr byte a size of Γ addr type base a ref size addr ref base a addr byte addr plus Γ j addr cast TType ucharT a size of Γ addr type base a ref size addr ref base a Proof destruct 2 as o r i τ σ σ p Hi intros simplify equality rewrite size of char Z mul 1 r Z2Nat inj add Nat2Z id by auto with zpos apply Nat lt le trans with i size of Γ σ lia destruct Hi as rewrite Nat mul succ l Nat mul comm Nat mul le mono pos l Nat le succ l Nat mul lt mono pos r size of Γ σ by eauto using ref typed type valid size of pos lia Qed Properties of operations on pointers Global Instance ptr alive dec m p Decision ptr alive m p Proof refine match p with Ptr a decide index alive m addr index a left end done Defined Lemma ptr alive weaken m1 m2 p ptr alive m1 p o index alive m1 o index alive m2 o ptr alive m2 p Proof destruct p simpl auto Qed Lemma ptr alive 1 m p ptr alive m p ptr alive m p Proof destruct p simpl eauto Qed Hint Resolve ptr alive 1 Lemma ptr alive erase m p ptr alive cmap erase m p ptr alive m p Proof unfold ptr alive by destruct p rewrite index alive erase Qed Global Instance ptr compare ok dec Γ m c p1 p2 Decision ptr compare ok Γ m c p1 p2 Proof destruct p1 p2 c apply Defined Global Instance ptr plus ok dec Γ m j p Decision ptr plus ok Γ m j p Proof destruct p apply Defined Global Instance ptr minus ok dec Γ m p1 p2 Decision ptr minus ok Γ m p1 p2 Proof destruct p1 p2 apply Defined Global Instance ptr cast ok dec Γ m σ p p Decision ptr cast ok Γ m σ p p Proof destruct p apply Defined Global Instance ptr cast typed dec τ p σ p Decision ptr cast typed τ p σ p Proof refine match τ p σ p with TType TAny TAny TAny TType left TType τ1 TType τ2 cast if decide τ1 τ2 τ2 ucharT τ1 ucharT τ s1 τ1 τ s2 τ2 cast if and decide τ s1 τ s2 decide τ1 τ2 right end BT abstract first by intuition subst constructor by inversion 1 intuition Defined Lemma ptr plus typed Γ Δ m p σ p j Γ Γ Δ p σ p ptr plus ok Γ m j p Γ Δ ptr plus Γ j p σ p Proof destruct 2 simpl constructor eauto using addr plus typed Qed Lemma ptr minus typed Γ m p1 p2 ptr minus ok Γ m p1 p2 int typed ptr minus Γ p1 p2 sptrT Proof destruct p1 p2 simpl eauto using addr minus typed int typed small with lia Qed Lemma ptr cast typed Γ Δ m p τ p σ p Γ Δ p τ p ptr cast typed τ p σ p Γ σ p ptr cast ok Γ m σ p p Γ Δ ptr cast σ p p σ p Proof destruct 1 inversion 1 intros simplify equality constructor eauto using addr cast typed Qed Lemma ptr cast typed self τ p ptr cast typed τ p τ p Proof destruct τ p constructor Qed Lemma ptr compare ok weaken Γ1 Γ2 Δ1 m1 m2 c p1 p2 τ p1 τ p2 Γ1 Γ1 Δ1 p1 τ p1 Γ1 Δ1 p2 τ p2 ptr compare ok Γ1 m1 c p1 p2 Γ1 Γ2 o index alive m1 o index alive m2 o ptr compare ok Γ2 m2 c p1 p2 Proof destruct 2 1 simpl repeat case match eauto using addr compare ok weaken Qed Lemma ptr compare ok erase Γ m c p1 p2 ptr compare ok Γ cmap erase m c p1 p2 ptr compare ok Γ m c p1 p2 Proof unfold ptr compare ok by destruct p1 p2 rewrite index alive erase addr compare ok erase Qed Lemma ptr compare weaken Γ1 Γ2 Δ1 c p1 p2 τ p1 τ p2 Γ1 Γ1 Δ1 p1 τ p1 Γ1 Δ1 p2 τ p2 Γ1 Γ2 ptr compare Γ1 c p1 p2 ptr compare Γ2 c p1 p2 Proof destruct 2 1 simpl intros eauto 2 using addr compare weaken Qed Lemma ptr plus ok weaken Γ1 Γ2 Δ1 m1 m2 p τ p j Γ1 Γ1 Δ1 p τ p ptr plus ok Γ1 m1 j p Γ1 Γ2 o index alive m1 o index alive m2 o ptr plus ok Γ2 m2 j p Proof destruct 2 simpl eauto using addr plus ok weaken Qed Lemma ptr plus ok erase Γ m j p ptr plus ok Γ cmap erase m j p ptr plus ok Γ m j p Proof destruct p simpl auto using addr plus ok erase Qed Lemma ptr plus weaken Γ1 Γ2 Δ1 p τ p j Γ1 Γ1 Δ1 p τ p Γ1 Γ2 ptr plus Γ1 j p ptr plus Γ2 j p Proof destruct 2 simpl eauto using addr plus weaken f equal Qed Lemma ptr minus ok weaken Γ1 Γ2 Δ1 m1 m2 p1 p2 τ p1 Γ1 Γ1 Δ1 p1 τ p1 ptr minus ok Γ1 m1 p1 p2 Γ1 Γ2 o index alive m1 o index alive m2 o ptr minus ok Γ2 m2 p1 p2 Proof destruct 2 p2 simpl eauto using addr minus ok weaken Qed Lemma ptr minus ok erase Γ m p1 p2 ptr minus ok Γ cmap erase m p1 p2 ptr minus ok Γ m p1 p2 Proof destruct p1 p2 simpl auto using addr minus ok erase Qed Lemma ptr minus weaken Γ1 Γ2 Δ1 p1 p2 τ p1 τ p2 Γ1 Γ1 Δ1 p1 τ p1 Γ1 Δ1 p2 τ p2 Γ1 Γ2 ptr minus Γ1 p1 p2 ptr minus Γ2 p1 p2 Proof destruct 2 1 simpl eauto using addr minus weaken Qed Lemma ptr cast ok weaken Γ1 Γ2 Δ1 m1 m2 p τ p σ p Γ1 Γ1 Δ1 p τ p ptr cast ok Γ1 m1 σ p p Γ1 Γ2 o index alive m1 o index alive m2 o ptr cast ok Γ2 m2 σ p p Proof destruct 2 simpl eauto using addr cast ok weaken Qed Lemma ptr cast ok erase Γ m p τ p ptr cast ok Γ cmap erase m τ p p ptr cast ok Γ m τ p p Proof destruct p simpl auto using addr cast ok erase Qed Lemma ptr compare ok alive l Γ m c p1 p2 ptr compare ok Γ m c p1 p2 ptr alive m p1 Proof destruct p1 p2 c simpl unfold addr minus ok addr compare ok naive solver Qed Lemma ptr compare ok alive r Γ m c p1 p2 ptr compare ok Γ m c p1 p2 ptr alive m p2 Proof destruct p1 as p2 as c csimpl unfold addr compare ok naive solver Qed Lemma ptr plus ok alive Γ m p j ptr plus ok Γ m j p ptr alive m p Proof destruct p done intros simpl eauto done Qed Lemma ptr minus ok alive l Γ m p1 p2 ptr minus ok Γ m p1 p2 ptr alive m p1 Proof destruct p1 p2 simpl try done intros eauto Qed Lemma ptr minus ok alive r Γ m p1 p2 ptr minus ok Γ m p1 p2 ptr alive m p2 Proof destruct p1 p2 simpl try done intros eauto Qed Lemma ptr cast ok alive Γ m p σ p ptr cast ok Γ m σ p p ptr alive m p Proof destruct p simpl done intros eauto done Qed Properties of operations on base values Global Instance base val branchable dec m vb Decision base val branchable m vb Proof destruct vb apply Defined Global Instance base val is 0 dec vb Decision base val is 0 vb Proof refine match vb with VInt x decide x 0 VPtr NULL left right end abstract naive solver Defined Lemma base val branchable weaken m1 m2 vb base val branchable m1 vb o index alive m1 o index alive m2 o base val branchable m2 vb Proof destruct vb simpl eauto using ptr alive weaken Qed Lemma base val branchable erase m vb base val branchable cmap erase m vb base val branchable m vb Proof by destruct vb simpl rewrite ptr alive erase Qed Lemma base val is 0 branchable m vb base val is 0 vb base val branchable m vb Proof by destruct vb as Qed Global Instance base val unop ok dec m op vb Decision base val unop ok m op vb Proof destruct vb op try apply Defined Global Instance base val binop ok dec Γ m op vb1 vb2 Decision base val binop ok Γ m op vb1 vb2 Proof destruct vb1 vb2 op as op try apply destruct op apply Defined Global Instance base val cast ok dec Γ m σ b vb Decision base val cast ok Γ m σ b vb Proof destruct vb σ b apply Defined Lemma base unop typed type valid Γ op τ b σ b

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

  • Module operations_refine
    using size of castable Nat divide add r Nat divide mul l Qed Lemma addr cast refine Γ α f m1 m2 a1 a2 σ p τ p addr cast ok Γ m1 τ p a1 a1 Γ α f m1 m2 a2 σ p addr cast τ p a1 Γ α f m1 m2 addr cast τ p a2 τ p Proof intros destruct 1 simplify equality econstructor eauto Qed Refinements of operations on pointers Lemma ptr alive refine Γ α f m1 m2 p1 p2 σ p ptr alive m1 p1 p1 Γ α f m1 m2 p2 σ p ptr alive m2 p2 Proof destruct 2 simpl in eauto using addr alive refine Qed Lemma ptr compare ok refine Γ α f m1 m2 c p1 p2 p3 p4 σ p p1 Γ α f m1 m2 p2 σ p p3 Γ α f m1 m2 p4 σ p ptr compare ok Γ m1 c p1 p3 ptr compare ok Γ m2 c p2 p4 Proof destruct 1 1 c simpl eauto using addr minus ok refine addr alive refine addr compare ok refine Qed Lemma ptr compare refine Γ α f m1 m2 c p1 p2 p3 p4 σ p Γ ptr compare ok Γ m1 c p1 p3 p1 Γ α f m1 m2 p2 σ p p3 Γ α f m1 m2 p4 σ p ptr compare Γ c p1 p3 ptr compare Γ c p2 p4 Proof destruct 3 1 simpl repeat case match eauto 2 using addr compare refine Qed Lemma ptr plus ok refine Γ α f m1 m2 p1 p2 σ p j p1 Γ α f m1 m2 p2 σ p ptr plus ok Γ m1 j p1 ptr plus ok Γ m2 j p2 Proof destruct 1 simpl eauto using addr plus ok refine Qed Lemma ptr plus refine Γ α f m1 m2 p1 p2 σ p j Γ ptr plus ok Γ m1 j p1 p1 Γ α f m1 m2 p2 σ p ptr plus Γ j p1 Γ α f m1 m2 ptr plus Γ j p2 σ p Proof destruct 3 simpl constructor eauto using addr plus refine Qed Lemma ptr minus ok refine Γ α f m1 m2 p1 p2 p3 p4 σ p p1 Γ α f m1 m2 p2 σ p p3 Γ α f m1 m2 p4 σ p ptr minus ok Γ m1 p1 p3 ptr minus ok Γ m2 p2 p4 Proof destruct 1 1 simpl eauto using addr minus ok refine Qed Lemma ptr minus refine Γ α f m1 m2 p1 p2 p3 p4 σ p Γ ptr minus ok Γ m1 p1 p3 p1 Γ α f m1 m2 p2 σ p p3 Γ α f m1 m2 p4 σ p ptr minus Γ p1 p3 ptr minus Γ p2 p4 Proof destruct 3 1 simpl eauto using addr minus refine Qed Lemma ptr cast ok refine Γ α f m1 m2 p1 p2 σ p τ p Γ p1 Γ α f m1 m2 p2 σ p ptr cast ok Γ m1 τ p p1 ptr cast ok Γ m2 τ p p2 Proof destruct 2 simpl eauto using addr cast ok refine Qed Lemma ptr cast refine Γ α f m1 m2 p1 p2 σ p τ p ptr cast ok Γ m1 τ p p1 ptr cast typed σ p τ p Γ τ p p1 Γ α f m1 m2 p2 σ p ptr cast τ p p1 Γ α f m1 m2 ptr cast τ p p2 τ p Proof destruct 2 inversion 2 intros simplify equality constructor eauto using addr cast refine Qed Refinements of operations on base values Lemma base val branchable refine Γ α f m1 m2 vb1 vb2 τ b vb1 Γ α f m1 m2 vb2 τ b base val branchable m1 vb1 base val branchable m2 vb2 Proof destruct 1 naive solver eauto 10 using ptr alive refine Qed Lemma base val is 0 refine Γ α f Δ1 Δ2 vb1 vb2 τ b vb1 Γ α f Δ1 Δ2 vb2 τ b base val is 0 vb1 base val is 0 vb2 Proof by destruct 1 as Qed Lemma base val is 0 refine inv Γ α f m1 m2 vb1 vb2 τ b vb1 Γ α f m1 m2 vb2 τ b base val branchable m1 vb1 base val is 0 vb2 base val is 0 vb1 Proof destruct 1 as naive solver eauto 10 using addr alive refine Qed Lemma base val true refine inv Γ α f m1 m2 vb1 vb2 τ b vb1 Γ α f m1 m2 vb2 τ b base val branchable m2 vb2 base val is 0 vb2 1 base val branchable m1 vb1 base val is 0 vb1 2 α base val branchable m1 vb1 Proof intros destruct α eauto 10 using base val branchable refine base val refine inverse base val is 0 refine destruct decide base val branchable m1 vb1 eauto 10 using base val is 0 refine Qed Lemma base val false refine inv Γ α f m1 m2 vb1 vb2 τ b vb1 Γ α f m1 m2 vb2 τ b base val is 0 vb2 base val is 0 vb1 α base val branchable m1 vb1 Proof intros destruct α eauto using base val is 0 refine base val refine inverse destruct decide base val branchable m1 vb1 eauto using base val is 0 refine inv Qed Lemma base val unop ok refine Γ α f m1 m2 op vb1 vb2 τ b vb1 Γ α f m1 m2 vb2 τ b base val unop ok m1 op vb1 base val unop ok m2 op vb2 Proof destruct op 1 naive solver eauto using ptr alive refine Qed Lemma base val unop refine Γ α f m1 m2 op vb1 vb2 τ b σ b Γ base unop typed op τ b σ b base val unop ok m1

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

  • Module expressions
    locks e e1 e2 e1 e2 e1 e2 e1 e2 locks e1 locks e2 if e1 e2 else e3 locks e1 locks e2 locks e3 end Lemma expr locks freeze K β e expr K locks freeze β e locks e Proof assert es list expr K Forall λ e locks freeze β e locks e es locks freeze β es locks es induction 1 solve elem of induction e using expr ind alt csimpl try solve elem of f equal auto Qed An expression is pure or side effect free if it does not modify the memory Although pure expressions may have sequence points namely at the conditional and call expressions these sequence points are not observable because pure expressions do not allow any locations to get locked in the first place Inductive is pure K expr K Prop EVar pure x is pure var x EVal pure v is pure v ERtoL pure e is pure e is pure e ERofL pure e is pure e is pure e EEltR pure e rs is pure e is pure e rs EEltL pure e rs is pure e is pure e rs EUnOp pure op e is pure e is pure op e EBinOp pure op e1 e2 is pure e1 is pure e2 is pure e1 op e2 EIf pure e1 e2 e3 is pure e1 is pure e2 is pure e3 is pure if e1 e2 else e3 EComma pure el er is pure el is pure er is pure el er ECast pure τ e is pure e is pure cast τ e EInsert pure r e1 e2 is pure e1 is pure e2 is pure r e1 e2 Section is pure ind Context K fs funset P expr K Prop Context Pvar x P var x Context Pval v P v Context Prtol e is pure e P e P e Context Profl e is pure e P e P e Context Peltl e rs is pure e P e P e rs Context Peltr e rs is pure e P e P e rs Context Punop op e is pure e P e P op e Context Pbinop op e1 e2 is pure e1 P e1 is pure e2 P e2 P e1 op e2 Context Pif e1 e2 e3 is pure e1 P e1 is pure e2 P e2 is pure e3 P e3 P if e1 e2 else e3 Context Pcomma e1 e2 is pure e1 P e1 is pure e2 P e2 P e1 e2 Context Pcast τ e is pure e P e P cast τ e Context Pinsert r e1 e2 is pure e1 P e1 is pure e2 P e2 P r e1 e2 Definition is pure ind alt e is pure e P e Proof fix 2 destruct 1 eauto using Forall impl Qed End is pure ind Instance is pure dec K e expr K Decision is pure e Proof refine fix go e match e return Decision is pure e with var left Ω cast if decide Ω e e e e cast e cast if decide is pure e op e cast if decide is pure e e1 e2 e1 e2 e1 e2 cast if and decide is pure e1 decide is pure e2 if e1 e2 else e3 cast if and3 decide is pure e1 decide is pure e2 decide is pure e3 right end clear go first by subst constructor abstract by inversion 1 subst Defined Lemma is pure locks K e expr K is pure e locks e Proof assert es list expr K oi Forall λ e oi locks e es oi locks es induction 1 esolve elem of intros He apply elem of equiv empty L intros oi induction He using is pure ind alt esolve elem of Qed The operation e increases all De Bruijn indexes of variables in e by one That means each variable var x in e becomes var S x Reserved Notation e at level 20 format e Fixpoint expr lift K e expr K expr K match e with var x var S x Ω ν Ω ν e e e e e1 ass e2 e1 ass e2 call e es call e expr lift es abort τ abort τ load e load e e rs e rs e rs e rs alloc τ e alloc τ e free e free e op e op e e1 op e2 e1 op e2 if e1 e2 else e3 if e1 e2 else e3 e1 e2 e1 e2 cast τ e cast τ e r e1 e2 r e1 e2 end where e expr lift e expr scope The predicate is nf e states that e is in normal form and is redex e states that e is a head redex with respect to the semantics in the file smallstep Inductive is nf K expr K Prop EVal nf Ω ν is nf Ω ν Inductive is redex K expr K Prop EVar redex x is redex var x ERtoL redex e is nf e is redex e ERofL redex e is nf e is redex e EAssign redex ass e1 e2 is nf e1 is nf e2 is redex e1 ass e2 ECall redex e es is nf e Forall is nf es is redex call e es EAbort redex τ is redex abort τ ELoad redex e is nf e is redex load e EEltL redex e rs is nf e is redex e rs EEltR redex e rs is nf e is redex e rs EAlloc redex τ e is nf e is redex alloc τ e EFree redex e is nf e is redex free e EUnOp redex op e is nf e is redex op e EBinOp redex op e1 e2 is nf e1 is nf e2 is redex e1 op e2 EIf redex e1 e2 e3 is nf e1 is redex if e1 e2 else e3 EComma redex e1 e2 is nf e1 is redex e1 e2 ECast redex τ e is nf e is redex cast τ e EInsert redex r e1 e2 is nf e1 is nf e2 is redex r e1 e2 Instance is nf dec K e expr K Decision is nf e Proof refine match e with left right end try constructor abstract inversion 1 Defined Instance is redex dec K e expr K Decision is redex e Proof refine match e with var abort left e e cast e load e e e alloc e free e e if e else e cast if decide is nf e call e es cast if and decide is nf e decide Forall is nf es e1 e2 e1 e2 e1 e2 cast if and decide is nf e1 decide is nf e2 right end first by constructor abstract by inversion 1 Defined Lemma is redex nf K e expr K is redex e is nf e False Proof destruct 1 inversion 1 Qed Lemma EVal not redex K Ω ν lrval K is redex Ω ν Proof inversion 1 Qed Lemma EVals nf K Ω s vs list val K Forall is nf Ω s vs Proof revert vs induction Ω s intros repeat constructor auto Qed Lemma EVals nf alt K es Ω s vs list val K es Ω s vs Forall is nf es Proof intros by apply EVals nf Qed Definition maybe ECall redex K e expr K option lockset funname list type K type K list lockset list val K e es maybe2 ECall e Ω p maybe2 λ Ω p Ω p e f τ s τ maybe3 FunPtr p v Ω s mapM maybe2 λ Ω v Ω v es Some Ω f τ s τ v Ω s 1 v Ω s 2 Lemma maybe EAlloc Some K e expr K τ e maybe2 EAlloc e Some τ e e alloc τ e Proof split by destruct e intros simplify equality by intros Qed Lemma maybe ECall Some K e expr K e es maybe2 ECall e Some e es e call e es Proof split by destruct e intros simplify equality by intros Qed Lemma maybe ECall redex Some 2 K Ω f τ s τ Ω s vs list val K length Ω s length vs maybe ECall redex call Ω FunPtr f τ s τ Ω s vs Some Ω f τ s τ Ω s vs Proof intros unfold maybe ECall redex csimpl rewrite zip with zip mapM fmap Some by by intros csimpl by rewrite fst zip snd zip by lia Qed Lemma maybe ECall redex Some K e expr K Ω f τ s τ Ω s vs maybe ECall redex e Some Ω f τ s τ Ω s vs e call Ω FunPtr f τ s τ Ω s vs length Ω s length vs Proof assert es list expr K Ω vs mapM maybe2 λ Ω v Ω v es Some Ω vs es Ω vs 1 Ω vs 2 E intros es Ω vs rewrite mapM Some induction 1 as e f equal eauto by destruct e repeat case match simplify option equality split intros eauto using maybe ECall redex Some 2 unfold maybe ECall redex csimpl intros destruct maybe2 ECall e as e es eqn repeat case match simplify option equality rewrite fmap length auto with f equal Qed Contexts with one hole We define singular expression contexts ectx item and then full expression evaluation contexts ectx are lists of expression contexts These expression contexts allow us to enforce an evaluation strategy In particular for the conditional we merely allow a hole for the first branch Inductive ectx item K Set Set CRtoL ectx item K CLtoR ectx item K CAssignL assign expr K ectx item K CAssignR assign expr K ectx item K CCallL list expr K ectx item K CCallR expr K list expr K list expr K ectx item K CLoad ectx item K CEltL ref seg K ectx item K CEltR ref seg K ectx item K CAlloc type K ectx item K CFree ectx item K CUnOp unop ectx item K CBinOpL binop expr K ectx item K CBinOpR binop expr K ectx item K CIf expr K expr K ectx item K CComma expr K ectx item K CCast type K ectx item K CInsertL ref K expr K ectx item K CInsertR ref K expr K ectx item K Notation ectx K list ectx item K Bind Scope expr scope with ectx item Arguments CRtoL Arguments CLtoR Arguments CAssignL Arguments CAssignR Arguments CCallL Arguments CCallR Arguments CLoad Arguments CEltL Arguments CEltR Arguments CAlloc Arguments CFree Arguments CUnOp Arguments CBinOpL Arguments CBinOpR Arguments CIf Arguments CComma Arguments CCast Arguments CInsertL Arguments CInsertR Notation CRtoL at level 24 format expr scope Notation CLtoR at level 24 format expr scope Notation ass e2 CAssignL ass e2 at level 54 format ass e2 expr scope Notation e1 ass CAssignR ass e1 at level 54 format e1 ass expr scope Notation call es CCallL es at level 10 es1 at level 66 expr scope Notation call f es1 es2 CCallR f es1 es2 at level 10 es1 at level 66 es2 at level 66 expr scope Notation load CLoad at level 10 format load expr scope Notation rs CEltL rs at level 22 format rs expr scope Notation rs CEltR rs at level 22 format rs expr scope Notation alloc τ CAlloc τ at level 10 format alloc τ expr scope Notation free CFree at level 10 format free expr scope Notation op CUnOp op at level 35 format op expr scope Notation op e2 CBinOpL op e2 at level 50 format op e2 expr scope Notation e1 op CBinOpR op e1 at level 50 format e1 op expr scope Notation if e2 else e3 CIf e2 e3 at level 56 format if e2 else e3 expr scope Notation e2 CComma e2 at level 58 format e2 expr scope Notation cast τ CCast τ at level 10 format cast τ expr scope Notation r e2 CInsertL r e2 at level 10 format r e2 expr scope Notation r e1 CInsertR r e1 at level 10 format r e1 expr scope Instance ectx item dec K Set k1 k2 K Decision k1 k2 Ei1 Ei2 ectx item K Decision Ei1 Ei2 Proof solve decision Defined Substitution is defined in a straightforward way Using the type class instances in the file contexts it is lifted to full expression contexts Instance ectx item subst K Subst ectx item K expr K expr K λ Ei e match Ei with e e ass er e ass er el ass el ass e call es call e es call e es1 es2 call e reverse es1 e es2 load load e rs e rs rs e rs alloc τ alloc τ e free free e op op e op e2 e op e2 e1 op e1 op e e2 e e2 if e2 else e3 if e e2 else e3 cast τ cast τ e r e2 r e e2 r e1 r e1 e end Instance DestructSubst ectx item subst K Instance Ei ectx item K Injective subst Ei Proof by destruct Ei intros simplify list equality Qed Lemma is nf ectx item K Ei ectx item K e is nf subst Ei e Proof destruct Ei inversion 1 Qed Lemma is nf ectx K E ectx K e is nf subst E e E Proof destruct E using rev ind auto rewrite subst snoc intros edestruct is nf ectx item eauto Qed Lemma is nf redex ectx K E ectx K e is redex e is nf subst E e Proof intros HEe rewrite is nf ectx E e in HEe by done simpl in HEe eauto using is redex nf Qed Lemma is redex ectx item K Ei ectx item K e is redex subst Ei e is nf e Proof destruct Ei inversion 1 decompose Forall hyps auto Qed Lemma is redex ectx K E ectx K e is redex subst E e E is redex e Ei E Ei is nf e Proof destruct E as Ei E using rev ind eauto rewrite subst snoc intros feed pose proof is redex ectx item Ei subst E e auto feed pose proof is nf ectx E e subst simpl in eauto Qed Instance ectx locks K Locks ectx item K λ Ei match Ei with cast e e locks e call es locks es call e es1 es2 locks e locks es1 locks es2 load alloc free e e e e e locks e if e2 else e3 locks e2 locks e3 end Lemma ectx item is pure K Ei ectx item K e expr K is pure subst Ei e is pure e Proof destruct Ei simpl inversion clear 1 decompose Forall hyps eauto Qed Lemma ectx is pure K E ectx K e is pure subst E e is pure e Proof induction E using rev ind rewrite subst snoc eauto using ectx item is pure Qed Lemma ectx item subst is pure K Ei ectx item K e1 e2 expr K is pure e2 is pure subst Ei e1 is pure subst Ei e2 Proof destruct Ei simpl inversion clear 2 constructor decompose Forall eauto Qed Lemma ectx subst is pure K E ectx K e1 e2 expr K is pure e2 is pure subst E e1 is pure subst E e2 Proof induction E using rev ind rewrite subst snoc eauto using ectx item subst is pure ectx item is pure Qed Lemma ectx item subst locks K Ei ectx item K e locks subst Ei e locks Ei locks e Proof apply elem of equiv L intro destruct Ei simpl try solve elem of rewrite fmap app fmap reverse csimpl rewrite union list app L union list cons union list reverse L solve elem of Qed Lemma ectx subst locks K E ectx K e locks subst E e locks E locks e Proof apply elem of equiv L intros revert e induction E as Ei E IH simpl solve elem of intros rewrite IH ectx item subst locks solve elem of Qed Instance ectx item size K Size ectx item K λ Ei match Ei with load alloc free cast 1 e e e e e e e S size e call es S sum list with size es call e es1 es2 S size e sum list with size es1 sum list with size es2 if e2 else e3 S size e2 size e3 end Lemma ectx item subst size K Ei ectx item K e size subst Ei e size Ei size e nat Proof destruct Ei simpl auto with lia rewrite sum list with app sum list with reverse simpl lia Qed Lemma ectx subst size K E ectx K e size subst E e sum list with size E size e nat Proof revert e induction E as Ei E IH intros e simpl done rewrite IH ectx item subst size lia Qed The induction principle ectx expr ind is used to perform simultaneous induction on an expression e and context E Although a similar result can be obtained by generalizing over E before doing the induction on e this induction principle is more useful together with automation Automation now does not have to instantiate the induction hypothesis with the appropriate context Section ectx expr ind Context K P ectx K expr K Prop Context Pvar E x P E var x Context Pval E Ω ν P E Ω ν Context Prtol E e P E e P E e Context Profl E e P E e P E e Context Passign E ass e1 e2 P ass e2 E e1 P e1 ass E e2 P E e1 ass e2 Context Pcall E e es P call es E e zipped Forall λ

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

  • Module statements
    injection 1 Qed Instance stmt gotos K Gotos stmt K fix go s let Gotos go in match s with skip throw ret label scase goto l l local s catch s loop s switch s gotos s s1 s2 if s1 else s2 gotos s1 gotos s2 end Instance stmt labels K Labels stmt K fix go s let Labels go in match s with skip goto throw ret scase label l l catch s local s loop s switch s labels s s1 s2 if s1 else s2 labels s1 labels s2 end Instance stmt cases K Cases stmt K fix go s let Cases go in match s with skip goto throw ret label scase mz mz catch s local s loop s cases s s1 s2 if s1 else s2 cases s1 cases s2 switch end Fixpoint throws valid K n nat s stmt K Prop match s with ret skip goto label scase True throw i i n local s loop s switch s throws valid n s catch s throws valid S n s s1 s2 if s1 else s2 throws valid n s1 throws valid n s2 end Instance throws valid dec K n s stmt K Decision throws valid n s Proof refine fix go n s match s return Decision throws valid n s with ret skip goto label scase left throw i cast if decide i n local s loop s switch s go n s catch s go S n s s1 s2 if s1 else s2 cast if and go n s1 go n s2 end clear go abstract naive solver Defined Lemma throws valid weaken K n n s stmt K throws valid n s n n throws valid n s Proof revert n n induction s simpl intuition eauto with lia Qed Program contexts We first define the data type sctx item of singular statement contexts A pair E s consisting of a list of singular statement contexts E and a statement s forms a zipper for statements without block scope variables Inductive sctx item K Set Set CCatch sctx item K CCompL stmt K sctx item K CCompR stmt K sctx item K CLoop sctx item K CIfL expr K stmt K sctx item K CIfR expr K stmt K sctx item K CSwitch expr K sctx item K Instance sctx item eq dec K Set k1 k2 K Decision k1 k2 E1 E2 sctx item K Decision E1 E2 Proof solve decision Defined Arguments CCatch Arguments CCompL Arguments CCompR Arguments CLoop Arguments CIfL Arguments CIfR Arguments CSwitch Bind Scope stmt scope with sctx item Notation catch CCatch at level 10 format catch stmt scope Notation s CCompL s at level 80 format s stmt scope Notation s CCompR s at level 80 format s stmt scope Notation loop CLoop at level 10 format loop stmt scope Notation if e else s2 CIfL e s2 at level 56 format if e else s2 stmt scope

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

  • Module state
    Notation n Throw n at level 20 C scope Notation mx Switch mx at level 20 C scope Instance direction eq dec K Set k1 k2 K Decision k1 k2 d1 d2 direction K Decision d1 d2 Proof solve decision Defined Definition direction in K d direction K s stmt K Prop match d with True l l labels s mx mx cases s False end Definition direction out K d direction K s stmt K Prop match d with True l l labels s True False end Arguments direction in simpl nomatch Arguments direction out simpl nomatch Hint Unfold direction in direction out Lemma direction in out K d direction K s direction in d s direction out d s False Proof by destruct d Qed The data type focus describes the part of the program that is focused An execution state state equips a focus with a program context and memory The focus Stmt is used for execution of statements it contains the statement to be executed and the direction in which traversal should be performed The focus Expr is used for expressions and contains the whole expression that is being executed Notice that this constructor does not contain the set of locked locations due to sequenced writes these are contained more structurally in the expression itself The focus Call is used to call a function it contains the name of the called function and the values of the arguments The focus Return is used to return from the called function to the calling function it contains the return value The focus Undef is used to capture undefined behavior It contains the expression that got stuck These focuses correspond to the five variants of execution states as described above Inductive undef state K Set Set UndefExpr ectx K

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

  • Module smallstep
    ₛ State k Stmt s1 s2 m State CStmt s2 k Stmt s1 m cstep out comp1 m k s1 s2 Γ δ ₛ State CStmt s2 k Stmt s1 m State CStmt s1 k Stmt s2 m cstep out comp2 m k s1 s2 Γ δ ₛ State CStmt s1 k Stmt s2 m State k Stmt s1 s2 m cstep in catch m k s Γ δ ₛ State k Stmt catch s m State CStmt catch k Stmt s m cstep out catch m k s Γ δ ₛ State CStmt catch k Stmt s m State k Stmt catch s m cstep in loop m k s Γ δ ₛ State k Stmt loop s m State CStmt loop k Stmt s m cstep out loop m k s Γ δ ₛ State CStmt loop k Stmt s m State k Stmt loop s m cstep out if1 m k e s1 s2 Γ δ ₛ State CStmt if e else s2 k Stmt s1 m State k Stmt if e s1 else s2 m cstep out if2 m k e s1 s2 Γ δ ₛ State CStmt if e s1 else k Stmt s2 m State k Stmt if e s1 else s2 m cstep out switch m k e s Γ δ ₛ State CStmt switch e k Stmt s m State k Stmt switch e s m For function calls cstep call m k f s os vs δ f Some s Forall fresh dom indexset m os length os length vs Γ δ ₛ State k Call f vs m State CParams f zip os type of vs k Stmt s mem alloc list Γ os vs m cstep free params m k f o τ s s Γ δ ₛ State CParams f o τ s k Stmt s m State k Return f voidV foldr mem free m o τ s 1 cstep free params top m k f o τ s v s Γ δ ₛ State CParams f o τ s k Stmt v s m State k Return f v foldr mem free m o τ s 1 cstep return m k f E v Γ δ ₛ State CFun E k Return f v m State k Expr subst E v E m For non local control flow cstep label here m k l Γ δ ₛ State k Stmt l label l m State k Stmt label l m cstep throw here m k s Γ δ ₛ State CStmt catch k Stmt 0 s m State k Stmt catch s m cstep throw further m k s n Γ δ ₛ State CStmt catch k Stmt S n s m State k Stmt n catch s m cstep case here m k mx Γ δ ₛ State k Stmt mx scase mx m State k Stmt scase mx m cstep goto in m k Es l s l labels s Γ δ ₛ State k Stmt l subst Es s m State CStmt Es k Stmt l s m cstep switch in m k Es mx s maybe CSwitch Es None mx cases s Γ δ ₛ State k Stmt mx subst Es s m State CStmt Es k Stmt mx s m cstep top out m k Es v s Γ δ ₛ State CStmt Es k Stmt v s m State k Stmt v subst Es s m cstep goto out m k Es l s l labels s Γ δ ₛ State CStmt Es k Stmt l s m State k Stmt l subst Es s m cstep throw out m k Es n s Es catch Γ δ ₛ State CStmt Es k Stmt n s m State k Stmt n subst Es s m For block scopes cstep in block m k d o τ s direction in d s o dom indexset m Γ δ ₛ State k Stmt d local τ s m State CLocal o τ k Stmt d s mem alloc Γ o false perm full val new Γ τ m cstep out block m k d o τ s direction out d s Γ δ ₛ State CLocal o τ k Stmt d s m State k Stmt d local τ s mem free o m where Γ δ ₛ S1 S2 cstep Γ δ S1 S S2 S C scope The reflexive transitive closure Notation Γ δ ₛ S1 S2 rtc cstep Γ δ S1 S2 at level 74 δ at next level format Γ δ ₛ S1 S2 C scope Inversion tactics Ltac inv assign sem match goal with H assign sem inversion H subst clear H end Ltac inv ehstep match goal with H ₕ inversion H subst clear H end Step tactics Hint Constructors assign sem ehstep ehsafe cstep cstep Ltac do ehstep match goal with ₕ constructor solve eauto with cstep ₕ solve eauto with cstep end The quote stmt s tactic yields a list of possible ways to write a statement s as subst E s where E is a singular statement context and s a statement subst E s where E is a singular expression in statement context and s a statement This tactic is useful to automatically perform reductions as for example cstep label down whose starting state is State k Stmt l subst E s m Ltac quote stmt s lazymatch s with e constr subst e ret e constr subst ret e s1 s2 constr subst s1 s2 subst s2 s1 loop s constr subst loop s catch s constr subst catch s if e s1 else s2 constr subst if e s1 else s2 subst if e else s2 s1 subst if s1 else s2 e switch e s constr subst switch e s subst switch s e end The quote expr e tactic yields a list of possible ways to write an expression e as subst E e where E is an

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

  • Module type_system
    ectx item typed Γ Δ τ s op inr τ inr σ CBinOpL typed op e2 τ1 τ2 σ binop typed op τ1 τ2 σ Γ Δ τ s e2 inr τ2 ectx item typed Γ Δ τ s op e2 inr τ1 inr σ CBinOpR typed op e1 τ1 τ2 σ binop typed op τ1 τ2 σ Γ Δ τ s e1 inr τ1 ectx item typed Γ Δ τ s e1 op inr τ2 inr σ CIf typed e2 e3 τ b σ lr τ b TVoid Γ Δ τ s e2 σ lr Γ Δ τ s e3 σ lr ectx item typed Γ Δ τ s if e2 else e3 inr baseT τ b σ lr CComma typed e2 τ lr1 τ lr2 Γ Δ τ s e2 τ lr2 ectx item typed Γ Δ τ s e2 τ lr1 τ lr2 CCast typed τ σ cast typed τ σ Γ σ ectx item typed Γ Δ τ s cast σ inr τ inr σ CInsertL typed r e2 τ σ Γ r τ σ Γ Δ τ s e2 inr τ ectx item typed Γ Δ τ s r e2 inr σ inr τ CInsertR typed r e1 τ σ Γ r τ σ Γ Δ τ s e1 inr σ ectx item typed Γ Δ τ s r e1 inr τ inr τ Global Instance ectx item typed PathTyped envs lrtype K lrtype K ectx item K curry3 ectx item typed Inductive ectx typed Γ s envs ectx K lrtype K lrtype K Prop ectx nil typed 2 τ ectx typed Γ s τ τ ectx cons typed 2 Ei E τ1 τ2 τ3 Γ s Ei τ1 τ2 ectx typed Γ s E τ2 τ3 ectx typed Γ s Ei E τ1 τ3 Global Instance ectx typed PathTyped envs lrtype K lrtype K ectx K ectx typed Inductive rettype union option type K option type K option type K Prop rettype union idempotent m σ rettype union m σ m σ m σ rettype union Some r σ rettype union None Some σ Some σ rettype union Some l σ rettype union Some σ None Some σ Inductive rettype match rettype K type K Prop rettype match true Some σ rettype match true Some σ σ rettype match false Some rettype match false Some voidT voidT rettype match true None σ rettype match true None σ rettype match false None rettype match false None voidT Inductive stmt typed Γ env K Δ memenv K τ s list type K stmt K rettype K Prop SSkip typed stmt typed Γ Δ τ s skip false None SDo typed e τ Γ Δ τ s e inr τ locks e stmt typed Γ Δ τ s e false None SGoto typed l stmt typed Γ Δ τ s goto l true None SThrow typed n stmt typed Γ Δ τ s throw n true None SReturn typed e τ Γ Δ τ s e inr τ locks e stmt typed Γ Δ τ s ret e true Some τ SCase typed mx stmt typed Γ Δ τ s scase mx false None SLabel typed l stmt typed Γ Δ τ s label l false None SLocal typed τ s c m σ Γ τ stmt typed Γ Δ τ τ s s c m σ stmt typed Γ Δ τ s local τ s c m σ SComp typed s1 s2 c1 m σ1 c2 m σ2 m σ stmt typed Γ Δ τ s s1 c1 m σ1 stmt typed Γ Δ τ s s2 c2 m σ2 rettype union m σ1 m σ2 m σ stmt typed Γ Δ τ s s1 s2 c2 m σ SCatch typed s c m σ stmt typed Γ Δ τ s s c m σ stmt typed Γ Δ τ s catch s false m σ SLoop typed s c m σ stmt typed Γ Δ τ s s c m σ stmt typed Γ Δ τ s loop s true m σ SIf typed e τ b s1 s2 c1 m σ1 c2 m σ2 m σ Γ Δ τ s e inr baseT τ b τ b TVoid locks e stmt typed Γ Δ τ s s1 c1 m σ1 stmt typed Γ Δ τ s s2 c2 m σ2 rettype union m σ1 m σ2 m σ stmt typed Γ Δ τ s if e s1 else s2 c1 c2 m σ SSwitch typed e τ i s c m σ Γ Δ τ s e inr intT τ i locks e stmt typed Γ Δ τ s s c m σ stmt typed Γ Δ τ s switch e s false m σ Global Instance stmt typed Typed envs rettype K stmt K curry3 stmt typed Inductive sctx item typed Γ env K Δ memenv K τ s list type K sctx item K relation rettype K CCompL typed s2 c1 m σ1 c2 m σ2 m σ Γ Δ τ s s2 c2 m σ2 rettype union m σ1 m σ2 m σ sctx item typed Γ Δ τ s s2 c1 m σ1 c2 m σ CCompR typed s1 c1 m σ1 c2 m σ2 m σ Γ Δ τ s s1 c1 m σ1 rettype union m σ1 m σ2 m σ sctx item typed Γ Δ τ s s1 c2 m σ2 c2 m σ Ccatch typed c m σ sctx item typed Γ Δ τ s catch c m σ false m σ CLoop typed c m σ sctx item typed Γ Δ τ s loop c m σ true m σ CIfL typed e τ b s2 c1 m σ1 c2 m σ2 m σ Γ Δ τ s e inr baseT τ b τ b TVoid locks e Γ Δ τ s s2 c2 m σ2 rettype union m σ1 m σ2 m σ sctx item typed Γ Δ τ s if e else s2 c1 m σ1 c1 c2 m σ CIfR typed e τ b s1 c1 m σ1 c2 m σ2 m σ Γ Δ τ s e inr baseT τ b τ b TVoid locks e Γ Δ τ s s1 c1 m σ1 rettype union m σ1 m σ2 m σ sctx item typed Γ Δ τ s if e s1 else c2 m σ2 c1 c2 m σ CSWitch typed e τ i c m σ Γ Δ τ s e inr intT τ i locks e sctx item typed Γ Δ τ s switch e c m σ false m σ Global Instance sctx typed PathTyped envs rettype K rettype K sctx item K curry3 sctx item typed Inductive esctx item typed Γ env K Δ memenv K τ s list type K esctx item K type K rettype K Prop CDoE typed τ esctx item typed Γ Δ τ s τ false None CReturnE typed τ esctx item typed Γ Δ τ s ret τ true Some τ CIfE typed τ b s1 s2 c1 m σ1 c2 m σ2 m σ τ b TVoid Γ Δ τ s s1 c1 m σ1 Γ Δ τ s s2 c2 m σ2 rettype union m σ1 m σ2 m σ esctx item typed Γ Δ τ s if s1 else s2 S baseT τ b c1 c2 m σ CSwitchE typed τ i s c m σ Γ Δ τ s s c m σ esctx item typed Γ Δ τ s switch s intT τ i false m σ Global Instance esctx item typed PathTyped envs type K rettype K esctx item K curry3 esctx item typed Inductive ctx item typed Γ env K Δ memenv K τ s list type K ctx item K focustype K focustype K Prop CStmt typed Es cm σ1 cm σ2 Γ Δ τ s Es cm σ1 cm σ2 ctx item typed Γ Δ τ s CStmt Es Stmt type cm σ1 Stmt type cm σ2 CLocal typed o τ c m σ Δ o τ ctx item typed Γ Δ τ s CLocal o τ Stmt type c m σ Stmt type c m σ CExpr typed e Ee τ cm σ Γ Δ τ s e inr τ locks e Γ Δ τ s Ee τ cm σ ctx item typed Γ Δ τ s CExpr e Ee Expr type τ Stmt type cm σ CFun typed E f σ s τ σ Γ f Some σ s τ Γ Δ τ s E inr τ inr σ ctx item typed Γ Δ τ s CFun E Fun type f Expr type σ CParams typed f σ s os cm σ σ Γ f Some σ s σ Δ os σ s rettype match cm σ σ ctx item typed Γ Δ τ s CParams f zip os σ s Stmt type cm σ Fun type f Global Instance ctx item typed PathTyped envs focustype K focustype K ctx item K curry3 ctx item typed Inductive ctx typed Γ s env K memenv K ctx K focustype K focustype K Prop ctx nil typed 2 τ f ctx typed Γ s τ f τ f ctx cons typed 2 Ek k τ f1 τ f2 τ f3 Γ s locals k 2 Ek τ f1 τ f2 ctx typed Γ s k τ f2 τ f3 ctx typed Γ s Ek k τ f1 τ f3 Global Instance ctx typed PathTyped env K memenv K focustype K focustype K ctx K ctx typed Inductive direction typed Γ env K Δ memenv K direction K rettype K Prop Down typed cm τ direction typed Γ Δ cm τ Up typed m τ direction typed Γ Δ false m τ Top typed c v τ Γ Δ v τ direction typed Γ Δ v c Some τ Goto typed l cm τ direction typed Γ Δ l cm τ Throw typed n cm τ direction typed Γ Δ n cm τ Switch typed mx cm τ direction typed Γ Δ mx cm τ Global Instance direction typed Typed env K memenv K rettype K direction K curry direction typed Inductive focus typed Γ env K Δ memenv K τ s list type K focus K focustype K Prop Stmt typed d s cm σ Γ Δ τ s s cm σ Γ Δ d cm σ focus typed Γ Δ τ s Stmt d s Stmt type cm σ Expr typed e τ Γ Δ τ s e inr τ focus typed Γ Δ τ s Expr e Expr type τ Call typed f vs σ s σ Γ f Some σ s σ Γ Δ vs σ s focus typed Γ Δ τ s Call f vs Fun type f Return typed f σ s σ v Γ f Some σ s σ Γ Δ v σ focus typed Γ Δ τ s Return f v Fun type f UndefExpr typed E e τ lr τ Γ Δ τ s e τ lr Γ Δ τ s E τ lr inr τ focus typed Γ Δ τ s Undef UndefExpr E e Expr type τ UndefBranch typed Es Ω v τ m σ Γ Δ Ω Γ Δ v τ Γ Δ τ s Es τ m σ focus typed Γ Δ τ s Undef UndefBranch Es Ω v Stmt type m σ Global Instance focus typed Typed envs focustype K focus K curry3 focus typed Global Instance state typed Typed env K focustype K state K λ Γ S σ f τ f let State k φ m S in Γ m locals k 2 φ τ f Γ m k τ f σ f Γ m Definition funenv prevalid Γ env K Δ memenv K δ funenv K map Forall λ f s τ s τ cm τ Γ f Some τ s τ Forall type complete Γ τ s Γ Δ τ s s cm τ rettype match cm τ τ gotos s labels s throws valid 0 s δ Global Instance funenv valid Valid env K memenv K funenv K λ ΓΔ δ let Γ Δ ΓΔ in funenv prevalid Γ Δ δ dom funset env f Γ dom funset δ End typing Section properties Context EnvSpec K Implicit Types Γ env K Implicit Types o index Implicit Types Δ memenv K Implicit Types m mem K Implicit Types e expr K Implicit Types s stmt K Implicit Types τ σ type K Implicit Types m τ m σ option type K Implicit Types τ lr lrtype K Implicit Types a addr K Implicit Types v val K Implicit Types ν lrval K Implicit Types Ei ectx item K Implicit Types E ectx K Implicit Types Es sctx item K Implicit Types Ee esctx item K Implicit Types Ek ctx item K Implicit Types k ctx K Implicit Types d direction K Lemma SLocal typed Γ Δ τ s τ s c m σ Γ τ Γ Δ τ τ s s c m σ Γ Δ τ s local τ s c m σ Proof by constructor Qed Lemma ltype valid inv Γ τ p Γ inl τ p Γ τ p Proof by inversion 1 Qed Lemma rtype valid inv Γ τ Γ inr τ Γ τ Proof by inversion 1 Qed Lemma lval typed inv Γ Δ p τ p Γ Δ inl p inl τ p Γ Δ p τ p Proof by inversion 1 Qed Lemma rval typed inv Γ Δ v τ Γ Δ inr v inr τ Γ Δ v τ Proof by inversion 1 Qed Lemma lrval typed type valid Γ Δ ν τ lr Γ Γ Δ ν τ lr Γ τ lr Proof destruct 2 constructor eauto using val typed type valid ptr typed type valid Qed Lemma expr typed type valid Γ Δ τ s e τ lr Γ Γ τ s Γ Δ τ s e τ lr Γ τ lr Proof induction 3 using expr typed ind decompose Forall hyps repeat match goal with H inl valid inversion H H inr valid inversion H end try constructor eauto 5 using lrval typed type valid type valid ptr type valid unop typed type valid binop typed type valid TBase valid TPtr valid TVoid valid type valid ptr type valid ref seg typed ptr type valid TBase valid inv TPtr valid inv TFun valid inv ret type complete valid assign typed type valid Qed Lemma expr inl typed type valid Γ Δ τ s e τ p Γ Γ τ s Γ Δ τ s e inl τ p Γ τ p Proof eauto using expr typed type valid ltype valid inv Qed Lemma expr inr typed type valid Γ Δ τ s e τ Γ Γ τ s Γ Δ τ s e inr τ Γ τ Proof eauto using expr typed type valid rtype valid inv Qed Lemma rettype true Some valid Γ β σ Γ σ Γ β Some σ Proof done Qed Lemma rettype union type valid Γ m σ1 m σ2 c1 c2 m σ rettype union m σ1 m σ2 m σ Γ c1 m σ1 Γ c2 m σ2 Γ c2 m σ Proof destruct 1 eauto Qed Lemma stmt typed type valid Γ Δ τ s s mc τ Γ Γ τ s Γ Δ τ s s mc τ Γ mc τ Proof by induction 3 eauto eauto using expr inr typed type valid rettype union type valid rettype true Some valid Qed Lemma lrval typed weaken Γ1 Γ2 Δ1 Δ2 ν τ lr Γ1 Γ1 Δ1 ν τ lr Γ1 Γ2 Δ1 ₘ Δ2 Γ2 Δ2 ν τ lr Proof destruct 2 typed constructor eauto using val typed weaken ptr typed weaken Qed Lemma expr typed weaken Γ1 Γ2 Δ1 Δ2 τ s1 τ s2 e τ lr Γ1 Γ1 Δ1 τ s1 e τ lr Γ1 Γ2 Δ1 ₘ Δ2 τ s1 prefix of τ s2 Γ2 Δ2 τ s2 e τ lr Proof intros He σ s induction He using expr typed ind typed constructor erewrite 1 size of weaken by eauto eauto using lrval typed weaken lookup weaken type valid weaken lookup app l Some ref typed weaken ref seg typed weaken lockset valid weaken type complete weaken Qed Lemma ectx item typed weaken Γ1 Γ2 Δ1 Δ2 τ s1 τ s2 Ei τ lr σ lr Γ1 Γ1 Δ1 τ s1 Ei τ lr σ lr Γ1 Γ2 Δ1 ₘ Δ2 τ s1 prefix of τ s2 Γ2 Δ2 τ s2 Ei τ lr σ lr Proof destruct 2 typed constructor eauto using type valid weaken expr typed weaken lookup weaken Forall2 impl ref seg typed weaken ref typed weaken type complete weaken Qed Lemma ectx typed weaken Γ1 Γ2 Δ1 Δ2 τ s1 τ s2 E τ lr σ lr Γ1 Γ1 Δ1 τ s1 E τ lr σ lr Γ1 Γ2 Δ1 ₘ Δ2 τ s1 prefix of τ s2 Γ2 Δ2 τ s2 E τ lr σ lr Proof intros HE revert τ lr HE induction E intros typed inversion all typed constructor eauto using ectx item typed weaken Qed Lemma stmt typed weaken Γ1 Γ2 Δ1 Δ2 τ s1 τ s2 s cm τ Γ1 Γ1 Δ1 τ s1 s cm τ Γ1 Γ2 Δ1 ₘ Δ2 τ s1 prefix of τ s2 Γ2 Δ2 τ s2 s cm τ Proof intros Hs revert τ s2 induction Hs typed constructor erewrite 1 size of weaken by eauto eauto using expr typed weaken type valid weaken unfold typed stmt typed in simpl in eauto using prefix of cons Qed Lemma sctx item typed weaken Γ1 Γ2 Δ1 Δ2 τ s1 τ s2 Es cm τ cm σ Γ1 Γ1 Δ1 τ s1 Es cm τ cm σ Γ1 Γ2 Δ1 ₘ Δ2 τ s1 prefix of τ s2 Γ2 Δ2 τ s2 Es cm τ cm σ

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