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 memory

simplify mem equality simplify mem equality by solve mem disjoint Free indexes in a memory A memory index is free if it contains no contents Definition is free m mem b index Prop m b None Lemma is free lookup None m b is free m b m b None Proof done Qed Hint Resolve is free lookup None mem Lemma is free Forall lookup None m bs Forall is free m bs Forall λ b m b None bs Proof done Qed Hint Resolve is free Forall lookup None mem Lemma is free lookup Some m b v is free m b m b Some v Proof unfold is free congruence Qed Lemma is free dom C Collection index C m b b dom C m is free m b Proof apply not elem of dom Qed Lemma is free subseteq m1 m2 mem b is free m2 b m1 m2 is free m1 b Proof apply lookup weaken None Qed Hint Immediate is free subseteq mem Lemma is free union m1 m2 b is free m1 m2 b is free m1 b is free m2 b Proof apply lookup union None Qed Lemma is free union 2 m1 m2 b is free m1 b is free m2 b is free m1 m2 b Proof by rewrite is free union Qed Hint Resolve is free union 2 mem Lemma is free insert m b b v is free b v m b is free m b b b Proof apply lookup insert None Qed Lemma is free insert 2 b b v m is free m b b b is free b v m b Proof rewrite is free insert auto Qed Hint Resolve is free insert 2 mem We lift the notion of free indexes to lists of indexes Inductive is free list m mem list index Prop is free nil is free list m is free cons b bs b bs is free m b is free list m bs is free list m b bs Hint Constructors is free list mem We prove that the inductive definition is free list m bs is equivalent to all bs being free and the list bs containing no duplicates Lemma is free list nodup m bs is free list m bs NoDup bs Proof induction 1 by constructor Qed Lemma is free list free m bs is free list m bs Forall is free m bs Proof induction 1 firstorder Qed Hint Resolve is free list nodup is free list free mem Lemma is free list make m bs NoDup bs Forall is free m bs is free list m bs Proof induction 1 inversion 1 auto with mem Qed Lemma is free list subseteq m1 m2 bs m1 m2 is free list m2 bs is free list m1 bs Proof induction 2 eauto with mem Qed Lemma is free insert list m b l b fst l is free m b is free insert list l m b

Original URL path: http://robbertkrebbers.nl/research/ch2o/fossacs2013/memory.html (2015-08-10)

Open archived version from archive - Module expressions

int 20 Delimit Scope expr scope with E Bind Scope expr scope with expr Arguments ELoad expr scope Arguments EBinOp expr scope expr scope Notation var x EVar x at level 10 expr scope Notation val v EVal v at level 10 expr scope Notation int x EVal int x Z expr scope Notation ptr b EVal ptr b N expr scope Notation null EVal null expr scope Notation load e ELoad e at level 10 expr scope Notation e1 op e2 EBinOp op e1 e2 at level 50 next at level 50 expr scope Infix EBinOp PlusOp expr scope Infix EBinOp MultOp expr scope Infix EBinOp MinusOp expr scope Infix EBinOp LeOp expr scope Infix EBinOp EqOp expr scope Infix div EBinOp DivOp at level 35 nat scope Infix mod EBinOp ModOp at level 35 nat scope Reserved Notation e at level 20 Fixpoint expr lift e expr expr match e with var x var S x val v val v load e load e e1 op e2 e1 op e2 end E where e expr lift e expr scope Fixpoint expr load free e expr Prop match e with var True val True load False e1 e2 expr load free e1 expr load free e2 end E Instance expr load free dec e Decision expr load free e Proof refine fix go e match e return Decision expr load free e with var left val left load right e1 e2 cast if and go e1 go e2 end E simpl tauto Defined Fixpoint expr vars e expr listset nat match e with var x x val load e expr vars e e1 e2 expr vars e1 expr vars e2 end E Hint Extern 1 expr load free assumption typeclass instances Hint Extern 100 expr load free e apply bool decide unpack vm compute exact I typeclass instances Hint Extern 1 expr vars assumption typeclass instances Hint Extern 100 expr vars apply bool decide unpack vm compute exact I typeclass instances Semantics We define the semantics of expressions by structural recursion Reserved Notation e at level 2 format e Fixpoint expr eval e expr ρ stack m mem option value match e with var x b ρ x Some ptr b V val v Some v load e v e ρ m b is ptr v m b e1 op e2 v1 e1 ρ m v2 e2 ρ m value eval binop op v1 v2 end E where e expr eval e Theorems Evaluation of expressions is preserved under extending the memory and the stack Lemma expr eval weaken mem e ρ m1 m2 v m1 m2 e ρ m1 Some v e ρ m2 Some v Proof revert v induction e simpl intros simplify option equality auto Qed Lemma expr eval weaken stack e ρ ρ m v e ρ m Some v e ρ ρ m Some v Proof revert v induction e simpl intros simplify option equality auto rewrite lookup app l by simplify option equality

Original URL path: http://robbertkrebbers.nl/research/ch2o/fossacs2013/expressions.html (2015-08-10)

Open archived version from archive - Module statements

