From 2832696faacd4e0666ac9e6da45b041bb1e13e8b Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 18 Mar 2017 14:42:13 -0400 Subject: [PATCH] Start of CompilerCorrectness: cfoldExprs_ok --- CompilerCorrectness.v | 312 +++++++++++++++++++++++++++++++ ConcurrentSeparationLogic.v | 2 +- DeepAndShallowEmbeddings.v | 2 +- HoareLogic.v | 2 +- LambdaCalculusAndTypeSoundness.v | 2 +- MessagesAndRefinement.v | 2 +- README.md | 17 +- SeparationLogic.v | 2 +- SharedMemory.v | 2 +- TypesAndMutation.v | 2 +- 10 files changed, 329 insertions(+), 16 deletions(-) create mode 100644 CompilerCorrectness.v diff --git a/CompilerCorrectness.v b/CompilerCorrectness.v new file mode 100644 index 0000000..748d290 --- /dev/null +++ b/CompilerCorrectness.v @@ -0,0 +1,312 @@ +(** Formal Reasoning About Programs + * Chapter 9: Compiler Correctness + * Author: Adam Chlipala + * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) + +Require Import Frap. + +Set Implicit Arguments. + + +(* In this chapter, we'll work with a small variation on the imperative language + * from the previous chapter. *) + +Inductive arith : Set := +| Const (n : nat) +| Var (x : var) +| Plus (e1 e2 : arith) +| Minus (e1 e2 : arith) +| Times (e1 e2 : arith). + +Inductive cmd := +| Skip +| Assign (x : var) (e : arith) +| Sequence (c1 c2 : cmd) +| If (e : arith) (then_ else_ : cmd) +| While (e : arith) (body : cmd) +| Output (e : arith). +(* The last constructor above is the new one, for generating an _output_ value, + * say to display in a terminal. By including this operation, we create + * interesting differences between the behaviors of different nonterminating + * programs. A correct compiler should preserve these differences. *) + +(* The next span of notations and definitions is the same as last chapter. *) + +Coercion Const : nat >-> arith. +Coercion Var : var >-> arith. +Infix "+" := Plus : arith_scope. +Infix "-" := Minus : arith_scope. +Infix "*" := Times : arith_scope. +Delimit Scope arith_scope with arith. +Notation "x <- e" := (Assign x e%arith) (at level 75). +Infix ";;" := Sequence (at level 76). (* This one changed slightly, to avoid parsing clashes. *) +Notation "'when' e 'then' then_ 'else' else_ 'done'" := (If e%arith then_ else_) (at level 75, e at level 0). +Notation "'while' e 'loop' body 'done'" := (While e%arith body) (at level 75). + +Definition valuation := fmap var nat. +Fixpoint interp (e : arith) (v : valuation) : nat := + match e with + | Const n => n + | Var x => + match v $? x with + | None => 0 + | Some n => n + end + | Plus e1 e2 => interp e1 v + interp e2 v + | Minus e1 e2 => interp e1 v - interp e2 v + | Times e1 e2 => interp e1 v * interp e2 v + end. + +Inductive context := +| Hole +| CSeq (C : context) (c : cmd). + +Inductive plug : context -> cmd -> cmd -> Prop := +| PlugHole : forall c, plug Hole c c +| PlugSeq : forall c C c' c2, + plug C c c' + -> plug (CSeq C c2) c (Sequence c' c2). + +(* Here's our first difference. We add a new parameter to [step0], giving a + * _label_ that records which _externally visible effect_ the step has. For + * this language, output is the only externally visible effect, so a label + * records an optional output value. *) + +Inductive step0 : valuation * cmd -> option nat -> valuation * cmd -> Prop := +| Step0Assign : forall v x e, + step0 (v, Assign x e) None (v $+ (x, interp e v), Skip) +| Step0Seq : forall v c2, + step0 (v, Sequence Skip c2) None (v, c2) +| Step0IfTrue : forall v e then_ else_, + interp e v <> 0 + -> step0 (v, If e then_ else_) None (v, then_) +| Step0IfFalse : forall v e then_ else_, + interp e v = 0 + -> step0 (v, If e then_ else_) None (v, else_) +| Step0WhileTrue : forall v e body, + interp e v <> 0 + -> step0 (v, While e body) None (v, Sequence body (While e body)) +| Step0WhileFalse : forall v e body, + interp e v = 0 + -> step0 (v, While e body) None (v, Skip) +| Step0Output : forall v e, + step0 (v, Output e) (Some (interp e v)) (v, Skip). + +Inductive cstep : valuation * cmd -> option nat -> valuation * cmd -> Prop := +| CStep : forall C v c l v' c' c1 c2, + plug C c c1 + -> step0 (v, c) l (v', c') + -> plug C c' c2 + -> cstep (v, c1) l (v', c2). + +(* To characterize correct compilation, it is helpful to define a relation to + * capture which output _traces_ a command might generate. Note that, for us, a + * trace is a list of output values, where [None] labels are simply dropped. *) +Inductive generate : valuation * cmd -> list nat -> Prop := +| GenDone : forall vc, + generate vc [] +| GenSilent : forall vc vc' ns, + cstep vc None vc' + -> generate vc' ns + -> generate vc ns +| GenOutput : forall vc n vc' ns, + cstep vc (Some n) vc' + -> generate vc' ns + -> generate vc (n :: ns). + +Hint Constructors plug step0 cstep generate. + +Definition traceInclusion (vc1 vc2 : valuation * cmd) := + forall ns, generate vc1 ns -> generate vc2 ns. +Infix "<|" := traceInclusion (at level 70). + +Definition traceEquivalence (vc1 vc2 : valuation * cmd) := + vc1 <| vc2 /\ vc2 <| vc1. +Infix "=|" := traceEquivalence (at level 70). + + +(** * Basic Simulation Arguments and Optimizing Expressions *) + +Fixpoint cfoldArith (e : arith) : arith := + match e with + | Const _ => e + | Var _ => e + | Plus e1 e2 => + let e1' := cfoldArith e1 in + let e2' := cfoldArith e2 in + match e1', e2' with + | Const n1, Const n2 => Const (n1 + n2) + | _, _ => Plus e1' e2' + end + | Minus e1 e2 => + let e1' := cfoldArith e1 in + let e2' := cfoldArith e2 in + match e1', e2' with + | Const n1, Const n2 => Const (n1 - n2) + | _, _ => Minus e1' e2' + end + | Times e1 e2 => + let e1' := cfoldArith e1 in + let e2' := cfoldArith e2 in + match e1', e2' with + | Const n1, Const n2 => Const (n1 * n2) + | _, _ => Times e1' e2' + end + end. + +Theorem cfoldArith_ok : forall v e, + interp (cfoldArith e) v = interp e v. +Proof. + induct e; simplify; try equality; + repeat (match goal with + | [ |- context[match ?E with _ => _ end] ] => cases E + | [ H : _ = interp _ _ |- _ ] => rewrite <- H + end; simplify); subst; ring. +Qed. + +Fixpoint cfoldExprs (c : cmd) : cmd := + match c with + | Skip => c + | Assign x e => Assign x (cfoldArith e) + | Sequence c1 c2 => Sequence (cfoldExprs c1) (cfoldExprs c2) + | If e then_ else_ => If (cfoldArith e) (cfoldExprs then_) (cfoldExprs else_) + | While e body => While (cfoldArith e) (cfoldExprs body) + | Output e => Output (cfoldArith e) + end. + +Section simulation. + Variable R : valuation * cmd -> valuation * cmd -> Prop. + + Hypothesis one_step : forall vc1 vc2, R vc1 vc2 + -> forall vc1' l, cstep vc1 l vc1' + -> exists vc2', cstep vc2 l vc2' /\ R vc1' vc2'. + + Lemma simulation' : forall vc1 ns, generate vc1 ns + -> forall vc2, R vc1 vc2 + -> generate vc2 ns. + Proof. + induct 1; simplify; eauto. + + eapply one_step in H; eauto. + first_order. + eauto. + + eapply one_step in H1; eauto. + first_order. + eauto. + Qed. + + Theorem simulation : forall vc1 vc2, R vc1 vc2 + -> vc1 <| vc2. + Proof. + unfold traceInclusion; eauto using simulation'. + Qed. +End simulation. + +Lemma cfoldExprs_ok1' : forall v1 c1 l v2 c2, + step0 (v1, c1) l (v2, c2) + -> step0 (v1, cfoldExprs c1) l (v2, cfoldExprs c2). +Proof. + invert 1; simplify; + try match goal with + | [ _ : context[interp ?e ?v] |- _ ] => rewrite <- (cfoldArith_ok v e) in * + | [ |- context[interp ?e ?v] ] => rewrite <- (cfoldArith_ok v e) + end; eauto. +Qed. + +Hint Resolve cfoldExprs_ok1'. + +Fixpoint cfoldExprsContext (C : context) : context := + match C with + | Hole => Hole + | CSeq C c => CSeq (cfoldExprsContext C) (cfoldExprs c) + end. + +Lemma plug_cfoldExprs1 : forall C c1 c2, plug C c1 c2 + -> plug (cfoldExprsContext C) (cfoldExprs c1) (cfoldExprs c2). +Proof. + induct 1; simplify; eauto. +Qed. + +Hint Resolve plug_cfoldExprs1. + +Lemma cfoldExprs_ok1 : forall v c, + (v, c) <| (v, cfoldExprs c). +Proof. + simplify. + apply simulation with (R := fun vc1 vc2 => fst vc1 = fst vc2 + /\ snd vc2 = cfoldExprs (snd vc1)); + simplify; propositional. + + invert H0; simplify; subst. + apply cfoldExprs_ok1' in H3. + cases vc2; simplify; subst. + eauto 7. +Qed. + +Lemma cfoldExprs_ok2' : forall v1 c1 l v2 c2, + step0 (v1, cfoldExprs c1) l (v2, c2) + -> exists c2', step0 (v1, c1) l (v2, c2') /\ c2 = cfoldExprs c2'. +Proof. + invert 1; + repeat match goal with + | [ H : _ = cfoldExprs ?c |- _ ] => cases c; invert H + end; repeat rewrite cfoldArith_ok in *; eauto. +Qed. + +Hint Resolve cfoldExprs_ok2'. + +Lemma plug_cfoldExprs2 : forall C c1 c2, plug C c1 (cfoldExprs c2) + -> exists C' c1', plug C' c1' c2 + /\ C = cfoldExprsContext C' + /\ c1 = cfoldExprs c1'. +Proof. + induct 1; simplify; eauto. + cases c2; simplify; invert x. + specialize (IHplug _ eq_refl). + first_order; subst. + eauto 7. +Qed. + +Lemma plug_cfoldExprs2' : forall C c1 c2, plug (cfoldExprsContext C) (cfoldExprs c1) c2 + -> exists c2', plug C c1 c2' + /\ c2 = cfoldExprs c2'. +Proof. + induct 1; simplify; eauto. + + cases C; invert x. + eauto. + + cases C; invert x. + specialize (IHplug _ _ eq_refl eq_refl). + first_order; subst. + eauto. +Qed. + +Lemma cfoldExprs_ok2 : forall v c, + (v, cfoldExprs c) <| (v, c). +Proof. + simplify. + apply simulation with (R := fun vc1 vc2 => fst vc1 = fst vc2 + /\ snd vc1 = cfoldExprs (snd vc2)); + simplify; propositional. + + invert H0; simplify; subst. + eapply plug_cfoldExprs2 in H. + first_order; subst. + apply cfoldExprs_ok2' in H3. + first_order; subst. + cases vc2; simplify; subst. + apply plug_cfoldExprs2' in H4. + first_order; subst. + eauto. +Qed. + +Theorem cfoldExprs_ok : forall v c, + (v, cfoldExprs c) =| (v, c). +Proof. + simplify. + split. + apply cfoldExprs_ok2. + apply cfoldExprs_ok1. +Qed. diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v index 1f96af0..6b4043e 100644 --- a/ConcurrentSeparationLogic.v +++ b/ConcurrentSeparationLogic.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 15: Concurrent Separation Logic + * Chapter 16: Concurrent Separation Logic * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v index 03e289a..660d2bf 100644 --- a/DeepAndShallowEmbeddings.v +++ b/DeepAndShallowEmbeddings.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 12: Deep and Shallow Embeddings + * Chapter 13: Deep and Shallow Embeddings * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/HoareLogic.v b/HoareLogic.v index fb588d0..602e193 100644 --- a/HoareLogic.v +++ b/HoareLogic.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 11: Hoare Logic: Verifying Imperative Programs + * Chapter 12: Hoare Logic: Verifying Imperative Programs * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/LambdaCalculusAndTypeSoundness.v b/LambdaCalculusAndTypeSoundness.v index 805856a..5903a3f 100644 --- a/LambdaCalculusAndTypeSoundness.v +++ b/LambdaCalculusAndTypeSoundness.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 9: Lambda Calculus and Simple Type Soundness + * Chapter 10: Lambda Calculus and Simple Type Soundness * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/MessagesAndRefinement.v b/MessagesAndRefinement.v index 7b77d31..6a6f9d7 100644 --- a/MessagesAndRefinement.v +++ b/MessagesAndRefinement.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 16: Process Algebra and Behavioral Refinement + * Chapter 17: Process Algebra and Behavioral Refinement * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/README.md b/README.md index 9900bff..0801854 100644 --- a/README.md +++ b/README.md @@ -19,11 +19,12 @@ The main narrative, also present in the book PDF, presents standard program-proo * Chapter 7: `OperationalSemantics.v` * `LogicProgramming.v`: 'eauto' and friends, to automate proofs via logic programming * Chapter 8: `AbstractInterpretation.v` -* Chapter 9: `LambdaCalculusAndTypeSoundness.v` -* Chapter 10: `TypesAndMutation.v` -* Chapter 11: `HoareLogic.v` -* Chapter 12: `DeepAndShallowEmbeddings.v` -* Chapter 13: `SeparationLogic.v` -* Chapter 14: `SharedMemory.v` -* Chapter 15: `ConcurrentSeparationLogic.v` -* Chapter 16: `MessagesAndRefinement.v` +* Chapter 9: `CompilerCorrectness.v` +* Chapter 10: `LambdaCalculusAndTypeSoundness.v` +* Chapter 11: `TypesAndMutation.v` +* Chapter 12: `HoareLogic.v` +* Chapter 13: `DeepAndShallowEmbeddings.v` +* Chapter 14: `SeparationLogic.v` +* Chapter 15: `SharedMemory.v` +* Chapter 16: `ConcurrentSeparationLogic.v` +* Chapter 17: `MessagesAndRefinement.v` diff --git a/SeparationLogic.v b/SeparationLogic.v index d1b701b..5ab9f8a 100644 --- a/SeparationLogic.v +++ b/SeparationLogic.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 13: Separation Logic + * Chapter 14: Separation Logic * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/SharedMemory.v b/SharedMemory.v index 4956e6d..f998d9c 100644 --- a/SharedMemory.v +++ b/SharedMemory.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 14: Operational Semantics for Shared-Memory Concurrency + * Chapter 15: Operational Semantics for Shared-Memory Concurrency * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) diff --git a/TypesAndMutation.v b/TypesAndMutation.v index a37b8d7..713305b 100644 --- a/TypesAndMutation.v +++ b/TypesAndMutation.v @@ -1,5 +1,5 @@ (** Formal Reasoning About Programs - * Chapter 10: Types and Mutation + * Chapter 11: Types and Mutation * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)