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 type_classes
    change T with valid Valid T Γ end Ltac typed constructor intros match goal with typed Typed T Γ let T eval hnf in T Γ in econstructor change T with typed Typed T Γ path typed PathTyped T Γ let T eval hnf in T Γ in econstructor change T with path typed PathTyped T Γ end Ltac valid inversion H match type of H with valid Valid T Γ let T eval hnf in T Γ in inversion H clear H simplify equality try change T with valid Valid T Γ in end Ltac typed inversion H match type of H with typed Typed T Γ let T eval hnf in T Γ in inversion H clear H simplify equality try change T with typed Typed T Γ in path typed PathTyped T Γ let T eval hnf in T Γ in inversion H clear H simplify equality try change T with path typed PathTyped T Γ in end Ltac typed inversion all repeat match goal with H x first is var x fail 1 typed inversion H idtac by typed inversion H H x first is var x fail 1 typed inversion H idtac by typed inversion H end Section typed Context Typed E T V Lemma Forall2 Forall typed Γ vs τ s τ Γ vs τ s Forall τ τ s Γ vs τ Proof induction 1 inversion 1 subst eauto Qed End typed Section type check Context TypeCheckSpec E T V P Lemma type check None Γ x τ P Γ type check Γ x None Γ x τ Proof intro rewrite type check correct by done congruence Qed Lemma type check sound Γ x τ P Γ type check Γ x Some τ Γ x τ Proof intro by rewrite type check correct by done Qed Lemma type check complete Γ x τ P Γ Γ x τ type check Γ x Some τ Proof intro by rewrite type check correct by done Qed Lemma typed unique Γ x τ1 τ2 P Γ Γ x τ1 Γ x τ2 τ1 τ2 Proof intro rewrite type check correct by done congruence Qed Lemma mapM type check sound Γ xs τ s P Γ mapM type check Γ xs Some τ s Γ xs τ s Proof rewrite mapM Some induction 2 eauto using type check sound Qed Lemma mapM type check complete Γ xs τ s P Γ Γ xs τ s mapM type check Γ xs Some τ s Proof rewrite mapM Some induction 2 eauto using type check complete Qed End type check Section type of Context TypeOfSpec E T V Lemma type of typed Γ x τ Γ x τ Γ x type of x Proof intros erewrite type of correct eauto Qed Lemma typed unique alt Γ x τ1 τ2 Γ x τ1 Γ x τ2 τ1 τ2 Proof intros H τ1 H τ2 apply type of correct in H τ1 apply type of correct in H τ2 congruence Qed

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


  • Module types
    env f Γ Instance env insert fun K Insert funname list type K type K env K λ f τ s τ Γ mk env env t Γ f τ s τ env f Γ Instance env delete compound K Delete tag env K λ t Γ mk env delete t env t Γ env f Γ Instance env delete fun K Delete funname env K λ f Γ mk env env t Γ delete f env f Γ Well formed types Not all pseudo types are valid C types in particular circular unions and structs like struct t struct t x are not excluded The predicate type valid Γ describes that a type is valid with respect to Γ That means recursive occurrences of unions and structs are always guarded by a pointer The predicate env valid describes that an environment is valid Section types Context K Set k1 k2 K Decision k1 k2 Implicit Types Γ Σ env K Implicit Types τ type K Implicit Types τ p ptr type K Implicit Types τ s list type K Implicit Types τ ps list ptr type K Implicit Types τ b base type K Implicit Types τ i int type K Implicit Types t tag Implicit Types f funname Inductive type valid Γ type K Prop TBase valid τ b base type valid Γ τ b type valid Γ baseT τ b TArray valid τ n type valid Γ τ n 0 type valid Γ τ n TCompound valid c t is Some Γ t type valid Γ compoundT c t with ptr type valid Γ ptr type K Prop TAny ptr valid ptr type valid Γ TAny TBase ptr valid τ b base type valid Γ τ b ptr type valid Γ baseT τ b TArray ptr valid τ n type valid Γ τ n 0 ptr type valid Γ τ n TCompound ptr valid c t ptr type valid Γ compoundT c t TFun ptr valid τ s τ Forall ptr type valid Γ TType τ s ptr type valid Γ TType τ ptr type valid Γ τ s τ with base type valid Γ base type K Prop TVoid valid base type valid Γ voidT TInt valid τ i base type valid Γ intT τ i TPtr valid τ p ptr type valid Γ τ p base type valid Γ τ p Global Instance type valid Valid env K type K type valid Global Instance ptr type valid Valid env K ptr type K ptr type valid Global Instance base type valid Valid env K base type K base type valid Lemma TBase valid Γ τ b Γ τ b Γ baseT τ b Proof by constructor Qed Lemma TArray valid Γ τ n Γ τ n 0 Γ τ n Proof by constructor Qed Lemma TCompound valid Γ c t is Some Γ t Γ compoundT c t Proof by constructor Qed Lemma TAny ptr valid Γ Γ TAny Proof constructor Qed Lemma TBase ptr valid Γ τ b Γ τ b Γ baseT τ b PT Proof by constructor Qed Lemma TArray ptr valid Γ τ n Γ τ n 0 Γ τ n PT Proof by constructor Qed Lemma TCompound ptr valid Γ c t Γ compoundT c t PT Proof by constructor Qed Lemma TFun ptr valid Γ τ s τ Γ TType τ s Γ TType τ Γ τ s τ Proof by constructor Qed Lemma TVoid valid Γ Γ voidT BT Proof by constructor Qed Lemma TInt valid Γ τ i Γ intT τ i BT Proof by constructor Qed Lemma TPtr valid Γ τ p Γ τ p Γ τ p BT Proof by constructor Qed Lemma TBase valid inv Γ τ b Γ baseT τ b Γ τ b Proof by inversion clear 1 Qed Lemma TArray valid inv Γ τ n Γ τ n Γ τ n 0 Proof by inversion clear 1 Qed Lemma TArray valid inv type Γ τ n Γ τ n Γ τ Proof by inversion clear 1 Qed Lemma TArray valid inv size Γ τ n Γ τ n n 0 Proof by inversion clear 1 Qed Lemma TArray ptr valid inv size Γ τ n Γ TType τ n n 0 Proof by inversion clear 1 Qed Lemma TCompound valid inv Γ c t Γ compoundT c t is Some Γ t Proof by inversion clear 1 Qed Lemma TBase ptr valid inv Γ τ b Γ baseT τ b PT Γ τ b Proof by inversion clear 1 Qed Lemma TArray ptr valid inv type Γ τ n Γ τ n PT Γ τ Proof by inversion clear 1 Qed Lemma TFun valid inv Γ τ s τ Γ τ s τ Γ TType τ s Γ TType τ Proof by inversion 1 Qed Lemma TFun valid inv args Γ τ s τ Γ τ s τ Γ TType τ s Proof by inversion 1 Qed Lemma TFun valid inv ret Γ τ s τ Γ τ s τ Γ TType τ Proof by inversion 1 Qed Lemma TPtr valid inv Γ τ p Γ τ p BT Γ τ p Proof by inversion clear 1 Qed Fixpoint type valid dec Γ τ Decision Γ τ with ptr type valid dec Γ τ p Decision Γ τ p with ptr type valid dec aux Γ τ Decision Γ TType τ with base type valid dec Γ τ b Decision Γ τ b Proof refine match τ with baseT τ b cast if decide Γ τ b τ n cast if and decide n 0 decide Γ τ compoundT c t cast if decide is Some Γ t end clear type valid dec ptr type valid dec ptr type valid dec aux base type valid dec abstract first by constructor by inversion 1 refine match τ p with TAny left TType τ cast if decide Γ TType τ τ s τ cast if and decide Forall ptr type valid Γ TType τ s decide Γ TType τ end clear type valid dec ptr type valid dec base type valid dec ptr type valid dec aux abstract repeat match goal with H rewrite Forall fmap in H end first done by constructor by inversion 1 refine match τ with baseT τ b cast if decide Γ τ b τ n cast if and decide n 0 decide Γ τ compoundT left end clear type valid dec ptr type valid dec base type valid dec ptr type valid dec aux abstract first by constructor by inversion 1 refine match τ b with τ p cast if decide Γ τ p left end BT clear type valid dec ptr type valid dec base type valid dec ptr type valid dec aux abstract first by repeat constructor by inversion 1 Defined Global Existing Instance type valid dec Global Existing Instance base type valid dec Global Existing Instance ptr type valid dec Lemma type valid inv Γ P Prop τ Γ τ match τ with baseT τ Γ τ P P τ n Γ τ n 0 P P compoundT c t is Some Γ t P P end Proof destruct 1 eauto Qed Lemma type valid ptr type valid Γ τ Γ τ Γ TType τ Proof by destruct 1 constructor Qed Lemma types valid ptr types valid Γ τ s Γ τ s Γ TType τ s Proof induction 1 csimpl eauto using type valid ptr type valid Qed Inductive type complete Γ env K type K Prop TBase complete τ b type complete Γ baseT τ b TArray complete τ n type complete Γ τ n TCompound complete c t is Some Γ t type complete Γ compoundT c t Global Instance type complete dec Γ τ Decision type complete Γ τ Proof refine match τ with compoundT t cast if decide is Some Γ t left end abstract first by constructor by inversion 1 Defined Lemma type valid complete Γ τ Γ τ type complete Γ τ Proof by destruct 1 constructor Qed Lemma type complete valid Γ τ Γ TType τ type complete Γ τ Γ τ Proof by do 2 inversion 1 constructor Qed Lemma types complete valid Γ τ s Γ TType τ s Forall type complete Γ τ s Γ τ s Proof induction 2 decompose Forall eauto using type complete valid Qed Global Instance PartialOrder relation env K Proof split split done intros split etransitivity eauto by intros f equal apply anti symmetric Qed Lemma env wf wf relation env K Proof intros Γ c Γ f revert Γ f induction map wf Γ c as Γ c IH intros Γ f induction map wf Γ f as Γ f IHf constructor intros Γ c Γ f H Γ cut Γ c Γ c Γ c Γ c Γ f Γ f intros eauto destruct H Γ as H Γ destruct subseteq inv L Γ c Γ c simplify equality auto right repeat split auto by contradict H Γ Qed Lemma lookup compound weaken Γ1 Γ2 t τ s Γ1 t Some τ s Γ1 Γ2 Γ2 t Some τ s Proof by intros apply lookup weaken env t Γ1 Qed Lemma lookup fun weaken Γ1 Γ2 f τ s τ Γ1 f Some τ s τ Γ1 Γ2 Γ2 f Some τ s τ Proof by intros apply lookup weaken env f Γ1 Qed Lemma lookup compound weaken is Some Γ1 Γ2 t is Some Γ1 t Γ1 Γ2 is Some Γ2 t Proof intros τ s exists τ s eauto using lookup compound weaken Qed Lemma lookup insert compound Γ t τ s t τ s Γ t Some τ s Proof apply lookup insert Qed Lemma lookup insert compound ne Γ t t τ s t t t τ s Γ t Γ t Proof apply lookup insert ne env t Γ Qed Lemma lookup fun compound Γ f τ s τ f τ s τ Γ f Some τ s τ Proof apply lookup insert Qed Lemma lookup fun compound ne Γ f f τ s τ f f f τ s τ Γ f Γ f Proof apply lookup insert ne env f Γ Qed Lemma insert fun id Γ f τ s τ Γ f Some τ s τ f τ s τ Γ Γ Proof destruct Γ intros unfold insert env insert fun f equal by apply insert id Qed Lemma delete compound subseteq compat Γ1 Γ2 t Γ1 Γ2 delete t Γ1 delete t Γ2 Proof intros split by apply delete subseteq compat done Qed Lemma delete compound subseteq Γ t is Some Γ t delete t Γ Γ Proof split apply delete subseteq done Qed Lemma delete compound subset Γ t is Some Γ t delete t Γ Γ Proof split by apply delete compound subseteq intros by destruct delete subset env t Γ t Qed Lemma delete compound subset alt Γ t τ s Γ t Some τ s delete t Γ Γ Proof eauto using delete compound subset Qed Lemma insert compound subseteq Γ t τ s Γ t None Γ t τ s Γ Proof split by apply insert subseteq done Qed Lemma insert fun subseteq Γ f τ s τ Γ f None Γ f τ s τ Γ Proof split done by apply insert subseteq Qed Lemma type valid weaken help Γ1 Γ2 τ Γ1 τ env t Γ1 env t Γ2 Γ2 τ with ptr type valid weaken help Γ1 Γ2 τ p Γ1 τ p env t Γ1 env t Γ2 Γ2 τ p with base type valid weaken help Γ1 Γ2 τ b Γ1 τ b env t Γ1 env t Γ2 Γ2 τ b Proof unfold valid base type valid type valid in destruct 1 constructor eauto eapply lookup weaken is Some env t eauto unfold valid base type valid type valid ptr type valid in destruct 1 econstructor eauto using Forall impl unfold valid base type valid ptr type valid type valid in destruct 1 econstructor eauto Qed Lemma type valid weaken Γ1 Γ2 τ Γ1 τ Γ1 Γ2 Γ2 τ Proof intros eapply type valid weaken help eauto Qed Lemma ptr type valid weaken Γ1 Γ2 τ p Γ1 τ p Γ1 Γ2 Γ2 τ p Proof intros eapply ptr type valid weaken help eauto Qed Lemma base type valid weaken Γ1 Γ2 τ b Γ1 τ b Γ1 Γ2 Γ2 τ b Proof intros eapply base type valid weaken help eauto Qed Lemma type valid strict weaken Γ Σ τ Γ τ Γ Σ Σ τ Proof intros eapply type valid weaken strict include eauto Qed Lemma types valid weaken Γ Σ τ s Γ τ s Γ Σ Σ τ s Proof eauto using Forall impl type valid weaken Qed Lemma ptr types valid weaken Γ Σ τ ps Γ τ ps Γ Σ Σ τ ps Proof eauto using Forall impl ptr type valid weaken Qed Lemma types valid strict weaken Γ Σ τ s Γ τ s Γ Σ Σ τ s Proof eauto using Forall impl type valid strict weaken Qed Lemma type complete weaken Γ Σ τ type complete Γ τ Γ Σ type complete Σ τ Proof intros constructor eauto eapply lookup weaken is Some env t eauto Qed Lemma types complete weaken Γ Σ τ s Forall type complete Γ τ s Γ Σ Forall type complete Σ τ s Proof induction 1 eauto using type complete weaken Qed Inductive env valid Valid env K env empty valid env insert compound valid Γ t τ s Γ Γ τ s τ s Γ t None t τ s Γ env insert fun valid Γ f τ s τ Γ Γ TType τ s Γ TType τ Γ f None f τ s τ Γ Global Existing Instance env valid Lemma env valid delete Γ t τ s Γ Γ t Some τ s Γ Γ delete t Γ Γ τ s τ s Γ Proof intros H Γ Ht induction H Γ as Γ t τ s H Γ IH H τ s Hlen Γ f τ s τ IH done destruct decide t t as rewrite lookup insert compound in Ht simplify equality by exists Γ repeat split simpl rewrite delete insert by done rewrite lookup insert compound ne in Ht by done destruct IH as Γ auto exists Γ split ands auto transitivity delete t Γ auto using delete compound subseteq compat insert compound subseteq destruct IH Ht as Γ exists Γ split ands auto transitivity delete t Γ auto using delete compound subseteq compat insert fun subseteq Qed Lemma env valid lookup subset Γ t τ s Γ Γ t Some τ s Γ Γ Γ Γ τ s τ s Γ Proof intros destruct env valid delete Γ t τ s as Γ auto exists Γ split ands auto eapply strict transitive r eauto using delete compound subset Qed Lemma env valid lookup Γ t τ s Γ Γ t Some τ s Γ τ s Proof intros destruct env valid lookup subset Γ t τ s as eauto using types valid strict weaken Qed Lemma env valid lookup lookup Γ t τ s i τ Γ Γ t Some τ s τ s i Some τ Γ τ Proof intros Ht Hi eapply Forall lookup 1 Hi eauto using env valid lookup Qed Lemma env valid lookup singleton Γ t τ Γ Γ t Some τ Γ τ Proof intros by apply env valid lookup lookup Γ t τ 0 τ Qed Lemma env valid fun valid Γ f τ s τ Γ Γ f Some τ s τ Γ TType τ s Γ TType τ Proof intros H Γ Hf induction H Γ as Γ f τ s τ IH done naive solver eauto using ptr type valid weaken ptr types valid weaken insert compound subseteq destruct decide f f as rewrite lookup fun compound lookup fun compound ne in Hf by done naive solver eauto using ptr type valid weaken ptr types valid weaken insert fun subseteq Qed Lemma env valid args valid Γ f τ s τ Γ Γ f Some τ s τ Γ TType τ s Proof eapply env valid fun valid Qed Lemma env valid ret valid Γ f τ s τ Γ Γ f Some τ s τ Γ TType τ Proof eapply env valid fun valid Qed End types A very inefficient decision procedure for wellformedness of environments It checks wellformedness by trying all permutations of the environment This decision procedure is not intended to be used for computation Section env valid dec Context K Set Definition env f valid Γ env K Prop map Forall λ τ s τ Γ TType τ s τ 1 Γ TType τ s τ 2 env f Γ Inductive env c valid list tag list type K Prop env nil valid env c valid env cons valid Γ c t τ s env c valid Γ c mk env map of list Γ c τ s τ s t Γ c 1 env c valid t τ s Γ c Lemma env c valid nodup Γ c env c valid Γ c NoDup Γ c 1 Proof by induction 1 csimpl constructor Qed Global Instance env c valid dec Γ c Decision env c valid Γ c Proof refine fix go Γ c match Γ c return Decision env c valid Γ c with left s τ s Γ c cast if and4 decide mk env map of list Γ c τ s decide τ s decide s Γ c 1 go Γ c end clear go first by constructor by inversion 1 Defined Lemma env c valid correct Γ Γ env f valid Γ Γ c map to list env t Γ ₚ Γ c env c valid Γ c Proof split intros H Γ split intros split eauto using env valid args valid env valid ret valid

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

  • Module type_environment
    size of char Γ si bit size of Γ intT IntType si char rank char bits Proof rewrite bit size of int by apply int width char Qed Lemma bit size of int same kind Γ τ i1 τ i2 rank τ i1 rank τ i2 bit size of Γ intT τ i1 bit size of Γ intT τ i2 Proof destruct τ i1 τ i2 intros simplify equality by rewrite bit size of int Qed Lemma bit size of array Γ τ n bit size of Γ τ n n bit size of Γ τ Proof unfold bit size of by rewrite size of array Nat mul assoc Qed Lemma bit size of struct Γ t τ s Γ Γ t Some τ s bit size of Γ structT t sum list field bit sizes Γ τ s Proof unfold bit size of field bit sizes intros erewrite size of struct by eauto elim field sizes Γ τ s csimpl auto with lia Qed Lemma bit size of fields Γ τ s Γ Forall2 λ τ sz bit size of Γ τ sz τ s field bit sizes Γ τ s Proof intros H Γ unfold bit size of field bit sizes induction size of fields Γ τ s H Γ simpl constructor auto using Nat mul le mono nonneg r with lia Qed Lemma bit size of union Γ t τ s Γ Γ t Some τ s Forall λ τ bit size of Γ τ bit size of Γ unionT t τ s Proof intros H τ s apply size of union in H τ s auto unfold bit size of induction H τ s constructor auto using Nat mul le mono nonneg r with lia Qed Lemma bit size of union lookup Γ t τ s i τ Γ Γ t Some τ s τ s i Some τ bit size of Γ τ bit size of Γ unionT t Proof intros unfold bit size of apply Nat mul le mono nonneg r eauto using size of union lookup with lia Qed Lemma bit size of union singleton Γ t τ Γ Γ t Some τ bit size of Γ τ bit size of Γ unionT t Proof intros by apply bit size of union lookup Γ t τ 0 Qed Lemma ptr bit size of alt Γ τ p ptr bit size of Γ τ p ptr size of Γ τ p char bits Proof destruct τ p simpl unfold bit size of lia Qed Lemma field bit sizes weaken Γ1 Γ2 τ s Γ1 Γ1 τ s Γ1 Γ2 field bit sizes Γ1 τ s field bit sizes Γ2 τ s Proof unfold field bit sizes auto using fields sizes weaken with f equal Qed Lemma field bit sizes length Γ τ s Γ length field bit sizes Γ τ s length τ s Proof symmetry by eapply Forall2 length bit size of fields Qed Lemma field bit sizes nil Γ Γ field bit

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

  • Module architecture_spec
    arch rank A char rank ARank CharRank char signedness arch char signedness A short rank ARank ShortRank int rank ARank IntRank long rank ARank LongRank longlong rank ARank LongLongRank ptr rank ARank PtrRank char bits arch char bits A rank size arch size A rank subseteq k1 k2 k1 c rank k2 c rank endianize λ if arch big endian A then reverse else id deendianize λ if arch big endian A then reverse else id Instance arch int env IntEnv arch rank A int arithop ok op x τ i1 y τ i2 let τ i int promote τ i1 int promote τ i2 in int pre arithop ok op int pre cast τ i x int pre cast τ i y τ i int arithop op x τ i1 y τ i2 let τ i int promote τ i1 int promote τ i2 in int pre arithop op int pre cast τ i x int pre cast τ i y τ i int shiftop ok op x τ i1 y τ i2 let τ i int promote τ i1 in int pre shiftop ok op int pre cast τ i x y τ i int shiftop op x τ i1 y τ i2 let τ i int promote τ i1 in int pre shiftop op int pre cast τ i x y τ i int cast ok int pre cast ok int cast int pre cast Instance IntCodingSpec arch rank A Proof split by apply arch char bits ge 8 by apply arch size char intros k1 k2 by apply Nat2Z inj le arch size preserving by repeat split red apply bool decide unpack vm compute by intros by apply bool decide unpack by apply bool decide unpack by apply bool decide unpack by apply bool decide unpack

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

  • Module architectures
    data models LLP64 is used by Microsoft Windows x86 64 and IA 64 Definition llp64 architecture sizes Proof refine arch char bits 8 arch size k match k with CharRank 1 ShortRank 2 IntRank LongRank 4 PtrRank LongLongRank 8 end arch align k match k with CharRank 1 ShortRank 2 IntRank LongRank 4 PtrRank LongLongRank 8 end by apply bool decide unpack vm compute Defined LP64 is used by most

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

  • Module separation
    Proof intros Hxy by rewrite sep right id x Hxy sep union difference by eauto using sep subseteq valid l Qed Properties of the half operation Lemma sep splittable valid x sep splittable x sep valid x Proof intros rewrite sep union half x by done auto using sep union valid sep disjoint half Qed Lemma sep half valid x sep splittable x sep valid ½ x Proof eauto using sep disjoint valid l sep disjoint half Qed Lemma sep half subseteq x sep splittable x ½ x x Proof rewrite sep subseteq spec intros exists ½ x eauto using sep disjoint half sep union half eq sym Qed Lemma sep splittable empty sep splittable Proof rewrite sep right id by auto using sep empty valid apply sep splittable union auto using sep disjoint empty l sep empty valid Qed Lemma sep half empty ½ A Proof apply sep positive l with ½ eauto using sep union half sep disjoint half sep splittable empty Qed Lemma sep half empty rev x sep splittable x ½ x x Proof intros Hx by rewrite sep union half x Hx sep left id by auto using sep empty valid Qed Lemma sep splittable half x sep splittable x sep splittable ½ x Proof eauto using sep splittable weaken sep half subseteq Qed Properties of the sep unmapped predicate Lemma sep unmapped empty alt x x sep unmapped x Proof intros by apply sep unmapped empty Qed Lemma sep unmapped union l x y x y sep unmapped x y sep unmapped x Proof eauto using sep unmapped weaken sep union subseteq l Qed Lemma sep unmapped union r x y x y sep unmapped x y sep unmapped y Proof eauto using sep unmapped weaken sep union subseteq r Qed Lemma sep unmapped union x y x y sep unmapped x y sep unmapped x sep unmapped y Proof naive solver eauto using sep unmapped union l sep unmapped union r sep unmapped union 2 Qed Lemma sep unmapped half x sep splittable x sep unmapped ½ x sep unmapped x Proof intros rewrite sep union half x at 2 by done rewrite sep unmapped union by eauto using sep disjoint half tauto Qed Lemma sep unmapped half 1 x sep splittable x sep unmapped ½ x sep unmapped x Proof intros by apply sep unmapped half Qed Lemma sep unmapped difference x y x y sep unmapped x sep unmapped y x sep unmapped y Proof intros rewrite sep union difference x y at 2 by done by rewrite sep unmapped union by eauto using sep disjoint difference Qed Lemma sep unmapped difference 1 x y x y sep unmapped x sep unmapped y x sep unmapped y Proof intros by apply sep unmapped difference x y Qed Lemma sep unmapped difference 2 x y x y sep unmapped y sep unmapped y x Proof intros by apply sep unmapped difference x y Qed Properties of the sep unshared predicate Lemma sep unshared empty sep unshared Proof rewrite sep unshared spec intros destruct sep inhabited A as x eauto using sep disjoint empty l Qed Lemma sep unshared ne empty x sep unshared x x Proof intros by apply sep unshared empty Qed Lemma sep unshared valid x sep unshared x sep valid x Proof rewrite sep unshared spec by intros Qed Lemma sep disjoint unshared unmapped x y x y sep unshared x sep unmapped y Proof rewrite sep unshared spec naive solver Qed Lemma sep unshared weaken x y sep unshared x x y sep unshared y Proof rewrite sep unshared spec naive solver eauto using sep disjoint weaken l sep subseteq valid r Qed Lemma sep unshared union l x y x y sep unshared x sep unshared x y Proof eauto using sep unshared weaken sep union subseteq l Qed Lemma sep unshared union r x y x y sep unshared y sep unshared x y Proof eauto using sep unshared weaken sep union subseteq r Qed Properties of disjointness of lists Lemma sep disjoint list valid xs xs Forall sep valid xs Proof induction 1 constructor eauto using sep disjoint valid l Qed Lemma sep disjoint list singleton x x sep valid x Proof intros rewrite disjoint list cons disjoint list nil simpl intuition eauto using sep disjoint empty r sep disjoint valid l Qed Lemma sep disjoint list double x y x y x y Proof rewrite disjoint list cons sep disjoint list singleton simpl split intros Hxy by rewrite sep right id in Hxy intros rewrite sep right id eauto using sep disjoint valid r Qed Lemma sep disjoint list double 1 x y x y x y Proof by rewrite sep disjoint list double Qed Lemma sep disjoint list double 2 x y x y x y Proof by rewrite sep disjoint list double Qed Lemma sep disjoint list symmetric x y x y y x Proof by rewrite sep disjoint list double Qed Hint Immediate sep disjoint list double 1 sep disjoint list symmetric Hint Resolve sep disjoint list double 2 Lemma sep subseteq spec x y x y z y x z x z Proof setoid rewrite sep disjoint list double apply sep subseteq spec Qed Lemma sep associative x y z x y z x y z x y z Proof rewrite disjoint list cons simpl intros Hxyz Hyz rewrite sep right id in Hxyz Hyz by eauto using sep disjoint valid l by apply sep associative Qed Lemma sep commutative x y x y x y y x Proof rewrite sep disjoint list double apply sep commutative Qed Lemma sep cancel l x y z z x z y z x z y x y Proof eauto using sep cancel l sep disjoint list double 1 Qed Lemma sep cancel r x y z x z y z x z y z x y Proof intros rewrite sep commutative z by done eauto using sep cancel l Qed Lemma sep positive l x y x y x y x Proof rewrite sep disjoint list double eauto using sep positive l Qed Lemma sep positive r x y x y x y y Proof rewrite sep disjoint list double apply sep positive r Qed Lemma sep union subseteq l x y x y x x y Proof rewrite sep disjoint list double apply sep union subseteq l Qed Lemma sep union subseteq r x y x y y x y Proof rewrite sep disjoint list double apply sep union subseteq r Qed Lemma sep union subseteq l transitive x y z y z x y x y z Proof intros transitivity y auto using sep union subseteq l Qed Lemma sep union subseteq r transitive x y z y z x z x y z Proof intros transitivity z auto using sep union subseteq r Qed Lemma sep preserving l x y z z y x y z x z y Proof rewrite sep subseteq spec setoid rewrite sep disjoint list double intros z1 exists z1 rewrite sep associative auto using sep disjoint move r Qed Lemma sep preserving r x y z y z x y x z y z Proof rewrite sep disjoint list double intros rewrite sep commutative z by eauto using sep disjoint weaken l apply sep preserving l auto Qed Lemma sep preserving x y z z y z x y z z x z y z Proof rewrite sep disjoint list double intros transitivity x z auto using sep preserving r apply sep preserving l eauto using sep disjoint weaken l Qed Lemma sep reflecting l x y z z x z y z x z y x y Proof rewrite sep subseteq spec setoid rewrite sep disjoint list double intros z1 exists z1 split eauto 2 using sep disjoint lr apply sep cancel l z auto using sep disjoint move l by rewrite sep associative by eauto using sep disjoint lr sep disjoint move l Qed Lemma sep reflecting r x y z x z y z x z y z x y Proof intros rewrite sep commutative z by done eauto using sep reflecting l Qed Lemma sep disjoint difference x y x y x y x Proof rewrite sep disjoint list double apply sep disjoint difference Qed Lemma sep splittable union x x x sep splittable x x Proof rewrite sep disjoint list double apply sep splittable union Qed Lemma sep disjoint half x sep splittable x ½ x ½ x Proof rewrite sep disjoint list double apply sep disjoint half Qed Lemma sep splittable spec x sep splittable x y x y y y y Proof split exists ½ x eauto using sep disjoint half sep union half eq sym intros auto using sep splittable union Qed Lemma sep union half distr x y x y sep splittable x y ½ x y ½ x ½ y Proof rewrite sep disjoint list double apply sep union half distr Qed Lemma sep half unique x y y y x y y y ½ x Proof intros assert sep splittable y y by auto using sep splittable union assert sep splittable y by eauto using sep splittable weaken sep union subseteq l by rewrite sep union half distr sep union half by done Qed Lemma sep union list valid xs xs sep valid xs Proof induction 1 simpl auto using sep empty valid sep union valid Qed Lemma sep disjoint contains aux xs1 xs2 xs2 xs1 contains xs2 xs1 xs1 xs2 Proof intros Hxs2 Hxs revert Hxs2 induction Hxs as x xs1 xs2 IH x1 x2 xs x xs1 xs2 IH xs1 xs2 xs3 IH1 IH2 simpl in auto using sep reflexive sep empty valid rewrite disjoint list cons intros destruct IH as IH1 IH2 auto eauto 7 using sep preserving l sep disjoint weaken r rewrite disjoint list cons simpl intros split ands apply sep disjoint move l symmetry eauto using sep disjoint rl rewrite sep commutative by symmetry eauto using sep disjoint rl eauto using sep disjoint move r eauto using sep disjoint rr done rewrite sep associative x1 sep commutative x1 x2 by eauto using sep disjoint rl assert x2 x1 xs rewrite sep commutative x1 by eauto 2 using sep disjoint rr by apply sep disjoint move l rewrite sep associative by eauto 2 using sep disjoint rr by apply sep reflexive sep union valid rewrite disjoint list cons intros destruct IH as IH1 IH2 eauto using sep union subseteq r transitive intros destruct IH1 auto destruct IH2 auto split auto by transitivity xs2 Qed Lemma sep disjoint contains xs1 xs2 xs2 xs1 contains xs2 xs1 Proof intros by apply sep disjoint contains aux xs1 xs2 Qed Lemma sep union list subseteq xs1 xs2 xs2 xs1 contains xs2 xs1 xs2 Proof intros by apply sep disjoint contains aux Qed Global Instance Proper Permutation A iff disjoint list Proof intros xs1 xs2 Hxs split intros apply sep disjoint contains xs2 xs1 done by rewrite Hxs apply sep disjoint contains xs1 xs2 done by rewrite Hxs Qed Lemma sep list preserving xs1 xs2 xs2 xs1 xs2 xs1 xs2 Proof intros Hxs2 induction 1 simpl inversion clear Hxs2 auto using sep preserving sep reflexive sep empty valid Qed Lemma sep disjoint empty alt xs xs xs Proof rewrite disjoint list cons intuition auto using sep disjoint empty l eauto using sep disjoint empty l sep union list valid Qed Lemma sep disjoint alt x y xs x y xs x y x y xs Proof rewrite disjoint list cons simpl split intros eauto using sep disjoint rl sep disjoint move r eauto using sep disjoint lr sep disjoint move l Qed Lemma sep disjoint list alt xs1 xs2 xs1 xs2 xs1 xs1 xs2 Proof revert xs2 induction xs1 as x xs1 IH simpl intros xs2 rewrite sep disjoint empty alt disjoint list nil naive solver rewrite Permutation middle IH Permutation swap sep disjoint alt rewrite disjoint list cons x naive solver Qed Lemma sep unmapped union l x y x y sep unmapped x y sep unmapped x Proof eauto using sep unmapped weaken sep union subseteq l Qed Lemma sep unmapped union r x y x y sep unmapped x y sep unmapped y Proof eauto using sep unmapped weaken sep union subseteq r Qed Properties of Global Instance PreOrder Proof unfold sep disjoint le split red naive solver Qed Global Instance Proper impl disjoint list Proof intros xs1 xs2 Hxs red rewrite sep disjoint empty alt xs1 sep disjoint empty alt xs2 by apply Hxs Qed Global Instance Proper ₚ ₚ iff Proof unfold sep disjoint le impl intros xs1 xs2 Hxs12 xs3 xs4 Hxs34 by setoid rewrite Hxs12 setoid rewrite Hxs34 Qed Global Instance Proper z Proof unfold sep disjoint le impl intros z xs1 xs2 Hxs12 y subst rewrite sep disjoint alt naive solver Qed Global Instance Proper flip flip z Proof by intros z x y Hxy simpl in rewrite Hxy Qed Global Instance Proper Proof unfold sep disjoint le intros xs1 xs2 Hxs12 xs3 xs4 Hxs34 y apply impl transitive with y xs2 xs3 rewrite commutative xs3 app comm cons rewrite sep disjoint list alt naive solver rewrite app comm cons sep disjoint list alt naive solver Qed Global Instance Proper flip flip flip Proof by intros x1 y1 Hxy1 x2 y2 Hxy2 simpl in rewrite Hxy1 Hxy2 Qed Lemma sep disjoint cons le inj x y xs x y x xs y xs Proof intros change x xs y xs by f equiv Qed Properties of Lemma sep disjoint equiv alt xs1 xs2 xs1 xs2 x x xs1 x xs2 Proof unfold sep disjoint equiv sep disjoint le naive solver Qed Global Instance Equivalence Proof split done by intros by intros x y z split transitivity y Qed Global Instance AntiSymmetric Proof by split Qed Global Instance Proper iff disjoint list Proof intros Hxs1 Hxs2 split by rewrite Hxs1 by rewrite Hxs2 Qed Global Instance Proper iff Proof intros x y z x4 split intro transitivity x auto transitivity z auto transitivity y auto transitivity x4 auto Qed Global Instance Proper ₚ ₚ iff Proof intros xs1 xs2 Hxs12 xs3 xs4 Hxs34 rewrite sep disjoint equiv alt by setoid rewrite Hxs12 setoid rewrite Hxs34 Qed Global Instance Proper Proof intros Hxs1 Hxs2 subst split by rewrite Hxs1 by rewrite Hxs2 Qed Global Instance Proper Proof intros Hxs1 Hxs2 Hxs3 Hxs4 split by rewrite Hxs1 Hxs3 by rewrite Hxs2 Hxs4 Qed Lemma sep disjoint cons inj x y xs x y x xs y xs Proof intros change x xs y xs by f equiv Qed Lemma sep disjoint equiv empty xs xs xs Proof by split intros y rewrite Permutation swap y sep disjoint empty alt Qed Lemma sep disjoint le union x y xs x y xs x y xs Proof intros y rewrite Permutation swap y sep disjoint alt x y sep disjoint list double by intros Qed Lemma sep disjoint equiv union x y xs x y x y xs x y xs Proof split auto using sep disjoint le union intros y rewrite Permutation swap y sep disjoint alt x y sep disjoint list double tauto Qed Lemma sep disjoint le union list xs1 xs2 xs1 xs2 xs1 xs2 Proof intros y rewrite Permutation swap y Permutation middle sep disjoint list alt tauto Qed Lemma sep disjoint le union list singleton xs xs xs Proof by rewrite sep disjoint le union list right id L Qed Lemma sep disjoint equiv union list xs1 xs2 xs1 xs1 xs2 xs1 xs2 Proof split auto using sep disjoint le union list intros y rewrite Permutation swap y Permutation middle sep disjoint list alt tauto Qed Lemma sep disjoint equiv union list singleton xs xs xs xs Proof intros by rewrite sep disjoint equiv union list right id L Qed Lemma sep disjoint equiv difference x y xs x y y xs x y x xs Proof intros by rewrite sep disjoint equiv union sep union difference by auto using sep disjoint difference Qed Lemma sep subseteq disjoint le x y xs x y y xs x xs Proof rewrite sep subseteq spec intros z intros y rewrite sep disjoint equiv union by done intros Hyxz apply sep disjoint contains Hyxz solve contains Qed Lemma sep difference distr l x y z z x x y x y z x z y Proof intros apply sep cancel l z by apply sep disjoint difference sep union subseteq l transitive by rewrite sep disjoint le union sep disjoint equiv difference assert z x z y by by rewrite sep disjoint equiv difference by rewrite sep associative sep union difference by auto using sep union subseteq l transitive Qed Lemma sep difference distr r x y z z y x y x y z x y z Proof intros assert y z x apply disjoint list cons z rewrite sep disjoint equiv difference eauto by rewrite sep commutative x sep difference distr l by eauto Qed Lemma sep disjoint equiv half x xs sep splittable x ½ x ½ x xs x xs Proof intros by rewrite sep disjoint equiv union sep union half by auto using sep disjoint half Qed Properties with respect to vectors Lemma sep disjoint equiv insert n xs vec A n i fin n x vinsert i x xs x delete fin to nat i vec to list xs Proof induction xs as x xs IH inv fin i simpl done intros i by rewrite Permutation swap IH Qed Lemma sep disjoint equiv delete n xs vec A n i fin n xs i delete fin to nat i vec to list xs xs Proof by rewrite sep disjoint equiv insert vlookup insert self Qed Lemma sep union delete n xs vec A n i fin n xs xs i delete fin to nat i vec to list xs xs Proof induction xs as x xs IH inversion clear 1 inv fin

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

  • Module separation_instances
    Qcopp injective Qcplus 1 Hx split ands auto by ring simplify by apply Qcplus le mono l 1 x 1 Qcopp le compat by intros x Qed Record counter A Set Set Counter counter count Qc counter perm A Add Printing Constructor counter Arguments Counter Arguments counter perm Arguments counter count Local Notation p 1 counter count p Local Notation p 2 counter perm p Instance Injective2 Counter A Proof by injection 1 Qed Lemma counter injective projections A x y counter A x 1 y 1 x 2 y 2 x y Proof by destruct x y simpl intros Qed Instance counter ops A Set SeparationOps A SeparationOps counter A sep valid x sep valid x 2 sep unmapped x 2 x 1 0 sep unshared x 2 0 x 1 sep empty Counter 0 sep disjoint x y x 2 y 2 sep unmapped x 2 x 1 0 sep unmapped y 2 y 1 0 sep unshared x 2 y 2 0 x 1 y 1 sep union x y Counter x 1 y 1 x 2 y 2 sep subseteq x y x 2 y 2 sep unmapped y 2 x 2 y 1 x 1 sep unmapped x 2 x 1 0 sep unshared y 2 0 y 1 sep difference x y Counter x 1 y 1 x 2 y 2 sep splittable x sep splittable x 2 sep unmapped x 2 x 1 0 sep unshared x 2 0 x 1 sep half x Counter x 1 2 ½ x 2 sep unmapped x sep unmapped x 2 x 1 0 sep unshared x sep unshared x 2 0 x 1 Proof solve decision Defined Instance counter separation A Set Separation A Separation counter A Proof split destruct sep inhabited A as x exists Counter 0 x sep unfold naive solver intros x y Hxy Hx Hy Hxy repeat split eauto using sep disjoint valid l intros Hx rewrite Qcplus 0 r x 1 transitivity x 1 y 1 eauto using sep unshared union l apply Qcplus le mono l Hy eauto using sep disjoint unshared unmapped sep unfold intros x y split ands eauto using sep union valid intros apply Qcplus nonpos nonpos naive solver eauto using sep unmapped union l sep unmapped union r sep unfold intros x split ands eauto using sep disjoint empty l by rewrite sep left id Qcplus 0 l by done sep unfold intros by rewrite sep left id Qcplus 0 l by done sep unfold intros x y split ands auto by rewrite sep commutative Qcplus comm by done sep unfold intros by rewrite sep commutative Qcplus comm by done sep unfold intros Hxyz split ands eauto using sep disjoint ll intros assert sep unmapped y 2 apply sep disjoint unshared unmapped with x 2 z 2 auto rewrite sep commutative by eauto using sep disjoint ll by apply sep disjoint move r rewrite Qcplus 0 r x 1 transitivity x 1 y 1 z 1 auto apply Hxyz assert x 2 z 2 y 2 rewrite sep commutative by eauto using sep disjoint ll by apply sep disjoint move r rewrite sep permute by done eauto using sep unshared union l apply Qcplus le mono r Qcplus le mono l auto sep unfold intros split ands eauto using sep disjoint move l intros apply Qcplus nonpos nonpos eauto using sep unmapped union l sep unmapped union r sep disjoint lr by rewrite sep associative Qcplus assoc by eauto using sep disjoint lr sep disjoint move l sep unfold intros by rewrite sep associative Qcplus assoc by done sep unfold intros x y Hxy apply injective2 in Hxy destruct Hxy as Hxy Hxy apply counter injective projections simpl eauto using sep positive l apply anti symmetric eauto using sep unmapped union l sep unmapped empty alt apply Qcplus le mono r y 1 rewrite Qcplus 0 l Hxy eauto using sep positive r sep unmapped empty alt sep unfold intros simplify equality apply counter injective projections eauto using sep cancel l sep unfold intros x y Hx Hy split ands auto using sep union subseteq l rewrite sep union difference alt by done intros rewrite Qcplus 0 r x 1 at 2 apply Qcplus le mono l auto sep unfold intros x y Hxy rewrite sep union difference by done split ands auto using sep disjoint difference intros replace y 1 x 1 with x 1 y 1 by ring apply Qcopp le compat 0 proj1 Qcle minus iff auto replace x 1 y 1 x 1 with y 1 by ring auto sep unfold intros x y apply counter injective projections simpl auto using sep union difference ring sep unfold intros x split ands auto using sep splittable union intros apply Qcplus nonpos nonpos eauto using sep unmapped union l sep unfold intros x y Hxy split ands eauto using sep splittable weaken intros transitivity y 1 eauto using sep unshared weaken sep disjoint unshared unmapped sep disjoint difference sep unfold intros x assert sep unmapped ½ x 2 x 1 2 0 intros rewrite Qcmult 0 l 2 apply Qcmult le mono nonneg r auto using sep unmapped half 1 split ands auto using sep disjoint half rewrite sep union half by done intros rewrite Qcmult plus distr l apply Qcmult nonneg nonneg auto using Qcplus nonneg nonneg sep unfold intros x apply counter injective projections simpl transitivity x 1 2 2 ring by rewrite Qcmult inv r Qcmult 1 r by apply sep union half sep unfold intros x y apply counter injective projections simpl ring by apply sep union half distr sep unfold intros split ands auto using sep unmapped valid intros exfalso eauto using sep unshared unmapped sep unfold auto using sep unmapped empty sep unfold intros eauto using sep unmapped weaken sep unfold intros split ands eauto using sep unmapped union 2 intros apply Qcplus nonpos nonpos eauto using sep unmapped union l sep unmapped union r sep unfold

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

  • Module permissions
    perm kind spec γ Qed Lemma perm locked lock γ Some Writable perm kind γ perm locked perm lock γ true Proof by destruct perm kind spec γ Qed Lemma perm locked unlock γ perm locked perm unlock γ false Proof by destruct γ as Qed Lemma perm lock valid γ sep valid γ Some Writable perm kind γ sep valid perm lock γ Proof destruct perm kind spec γ repeat sep unfold intuition Qed Lemma perm lock empty γ perm lock γ γ Proof by destruct γ as Qed Lemma perm lock unmapped γ Some Writable perm kind γ sep unmapped γ sep unmapped perm lock γ Proof destruct perm kind spec γ repeat sep unfold naive solver Qed Lemma perm lock mapped γ sep unmapped perm lock γ sep unmapped γ Proof destruct γ as repeat sep unfold intuition Qed Lemma perm lock unshared γ sep unshared γ sep unshared perm lock γ Proof destruct γ as repeat sep unfold intuition Qed Lemma perm unlock lock γ sep valid γ Some Writable perm kind γ perm unlock perm lock γ γ Proof by destruct perm kind spec γ Qed Lemma perm unlock unlock γ perm unlock perm unlock γ perm unlock γ Proof by destruct γ as Qed Lemma perm unlock valid γ sep valid γ sep valid perm unlock γ Proof destruct γ as repeat sep unfold naive solver Qed Lemma perm unlock empty γ sep valid γ perm unlock γ γ Proof destruct γ as repeat sep unfold naive solver Qed Lemma perm unlock unmapped γ sep unmapped γ sep unmapped perm unlock γ Proof destruct γ as repeat sep unfold intuition Qed Lemma perm unlock mapped γ sep valid γ sep unmapped perm unlock γ sep unmapped γ Proof destruct γ as repeat sep unfold naive solver Qed Lemma perm unlock unshared γ sep unshared γ sep unshared perm unlock γ Proof destruct γ as repeat sep unfold intuition Qed Lemma perm unlock shared γ sep valid γ sep unshared perm unlock γ sep unshared γ Proof destruct γ as repeat sep unfold intuition Qed Lemma perm unshared γ sep valid γ Some Locked perm kind γ sep unshared γ Proof destruct perm kind spec γ repeat sep unfold intuition Qed Lemma perm mapped γ Some Readable perm kind γ sep unmapped γ Proof destruct perm kind spec γ repeat sep unfold naive solver Qed Lemma perm unmapped γ sep valid γ perm kind γ Some Existing sep unmapped γ Proof destruct perm kind spec γ repeat sep unfold naive solver Qed Lemma perm None unmapped γ sep valid γ perm kind γ None sep unmapped γ Proof destruct perm kind spec γ repeat sep unfold naive solver Qed Lemma perm token subseteq γ sep valid γ Some Writable perm kind γ perm token γ Proof assert x x 0 0 x 0 intros x change x 0 with x 0 by rewrite Qcplus 0 r rewrite strict spec alt unfold perm token destruct perm

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