assign the result SCall Some e f es calls f with arguments es and assigns the result to e The constructor SBlock represents a local variable declaration Since we treat variables in De Bruijn style it does not include a name of the variable Inductive stmt Type SAssign expr expr stmt SCall option expr funname list expr stmt SSkip stmt SGoto label stmt SReturn option expr stmt SBlock stmt stmt SComp stmt stmt stmt SLabel label stmt stmt SWhile expr stmt stmt SIf expr stmt stmt stmt Notation funenv funmap stmt Instance stmt eq dec s1 s2 stmt Decision s1 s2 Proof solve decision Defined We use the scope stmt scope for notations of statements Delimit Scope stmt scope with S Bind Scope stmt scope with stmt Open Scope stmt scope Arguments SBlock S Arguments SComp S S Arguments SLabel S Arguments SWhile E S Arguments SIf E S S Infix SAssign at level 60 stmt scope Notation call f es SCall None f es E at level 60 stmt scope Notation e call f es SCall Some e E f es E at level 60 format e call f es stmt scope Notation skip SSkip stmt scope Notation goto l SGoto l at level 10 stmt scope Notation ret e SReturn e E at level 10 stmt scope Notation block s SBlock s at level 10 stmt scope Infix SComp at level 80 right associativity stmt scope Infix SLabel at level 81 right associativity stmt scope Notation while e s SWhile e s at level 10 format while e s stmt scope Notation IF e then s1 else s2 SIf e s1 s2 stmt scope Instance Injective SBlock Proof congruence Qed Instance stmt gotos Gotos stmt fix go s stmt let Gotos go in match s with block s gotos s s1 s2 gotos s1 gotos s2 s gotos s while s gotos s IF then s1 else s2 gotos s1 gotos s2 goto l l end Instance stmt labels Labels stmt fix go s stmt let Labels go in match s with block s labels s s1 s2 labels s1 labels s2 l s l labels s while s labels s IF then s1 else s2 labels s1 labels s2 end Program contexts We first define the data type sctx item of singular program contexts for all constructors of stmt that do not require additional annotations That is for all constructors besides local variable declarations SBlock Inductive sctx item Type CCompL stmt sctx item CCompR stmt sctx item CLabel label sctx item CWhile expr sctx item CIfL expr stmt sctx item CIfR expr stmt sctx item Instance sctx item eq dec E1 E2 sctx item Decision E1 E2 Proof solve decision Defined Bind Scope stmt scope with sctx item Notation s CCompL s at level 80 stmt scope Notation s CCompR s at level 80 stmt scope Notation l CLabel l at level 81 stmt scope Notation while e CWhile e at level 10 format while e stmt

Original URL path: http://robbertkrebbers.nl/research/ch2o/fossacs2013/statements.html (2015-08-10)

Open archived version from archive - Module state

d simpl intuition Qed Definition down up dec d s down d s up d s match d with left I right I right I l decide rel l labels s end Tactic Notation discriminate down up hyp H repeat match type of H with up progress simpl in H down progress simpl in H True clear H False destruct H l destruct H solve stmt elem of l solve decompose elem of H end Tactic Notation discriminate down up repeat match goal with H up discriminate down up H H down discriminate down up H end The type focus describes the part of the program that is currently focused An execution state state is a focus equipped 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 the execution should be performed 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 Inductive focus Stmt direction stmt focus Call funname list value focus Return option value focus Record state State SCtx ctx SFoc focus SMem mem Add Printing Constructor state Instance focus eq dec φ1 φ2 focus Decision φ1 φ2 Proof solve decision Defined Instance state eq dec S1 S2 state Decision S1 S2 Proof solve decision Defined Theorems Our definition of execution state allows many incorrect states For example while in a Call state the context should always contain a CCall as its last element whereas this is not enforced by the definition of execution states We define the proposition ctx wf k φ k φ which states that starting at a state with focus φ in context k it is valid to build a state with focus φ in context k In the file smallstep we will prove that our operational semantics preserves well formed statements This is the key property to prove that if State k Stmt d s m reduces to State k Stmt d s m then we have s s We restrict to a type of focuss simple focus that contains less information than focus so as to obtain a more powerful induction principle for ctx wf Inductive simple focus Stmt stmt simple focus Call funname simple focus Return simple focus Definition to simple focus φ focus simple focus match φ with Stmt s Stmt s Call f Call f Return Return end Coercion to simple focus focus simple focus Definition simple focus related φ1 φ2 simple focus Prop match φ1 φ2 with Stmt s1 Stmt s2 s1 s2 Call f1 Call f2 f1 f2 True end Local Infix simple focus related at level 80 Arguments simple focus related Instance Reflexive simple focus related Proof by intros Qed Section ctx wf Context δ funenv Inductive ctx wf k ctx φ simple focus ctx

Original URL path: http://robbertkrebbers.nl/research/ch2o/fossacs2013/state.html (2015-08-10)

Open archived version from archive - Module smallstep

δ s n bsteps δ s n only parsing C scope Restricting small step reduction Reduction in our language consists of moving the focus on the substatement that is being executed Often and in particular for the soundness proofs of our axiomatic semantics we want to restrict this movement we want the focus to remain below a certain point A reduction δ S1 s k S2 is only allowed if S2 s program context is below k Definition cstep in ctx δ k relation state λ S1 S2 δ S1 s S2 suffix of k SCtx S2 Notation δ S1 s k S2 cstep in ctx δ k S1 S2 at level 80 S2 at level 70 k at level 80 format δ S1 s k S2 C scope Notation δ s k cstep in ctx δ k only parsing C scope Notation δ S1 s k S2 rtc δ s k S1 S2 at level 80 S2 at level 70 k at level 80 format δ S1 s k S2 C scope Notation δ s k rtc δ s k only parsing C scope Notation δ S1 s k n S2 bsteps δ s k n S1 S2 at level 80 S2 at level 70 k at level 80 n at level 1 format δ S1 s k n S2 C scope Notation δ s k n bsteps δ s k n only parsing C scope Instance cstep subrel suffix of δ k1 k2 PropHolds suffix of k1 k2 subrelation δ s k2 δ s k1 Proof intros S1 S2 split done by transitivity k2 Qed Instance cstep subrel δ k subrelation δ s k δ s Proof firstorder Qed Instance cstep subrel nil δ subrelation δ s δ s Proof intros S1 S2 split done solve suffix of Qed Tactics We implement some tactics to perform and to invert reduction steps We define a hint database cstep that is used by these tactics Hint Resolve expr eval weaken mem expr eval weaken stack cstep Hint Resolve finmap subseteq union l finmap subseteq union r cstep Hint Resolve Forall2 impl cstep Hint Extern 0 is writable red eauto with mem cstep The small step semantics is non determistic on entering a block or calling a function variables are given a memory cell that has an unspecified free index and is initialized with an unspecified value The following lemmas are deterministic variants that will be included in the cstep hint database to automatically perform reduction steps Lemma cstep in block fresh δ k s m let b fresh index m in δ State k Stmt block s m s State CBlock b k Stmt s b int 0 m V Proof constructor apply is free fresh index Qed Lemma cstep label block down fresh δ l k s m l labels s let b fresh index m in δ State k Stmt l block s m s State CBlock b k Stmt l s b int 0 m V Proof

Original URL path: http://robbertkrebbers.nl/research/ch2o/fossacs2013/smallstep.html (2015-08-10)

Open archived version from archive - Module assertions

ext MemIndep P MemExt Q MemExt P Q Proof solve assert Qed Instance assert and mem ext MemExt P MemExt Q MemExt P Q Proof solve assert Qed Instance assert or mem ext MemExt P MemExt Q MemExt P Q Proof solve assert Qed Instance assert forall mem ext A x A MemExt P x MemExt assert forall P Proof solve assert Qed Instance assert exist mem ext A x A MemExt P x MemExt assert exist P Proof solve assert Qed Proofs of other useful properties Instance Commutative A Proof solve assert Qed Instance Commutative A Proof solve assert Qed Instance Associative A Proof solve assert Qed Instance Idempotent A Proof solve assert Qed Instance Commutative A Proof solve assert Qed Instance Associative A Proof solve assert Qed Instance Idempotent A Proof solve assert Qed Instance LeftId True A A Proof solve assert Qed Instance RightId True A A Proof solve assert Qed Instance LeftAbsorb False A A Proof solve assert Qed Instance RightAbsorb False A A Proof solve assert Qed Instance LeftId False A A Proof solve assert Qed Instance RightId False A A Proof solve assert Qed Instance LeftAbsorb True A A Proof solve assert Qed Instance RightAbsorb True A A Proof solve assert Qed Instance LeftId True A A Proof solve assert Qed Instance RightAbsorb True A A Proof intros solve assert Qed Lemma Prop as assert impl P Q Prop P Q A P Q A Proof solve assert Qed Lemma Prop as assert not P Prop P A P A Proof solve assert Qed Lemma Prop as assert and P Q Prop P Q A P Q A Proof solve assert Qed Lemma Prop as assert or P Q Prop P Q A P Q A Proof solve assert Qed Lemma assert true intro P assert P True A Proof solve assert Qed Lemma assert false elim P assert False A P Proof solve assert Qed Lemma assert and l P Q assert P Q A P Proof solve assert Qed Lemma assert and r P Q assert P Q A Q Proof solve assert Qed Lemma assert and intro P Q1 Q2 P Q1 P Q2 P Q1 Q2 A Proof solve assert Qed Lemma assert and elim l P1 P2 Q P1 Q P1 P2 A Q Proof solve assert Qed Lemma assert and elim r P1 P2 Q P2 Q P1 P2 A Q Proof solve assert Qed Lemma assert forall intro A P Q A assert x P Q x P x Q x A Proof solve assert Qed Lemma assert forall specialize A P A assert Q x P x Q x P x A Q Proof solve assert Qed Lemma assert exists intro A P Q A assert x P Q x P x Q x A Proof solve assert Qed Lemma assert exists elim A P A assert Q x P x Q x P x A Q Proof solve assert Qed Lemma assert or l P Q assert P P Q A Proof solve assert Qed Lemma assert or r P Q assert P P Q A Proof solve assert Qed Lemma assert or elim P Q R assert P R Q R P Q A R Proof solve assert Qed Lemma assert and exists A P Q A assert P x Q x A x P Q x A Proof solve assert Qed Lemma assert exists and A P A assert Q x P x Q A x P x Q A Proof solve assert Qed The assertion e v asserts that the expression e evaluates to v and e asserts that the expression e evaluates to an arbitrary value in other words e does not impose undefined behavior Notation vassert value assert Definition assert expr e expr vassert λ v Assert λ ρ m e ρ m Some v Infix assert expr at level 60 assert scope Notation assert expr only parsing assert scope Notation e assert expr e only parsing assert scope Notation v λ e assert expr e v only parsing assert scope Notation e v e v A at level 60 format e assert scope Notation assert expr only parsing assert scope Instance assert expr mem ext e v MemExt e v Proof red unfold assert eauto using expr eval weaken mem Qed Instance assert expr mem indep e expr load free e MemIndep e v Proof intros ρ m1 m2 unfold assert by rewrite expr load free mem indep ρ m1 m2 Qed Instance assert expr mem indep e expr load free e MemIndep e Proof intros ρ m1 m2 v exists v unfold assert in by rewrite expr load free mem indep ρ m2 m1 Qed Instance assert expr stack indep e v expr vars e StackIndep e v Proof intros ρ1 ρ2 m unfold assert by rewrite expr var free stack indep ρ2 ρ1 Qed Instance assert expr stack indep e expr vars e StackIndep e Proof intros ρ1 ρ2 m unfold assert by rewrite expr var free stack indep ρ2 ρ1 Qed Lemma assert expr load e p v load e p load val p v A load load e v A Proof intros ρ m He unfold assert in by rewrite He Qed Lemma assert expr forget e v e v A e A Proof solve assert Qed Notation e true v e v value true v A at level 60 format e true assert scope Notation e false v e v value false v A at level 60 format e false assert scope Definition assert is true Pv vassert assert v Pv v value true v A Definition assert is false Pv vassert assert v Pv v value false v A Definition assert subst a index v value P assert Assert λ ρ m P ρ a v m Notation a v assert subst a v assert scope Instance a v Proper assert subst a v Proof solve assert Qed Lemma assert subst mem indep P MemIndep P a v a v P A P Proof solve assert Qed Lemma assert subst impl P Q a v a v P Q A a v P a v Q A Proof solve assert Qed Lemma assert subst not P a v a v P A a v P A Proof solve assert Qed Lemma assert subst and P Q a v a v P Q A a v P a v Q A Proof solve assert Qed Lemma assert subst or P Q a v a v P Q A a v P a v Q A Proof solve assert Qed Lemma assert subst forall P A assert a v a v x P x A x a v P x A Proof solve assert Qed Lemma assert subst exists P A assert a v a v x P x A x a v P x A Proof solve assert Qed Separation logic connectives The assertion emp asserts that the memory is empty The assertion P Q called separating conjunction asserts that the memory can be split into two disjoint parts such that P holds in the one part and Q in the other The assertion P Q called separating implication or magic wand asserts that if an arbitrary memory is extended with a disjoint part in which P holds then Q holds in the extended memory Definition assert emp assert Assert λ ρ m m Notation emp assert emp assert scope Definition assert sep P Q assert assert Assert λ ρ m m1 m2 m1 m2 m m1 m2 P ρ m1 Q ρ m2 Infix assert sep at level 80 right associativity assert scope Notation assert sep only parsing assert scope Notation P assert sep P only parsing assert scope Notation Q λ P assert sep P Q only parsing assert scope Definition assert wand P Q assert assert Assert λ ρ m1 m2 m1 m2 P ρ m2 Q ρ m1 m2 Infix assert wand at level 90 assert scope Notation assert wand only parsing assert scope Notation P assert wand P only parsing assert scope Notation Q λ P assert wand P Q only parsing assert scope Compatibility of the separation logic connectives with respect to order and equality Instance Proper A Proof solve assert Qed Instance Proper A Proof solve assert Qed Instance Proper flip A Proof solve assert Qed Instance Proper A Proof solve assert Qed Basic properties Lemma assert sep comm 1 P Q P Q A Q P A Proof intros m m1 m2 HP HQ exists m2 m1 by rewrite finmap union comm Qed Instance Commutative A Proof split apply assert sep comm 1 Qed Lemma assert sep left id 1 P emp P A P Proof intros m m1 m2 H Hm1 Hm2 Hm3 unfold assert in subst by rewrite left id Qed Lemma assert sep left id 2 P P emp P A Proof intros m exists mem m repeat split apply left id solve mem disjoint done Qed Instance LeftId emp A A Proof split apply assert sep left id 1 apply assert sep left id 2 Qed Instance RightId emp A A Proof intros rewrite commutative apply left id Qed Instance LeftAbsorb False A A Proof solve assert Qed Instance RightAbsorb False A A Proof solve assert Qed Lemma assert sep assoc 1 P Q R P Q R A P Q R A Proof intros mR mP mQ intuition subst exists mP mQ mR repeat split apply associative solve mem disjoint done exists mQ mR solve mem disjoint Qed Lemma assert sep assoc 2 P Q R P Q R A P Q R A Proof intros mP mQ mR intuition subst exists mP mQ mR repeat split by rewrite associative solve mem disjoint exists mP mQ solve mem disjoint done Qed Instance Associative A Proof split apply assert sep assoc 2 apply assert sep assoc 1 Qed Lemma assert wand 1 P Q R S assert P Q A R P Q R A Proof solve assert Qed Lemma assert wand 2 P Q assert P P Q A Q Proof rewrite commutative A solve assert Qed Lemma assert and sep assoc P Q R assert MemIndep P P Q R A P Q R A Proof solve assert Qed Lemma assert sep and assoc P Q R assert MemIndep R P Q R A P Q R A Proof solve assert Qed The separation conjunction allows us to give an alternative formulation of memory extensibility Lemma mem ext sep true MemExt P P P True A Proof split intros m exists m mem repeat split apply right id solve mem disjoint done intros m1 m2 subst eauto using mem ext finmap subseteq union l Qed Lemma assert sep true mem ext P P P True A MemExt P Proof intros H ρ m1 m2 rewrite H exists m1 m2 m1 repeat split auto by rewrite finmap union difference by apply finmap disjoint difference r Qed Lemma mem ext sep true iff P P P True A MemExt P Proof split intros by apply assert sep true mem ext by apply mem ext sep true Qed Other type class instances for stack independence memory independence and memory extensibility Instance assert emp stack indep StackIndep emp Proof solve assert Qed Instance assert sep stack indep StackIndep P StackIndep Q StackIndep P Q Proof solve assert Qed Instance assert sep mem indep MemIndep P MemIndep Q MemIndep P Q Proof intros m1 m2 m2 m2 subst exists m2 mem repeat split by apply right id solve mem disjoint solve assert solve assert Qed Instance assert sep mem ext 2 MemExt Q MemExt P Q Proof intros m1 m2 m2 m2 subst exists m2 m2 m2 m2 m2 repeat split by rewrite associative finmap union difference solve mem disjoint done apply mem ext with m2 auto with mem Qed Instance assert sep mem ext l MemExt P MemExt P Q Proof intros P Q rewrite commutative P A by apply assert sep mem ext 2 Qed Proofs of other useful properties Lemma assert and sep emp l P Q assert MemIndep P P Q A P emp Q A Proof intro by rewrite assert and sep assoc left id emp A Qed Lemma assert and sep emp r P Q assert MemIndep Q P Q A P Q emp A Proof intro by rewrite commutative P assert and sep emp l Qed Lemma assert sep elim l P1 P2 Q MemExt Q P1 Q P1 P2 A Q Proof intros H by rewrite mem ext sep true H assert true intro Qed Lemma assert sep elim r P1 P2 Q MemExt Q P2 Q P1 P2 A Q Proof rewrite commutative A apply assert sep elim l Qed The assertion Π Ps states that the memory can be split into disjoint parts such that for each part the corresponding assertion in Ps holds Definition assert sep list list assert assert foldr A emp A Notation Π Ps assert sep list Ps at level 20 format Π Ps assert scope Lemma assert sep list alt Ps list assert ρ m Π Ps A ρ m ms m ms list disjoint ms Forall2 λ P assert m P ρ m Ps ms Proof split revert m induction Ps as P Ps IH eexists by repeat constructor intros m1 m2 subst destruct IH m2 as ms trivial subst exists m1 ms repeat constructor trivial by apply finmap disjoint union list r intros m2 Hdisjoint Hassert subst revert Hdisjoint induction Hassert as P m Ps ms IH inversion clear 1 done exists m ms rewrite finmap disjoint union list r intuition Qed Lemma assert sep list alt vec n Ps vec assert n ρ m Π Ps A ρ m ms vec mem n m ms list disjoint ms i Ps i ρ ms i Proof rewrite assert sep list alt split intros ms Hms assert n length ms subst by erewrite Forall2 length vec to list length by eauto exists list to vec ms rewrite vec to list of list by rewrite vec to list of list ms Forall2 vlookup in Hms intros ms exists ms by rewrite Forall2 vlookup Qed Lemma assert sep list alt vec 2 n Ps vec assert n ρ ms vec mem n list disjoint ms i Ps i ρ ms i Π Ps A ρ ms Proof intros apply assert sep list alt vec by exists ms Qed Instance Proper eqlistA assert sep list Proof induction 1 simpl by f equiv Qed The assertion e1 e2 asserts that the memory consists of exactly one cell at address e1 with contents e2 and the assertion e1 asserts that the memory consists of exactly one cell at address e1 with arbitrary contents Definition assert singleton e1 e2 expr assert Assert λ ρ m a v e1 ρ m Some ptr a V e2 ρ m Some v m a v Notation e1 e2 assert singleton e1 e2 A at level 20 assert scope Definition assert singleton e expr assert Assert λ ρ m a v e ρ m Some ptr a V m a v Notation e assert singleton e A at level 20 format e assert scope Lemma assert singleton forget e1 e2 e1 e2 A e1 A Proof solve assert Qed Instance assert singleton stack indep e1 e2 expr vars e1 expr vars e2 StackIndep e1 e2 Proof intros ρ1 ρ2 m a v exists a v by rewrite expr var free stack indep ρ2 ρ1 Qed Instance assert singleton stack indep e expr vars e StackIndep e Proof intros ρ1 ρ2 m a v exists a v by rewrite expr var free stack indep ρ2 ρ1 Qed Lemma assert singleton eval l e1 v1 e2 e1 v1 val v1 e2 A e1 e2 A Proof solve assert Qed Lemma assert singleton eval r e1 v2 e2 e1 val v2 e2 v2 A e1 e2 A Proof solve assert Qed Lemma assert singleton eval e v e v val v A e A Proof solve assert Qed Definition assert assign e1 e2 expr assert Assert λ ρ m a v e1 ρ m Some ptr a V e2 ρ m Some v m a Some v Notation e v assert assign e v A at level 20 assert scope Definition assert assign e expr assert Assert λ ρ m a v e ρ m Some ptr a V m a Some v Notation e assert assign e A at level 20 format e assert scope Lemma assert assign forget e1 e2 e1 e2 A e1 A Proof solve assert Qed Lemma assert singleton assign e1 e2 e1 e2 A e1 e2 A Proof intros ρ a v subst exists a v by rewrite lookup singleton Qed Lemma assert singleton assign e e A e A Proof intros ρ a v subst exists a v by rewrite lookup singleton Qed Lemma assert assign eval l e1 v1 e2 e1 v1 val v1 e2 A e1 e2 A Proof solve assert Qed Lemma assert assign eval r e1 v2 e2 e1 val v2 e2 v2 A e1 e2 A Proof solve assert Qed Lemma assert assign eval e v e v val v A e A Proof solve assert Qed Instance assert assign stack indep e1 e2 expr vars e1 expr vars e2 StackIndep e1 e2 Proof intros ρ1 ρ2 m a v exists a v by rewrite expr var free stack indep ρ2 ρ1 Qed Instance assert assign stack indep e expr vars e StackIndep e Proof intros ρ1 ρ2 m a v exists a v by rewrite expr var free stack indep ρ2 ρ1 Qed Instance assert assign mem ext e1 e2 MemExt e1 e2 Proof intros ρ m1 m2 a v exists a v repeat split eauto using expr eval weaken mem lookup weaken Qed Instance assert assign mem ext e MemExt e Proof intros ρ m1 m2 a v

Original URL path: http://robbertkrebbers.nl/research/ch2o/fossacs2013/assertions.html (2015-08-10)

Open archived version from archive - Module axiomatic

m mf ₜ P s λ False m mf P m looping δ s State Stmt s m mf Proof intros Hax apply looping alt intros S p by destruct ax stmt sound sep P λ False A s m mf S as intuition Qed Lemma ax stmt looping P s m ₜ P s λ False P m looping δ s State Stmt s m Proof intros rewrite right id eq m eapply ax stmt looping sep eauto with mem Qed The Hoare rules We prove that the Hoare rules can be derived from the semantic definition of the Hoare judgment Logical rules Lemma ax stmt weak packed Δ Pd Pd s d down d s Pd d Pd d d up d s Pd d Pd d ax stmt packed Δ s Pd ax stmt packed Δ s Pd Proof intros Hdown Hup Hax n k d m mf S p feed destruct Hax n k d m mf S as m auto by apply Hdown by left apply cstep bsteps preserves stmt in p subst right constructor done by apply Hup done Qed Lemma ax stmt weak Δ J J R R P P Q Q s l l labels s J l J l l l labels s J l J l v R v R v P P Q Q Δ J R P s Q Δ J R P s Q Proof intros apply ax stmt weak packed intros solve assert Qed Lemma ax stmt weak jmp Δ J J R P Q s l l labels s J l J l l l labels s J l J l Δ J R P s Q Δ J R P s Q Proof intros apply ax stmt weak solve assert Qed Lemma ax stmt weak ret Δ J R R P Q s v R v R v Δ J R P s Q Δ J R P s Q Proof intro apply ax stmt weak solve assert Qed Lemma ax stmt weak pre Δ J R P P Q s P P Δ J R P s Q Δ J R P s Q Proof intro apply ax stmt weak solve assert Qed Lemma ax stmt weak post Δ J R P Q Q s Q Q Δ J R P s Q Δ J R P s Q Proof intro apply ax stmt weak solve assert Qed Lemma ax stmt frame packed Δ A Pd s ax stmt packed Δ s Pd ax stmt packed Δ s λ P A P A Pd Proof intros Hax n k d m mf S Hpre p rewrite directed fmap spec in Hpre destruct Hpre as m2 m3 simplify equality feed destruct Hax n k d m3 m2 mf S as m2 auto solve mem disjoint by rewrite associative eq finmap union comm m3 by solve mem disjoint rewrite associative eq left solve mem disjoint by rewrite associative eq rewrite associative eq right constructor auto rewrite directed fmap spec exists m2 m2 intuition apply finmap union comm solve mem disjoint solve mem disjoint Qed Lemma ax stmt frame l Δ J R A P Q s Δ J R P s Q Δ λ l A J l λ v A R v A P s A Q Proof apply ax stmt frame packed Qed Lemma ax stmt frame r Δ J R A P Q s Δ J R P s Q Δ λ l J l A λ v R v A P A s Q A Proof setoid rewrite commutative assert sep A apply ax stmt frame packed Qed Lemma ax stmt frame simple l Δ A P Q s Δ λ False λ False P s Q Δ λ False λ False A P s A Q Proof intros setoid rewrite right absorb False A assert sep A by apply ax stmt frame l Qed Lemma ax stmt frame simple r Δ A P Q s Δ λ False λ False P s Q Δ λ False λ False P A s Q A Proof intros setoid rewrite left absorb False A assert sep A by apply ax stmt frame r Qed Lemma ax stmt and post Δ J R P Q Q s Δ J R P s Q Δ J R P s Q Δ J R P s Q Q Proof intros Hax1 Hax2 n k d m mf S p feed destruct Hax1 n k d m mf S as m d s auto by destruct d intuition by left feed inversion Hax2 n k d m mf State k Stmt d s m mf as m d s auto by destruct d intuition by left simplify equality right constructor auto simplify mem equality destruct d intuition auto by split done Qed Lemma ax stmt or pre Δ J R P P Q s Δ J R P s Q Δ J R P s Q Δ J R P P s Q Proof intros Hax1 Hax2 n k m mf S Hpre p try contradiction destruct Hpre feed destruct Hax1 n k m mf S as m d s auto by left right constructor done by destruct d try left done feed destruct Hax2 n k m mf S as m d s auto by left right constructor done by destruct d try right done feed destruct Hax1 n k l m mf S as m d s auto by left right constructor done by destruct d try right done Qed Lemma ax stmt ex pre Inhabited A Δ J R P A assert Q s x Δ J R P x s Q Δ J R x P x s Q Proof intros Hax n k m mf S H Δ Hpre p try contradiction destruct Hpre as x Hpre feed destruct Hax x n k m mf S as m d s auto by left right constructor done by destruct d done destruct Inhabited A as x feed destruct Hax x n k l m mf S as m d s auto by left right constructor done by destruct d done Qed Lemma ax stmt ex post A Δ J R P Q A assert s x Δ J R P s Q x Δ J R P s x Q x Proof intros Hax n k m mf S H Δ Hpre p try contradiction feed destruct Hax n k m mf S as m d s auto by left right constructor done by destruct d try exists x done feed destruct Hax n k l m mf S as m d s auto by left right constructor done by destruct d try exists x done Qed Lemma ax stmt ex pre alt A Δ R P A assert Q s x Δ λ False R P x s Q Δ λ False R x P x s Q Proof intros Hax n k m mf S H Δ Hpre p try contradiction destruct Hpre as x Hpre feed destruct Hax x n k m mf S as m d s auto by left right constructor done by destruct d done Qed Lemma ax stmt and Prop pre Δ R A Prop P Q s A Δ λ False R P s Q Δ λ False R P A s Q Proof assert P A A A P A as HA by solve assert rewrite HA apply ax stmt ex pre alt Qed Lemma ax stmt top weak Δ P P R R s v R v R v P P Δ ₜ P s R Δ ₜ P s R Proof intros rewrite ax stmt top unfold apply ax stmt weak auto Qed Lemma ax stmt top false pre Δ R s Δ ₜ False s R Proof by intros Qed Lemma ax stmt top and Prop pre Δ A Prop P Q s A Δ ₜ P s Q Δ ₜ P A s Q Proof apply ax stmt and Prop pre Qed Rules for function calls Lemma ax call J R Δ f es Pf A c fcommon Pf vs MemIndep A Δ f Some Pf assert forall2 es vs fpre Pf c vs A A Δ J R assert forall2 es vs fpre Pf c vs call f es mv A fpost Pf c vs mv Proof intros Hf HA n k m mf S H Δ Hpre p discriminate down up specialize HA Hpre destruct Hpre as Hvs Hpre apply assert forall2 correct in Hvs inv csteps p as n p1 p2 left done solve cred inv cstep p1 unfold assert in Hvs simplify expr eval feed destruct ax split ax fun P Pf c vs S n Call f vs CCall None f es k m mf S as m m Hpost p3 intros apply H Δ done by apply stack indep get stack k done by apply bsteps S left done by apply red subrel δ s CCall None f es k inv csteps p3 as n p3 p4 left done solve cred inv cstep p3 last cstep p4 right constructor auto eexists split by apply mem indep m apply stack indep Hpost done Qed Lemma ax call alt J R Δ f es Pf P c fcommon Pf vs MemIndep P vs Δ f Some Pf vs assert forall2 es vs fpre Pf c vs A P vs Δ J R vs assert forall2 es vs fpre Pf c vs call f es vs mv P vs fpost Pf c vs mv Proof intros apply ax stmt ex pre intros vs apply ax stmt ex post with vs auto using ax call Qed Lemma ax call Some J R Δ A B f e es Pf c fcommon Pf vs a v Q MemIndep B Δ f Some Pf assert forall2 es vs A fpre Pf c vs A B mv B A fpost Pf c vs mv A e ptr a mv Some v ptr a a v Q A Δ J R assert forall2 es vs A fpre Pf c vs e call f es Q Proof setoid rewrite commutative A A intros Hf HB HQ n k m mf S H Δ Hpre p discriminate down up specialize HB Hpre destruct Hpre as Hvs m1 m2 Hpre HA subst apply assert forall2 correct in Hvs decompose map disjoint inv csteps p as n p1 p2 left solve mem disjoint solve cred inv cstep p1 unfold assert in Hvs decompose map disjoint simplify expr eval feed destruct ax split ax fun P Pf c vs S n Call f vs CCall Some e f es k m1 m2 mf S as m Hred m Hpost p3 intros apply H Δ done by apply stack indep get stack k solve mem disjoint rewrite associative eq by apply bsteps S rewrite associative eq in Hred left solve mem disjoint by apply red subrel δ s CCall Some e f es k decompose map disjoint edestruct HQ as a v split eapply mem indep eauto exists m m2 repeat split solve mem disjoint eapply stack indep eauto eassumption unfold assert in simplify option equality rewrite associative eq in p3 inv csteps p3 as n p3 p4 left solve mem disjoint solve cred inv cstep p3 last cstep p4 simplify expr eval rewrite insert union l right constructor done simpl done eapply finmap disjoint insert l split solve mem disjoint eapply finmap disjoint Some l eassumption solve mem disjoint Qed Lemma ax stmt packed add funs Δ Δ s Pd f Pf Δ f Some Pf is Some δ f f Pf sf c vs Δ f Some Pf δ f Some sf Δ Δ ₜ Π imap λ i v var i val v vs fpre Pf c vs sf λ mv Π imap λ i var i vs fpost Pf c vs mv ax stmt packed Δ Δ s Pd ax stmt packed Δ s Pd Proof intros H Δ Hax Δ revert s cut f Pf sf n c vs m mf m k bs S Δ f Some Pf δ f Some sf ax funs n Δ Δ m mf alloc params m mf bs vs m fpre Pf c vs get stack k m δ State CParams bs k Stmt sf m s k n S ax valid ax fun P Pf c vs k mf S intros help s Hax n k d m mf S H Δ eapply Hax clear d s Pd k m mf S Hax induction n as n IH using lt wf ind intros f Pf c vs m mf k S Hf p rewrite lookup union Some raw in Hf destruct Hf as eapply H Δ eauto feed inversion H Δ f Pf subst trivial inv csteps p as n p1 p2 left done solve cred inv cstep p1 apply ax funs weaken n in H Δ omega eapply help eauto intros f Pf sf n c vs m mf m k bs S3 Hparams Hpre p1 apply alloc params insert list in Hparams destruct Hparams as subst rewrite insert list union associative eq in p1 decompose is free feed destruct ax split ax stmt P dassert pack top Π imap λ i v var i val v vs fpre Pf c vs λ mv Π imap λ i var i vs fpost Pf c vs mv A n Stmt sf CParams bs k finmap of list zip bs vs m mf S3 as m m S2 Hpost p2 intros eapply Hax Δ eauto simpl rewrite insert list union apply assert alloc params alt auto solve mem disjoint done left done by apply red subrel δ s CParams bs k inv csteps p2 as n3 S3 p2 p3 left done solve cred inv cstep p2 last cstep p3 rewrite finmap union delete list delete list notin mf by by apply is free list free right constructor apply assert free params with vs eauto with mem by auto with mem last cstep p3 rewrite finmap union delete list delete list notin mf by by apply is free list free right constructor apply assert free params with vs eauto with mem by auto with mem Qed Lemma ax stmt add funs Δ Δ J R P Q s f Pf Δ f Some Pf is Some δ f f Pf sf c vs Δ f Some Pf δ f Some sf Δ Δ ₜ Π imap λ i v var i val v vs fpre Pf c vs sf λ mv Π imap λ i var i vs fpost Pf c vs mv Δ Δ J R P s Q Δ J R P s Q Proof apply ax stmt packed add funs Qed Structural rules Lemma ax skip Δ J R P Δ J R P skip P Proof intros n k d m mf S p inv csteps p as p1 p2 left done solve cred inv cstep p1 last cstep p2 right by constructor done Qed Lemma ax goto Δ J R Q l Δ J R J l goto l Q Proof intros n k d m mf S p inv csteps p as p1 p2 left done solve cred inv cstep p1 last cstep p2 right constructor solve elem of done Qed Lemma ax return None Δ J R Q Δ J R R None ret None Q Proof intros n k d m mf S p inv csteps p as p1 p2 left done solve cred inv cstep p1 last cstep p2 right by constructor done Qed Lemma ax return Some Δ J R e v Q Δ J R e v R Some v ret Some e Q Proof intros n k m mf S Hpre p discriminate down up destruct Hpre as unfold assert in inv csteps p as p1 p2 left done solve cred inv cstep p1 last cstep p2 simplify expr eval right by constructor done Qed Lemma ax return Some alt Δ J R e Q Δ J R v e v R Some v ret Some e Q Proof apply ax stmt ex pre intro v auto using ax return Some Qed Lemma ax assign Δ J R e1 e2 a v Q Δ J R e1 ptr a e2 v ptr a a v Q e1 e2 Q Proof intros n k m mf S Hpre p discriminate down up destruct Hpre as a v unfold assert in simplify option equality inv csteps p as p1 p2 left done solve cred inv cstep p1 last cstep p2 simplify expr eval rewrite insert union l right by constructor apply finmap disjoint insert l split solve mem disjoint eauto using finmap disjoint Some l Qed Lemma ax assign alt Δ J R e1 e2 Q Δ J R a v e1 ptr a e2 v ptr a a v Q e1 e2 Q Proof apply ax stmt ex pre intro a apply ax stmt ex pre intro v auto using ax assign Qed Lemma ax assign sep Δ J R e1 e2 P w expr load free e1 P e2 w A Δ J R e1 P e1 e2 e1 val w P Proof intros HP eapply ax stmt weak pre ax assign alt intros ρ m2 a1 v1 subst exists a1 w repeat split unfold assert eapply expr eval weaken mem with a1 v1 eauto using finmap subseteq union l do 2 red in HP unfold assert in apply expr eval weaken mem with m2 eauto using finmap subseteq union r exists a1 v1 unfold assert by simpl map eexists a1 w m2 repeat split auto by rewrite insert union l insert singleton solve mem disjoint exists a1 w simpl repeat split erewrite expr load free mem indep eauto Qed Lemma ax assign load sep Δ J R e1 e2 P p w expr load free e1 expr load free p P e2 w A

Original URL path: http://robbertkrebbers.nl/research/ch2o/fossacs2013/axiomatic.html (2015-08-10)

Open archived version from archive - Module gcd

fassert fassert env apply ax stmt add funs with Δ intros f Pf unfold Δ rewrite lookup singleton Some intros subst eauto intros f Pf sf c vs unfold Δ rewrite lookup singleton Some intros simplify map equality destruct c as v w vs as p q simpl try setoid rewrite right absorb False A auto using ax stmt top false pre setoid rewrite right id emp A setoid rewrite associative A eapply ax stmt top weak with R λ 0 p 1 q p w q v A swap spec done intro by rewrite assert singleton forget var eapply ax stmt weak pre ax stmt weak post ax call alt with Pf swap fassert P λ vs match vs with a1 a2 e1 a1 e2 a2 False end A c x y simpl intros a1 a2 subst exists ptr a1 ptr a2 V simpl split unfold assert simpl repeat split eauto with cstep solve assert simpl apply assert exists elim intro vs apply assert exists elim simpl intros destruct vs as p1 p2 try solve assert rewrite assert singleton eval l e1 p1 rewrite assert singleton eval l e2 p2 rewrite associative A commutative e2 A rewrite assert and sep assoc assert sep and assoc by apply by rewrite commutative e2 A intros apply unfold Δ by simpl map intros solve assert Qed Lemma gcd spec δ Δ L SWAP x y Z δ SWAP Some swap stmt 0 x Z 0 y Z δ Δ ₜ 0 int x V 1 int y V gcd stmt L SWAP λ mv 0 1 match mv with Some int z V z Z gcd x y False end Proof intros H δ apply ax stmt top unfold set R λ mv 0 1 match mv with Some VInt z z Z gcd x y False end A set J λ l if decide l L then x y 0 int x V 1 int y V 0 x Z 0 y Z Z gcd x y Z gcd x y else False A apply ax stmt weak jmp with J solve assert intro unfold J gcd stmt case decide solve elem of assert J L x y 0 int x V 1 int y V 0 x Z 0 y Z Z gcd x y Z gcd x y A as HJ unfold J case decide intuition unfold gcd stmt apply ax label alt rewrite HJ intros ρ m exists x y split solve assert apply ax comp with 0 int Z gcd x y V 1 int 0 A apply ax if alt rewrite HJ apply assert exists elim intros x apply assert exists elim intros y apply assert and elim l apply assert sep elim r by rewrite assert singleton forget assert singleton load rewrite HJ repeat setoid rewrite assert and exists apply ax stmt ex pre intro x apply ax stmt ex pre intro y eapply ax comp with 0 int x mod y V 1 int

Original URL path: http://robbertkrebbers.nl/research/ch2o/fossacs2013/gcd.html (2015-08-10)

Open archived version from archive