text:
(** * PE: Partial Evaluation *)

(* $Date: 2013-07-18 05:19:11 +0900 (木, 18  7月 2013) $ *)
(* Chapter author/maintainer: Chung-chieh Shan *)

(** Equiv.v introduced constant folding as an example of a program
    transformation and proved that it preserves the meaning of the
    program.  Constant folding operates on manifest constants such
    as [ANum] expressions.  For example, it simplifies the command
    [Y ::= APlus (ANum 3) (ANum 1)] to the command [Y ::= ANum 4].
    However, it does not propagate known constants along data flow.
    For example, it does not simplify the sequence
        X ::= ANum 3;; Y ::= APlus (AId X) (ANum 1)
    to
        X ::= ANum 3;; Y ::= ANum 4
    because it forgets that [X] is [3] by the time it gets to [Y].

    We naturally want to enhance constant folding so that it
    propagates known constants and uses them to simplify programs.
    Doing so constitutes a rudimentary form of _partial evaluation_.
    As we will see, partial evaluation is so called because it is
    like running a program, except only part of the program can be
    evaluated because only part of the input to the program is known.
    For example, we can only simplify the program
        X ::= ANum 3;; Y ::= AMinus (APlus (AId X) (ANum 1)) (AId Y)
    to
        X ::= ANum 3;; Y ::= AMinus (ANum 4) (AId Y)
    without knowing the initial value of [Y]. *)

Require Export Imp.
Require Import FunctionalExtensionality.

(* ####################################################### *)
(** * Generalizing Constant Folding *)

(** The starting point of partial evaluation is to represent our
    partial knowledge about the state.  For example, between the two
    assignments above, the partial evaluator may know only that [X] is
    [3] and nothing about any other variable. *)

(** ** Partial States *)

(** Conceptually speaking, we can think of such partial states as the
    type [id -> option nat] (as opposed to the type [id -> nat] of
    concrete, full states).  However, in addition to looking up and
    updating the values of individual variables in a partial state, we
    may also want to compare two partial states to see if and where
    they differ, to handle conditional control flow.  It is not possible
    to compare two arbitrary functions in this way, so we represent
    partial states in a more concrete format: as a list of [id * nat]
    pairs. *)

Definition pe_state := list (id * nat).

(** The idea is that a variable [id] appears in the list if and only
    if we know its current [nat] value.  The [pe_lookup] function thus
    interprets this concrete representation.  (If the same variable
    [id] appears multiple times in the list, the first occurrence
    wins, but we will define our partial evaluator to never construct
    such a [pe_state].) *)

Fixpoint pe_lookup (pe_st : pe_state) (V:id) : option nat :=
  match pe_st with
  | [] => None
  | (V',n')::pe_st => if eq_id_dec V V' then Some n'
                      else pe_lookup pe_st V
  end.

(** For example, [empty_pe_state] represents complete ignorance about
    every variable -- the function that maps every [id] to [None]. *)

Definition empty_pe_state : pe_state := [].

(** More generally, if the [list] representing a [pe_state] does not
    contain some [id], then that [pe_state] must map that [id] to
    [None].  Before we prove this fact, we first define a useful
    tactic for reasoning with [id] equality.  The tactic
        compare V V' SCase
    means to reason by cases over [eq_id_dec V V'].
    In the case where [V = V'], the tactic
    substitutes [V] for [V'] throughout. *)

Tactic Notation "compare" ident(i) ident(j) ident(c) :=
  let H := fresh "Heq" i j in
  destruct (eq_id_dec i j);
  [ Case_aux c "equal"; subst j
  | Case_aux c "not equal" ].

Theorem pe_domain: forall pe_st V n,
  pe_lookup pe_st V = Some n ->
  In V (map (@fst _ _) pe_st).
Proof. intros pe_st V n H. induction pe_st as [| [V' n'] pe_st].
  Case "[]". inversion H.
  Case "::". simpl in H. simpl. compare V V' SCase; auto. Qed.

(** *** Aside on [In].

    We will make heavy use of the [In] predicate from the standard library.
    [In] is equivalent to the [appears_in] predicate introduced in Logic.v, but
    defined using a [Fixpoint] rather than an [Inductive]. *)

Print In.
(* ===> Fixpoint In {A:Type} (a: A) (l:list A) : Prop :=
           match l with
           | [] => False
           | b :: m => b = a \/ In a m
            end
        : forall A : Type, A -> list A -> Prop *)

(**    [In] comes with various useful lemmas.  *)

Check in_or_app.
(* ===>  in_or_app: forall (A : Type) (l m : list A) (a : A),
                In a l \/ In a m -> In a (l ++ m) *)

Check filter_In.
(* ===> filter_In : forall (A : Type) (f : A -> bool) (x : A) (l : list A),
                 In x (filter f l) <-> In x l /\ f x = true  *)

Check in_dec.
(* ===> in_dec : forall A : Type,
             (forall x y : A, {x = y} + {x <> y}) ->
             forall (a : A) (l : list A), {In a l} + {~ In a l}] *)

(**  Note that we can compute with [in_dec], just as with [eq_id_dec]. *)

(** ** Arithmetic Expressions *)

(** Partial evaluation of [aexp] is straightforward -- it is basically
    the same as constant folding, [fold_constants_aexp], except that
    sometimes the partial state tells us the current value of a
    variable and we can replace it by a constant expression. *)

Fixpoint pe_aexp (pe_st : pe_state) (a : aexp) : aexp :=
  match a with
  | ANum n => ANum n
  | AId i => match pe_lookup pe_st i with (* <----- NEW *)
             | Some n => ANum n
             | None => AId i
             end
  | APlus a1 a2 =>
      match (pe_aexp pe_st a1, pe_aexp pe_st a2) with
      | (ANum n1, ANum n2) => ANum (n1 + n2)
      | (a1', a2') => APlus a1' a2'
      end
  | AMinus a1 a2 =>
      match (pe_aexp pe_st a1, pe_aexp pe_st a2) with
      | (ANum n1, ANum n2) => ANum (n1 - n2)
      | (a1', a2') => AMinus a1' a2'
      end
  | AMult a1 a2 =>
      match (pe_aexp pe_st a1, pe_aexp pe_st a2) with
      | (ANum n1, ANum n2) => ANum (n1 * n2)
      | (a1', a2') => AMult a1' a2'
      end
  end.

(** This partial evaluator folds constants but does not apply the
    associativity of addition. *)

Example test_pe_aexp1:
  pe_aexp [(X,3)] (APlus (APlus (AId X) (ANum 1)) (AId Y))
  = APlus (ANum 4) (AId Y).
Proof. reflexivity. Qed.

Example text_pe_aexp2:
  pe_aexp [(Y,3)] (APlus (APlus (AId X) (ANum 1)) (AId Y))
  = APlus (APlus (AId X) (ANum 1)) (ANum 3).
Proof. reflexivity. Qed.

(** Now, in what sense is [pe_aexp] correct?  It is reasonable to
    define the correctness of [pe_aexp] as follows: whenever a full
    state [st:state] is _consistent_ with a partial state
    [pe_st:pe_state] (in other words, every variable to which [pe_st]
    assigns a value is assigned the same value by [st]), evaluating
    [a] and evaluating [pe_aexp pe_st a] in [st] yields the same
    result.  This statement is indeed true. *)

Definition pe_consistent (st:state) (pe_st:pe_state) :=
  forall V n, Some n = pe_lookup pe_st V -> st V = n.

Theorem pe_aexp_correct_weak: forall st pe_st, pe_consistent st pe_st ->
  forall a, aeval st a = aeval st (pe_aexp pe_st a).
Proof. unfold pe_consistent. intros st pe_st H a.
  aexp_cases (induction a) Case; simpl;
    try reflexivity;
    try (destruct (pe_aexp pe_st a1);
         destruct (pe_aexp pe_st a2);
         rewrite IHa1; rewrite IHa2; reflexivity).
  (* Compared to fold_constants_aexp_sound,
     the only interesting case is AId *)
  Case "AId".
    remember (pe_lookup pe_st i) as l. destruct l.
    SCase "Some". rewrite H with (n:=n) by apply Heql. reflexivity.
    SCase "None". reflexivity.
Qed.

(** However, we will soon want our partial evaluator to remove
    assignments.  For example, it will simplify
        X ::= ANum 3;; Y ::= AMinus (AId X) (AId Y);; X ::= ANum 4
    to just
        Y ::= AMinus (ANum 3) (AId Y);; X ::= ANum 4
    by delaying the assignment to [X] until the end.  To accomplish
    this simplification, we need the result of partial evaluating
        pe_aexp [(X,3)] (AMinus (AId X) (AId Y))
    to be equal to [AMinus (ANum 3) (AId Y)] and _not_ the original
    expression [AMinus (AId X) (AId Y)].  After all, it would be
    incorrect, not just inefficient, to transform
        X ::= ANum 3;; Y ::= AMinus (AId X) (AId Y);; X ::= ANum 4
    to
        Y ::= AMinus (AId X) (AId Y);; X ::= ANum 4
    even though the output expressions [AMinus (ANum 3) (AId Y)] and
    [AMinus (AId X) (AId Y)] both satisfy the correctness criterion
    that we just proved.  Indeed, if we were to just define [pe_aexp
    pe_st a = a] then the theorem [pe_aexp_correct'] would already
    trivially hold.

    Instead, we want to prove that the [pe_aexp] is correct in a
    stronger sense: evaluating the expression produced by partial
    evaluation ([aeval st (pe_aexp pe_st a)]) must not depend on those
    parts of the full state [st] that are already specified in the
    partial state [pe_st].  To be more precise, let us define a
    function [pe_override], which updates [st] with the contents of
    [pe_st].  In other words, [pe_override] carries out the
    assignments listed in [pe_st] on top of [st]. *)

Fixpoint pe_override (st:state) (pe_st:pe_state) : state :=
  match pe_st with
  | [] => st
  | (V,n)::pe_st => update (pe_override st pe_st) V n
  end.

Example test_pe_override:
  pe_override (update empty_state Y 1) [(X,3);(Z,2)]
  = update (update (update empty_state Y 1) Z 2) X 3.
Proof. reflexivity. Qed.

(** Although [pe_override] operates on a concrete [list] representing
    a [pe_state], its behavior is defined entirely by the [pe_lookup]
    interpretation of the [pe_state]. *)

Theorem pe_override_correct: forall st pe_st V0,
  pe_override st pe_st V0 =
  match pe_lookup pe_st V0 with
  | Some n => n
  | None => st V0
  end.
Proof. intros. induction pe_st as [| [V n] pe_st]. reflexivity.
  simpl in *. unfold update.
  compare V0 V Case; auto. rewrite eq_id; auto. rewrite neq_id; auto. Qed.

(** We can relate [pe_consistent] to [pe_override] in two ways.
    First, overriding a state with a partial state always gives a
    state that is consistent with the partial state.  Second, if a
    state is already consistent with a partial state, then overriding
    the state with the partial state gives the same state. *)

Theorem pe_override_consistent: forall st pe_st,
  pe_consistent (pe_override st pe_st) pe_st.
Proof. intros st pe_st V n H. rewrite pe_override_correct.
  destruct (pe_lookup pe_st V); inversion H. reflexivity. Qed.

Theorem pe_consistent_override: forall st pe_st,
  pe_consistent st pe_st -> forall V, st V = pe_override st pe_st V.
Proof. intros st pe_st H V. rewrite pe_override_correct.
  remember (pe_lookup pe_st V) as l. destruct l; auto. Qed.

(** Now we can state and prove that [pe_aexp] is correct in the
    stronger sense that will help us define the rest of the partial
    evaluator.

    Intuitively, running a program using partial evaluation is a
    two-stage process.  In the first, _static_ stage, we partially
    evaluate the given program with respect to some partial state to
    get a _residual_ program.  In the second, _dynamic_ stage, we
    evaluate the residual program with respect to the rest of the
    state.  This dynamic state provides values for those variables
    that are unknown in the static (partial) state.  Thus, the
    residual program should be equivalent to _prepending_ the
    assignments listed in the partial state to the original program. *)

Theorem pe_aexp_correct: forall (pe_st:pe_state) (a:aexp) (st:state),
  aeval (pe_override st pe_st) a = aeval st (pe_aexp pe_st a).
Proof.
  intros pe_st a st.
  aexp_cases (induction a) Case; simpl;
    try reflexivity;
    try (destruct (pe_aexp pe_st a1);
         destruct (pe_aexp pe_st a2);
         rewrite IHa1; rewrite IHa2; reflexivity).
  (* Compared to fold_constants_aexp_sound, the only
     interesting case is AId. *)
  rewrite pe_override_correct. destruct (pe_lookup pe_st i); reflexivity.
Qed.

(** ** Boolean Expressions *)

(** The partial evaluation of boolean expressions is similar.  In
    fact, it is entirely analogous to the constant folding of boolean
    expressions, because our language has no boolean variables. *)

Fixpoint pe_bexp (pe_st : pe_state) (b : bexp) : bexp :=
  match b with
  | BTrue        => BTrue
  | BFalse       => BFalse
  | BEq a1 a2 =>
      match (pe_aexp pe_st a1, pe_aexp pe_st a2) with
      | (ANum n1, ANum n2) => if beq_nat n1 n2 then BTrue else BFalse
      | (a1', a2') => BEq a1' a2'
      end
  | BLe a1 a2 =>
      match (pe_aexp pe_st a1, pe_aexp pe_st a2) with
      | (ANum n1, ANum n2) => if ble_nat n1 n2 then BTrue else BFalse
      | (a1', a2') => BLe a1' a2'
      end
  | BNot b1 =>
      match (pe_bexp pe_st b1) with
      | BTrue => BFalse
      | BFalse => BTrue
      | b1' => BNot b1'
      end
  | BAnd b1 b2 =>
      match (pe_bexp pe_st b1, pe_bexp pe_st b2) with
      | (BTrue, BTrue) => BTrue
      | (BTrue, BFalse) => BFalse
      | (BFalse, BTrue) => BFalse
      | (BFalse, BFalse) => BFalse
      | (b1', b2') => BAnd b1' b2'
      end
  end.

Example test_pe_bexp1:
  pe_bexp [(X,3)] (BNot (BLe (AId X) (ANum 3)))
  = BFalse.
Proof. reflexivity. Qed.

Example test_pe_bexp2: forall b,
  b = BNot (BLe (AId X) (APlus (AId X) (ANum 1))) ->
  pe_bexp [] b = b.
Proof. intros b H. rewrite -> H. reflexivity. Qed.

(** The correctness of [pe_bexp] is analogous to the correctness of
    [pe_aexp] above. *)

Theorem pe_bexp_correct: forall (pe_st:pe_state) (b:bexp) (st:state),
  beval (pe_override st pe_st) b = beval st (pe_bexp pe_st b).
Proof.
  intros pe_st b st.
  bexp_cases (induction b) Case; simpl;
    try reflexivity;
    try (remember (pe_aexp pe_st a) as a';
         remember (pe_aexp pe_st a0) as a0';
         assert (Ha: aeval (pe_override st pe_st) a = aeval st a');
         assert (Ha0: aeval (pe_override st pe_st) a0 = aeval st a0');
           try (subst; apply pe_aexp_correct);
         destruct a'; destruct a0'; rewrite Ha; rewrite Ha0;
         simpl; try destruct (beq_nat n n0); try destruct (ble_nat n n0);
         reflexivity);
    try (destruct (pe_bexp pe_st b); rewrite IHb; reflexivity);
    try (destruct (pe_bexp pe_st b1);
         destruct (pe_bexp pe_st b2);
         rewrite IHb1; rewrite IHb2; reflexivity).
Qed.

(* ####################################################### *)
(** * Partial Evaluation of Commands, Without Loops *)

(** What about the partial evaluation of commands?  The analogy
    between partial evaluation and full evaluation continues: Just as
    full evaluation of a command turns an initial state into a final
    state, partial evaluation of a command turns an initial partial
    state into a final partial state.  The difference is that, because
    the state is partial, some parts of the command may not be
    executable at the static stage.  Therefore, just as [pe_aexp]
    returns a residual [aexp] and [pe_bexp] returns a residual [bexp]
    above, partially evaluating a command yields a residual command.

    Another way in which our partial evaluator is similar to a full
    evaluator is that it does not terminate on all commands.  It is
    not hard to build a partial evaluator that terminates on all
    commands; what is hard is building a partial evaluator that
    terminates on all commands yet automatically performs desired
    optimizations such as unrolling loops.  Often a partial evaluator
    can be coaxed into terminating more often and performing more
    optimizations by writing the source program differently so that
    the separation between static and dynamic information becomes more
    apparent.  Such coaxing is the art of _binding-time improvement_.
    The binding time of a variable tells when its value is known --
    either "static", or "dynamic."

    Anyway, for now we will just live with the fact that our partial
    evaluator is not a total function from the source command and the
    initial partial state to the residual command and the final
    partial state.  To model this non-termination, just as with the
    full evaluation of commands, we use an inductively defined
    relation.  We write
        c1 / st || c1' / st'
    to mean that partially evaluating the source command [c1] in the
    initial partial state [st] yields the residual command [c1'] and
    the final partial state [st'].  For example, we want something like
        (X ::= ANum 3 ;; Y ::= AMult (AId Z) (APlus (AId X) (AId X)))
        / [] || (Y ::= AMult (AId Z) (ANum 6)) / [(X,3)]
    to hold.  The assignment to [X] appears in the final partial state,
    not the residual command. *)

(** ** Assignment *)

(** Let's start by considering how to partially evaluate an
    assignment.  The two assignments in the source program above needs
    to be treated differently.  The first assignment [X ::= ANum 3],
    is _static_: its right-hand-side is a constant (more generally,
    simplifies to a constant), so we should update our partial state
    at [X] to [3] and produce no residual code.  (Actually, we produce
    a residual [SKIP].)  The second assignment [Y ::= AMult (AId Z)
    (APlus (AId X) (AId X))] is _dynamic_: its right-hand-side does
    not simplify to a constant, so we should leave it in the residual
    code and remove [Y], if present, from our partial state.  To
    implement these two cases, we define the functions [pe_add] and
    [pe_remove].  Like [pe_override] above, these functions operate on
    a concrete [list] representing a [pe_state], but the theorems
    [pe_add_correct] and [pe_remove_correct] specify their behavior by
    the [pe_lookup] interpretation of the [pe_state]. *)

Fixpoint pe_remove (pe_st:pe_state) (V:id) : pe_state :=
  match pe_st with
  | [] => []
  | (V',n')::pe_st => if eq_id_dec V V' then pe_remove pe_st V
                      else (V',n') :: pe_remove pe_st V
  end.

Theorem pe_remove_correct: forall pe_st V V0,
  pe_lookup (pe_remove pe_st V) V0
  = if eq_id_dec V V0 then None else pe_lookup pe_st V0.
Proof. intros pe_st V V0. induction pe_st as [| [V' n'] pe_st].
  Case "[]". destruct (eq_id_dec V V0); reflexivity.
  Case "::". simpl. compare V V' SCase.
    SCase "equal". rewrite IHpe_st.
      destruct (eq_id_dec V V0).  reflexivity.  rewrite neq_id; auto.
    SCase "not equal". simpl. compare V0 V' SSCase.
      SSCase "equal". rewrite neq_id; auto.
      SSCase "not equal". rewrite IHpe_st. reflexivity.
Qed.

Definition pe_add (pe_st:pe_state) (V:id) (n:nat) : pe_state :=
  (V,n) :: pe_remove pe_st V.

Theorem pe_add_correct: forall pe_st V n V0,
  pe_lookup (pe_add pe_st V n) V0
  = if eq_id_dec V V0 then Some n else pe_lookup pe_st V0.
Proof. intros pe_st V n V0. unfold pe_add. simpl.
  compare V V0 Case.
  Case "equal". rewrite eq_id; auto.
  Case "not equal". rewrite pe_remove_correct. repeat rewrite neq_id; auto.
Qed.

(** We will use the two theorems below to show that our partial
    evaluator correctly deals with dynamic assignments and static
    assignments, respectively. *)

Theorem pe_override_update_remove: forall st pe_st V n,
  update (pe_override st pe_st) V n =
  pe_override (update st V n) (pe_remove pe_st V).
Proof. intros st pe_st V n. apply functional_extensionality. intros V0.
  unfold update. rewrite !pe_override_correct. rewrite pe_remove_correct.
  destruct (eq_id_dec V V0); reflexivity. Qed.

Theorem pe_override_update_add: forall st pe_st V n,
  update (pe_override st pe_st) V n =
  pe_override st (pe_add pe_st V n).
Proof. intros st pe_st V n. apply functional_extensionality. intros V0.
  unfold update. rewrite !pe_override_correct. rewrite pe_add_correct.
  destruct (eq_id_dec V V0); reflexivity. Qed.

(** ** Conditional *)

(** Trickier than assignments to partially evaluate is the
    conditional, [IFB b1 THEN c1 ELSE c2 FI].  If [b1] simplifies to
    [BTrue] or [BFalse] then it's easy: we know which branch will be
    taken, so just take that branch.  If [b1] does not simplify to a
    constant, then we need to take both branches, and the final
    partial state may differ between the two branches!

    The following program illustrates the difficulty:
        X ::= ANum 3;;
        IFB BLe (AId Y) (ANum 4) THEN
            Y ::= ANum 4;;
            IFB BEq (AId X) (AId Y) THEN Y ::= ANum 999 ELSE SKIP FI
        ELSE SKIP FI
    Suppose the initial partial state is empty.  We don't know
    statically how [Y] compares to [4], so we must partially evaluate
    both branches of the (outer) conditional.  On the [THEN] branch,
    we know that [Y] is set to [4] and can even use that knowledge to
    simplify the code somewhat.  On the [ELSE] branch, we still don't
    know the exact value of [Y] at the end.  What should the final
    partial state and residual program be?

    One way to handle such a dynamic conditional is to take the
    intersection of the final partial states of the two branches.  In
    this example, we take the intersection of [(Y,4),(X,3)] and
    [(X,3)], so the overall final partial state is [(X,3)].  To
    compensate for forgetting that [Y] is [4], we need to add an
    assignment [Y ::= ANum 4] to the end of the [THEN] branch.  So,
    the residual program will be something like
        SKIP;;
        IFB BLe (AId Y) (ANum 4) THEN
            SKIP;;
            SKIP;;
            Y ::= ANum 4
        ELSE SKIP FI

    Programming this case in Coq calls for several auxiliary
    functions: we need to compute the intersection of two [pe_state]s
    and turn their difference into sequences of assignments.

    First, we show how to compute whether two [pe_state]s to disagree
    at a given variable.  In the theorem [pe_disagree_domain], we
    prove that two [pe_state]s can only disagree at variables that
    appear in at least one of them. *)

Definition pe_disagree_at (pe_st1 pe_st2 : pe_state) (V:id) : bool :=
  match pe_lookup pe_st1 V, pe_lookup pe_st2 V with
  | Some x, Some y => negb (beq_nat x y)
  | None, None => false
  | _, _ => true
  end.

Theorem pe_disagree_domain: forall (pe_st1 pe_st2 : pe_state) (V:id),
  true = pe_disagree_at pe_st1 pe_st2 V ->
  In V (map (@fst _ _) pe_st1 ++ map (@fst _ _) pe_st2).
Proof. unfold pe_disagree_at. intros pe_st1 pe_st2 V H.
  apply in_or_app.
  remember (pe_lookup pe_st1 V) as lookup1.
  destruct lookup1 as [n1|]. left.  apply pe_domain with n1. auto.
  remember (pe_lookup pe_st2 V) as lookup2.
  destruct lookup2 as [n2|]. right. apply pe_domain with n2. auto.
  inversion H. Qed.

(** We define the [pe_compare] function to list the variables where
    two given [pe_state]s disagree.  This list is exact, according to
    the theorem [pe_compare_correct]: a variable appears on the list
    if and only if the two given [pe_state]s disagree at that
    variable.  Furthermore, we use the [pe_unique] function to
    eliminate duplicates from the list. *)

Fixpoint pe_unique (l : list id) : list id :=
  match l with
  | [] => []
  | x::l => x :: filter (fun y => if eq_id_dec x y then false else true) (pe_unique l)
  end.

Theorem pe_unique_correct: forall l x,
  In x l <-> In x (pe_unique l).
Proof. intros l x. induction l as [| h t]. reflexivity.
  simpl in *. split.
  Case "->".
    intros. inversion H; clear H.
      left. assumption.
      destruct (eq_id_dec h x).
         left.  assumption.
         right.  apply filter_In. split.
           apply IHt. assumption.
           rewrite neq_id; auto.
  Case "<-".
    intros. inversion H; clear H.
       left. assumption.
       apply filter_In in H0.  inversion H0. right. apply IHt. assumption.
Qed.

Definition pe_compare (pe_st1 pe_st2 : pe_state) : list id :=
  pe_unique (filter (pe_disagree_at pe_st1 pe_st2)
    (map (@fst _ _) pe_st1 ++ map (@fst _ _) pe_st2)).

Theorem pe_compare_correct: forall pe_st1 pe_st2 V,
  pe_lookup pe_st1 V = pe_lookup pe_st2 V <->
  ~ In V (pe_compare pe_st1 pe_st2).
Proof. intros pe_st1 pe_st2 V.
  unfold pe_compare. rewrite <- pe_unique_correct. rewrite filter_In.
  split; intros Heq.
  Case "->".
    intro. destruct H. unfold pe_disagree_at in H0. rewrite Heq in H0.
    destruct (pe_lookup pe_st2 V).
    rewrite <- beq_nat_refl in H0. inversion H0.
    inversion H0.
  Case "<-".
    assert (Hagree: pe_disagree_at pe_st1 pe_st2 V = false).
      SCase "Proof of assertion".
      remember (pe_disagree_at pe_st1 pe_st2 V) as disagree.
      destruct disagree; [| reflexivity].
      apply  pe_disagree_domain in Heqdisagree.
      apply ex_falso_quodlibet. apply Heq. split. assumption. reflexivity.
    unfold pe_disagree_at in Hagree.
    destruct (pe_lookup pe_st1 V) as [n1|];
    destruct (pe_lookup pe_st2 V) as [n2|];
      try reflexivity; try solve by inversion.
    rewrite negb_false_iff in Hagree.
    apply beq_nat_true in Hagree. subst. reflexivity. Qed.

(** The intersection of two partial states is the result of removing
    from one of them all the variables where the two disagree.  We
    define the function [pe_removes], in terms of [pe_remove] above,
    to perform such a removal of a whole list of variables at once.

    The theorem [pe_compare_removes] testifies that the [pe_lookup]
    interpretation of the result of this intersection operation is the
    same no matter which of the two partial states we remove the
    variables from.  Because [pe_override] only depends on the
    [pe_lookup] interpretation of partial states, [pe_override] also
    does not care which of the two partial states we remove the
    variables from; that theorem [pe_compare_override] is used in the
    correctness proof shortly. *)

Fixpoint pe_removes (pe_st:pe_state) (ids : list id) : pe_state :=
  match ids with
  | [] => pe_st
  | V::ids => pe_remove (pe_removes pe_st ids) V
  end.

Theorem pe_removes_correct: forall pe_st ids V,
  pe_lookup (pe_removes pe_st ids) V =
  if in_dec eq_id_dec V ids then None else pe_lookup pe_st V.
Proof. intros pe_st ids V. induction ids as [| V' ids]. reflexivity.
  simpl. rewrite pe_remove_correct. rewrite IHids.
  compare V' V Case.
    reflexivity.
    destruct (in_dec eq_id_dec V ids);
      reflexivity.
Qed.

Theorem pe_compare_removes: forall pe_st1 pe_st2 V,
  pe_lookup (pe_removes pe_st1 (pe_compare pe_st1 pe_st2)) V =
  pe_lookup (pe_removes pe_st2 (pe_compare pe_st1 pe_st2)) V.
Proof. intros pe_st1 pe_st2 V. rewrite !pe_removes_correct.
  destruct (in_dec eq_id_dec V (pe_compare pe_st1 pe_st2)).
    reflexivity.
    apply pe_compare_correct. auto. Qed.

Theorem pe_compare_override: forall pe_st1 pe_st2 st,
  pe_override st (pe_removes pe_st1 (pe_compare pe_st1 pe_st2)) =
  pe_override st (pe_removes pe_st2 (pe_compare pe_st1 pe_st2)).
Proof. intros. apply functional_extensionality. intros V.
  rewrite !pe_override_correct. rewrite pe_compare_removes. reflexivity.
Qed.

(** Finally, we define an [assign] function to turn the difference
    between two partial states into a sequence of assignment commands.
    More precisely, [assign pe_st ids] generates an assignment command
    for each variable listed in [ids]. *)

Fixpoint assign (pe_st : pe_state) (ids : list id) : com :=
  match ids with
  | [] => SKIP
  | V::ids => match pe_lookup pe_st V with
              | Some n => (assign pe_st ids;; V ::= ANum n)
              | None => assign pe_st ids
              end
  end.

(** The command generated by [assign] always terminates, because it is
    just a sequence of assignments.  The (total) function [assigned]
    below computes the effect of the command on the (dynamic state).
    The theorem [assign_removes] then confirms that the generated
    assignments perfectly compensate for removing the variables from
    the partial state. *)

Definition assigned (pe_st:pe_state) (ids : list id) (st:state) : state :=
  fun V => if in_dec eq_id_dec V ids then
                match pe_lookup pe_st V with
                | Some n => n
                | None => st V
                end
           else st V.

Theorem assign_removes: forall pe_st ids st,
  pe_override st pe_st =
  pe_override (assigned pe_st ids st) (pe_removes pe_st ids).
Proof. intros pe_st ids st. apply functional_extensionality. intros V.
  rewrite !pe_override_correct. rewrite pe_removes_correct. unfold assigned.
  destruct (in_dec eq_id_dec V ids); destruct (pe_lookup pe_st V); reflexivity.
Qed.

Lemma ceval_extensionality: forall c st st1 st2,
  c / st || st1 -> (forall V, st1 V = st2 V) -> c / st || st2.
Proof. intros c st st1 st2 H Heq.
  apply functional_extensionality in Heq. rewrite <- Heq. apply H. Qed.

Theorem eval_assign: forall pe_st ids st,
  assign pe_st ids / st || assigned pe_st ids st.
Proof. intros pe_st ids st. induction ids as [| V ids]; simpl.
  Case "[]". eapply ceval_extensionality. apply E_Skip. reflexivity.
  Case "V::ids".
    remember (pe_lookup pe_st V) as lookup. destruct lookup.
    SCase "Some". eapply E_Seq. apply IHids. unfold assigned. simpl.
      eapply ceval_extensionality. apply E_Ass. simpl. reflexivity.
      intros V0. unfold update.  compare V V0 SSCase.
      SSCase "equal". rewrite <- Heqlookup. reflexivity.
      SSCase "not equal". destruct (in_dec eq_id_dec V0 ids); auto.
    SCase "None". eapply ceval_extensionality. apply IHids.
      unfold assigned. intros V0. simpl. compare V V0 SSCase.
      SSCase "equal". rewrite <- Heqlookup.
        destruct (in_dec eq_id_dec V ids); reflexivity.
      SSCase "not equal". destruct (in_dec eq_id_dec V0 ids); reflexivity. Qed.

(** ** The Partial Evaluation Relation *)

(** At long last, we can define a partial evaluator for commands
    without loops, as an inductive relation!  The inequality
    conditions in [PE_AssDynamic] and [PE_If] are just to keep the
    partial evaluator deterministic; they are not required for
    correctness. *)

Reserved Notation "c1 '/' st '||' c1' '/' st'"
  (at level 40, st at level 39, c1' at level 39).

Inductive pe_com : com -> pe_state -> com -> pe_state -> Prop :=
  | PE_Skip : forall pe_st,
      SKIP / pe_st || SKIP / pe_st
  | PE_AssStatic : forall pe_st a1 n1 l,
      pe_aexp pe_st a1 = ANum n1 ->
      (l ::= a1) / pe_st || SKIP / pe_add pe_st l n1
  | PE_AssDynamic : forall pe_st a1 a1' l,
      pe_aexp pe_st a1 = a1' ->
      (forall n, a1' <> ANum n) ->
      (l ::= a1) / pe_st || (l ::= a1') / pe_remove pe_st l
  | PE_Seq : forall pe_st pe_st' pe_st'' c1 c2 c1' c2',
      c1 / pe_st  || c1' / pe_st' ->
      c2 / pe_st' || c2' / pe_st'' ->
      (c1 ;; c2) / pe_st || (c1' ;; c2') / pe_st''
  | PE_IfTrue : forall pe_st pe_st' b1 c1 c2 c1',
      pe_bexp pe_st b1 = BTrue ->
      c1 / pe_st || c1' / pe_st' ->
      (IFB b1 THEN c1 ELSE c2 FI) / pe_st || c1' / pe_st'
  | PE_IfFalse : forall pe_st pe_st' b1 c1 c2 c2',
      pe_bexp pe_st b1 = BFalse ->
      c2 / pe_st || c2' / pe_st' ->
      (IFB b1 THEN c1 ELSE c2 FI) / pe_st || c2' / pe_st'
  | PE_If : forall pe_st pe_st1 pe_st2 b1 c1 c2 c1' c2',
      pe_bexp pe_st b1 <> BTrue ->
      pe_bexp pe_st b1 <> BFalse ->
      c1 / pe_st || c1' / pe_st1 ->
      c2 / pe_st || c2' / pe_st2 ->
      (IFB b1 THEN c1 ELSE c2 FI) / pe_st
        || (IFB pe_bexp pe_st b1
             THEN c1' ;; assign pe_st1 (pe_compare pe_st1 pe_st2)
             ELSE c2' ;; assign pe_st2 (pe_compare pe_st1 pe_st2) FI)
            / pe_removes pe_st1 (pe_compare pe_st1 pe_st2)

  where "c1 '/' st '||' c1' '/' st'" := (pe_com c1 st c1' st').

Tactic Notation "pe_com_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "PE_Skip"
  | Case_aux c "PE_AssStatic" | Case_aux c "PE_AssDynamic"
  | Case_aux c "PE_Seq"
  | Case_aux c "PE_IfTrue" | Case_aux c "PE_IfFalse" | Case_aux c "PE_If" ].

Hint Constructors pe_com.
Hint Constructors ceval.

(** ** Examples *)

(** Below are some examples of using the partial evaluator.  To make
    the [pe_com] relation actually usable for automatic partial
    evaluation, we would need to define more automation tactics in
    Coq.  That is not hard to do, but it is not needed here. *)

Example pe_example1:
  (X ::= ANum 3 ;; Y ::= AMult (AId Z) (APlus (AId X) (AId X)))
  / [] || (SKIP;; Y ::= AMult (AId Z) (ANum 6)) / [(X,3)].
Proof. eapply PE_Seq. eapply PE_AssStatic. reflexivity.
  eapply PE_AssDynamic. reflexivity. intros n H. inversion H. Qed.

Example pe_example2:
  (X ::= ANum 3 ;; IFB BLe (AId X) (ANum 4) THEN X ::= ANum 4 ELSE SKIP FI)
  / [] || (SKIP;; SKIP) / [(X,4)].
Proof. eapply PE_Seq. eapply PE_AssStatic. reflexivity.
  eapply PE_IfTrue. reflexivity.
  eapply PE_AssStatic. reflexivity. Qed.

Example pe_example3:
  (X ::= ANum 3;;
   IFB BLe (AId Y) (ANum 4) THEN
     Y ::= ANum 4;;
     IFB BEq (AId X) (AId Y) THEN Y ::= ANum 999 ELSE SKIP FI
   ELSE SKIP FI) / []
  || (SKIP;;
       IFB BLe (AId Y) (ANum 4) THEN
         (SKIP;; SKIP);; (SKIP;; Y ::= ANum 4)
       ELSE SKIP;; SKIP FI)
      / [(X,3)].
Proof. erewrite f_equal2 with (f := fun c st => _ / _ || c / st).
  eapply PE_Seq. eapply PE_AssStatic. reflexivity.
  eapply PE_If; intuition eauto; try solve by inversion.
  econstructor. eapply PE_AssStatic. reflexivity.
  eapply PE_IfFalse. reflexivity. econstructor.
  reflexivity. reflexivity. Qed.

(** ** Correctness of Partial Evaluation *)

(** Finally let's prove that this partial evaluator is correct! *)

Reserved Notation "c' '/' pe_st' '/' st '||' st''"
  (at level 40, pe_st' at level 39, st at level 39).

Inductive pe_ceval
  (c':com) (pe_st':pe_state) (st:state) (st'':state) : Prop :=
  | pe_ceval_intro : forall st',
    c' / st || st' ->
    pe_override st' pe_st' = st'' ->
    c' / pe_st' / st || st''
  where "c' '/' pe_st' '/' st '||' st''" := (pe_ceval c' pe_st' st st'').

Hint Constructors pe_ceval.

Theorem pe_com_complete:
  forall c pe_st pe_st' c', c / pe_st || c' / pe_st' ->
  forall st st'',
  (c / pe_override st pe_st || st'') ->
  (c' / pe_st' / st || st'').
Proof. intros c pe_st pe_st' c' Hpe.
  pe_com_cases (induction Hpe) Case; intros st st'' Heval;
  try (inversion Heval; subst;
       try (rewrite -> pe_bexp_correct, -> H in *; solve by inversion);
       []);
  eauto.
  Case "PE_AssStatic". econstructor. econstructor.
    rewrite -> pe_aexp_correct. rewrite <- pe_override_update_add.
    rewrite -> H. reflexivity.
  Case "PE_AssDynamic". econstructor. econstructor. reflexivity.
    rewrite -> pe_aexp_correct. rewrite <- pe_override_update_remove.
    reflexivity.
  Case "PE_Seq".
    edestruct IHHpe1. eassumption. subst.
    edestruct IHHpe2. eassumption.
    eauto.
  Case "PE_If". inversion Heval; subst.
    SCase "E'IfTrue". edestruct IHHpe1. eassumption.
      econstructor. apply E_IfTrue. rewrite <- pe_bexp_correct. assumption.
      eapply E_Seq. eassumption. apply eval_assign.
      rewrite <- assign_removes. eassumption.
    SCase "E_IfFalse". edestruct IHHpe2. eassumption.
      econstructor. apply E_IfFalse. rewrite <- pe_bexp_correct. assumption.
      eapply E_Seq. eassumption. apply eval_assign.
      rewrite -> pe_compare_override.
      rewrite <- assign_removes. eassumption.
Qed.

Theorem pe_com_sound:
  forall c pe_st pe_st' c', c / pe_st || c' / pe_st' ->
  forall st st'',
  (c' / pe_st' / st || st'') ->
  (c / pe_override st pe_st || st'').
Proof. intros c pe_st pe_st' c' Hpe.
  pe_com_cases (induction Hpe) Case;
    intros st st'' [st' Heval Heq];
    try (inversion Heval; []; subst); auto.
  Case "PE_AssStatic". rewrite <- pe_override_update_add. apply E_Ass.
    rewrite -> pe_aexp_correct. rewrite -> H. reflexivity.
  Case "PE_AssDynamic". rewrite <- pe_override_update_remove. apply E_Ass.
    rewrite <- pe_aexp_correct. reflexivity.
  Case "PE_Seq". eapply E_Seq; eauto.
  Case "PE_IfTrue". apply E_IfTrue.
    rewrite -> pe_bexp_correct. rewrite -> H. reflexivity. eauto.
  Case "PE_IfFalse". apply E_IfFalse.
    rewrite -> pe_bexp_correct. rewrite -> H. reflexivity. eauto.
  Case "PE_If".
    inversion Heval; subst; inversion H7;
      (eapply ceval_deterministic in H8; [| apply eval_assign]); subst.
    SCase "E_IfTrue".
      apply E_IfTrue. rewrite -> pe_bexp_correct. assumption.
      rewrite <- assign_removes. eauto.
    SCase "E_IfFalse".
      rewrite -> pe_compare_override.
      apply E_IfFalse. rewrite -> pe_bexp_correct. assumption.
      rewrite <- assign_removes. eauto.
Qed.

(** The main theorem. Thanks to David Menendez for this formulation! *)

Corollary pe_com_correct:
  forall c pe_st pe_st' c', c / pe_st || c' / pe_st' ->
  forall st st'',
  (c / pe_override st pe_st || st'') <->
  (c' / pe_st' / st || st'').
Proof. intros c pe_st pe_st' c' H st st''. split.
  Case "->". apply pe_com_complete. apply H.
  Case "<-". apply pe_com_sound. apply H.
Qed.

(* ####################################################### *)
(** * Partial Evaluation of Loops *)

(** It may seem straightforward at first glance to extend the partial
    evaluation relation [pe_com] above to loops.  Indeed, many loops
    are easy to deal with.  Considered this repeated-squaring loop,
    for example:
        WHILE BLe (ANum 1) (AId X) DO
            Y ::= AMult (AId Y) (AId Y);;
            X ::= AMinus (AId X) (ANum 1)
        END
    If we know neither [X] nor [Y] statically, then the entire loop is
    dynamic and the residual command should be the same.  If we know
    [X] but not [Y], then the loop can be unrolled all the way and the
    residual command should be
        Y ::= AMult (AId Y) (AId Y);;
        Y ::= AMult (AId Y) (AId Y);;
        Y ::= AMult (AId Y) (AId Y)
    if [X] is initially [3] (and finally [0]).  In general, a loop is
    easy to partially evaluate if the final partial state of the loop
    body is equal to the initial state, or if its guard condition is
    static.

    But there are other loops for which it is hard to express the
    residual program we want in Imp.  For example, take this program
    for checking if [Y] is even or odd:
        X ::= ANum 0;;
        WHILE BLe (ANum 1) (AId Y) DO
            Y ::= AMinus (AId Y) (ANum 1);;
            X ::= AMinus (ANum 1) (AId X)
        END
    The value of [X] alternates between [0] and [1] during the loop.
    Ideally, we would like to unroll this loop, not all the way but
    _two-fold_, into something like
        WHILE BLe (ANum 1) (AId Y) DO
            Y ::= AMinus (AId Y) (ANum 1);;
            IF BLe (ANum 1) (AId Y) THEN
                Y ::= AMinus (AId Y) (ANum 1)
            ELSE
                X ::= ANum 1;; EXIT
            FI
        END;;
        X ::= ANum 0
    Unfortunately, there is no [EXIT] command in Imp.  Without
    extending the range of control structures available in our
    language, the best we can do is to repeat loop-guard tests or add
    flag variables.  Neither option is terribly attractive.

    Still, as a digression, below is an attempt at performing partial
    evaluation on Imp commands.  We add one more command argument
    [c''] to the [pe_com] relation, which keeps track of a loop to
    roll up. *)

Module Loop.

Reserved Notation "c1 '/' st '||' c1' '/' st' '/' c''"
  (at level 40, st at level 39, c1' at level 39, st' at level 39).

Inductive pe_com : com -> pe_state -> com -> pe_state -> com -> Prop :=
  | PE_Skip : forall pe_st,
      SKIP / pe_st || SKIP / pe_st / SKIP
  | PE_AssStatic : forall pe_st a1 n1 l,
      pe_aexp pe_st a1 = ANum n1 ->
      (l ::= a1) / pe_st || SKIP / pe_add pe_st l n1 / SKIP
  | PE_AssDynamic : forall pe_st a1 a1' l,
      pe_aexp pe_st a1 = a1' ->
      (forall n, a1' <> ANum n) ->
      (l ::= a1) / pe_st || (l ::= a1') / pe_remove pe_st l / SKIP
  | PE_Seq : forall pe_st pe_st' pe_st'' c1 c2 c1' c2' c'',
      c1 / pe_st  || c1' / pe_st' / SKIP ->
      c2 / pe_st' || c2' / pe_st'' / c'' ->
      (c1 ;; c2) / pe_st || (c1' ;; c2') / pe_st'' / c''
  | PE_IfTrue : forall pe_st pe_st' b1 c1 c2 c1' c'',
      pe_bexp pe_st b1 = BTrue ->
      c1 / pe_st || c1' / pe_st' / c'' ->
      (IFB b1 THEN c1 ELSE c2 FI) / pe_st || c1' / pe_st' / c''
  | PE_IfFalse : forall pe_st pe_st' b1 c1 c2 c2' c'',
      pe_bexp pe_st b1 = BFalse ->
      c2 / pe_st || c2' / pe_st' / c'' ->
      (IFB b1 THEN c1 ELSE c2 FI) / pe_st || c2' / pe_st' / c''
  | PE_If : forall pe_st pe_st1 pe_st2 b1 c1 c2 c1' c2' c'',
      pe_bexp pe_st b1 <> BTrue ->
      pe_bexp pe_st b1 <> BFalse ->
      c1 / pe_st || c1' / pe_st1 / c'' ->
      c2 / pe_st || c2' / pe_st2 / c'' ->
      (IFB b1 THEN c1 ELSE c2 FI) / pe_st
        || (IFB pe_bexp pe_st b1
             THEN c1' ;; assign pe_st1 (pe_compare pe_st1 pe_st2)
             ELSE c2' ;; assign pe_st2 (pe_compare pe_st1 pe_st2) FI)
            / pe_removes pe_st1 (pe_compare pe_st1 pe_st2)
            / c''
  | PE_WhileEnd : forall pe_st b1 c1,
      pe_bexp pe_st b1 = BFalse ->
      (WHILE b1 DO c1 END) / pe_st || SKIP / pe_st / SKIP
  | PE_WhileLoop : forall pe_st pe_st' pe_st'' b1 c1 c1' c2' c2'',
      pe_bexp pe_st b1 = BTrue ->
      c1 / pe_st || c1' / pe_st' / SKIP ->
      (WHILE b1 DO c1 END) / pe_st' || c2' / pe_st'' / c2'' ->
      pe_compare pe_st pe_st'' <> [] ->
      (WHILE b1 DO c1 END) / pe_st || (c1';;c2') / pe_st'' / c2''
  | PE_While : forall pe_st pe_st' pe_st'' b1 c1 c1' c2' c2'',
      pe_bexp pe_st b1 <> BFalse ->
      pe_bexp pe_st b1 <> BTrue ->
      c1 / pe_st || c1' / pe_st' / SKIP ->
      (WHILE b1 DO c1 END) / pe_st' || c2' / pe_st'' / c2'' ->
      pe_compare pe_st pe_st'' <> [] ->
      (c2'' = SKIP \/ c2'' = WHILE b1 DO c1 END) ->
      (WHILE b1 DO c1 END) / pe_st
        || (IFB pe_bexp pe_st b1
             THEN c1';; c2';; assign pe_st'' (pe_compare pe_st pe_st'')
             ELSE assign pe_st (pe_compare pe_st pe_st'') FI)
            / pe_removes pe_st (pe_compare pe_st pe_st'')
            / c2''
  | PE_WhileFixedEnd : forall pe_st b1 c1,
      pe_bexp pe_st b1 <> BFalse ->
      (WHILE b1 DO c1 END) / pe_st || SKIP / pe_st / (WHILE b1 DO c1 END)
  | PE_WhileFixedLoop : forall pe_st pe_st' pe_st'' b1 c1 c1' c2',
      pe_bexp pe_st b1 = BTrue ->
      c1 / pe_st || c1' / pe_st' / SKIP ->
      (WHILE b1 DO c1 END) / pe_st'
        || c2' / pe_st'' / (WHILE b1 DO c1 END) ->
      pe_compare pe_st pe_st'' = [] ->
      (WHILE b1 DO c1 END) / pe_st
        || (WHILE BTrue DO SKIP END) / pe_st / SKIP
      (* Because we have an infinite loop, we should actually
         start to throw away the rest of the program:
         (WHILE b1 DO c1 END) / pe_st
         || SKIP / pe_st / (WHILE BTrue DO SKIP END) *)
  | PE_WhileFixed : forall pe_st pe_st' pe_st'' b1 c1 c1' c2',
      pe_bexp pe_st b1 <> BFalse ->
      pe_bexp pe_st b1 <> BTrue ->
      c1 / pe_st || c1' / pe_st' / SKIP ->
      (WHILE b1 DO c1 END) / pe_st'
        || c2' / pe_st'' / (WHILE b1 DO c1 END) ->
      pe_compare pe_st pe_st'' = [] ->
      (WHILE b1 DO c1 END) / pe_st
        || (WHILE pe_bexp pe_st b1 DO c1';; c2' END) / pe_st / SKIP

  where "c1 '/' st '||' c1' '/' st' '/' c''" := (pe_com c1 st c1' st' c'').

Tactic Notation "pe_com_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "PE_Skip"
  | Case_aux c "PE_AssStatic" | Case_aux c "PE_AssDynamic"
  | Case_aux c "PE_Seq"
  | Case_aux c "PE_IfTrue" | Case_aux c "PE_IfFalse" | Case_aux c "PE_If"
  | Case_aux c "PE_WhileEnd" | Case_aux c "PE_WhileLoop"
  | Case_aux c "PE_While" | Case_aux c "PE_WhileFixedEnd"
  | Case_aux c "PE_WhileFixedLoop" | Case_aux c "PE_WhileFixed" ].

Hint Constructors pe_com.

(** ** Examples *)

Ltac step i :=
  (eapply i; intuition eauto; try solve by inversion);
  repeat (try eapply PE_Seq;
          try (eapply PE_AssStatic; simpl; reflexivity);
          try (eapply PE_AssDynamic;
               [ simpl; reflexivity
               | intuition eauto; solve by inversion ])).

Definition square_loop: com :=
  WHILE BLe (ANum 1) (AId X) DO
    Y ::= AMult (AId Y) (AId Y);;
    X ::= AMinus (AId X) (ANum 1)
  END.

Example pe_loop_example1:
  square_loop / []
  || (WHILE BLe (ANum 1) (AId X) DO
         (Y ::= AMult (AId Y) (AId Y);;
          X ::= AMinus (AId X) (ANum 1));; SKIP
       END) / [] / SKIP.
Proof. erewrite f_equal2 with (f := fun c st => _ / _ || c / st / SKIP).
  step PE_WhileFixed. step PE_WhileFixedEnd. reflexivity.
  reflexivity. reflexivity. Qed.

Example pe_loop_example2:
  (X ::= ANum 3;; square_loop) / []
  || (SKIP;;
       (Y ::= AMult (AId Y) (AId Y);; SKIP);;
       (Y ::= AMult (AId Y) (AId Y);; SKIP);;
       (Y ::= AMult (AId Y) (AId Y);; SKIP);;
       SKIP) / [(X,0)] / SKIP.
Proof. erewrite f_equal2 with (f := fun c st => _ / _ || c / st / SKIP).
  eapply PE_Seq. eapply PE_AssStatic. reflexivity.
  step PE_WhileLoop.
  step PE_WhileLoop.
  step PE_WhileLoop.
  step PE_WhileEnd.
  inversion H. inversion H. inversion H.
  reflexivity. reflexivity. Qed.

Example pe_loop_example3:
  (Z ::= ANum 3;; subtract_slowly) / []
  || (SKIP;;
       IFB BNot (BEq (AId X) (ANum 0)) THEN
         (SKIP;; X ::= AMinus (AId X) (ANum 1));;
         IFB BNot (BEq (AId X) (ANum 0)) THEN
           (SKIP;; X ::= AMinus (AId X) (ANum 1));;
           IFB BNot (BEq (AId X) (ANum 0)) THEN
             (SKIP;; X ::= AMinus (AId X) (ANum 1));;
             WHILE BNot (BEq (AId X) (ANum 0)) DO
               (SKIP;; X ::= AMinus (AId X) (ANum 1));; SKIP
             END;;
             SKIP;; Z ::= ANum 0
           ELSE SKIP;; Z ::= ANum 1 FI;; SKIP
         ELSE SKIP;; Z ::= ANum 2 FI;; SKIP
       ELSE SKIP;; Z ::= ANum 3 FI) / [] / SKIP.
Proof. erewrite f_equal2 with (f := fun c st => _ / _ || c / st / SKIP).
  eapply PE_Seq. eapply PE_AssStatic. reflexivity.
  step PE_While.
  step PE_While.
  step PE_While.
  step PE_WhileFixed.
  step PE_WhileFixedEnd.
  reflexivity. inversion H. inversion H. inversion H.
  reflexivity. reflexivity. Qed.

Example pe_loop_example4:
  (X ::= ANum 0;;
   WHILE BLe (AId X) (ANum 2) DO
     X ::= AMinus (ANum 1) (AId X)
   END) / [] || (SKIP;; WHILE BTrue DO SKIP END) / [(X,0)] / SKIP.
Proof. erewrite f_equal2 with (f := fun c st => _ / _ || c / st / SKIP).
  eapply PE_Seq. eapply PE_AssStatic. reflexivity.
  step PE_WhileFixedLoop.
  step PE_WhileLoop.
  step PE_WhileFixedEnd.
  inversion H. reflexivity. reflexivity. reflexivity. Qed.

(** ** Correctness *)

(** Because this partial evaluator can unroll a loop n-fold where n is
    a (finite) integer greater than one, in order to show it correct
    we need to perform induction not structurally on dynamic
    evaluation but on the number of times dynamic evaluation enters a
    loop body. *)

Reserved Notation "c1 '/' st '||' st' '#' n"
  (at level 40, st at level 39, st' at level 39).

Inductive ceval_count : com -> state -> state -> nat -> Prop :=
  | E'Skip : forall st,
      SKIP / st || st # 0
  | E'Ass  : forall st a1 n l,
      aeval st a1 = n ->
      (l ::= a1) / st || (update st l n) # 0
  | E'Seq : forall c1 c2 st st' st'' n1 n2,
      c1 / st  || st'  # n1 ->
      c2 / st' || st'' # n2 ->
      (c1 ;; c2) / st || st'' # (n1 + n2)
  | E'IfTrue : forall st st' b1 c1 c2 n,
      beval st b1 = true ->
      c1 / st || st' # n ->
      (IFB b1 THEN c1 ELSE c2 FI) / st || st' # n
  | E'IfFalse : forall st st' b1 c1 c2 n,
      beval st b1 = false ->
      c2 / st || st' # n ->
      (IFB b1 THEN c1 ELSE c2 FI) / st || st' # n
  | E'WhileEnd : forall b1 st c1,
      beval st b1 = false ->
      (WHILE b1 DO c1 END) / st || st # 0
  | E'WhileLoop : forall st st' st'' b1 c1 n1 n2,
      beval st b1 = true ->
      c1 / st || st' # n1 ->
      (WHILE b1 DO c1 END) / st' || st'' # n2 ->
      (WHILE b1 DO c1 END) / st || st'' # S (n1 + n2)

  where "c1 '/' st '||' st' # n" := (ceval_count c1 st st' n).

Tactic Notation "ceval_count_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "E'Skip" | Case_aux c "E'Ass" | Case_aux c "E'Seq"
  | Case_aux c "E'IfTrue" | Case_aux c "E'IfFalse"
  | Case_aux c "E'WhileEnd" | Case_aux c "E'WhileLoop" ].

Hint Constructors ceval_count.

Theorem ceval_count_complete: forall c st st',
  c / st || st' -> exists n, c / st || st' # n.
Proof. intros c st st' Heval.
  induction Heval;
    try inversion IHHeval1;
    try inversion IHHeval2;
    try inversion IHHeval;
    eauto. Qed.

Theorem ceval_count_sound: forall c st st' n,
  c / st || st' # n -> c / st || st'.
Proof. intros c st st' n Heval. induction Heval; eauto. Qed.

Theorem pe_compare_nil_lookup: forall pe_st1 pe_st2,
  pe_compare pe_st1 pe_st2 = [] ->
  forall V, pe_lookup pe_st1 V = pe_lookup pe_st2 V.
Proof. intros pe_st1 pe_st2 H V.
  apply (pe_compare_correct pe_st1 pe_st2 V).
  rewrite H. intro. inversion H0. Qed.

Theorem pe_compare_nil_override: forall pe_st1 pe_st2,
  pe_compare pe_st1 pe_st2 = [] ->
  forall st, pe_override st pe_st1 = pe_override st pe_st2.
Proof. intros pe_st1 pe_st2 H st.
  apply functional_extensionality. intros V.
  rewrite !pe_override_correct.
  apply pe_compare_nil_lookup with (V:=V) in H.
  rewrite H. reflexivity. Qed.

Reserved Notation "c' '/' pe_st' '/' c'' '/' st '||' st'' '#' n"
  (at level 40, pe_st' at level 39, c'' at level 39,
   st at level 39, st'' at level 39).

Inductive pe_ceval_count (c':com) (pe_st':pe_state) (c'':com)
                         (st:state) (st'':state) (n:nat) : Prop :=
  | pe_ceval_count_intro : forall st' n',
    c' / st || st' ->
    c'' / pe_override st' pe_st' || st'' # n' ->
    n' <= n ->
    c' / pe_st' / c'' / st || st'' # n
  where "c' '/' pe_st' '/' c'' '/' st '||' st'' '#' n" :=
        (pe_ceval_count c' pe_st' c'' st st'' n).

Hint Constructors pe_ceval_count.

Lemma pe_ceval_count_le: forall c' pe_st' c'' st st'' n n',
  n' <= n ->
  c' / pe_st' / c'' / st || st'' # n' ->
  c' / pe_st' / c'' / st || st'' # n.
Proof. intros c' pe_st' c'' st st'' n n' Hle H. inversion H.
  econstructor; try eassumption. omega. Qed.

Theorem pe_com_complete:
  forall c pe_st pe_st' c' c'', c / pe_st || c' / pe_st' / c'' ->
  forall st st'' n,
  (c / pe_override st pe_st || st'' # n) ->
  (c' / pe_st' / c'' / st || st'' # n).
Proof. intros c pe_st pe_st' c' c'' Hpe.
  pe_com_cases (induction Hpe) Case; intros st st'' n Heval;
  try (inversion Heval; subst;
       try (rewrite -> pe_bexp_correct, -> H in *; solve by inversion);
       []);
  eauto.
  Case "PE_AssStatic". econstructor. econstructor.
    rewrite -> pe_aexp_correct. rewrite <- pe_override_update_add.
    rewrite -> H. apply E'Skip. auto.
  Case "PE_AssDynamic". econstructor. econstructor. reflexivity.
    rewrite -> pe_aexp_correct. rewrite <- pe_override_update_remove.
    apply E'Skip. auto.
  Case "PE_Seq".
    edestruct IHHpe1 as [? ? ? Hskip ?]. eassumption.
    inversion Hskip. subst.
    edestruct IHHpe2. eassumption.
    econstructor; eauto. omega.
  Case "PE_If". inversion Heval; subst.
    SCase "E'IfTrue". edestruct IHHpe1. eassumption.
      econstructor. apply E_IfTrue. rewrite <- pe_bexp_correct. assumption.
      eapply E_Seq. eassumption. apply eval_assign.
      rewrite <- assign_removes. eassumption. eassumption.
    SCase "E_IfFalse". edestruct IHHpe2. eassumption.
      econstructor. apply E_IfFalse. rewrite <- pe_bexp_correct. assumption.
      eapply E_Seq. eassumption. apply eval_assign.
      rewrite -> pe_compare_override.
      rewrite <- assign_removes. eassumption. eassumption.
  Case "PE_WhileLoop".
    edestruct IHHpe1 as [? ? ? Hskip ?]. eassumption.
    inversion Hskip. subst.
    edestruct IHHpe2. eassumption.
    econstructor; eauto. omega.
  Case "PE_While". inversion Heval; subst.
    SCase "E_WhileEnd". econstructor. apply E_IfFalse.
      rewrite <- pe_bexp_correct. assumption.
      apply eval_assign.
      rewrite <- assign_removes. inversion H2; subst; auto.
      auto.
    SCase "E_WhileLoop".
      edestruct IHHpe1 as [? ? ? Hskip ?]. eassumption.
      inversion Hskip. subst.
      edestruct IHHpe2. eassumption.
      econstructor. apply E_IfTrue.
      rewrite <- pe_bexp_correct. assumption.
      repeat eapply E_Seq; eauto. apply eval_assign.
      rewrite -> pe_compare_override, <- assign_removes. eassumption.
      omega.
  Case "PE_WhileFixedLoop". apply ex_falso_quodlibet.
    generalize dependent (S (n1 + n2)). intros n.
    clear - Case H H0 IHHpe1 IHHpe2. generalize dependent st.
    induction n using lt_wf_ind; intros st Heval. inversion Heval; subst.
    SCase "E'WhileEnd". rewrite pe_bexp_correct, H in H7. inversion H7.
    SCase "E'WhileLoop".
      edestruct IHHpe1 as [? ? ? Hskip ?]. eassumption.
      inversion Hskip. subst.
      edestruct IHHpe2. eassumption.
      rewrite <- (pe_compare_nil_override _ _ H0) in H7.
      apply H1 in H7; [| omega]. inversion H7.
  Case "PE_WhileFixed". generalize dependent st.
    induction n using lt_wf_ind; intros st Heval. inversion Heval; subst.
    SCase "E'WhileEnd". rewrite pe_bexp_correct in H8. eauto.
    SCase "E'WhileLoop". rewrite pe_bexp_correct in H5.
      edestruct IHHpe1 as [? ? ? Hskip ?]. eassumption.
      inversion Hskip. subst.
      edestruct IHHpe2. eassumption.
      rewrite <- (pe_compare_nil_override _ _ H1) in H8.
      apply H2 in H8; [| omega]. inversion H8.
      econstructor; [ eapply E_WhileLoop; eauto | eassumption | omega].
Qed.

Theorem pe_com_sound:
  forall c pe_st pe_st' c' c'', c / pe_st || c' / pe_st' / c'' ->
  forall st st'' n,
  (c' / pe_st' / c'' / st || st'' # n) ->
  (c / pe_override st pe_st || st'').
Proof. intros c pe_st pe_st' c' c'' Hpe.
  pe_com_cases (induction Hpe) Case;
    intros st st'' n [st' n' Heval Heval' Hle];
    try (inversion Heval; []; subst);
    try (inversion Heval'; []; subst); eauto.
  Case "PE_AssStatic". rewrite <- pe_override_update_add. apply E_Ass.
    rewrite -> pe_aexp_correct. rewrite -> H. reflexivity.
  Case "PE_AssDynamic". rewrite <- pe_override_update_remove. apply E_Ass.
    rewrite <- pe_aexp_correct. reflexivity.
  Case "PE_Seq". eapply E_Seq; eauto.
  Case "PE_IfTrue". apply E_IfTrue.
    rewrite -> pe_bexp_correct. rewrite -> H. reflexivity.
    eapply IHHpe. eauto.
  Case "PE_IfFalse". apply E_IfFalse.
    rewrite -> pe_bexp_correct. rewrite -> H. reflexivity.
    eapply IHHpe. eauto.
  Case "PE_If". inversion Heval; subst; inversion H7; subst; clear H7.
    SCase "E_IfTrue".
      eapply ceval_deterministic in H8; [| apply eval_assign]. subst.
      rewrite <- assign_removes in Heval'.
      apply E_IfTrue. rewrite -> pe_bexp_correct. assumption.
      eapply IHHpe1. eauto.
    SCase "E_IfFalse".
      eapply ceval_deterministic in H8; [| apply eval_assign]. subst.
      rewrite -> pe_compare_override in Heval'.
      rewrite <- assign_removes in Heval'.
      apply E_IfFalse. rewrite -> pe_bexp_correct. assumption.
      eapply IHHpe2. eauto.
  Case "PE_WhileEnd". apply E_WhileEnd.
    rewrite -> pe_bexp_correct. rewrite -> H. reflexivity.
  Case "PE_WhileLoop". eapply E_WhileLoop.
    rewrite -> pe_bexp_correct. rewrite -> H. reflexivity.
    eapply IHHpe1. eauto. eapply IHHpe2. eauto.
  Case "PE_While". inversion Heval; subst.
    SCase "E_IfTrue".
      inversion H9. subst. clear H9.
      inversion H10. subst. clear H10.
      eapply ceval_deterministic in H11; [| apply eval_assign]. subst.
      rewrite -> pe_compare_override in Heval'.
      rewrite <- assign_removes in Heval'.
      eapply E_WhileLoop. rewrite -> pe_bexp_correct. assumption.
      eapply IHHpe1. eauto.
      eapply IHHpe2. eauto.
    SCase "E_IfFalse". apply ceval_count_sound in Heval'.
      eapply ceval_deterministic in H9; [| apply eval_assign]. subst.
      rewrite <- assign_removes in Heval'.
      inversion H2; subst.
      SSCase "c2'' = SKIP". inversion Heval'. subst. apply E_WhileEnd.
        rewrite -> pe_bexp_correct. assumption.
      SSCase "c2'' = WHILE b1 DO c1 END". assumption.
  Case "PE_WhileFixedEnd". eapply ceval_count_sound. apply Heval'.
  Case "PE_WhileFixedLoop".
    apply loop_never_stops in Heval. inversion Heval.
  Case "PE_WhileFixed".
    clear - Case H1 IHHpe1 IHHpe2 Heval.
    remember (WHILE pe_bexp pe_st b1 DO c1';; c2' END) as c'.
    ceval_cases (induction Heval) SCase;
      inversion Heqc'; subst; clear Heqc'.
    SCase "E_WhileEnd". apply E_WhileEnd.
      rewrite pe_bexp_correct. assumption.
    SCase "E_WhileLoop".
      assert (IHHeval2' := IHHeval2 (refl_equal _)).
      apply ceval_count_complete in IHHeval2'. inversion IHHeval2'.
      clear IHHeval1 IHHeval2 IHHeval2'.
      inversion Heval1. subst.
      eapply E_WhileLoop. rewrite pe_bexp_correct. assumption. eauto.
      eapply IHHpe2. econstructor. eassumption.
      rewrite <- (pe_compare_nil_override _ _ H1). eassumption. apply le_n.
Qed.

Corollary pe_com_correct:
  forall c pe_st pe_st' c', c / pe_st || c' / pe_st' / SKIP ->
  forall st st'',
  (c / pe_override st pe_st || st'') <->
  (exists st', c' / st || st' /\ pe_override st' pe_st' = st'').
Proof. intros c pe_st pe_st' c' H st st''. split.
  Case "->". intros Heval.
    apply ceval_count_complete in Heval. inversion Heval as [n Heval'].
    apply pe_com_complete with (st:=st) (st'':=st'') (n:=n) in H.
    inversion H as [? ? ? Hskip ?]. inversion Hskip. subst. eauto.
    assumption.
  Case "<-". intros [st' [Heval Heq]]. subst st''.
    eapply pe_com_sound in H. apply H.
    econstructor. apply Heval. apply E'Skip. apply le_n.
Qed.

End Loop.

(* ####################################################### *)
(** * Partial Evaluation of Flowchart Programs *)

(** Instead of partially evaluating [WHILE] loops directly, the
    standard approach to partially evaluating imperative programs is
    to convert them into _flowcharts_.  In other words, it turns out
    that adding labels and jumps to our language makes it much easier
    to partially evaluate.  The result of partially evaluating a
    flowchart is a residual flowchart.  If we are lucky, the jumps in
    the residual flowchart can be converted back to [WHILE] loops, but
    that is not possible in general; we do not pursue it here. *)

(** ** Basic blocks *)

(** A flowchart is made of _basic blocks_, which we represent with the
    inductive type [block].  A basic block is a sequence of
    assignments (the constructor [Assign]), concluding with a
    conditional jump (the constructor [If]) or an unconditional jump
    (the constructor [Goto]).  The destinations of the jumps are
    specified by _labels_, which can be of any type.  Therefore, we
    parameterize the [block] type by the type of labels. *)

Inductive block (Label:Type) : Type :=
  | Goto : Label -> block Label
  | If : bexp -> Label -> Label -> block Label
  | Assign : id -> aexp -> block Label -> block Label.

Tactic Notation "block_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "Goto" | Case_aux c "If" | Case_aux c "Assign" ].

Arguments Goto {Label} _.
Arguments If   {Label} _ _ _.
Arguments Assign {Label} _ _ _.

(** We use the "even or odd" program, expressed above in Imp, as our
    running example.  Converting this program into a flowchart turns
    out to require 4 labels, so we define the following type. *)

Inductive parity_label : Type :=
  | entry : parity_label
  | loop  : parity_label
  | body  : parity_label
  | done  : parity_label.

(** The following [block] is the basic block found at the [body] label
    of the example program. *)

Definition parity_body : block parity_label :=
  Assign Y (AMinus (AId Y) (ANum 1))
   (Assign X (AMinus (ANum 1) (AId X))
     (Goto loop)).

(** To evaluate a basic block, given an initial state, is to compute
    the final state and the label to jump to next.  Because basic
    blocks do not _contain_ loops or other control structures,
    evaluation of basic blocks is a total function -- we don't need to
    worry about non-termination. *)

Fixpoint keval {L:Type} (st:state) (k : block L) : state * L :=
  match k with
  | Goto l => (st, l)
  | If b l1 l2 => (st, if beval st b then l1 else l2)
  | Assign i a k => keval (update st i (aeval st a)) k
  end.

Example keval_example:
  keval empty_state parity_body
  = (update (update empty_state Y 0) X 1, loop).
Proof. reflexivity. Qed.

(** ** Flowchart programs *)

(** A flowchart program is simply a lookup function that maps labels
    to basic blocks.  Actually, some labels are _halting states_ and
    do not map to any basic block.  So, more precisely, a flowchart
    [program] whose labels are of type [L] is a function from [L] to
    [option (block L)]. *)

Definition program (L:Type) : Type := L -> option (block L).

Definition parity : program parity_label := fun l =>
  match l with
  | entry => Some (Assign X (ANum 0) (Goto loop))
  | loop => Some (If (BLe (ANum 1) (AId Y)) body done)
  | body => Some parity_body
  | done => None (* halt *)
  end.

(** Unlike a basic block, a program may not terminate, so we model the
    evaluation of programs by an inductive relation [peval] rather
    than a recursive function. *)

Inductive peval {L:Type} (p : program L)
  : state -> L -> state -> L -> Prop :=
  | E_None: forall st l,
    p l = None ->
    peval p st l st l
  | E_Some: forall st l k st' l' st'' l'',
    p l = Some k ->
    keval st k = (st', l') ->
    peval p st' l' st'' l'' ->
    peval p st l st'' l''.

Example parity_eval: peval parity empty_state entry empty_state done.
Proof. erewrite f_equal with (f := fun st => peval _ _ _ st _).
  eapply E_Some. reflexivity. reflexivity.
  eapply E_Some. reflexivity. reflexivity.
  apply E_None. reflexivity.
  apply functional_extensionality. intros i. rewrite update_same; auto.
Qed.

Tactic Notation "peval_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "E_None" | Case_aux c "E_Some" ].

(** ** Partial evaluation of basic blocks and flowchart programs *)

(** Partial evaluation changes the label type in a systematic way: if
    the label type used to be [L], it becomes [pe_state * L].  So the
    same label in the original program may be unfolded, or blown up,
    into multiple labels by being paired with different partial
    states.  For example, the label [loop] in the [parity] program
    will become two labels: [([(X,0)], loop)] and [([(X,1)], loop)].
    This change of label type is reflected in the types of [pe_block]
    and [pe_program] defined presently. *)

Fixpoint pe_block {L:Type} (pe_st:pe_state) (k : block L)
  : block (pe_state * L) :=
  match k with
  | Goto l => Goto (pe_st, l)
  | If b l1 l2 =>
    match pe_bexp pe_st b with
    | BTrue  => Goto (pe_st, l1)
    | BFalse => Goto (pe_st, l2)
    | b'     => If b' (pe_st, l1) (pe_st, l2)
    end
  | Assign i a k =>
    match pe_aexp pe_st a with
    | ANum n => pe_block (pe_add pe_st i n) k
    | a' => Assign i a' (pe_block (pe_remove pe_st i) k)
    end
  end.

Example pe_block_example:
  pe_block [(X,0)] parity_body
  = Assign Y (AMinus (AId Y) (ANum 1)) (Goto ([(X,1)], loop)).
Proof. reflexivity. Qed.

Theorem pe_block_correct: forall (L:Type) st pe_st k st' pe_st' (l':L),
  keval st (pe_block pe_st k) = (st', (pe_st', l')) ->
  keval (pe_override st pe_st) k = (pe_override st' pe_st', l').
Proof. intros. generalize dependent pe_st. generalize dependent st.
  block_cases (induction k as [l | b l1 l2 | i a k]) Case;
    intros st pe_st H.
  Case "Goto". inversion H; reflexivity.
  Case "If".
    replace (keval st (pe_block pe_st (If b l1 l2)))
       with (keval st (If (pe_bexp pe_st b) (pe_st, l1) (pe_st, l2)))
       in H by (simpl; destruct (pe_bexp pe_st b); reflexivity).
    simpl in *. rewrite pe_bexp_correct.
    destruct (beval st (pe_bexp pe_st b)); inversion H; reflexivity.
  Case "Assign".
    simpl in *. rewrite pe_aexp_correct.
    destruct (pe_aexp pe_st a); simpl;
      try solve [rewrite pe_override_update_add; apply IHk; apply H];
      solve [rewrite pe_override_update_remove; apply IHk; apply H].
Qed.

Definition pe_program {L:Type} (p : program L)
  : program (pe_state * L) :=
  fun pe_l => match pe_l with (pe_st, l) =>
                option_map (pe_block pe_st) (p l)
              end.

Inductive pe_peval {L:Type} (p : program L)
  (st:state) (pe_st:pe_state) (l:L) (st'o:state) (l':L) : Prop :=
  | pe_peval_intro : forall st' pe_st',
    peval (pe_program p) st (pe_st, l) st' (pe_st', l') ->
    pe_override st' pe_st' = st'o ->
    pe_peval p st pe_st l st'o l'.

Theorem pe_program_correct:
  forall (L:Type) (p : program L) st pe_st l st'o l',
  peval p (pe_override st pe_st) l st'o l' <->
  pe_peval p st pe_st l st'o l'.
Proof. intros.
  split; [Case "->" | Case "<-"].
  Case "->". intros Heval.
    remember (pe_override st pe_st) as sto.
    generalize dependent pe_st. generalize dependent st.
    peval_cases (induction Heval as
      [ sto l Hlookup | sto l k st'o l' st''o l'' Hlookup Hkeval Heval ])
      SCase; intros st pe_st Heqsto; subst sto.
    SCase "E_None". eapply pe_peval_intro. apply E_None.
      simpl. rewrite Hlookup. reflexivity. reflexivity.
    SCase "E_Some".
      remember (keval st (pe_block pe_st k)) as x.
      destruct x as [st' [pe_st' l'_]].
      symmetry in Heqx. erewrite pe_block_correct in Hkeval by apply Heqx.
      inversion Hkeval. subst st'o l'_. clear Hkeval.
      edestruct IHHeval. reflexivity. subst st''o. clear IHHeval.
      eapply pe_peval_intro; [| reflexivity]. eapply E_Some; eauto.
      simpl. rewrite Hlookup. reflexivity.
  Case "<-". intros [st' pe_st' Heval Heqst'o].
    remember (pe_st, l) as pe_st_l.
    remember (pe_st', l') as pe_st'_l'.
    generalize dependent pe_st. generalize dependent l.
    peval_cases (induction Heval as
      [ st [pe_st_ l_] Hlookup
      | st [pe_st_ l_] pe_k st' [pe_st'_ l'_] st'' [pe_st'' l'']
        Hlookup Hkeval Heval ])
      SCase; intros l pe_st Heqpe_st_l;
      inversion Heqpe_st_l; inversion Heqpe_st'_l'; repeat subst.
    SCase "E_None". apply E_None. simpl in Hlookup.
      destruct (p l'); [ solve [ inversion Hlookup ] | reflexivity ].
    SCase "E_Some".
      simpl in Hlookup. remember (p l) as k.
      destruct k as [k|]; inversion Hlookup; subst.
      eapply E_Some; eauto. apply pe_block_correct. apply Hkeval.
Qed.

author: tyage

repo: coq-practice

save_path: github-repos/coq/tyage-coq-practice


text:
(** Wie in der Vorlesung Theoretische Informatik I werden die einzelne Komponenten eines
 deterministischen Transitionssystem (DTS) als 5-Tupel beschrieben.

DTS = (Q, Sigma, delta, q0, F) mit

* Q, als Zustandsmenge
* Sigma, als Eingabealphabet
* delta: Q x Sigma -> Q, als Zustandsüberführungsfunktion
* q0, als Startzustand
* F Teilmenge von Q, als Menge der akzeptierenden Zustände.

Diese Komponenten werden nachfolgend definiert.*)

Module Type Sigma.
Require Word_Prop.
(** Der Typ des Eingabealphabets.*)
Parameter Sigma : Type.
End Sigma.

Module Type Q.
(** Der Typ der Zustände.*)
Parameter Q : Type.
(** Der Startzustand. *)
Parameter q0 : Q.
End Q.
(*
Module Par (S:Sigma) (Q:Q).
Import Q.
Import Sigma.
Definition Q := Q.
Definition Sigma := Sigma.
(** Die Transitionsfunktion - delta.*)
Definition delta : Q -> Sigma -> Q.
(** Die Funktion, die entscheidet, ob ein Zustand ein akzeptierender Zustand ist. *)
Definition is_accepting : Q -> Type. (*Proofs as programs Pädagogik*)

*)
Require Import Word_Prop.
Module WordSig (S : Sigma) (Q : Q) : Sigma with Definition Sigma := @Word S.Sigma.
Import Q.
Definition Sigma := @Word S.Sigma.
Definition Q := Q.
Definition delta := Q -> Sigma -> Q.
Definition is_accepting := Q -> Type.
Definition q0 := q0.
End WordSig.

Module DTS_Fun (Par : DTS_Par) <: DTS_Par.
Import Par.
Import Word_Prop.

Definition Q := Q.
Definition delta := delta.
Definition is_accepting := is_accepting.
Definition q0 := q0.

(** Um zu definieren, wann ein Wort akzeptiert wird, müssen noch einige Vorüberlegungen
getroffen werden. Hierzu wird die erweiterte Transitionsfunktion [delta_hat] bzw. benötigt. *)

(** Die erweiterte Überführungsfunktion [delta_hat], wie in der Vorlesung definiert.*)
Fixpoint delta_hat (q : Q) (w : @Word Sigma) : Q :=
   match w with
    | eps       => q
    | snoc w' h => delta (delta_hat q w' ) h
  end.

(** Um ein zusätzliches Zeichen und ein Wort aus dem Eingabealphabet abzuarbeiten kann
erst das Zeichen vor das Wort gehängt werden, um dann [delta_hat] von dem Ausgangszustand
darauf anzuwenden. Die andere Variante ist, dass zuerst der Folgezustand mit [delta] von dem
Zeichen und dem Ausgangszustand berechnet wird und davon ausgehend dann das Wort
abgearbeitet wird.*)
Lemma delta_hat_Lemma (q : Q) (a : Sigma) (w : @Word Sigma) :
  delta_hat q (concat_word (snoc eps a) w) = delta_hat (delta q a) w.
Proof.
induction w.
  - simpl.
    reflexivity.
  - simpl.
    rewrite IHw.
    reflexivity.
Defined.

(** Die Abarbeitung eines aus zwei Teilwörtern bestehenden Wortes*)
Theorem delta_hat_app : forall w v : @Word Sigma, forall q : Q,
  delta_hat q (concat_word w v) = delta_hat (delta_hat q w) v.
Proof.
  induction v.
  - simpl.
    intros q.
    reflexivity.
  - simpl.
    intros.
    rewrite <- IHv.
    reflexivity.
Defined.

(** Die von einem deterministischen Transitionssystems beschriebene Sprachen definiert
durch [is_accepting].*)
Definition Lang_delta (w : @Word Sigma) : Type :=
  is_accepting (delta_hat q0 w).

(** Die Konfigurationsübergangsrelation*)

(** Der Typ der Konfigurationen eines DTS, Conf = Q x @Word Sigma*.*)
Definition Conf := Q * (@Word Sigma) : Type.

(** Ein einzelner Konfigurationsschritt. Ausgehend von einer Konfiguration, einem Zeichen a
aus Sigma und einem Wort w, wird das Zeichen durch [delta] abgearbeitet und führt zur
nachfolgenden Konfiguration.*)

Inductive Conf_step : Conf -> Conf -> Type :=
 | one_step : forall (q : Q) (a : Sigma) (w : @Word Sigma),
                        Conf_step (q, (concat_word [a] w)) (delta q a, w).

(** Die reflexiv-transitive Hülle von Conf_rel_DFA_step um die eigentliche Konfigurations-
übergangsrelation zu beschreiben.*)
Inductive Conf_rel : Conf -> Conf -> Type :=
  | refl  : forall (K : Conf), Conf_rel K K
  | step  : forall (K L M : Conf), Conf_step K L -> Conf_rel L M -> Conf_rel K M.

(** Die von einem deterministischen Transitionssystems beschriebene Sprachen definiert
durch [Conf_rel].*)
Definition Lang_Conf (w: @Word Sigma) : Type :=
{p : Q & (is_accepting p * Conf_rel (q0, w) (p, eps))%type}.

(** Für die Anwendung des Pumping Lemmas muss die Abarbeitung eines Wortes in einer Liste
gespeichert werden, da diese Informationen enthält, ob ein Zustand mehrfach durchlaufen wird.
Dies ist der Fall, wenn die Anzahl der Konfigurationen innerhalb der Liste länger ist, als die Anzahl
der Zustände des Automaten.*)

(* Ableiten der nächsten Konfiguration [next_Conf].*)
Fixpoint next_Conf  (conf : Conf) : option Conf :=
  match conf with
    | (q, eps)      => None
    | (q, snoc w a) => Some (delta q a, w)
  end.

(*Konfigurationssequenz in einer Liste speichern.*)
Fixpoint conf_seq' (w : @Word Sigma) : Q -> list Conf :=
  match w with
    | eps        => fun q : Q => cons (q, eps) nil
    | snoc w' a  => fun q : Q => cons (q, w) (conf_seq' w' (delta q a))
  end.

(*Print conf_seq'.*)
(* aber im 2. Fall muss (q, w) zur Liste hinzugefuegt werden, oder? *)

Fixpoint conf_seq (conf : Conf) : list Conf :=
  match conf with
    | (q, w) => conf_seq' w q
  end.

(*################# Alternativ ###################*)

(* Ich habe auch nichts wirklich Besseres zu bieten. Man koennte vermutlich einen
   anonymen Fixpunkt benutzen, aber dadurch wird es nicht lesbarer und
   ich sehe auch sonst keinen Vorteil.
   Die "Wrapper" Funktion muss dann natuerlich kein Fixpunkt sein. *)

Fixpoint conf_list (w : @Word Sigma) (q : Q) : list Conf :=
 let conf := (q, w) in
  match w with
    | eps       => cons conf nil
    | snoc w' a => cons conf (conf_list w' (delta q a))
  end.

Definition conf_to_conf_list (conf : Conf) : list Conf :=
  let (q, w) := conf in conf_list w q.

End DTS_Fun.

author: margrit

repo: Code

save_path: github-repos/coq/margrit-Code


Require Import Crypto.Specific.Framework.RawCurveParameters.
Require Import Crypto.Util.LetIn.

(***
Modulus : 2^384 - 2^128 - 2^96 + 2^32 - 1
Base: 20 + 4/19
***)

Definition curve : CurveParameters :=
  {|
    sz := 19%nat;
    base := 20 + 4/19;
    bitwidth := 32;
    s := 2^384;
    c := [(1, 1); (2^32, -1); (2^96, 1); (2^128, 1)];
    carry_chains := Some [[5; 3; 0; 18]; [6; 4; 1; 0; 7; 5; 2; 8; 3; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18]; [6; 4; 1; 0]]%nat;

    a24 := None;
    coef_div_modulus := Some 2%nat;

    goldilocks := None;
    karatsuba := None;
    montgomery := false;
    freeze := Some true;
    ladderstep := false;

    mul_code := None;

    square_code := None;

    upper_bound_of_exponent_loose := None;
    upper_bound_of_exponent_tight := None;
    allowable_bit_widths := None;
    freeze_extra_allowable_bit_widths := None;
    modinv_fuel := None
  |}.

Ltac extra_prove_mul_eq _ := idtac.
Ltac extra_prove_square_eq _ := idtac.


text:
(* This file is part of the Linear Logic formalization in Coq:
https://github.com/brunofx86/LL *)

(** ** Sets, Decidable Sets and Polarities
*)

Require Import Arith.

(** Just a set
 *)

Module Type Eqset.
  Parameter A : Type.
End Eqset.

(** A set with decidable equality
 *)
Module Type Eqset_dec <: Eqset.
  Parameter A : Type.
  Parameter eqA_dec : forall x y : A, {x = y} + {x <> y}.
End Eqset_dec.

(** A set with decidable equality and a function defining which atoms are positive
 *)

Module Type Eqset_dec_pol <: Eqset_dec.
  Parameter A : Type.
  Parameter eqA_dec : forall x y : A, {x = y} + {x <> y}.
  Parameter isPositive : nat -> bool.
End Eqset_dec_pol.

(** An example of Eqset_dec_pol *)
Module NatSet <: Eqset_dec_pol.
  Definition A := nat.
  Definition eqA_dec := Nat.eq_dec.
  Fixpoint isPositive (n:nat) :=
    match n with
    | 0%nat => false
    | 1%nat => true
    | S (S n) => isPositive n
    end.
End NatSet.

repo: LL


text:
Require Import Nat Arith Bool.

Inductive Nat : Type := zero : Nat | succ : Nat -> Nat.

Scheme Equality for Nat.

Inductive Lst : Type := nil : Lst | cons : Nat -> Lst -> Lst.

Inductive Tree : Type := node : Nat -> Tree -> Tree -> Tree |  leaf : Tree.

Inductive Pair : Type := mkpair : Nat -> Nat -> Pair
with ZLst : Type := zcons : Pair -> ZLst -> ZLst |  znil : ZLst.

Fixpoint less (less_arg0 : Nat) (less_arg1 : Nat) : bool
           := match less_arg0, less_arg1 with
              | x, zero => false
              | zero, succ x => true
              | succ x, succ y => less x y
              end.

Fixpoint mem (mem_arg0 : Nat) (mem_arg1 : Lst) : bool
           := match mem_arg0, mem_arg1 with
              | x, nil => false
              | x, cons y z => orb (Nat_beq x y) (mem x z)
              end.

Fixpoint insort (insort_arg0 : Nat) (insort_arg1 : Lst) : Lst
           := match insort_arg0, insort_arg1 with
              | i, nil => cons i nil
              | i, cons x y => if less i x then cons i (cons x y) else cons x (insort i y)
              end.

Fixpoint sort (sort_arg0 : Lst) : Lst
           := match sort_arg0 with
              | nil => nil
              | cons x y => insort x (sort y)
              end.

Lemma Nat_beq_eq : forall (x y : Nat), Nat_beq x y = true -> x = y.
Proof.
  intros.
  generalize dependent y.
  induction x.
  - intros. destruct y.
    + reflexivity.
    + discriminate.
  - intros. destruct y.
    + discriminate.
    + simpl in H. apply IHx in H. rewrite H. reflexivity.
Qed.

Theorem theorem0 : forall (x : Nat) (y : Nat) (z : Lst), not (eq x y) -> eq (mem x (insort y z)) true -> eq (mem x z) true.
Proof.
  intros.
  induction z.
  - simpl in H0. rewrite orb_false_r in H0. apply Nat_beq_eq in H0. contradiction.
  - simpl in H0. simpl. destruct (less y n) eqn:?.
    + simpl in H0. apply orb_true_iff in H0. destruct H0.
      * apply Nat_beq_eq in H0. contradiction.
      * assumption.
    + simpl in H0. apply orb_true_iff in H0. destruct H0.
      * rewrite H0. reflexivity.
      * apply IHz in H0. rewrite H0. apply orb_true_r.
Qed.

author: qsctr

repo: coq-quantified-theorems


text:
Require Import CodeProofDeps.
Require Import Ident.
Require Import Constants.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import CommonLib.
Require Import AbsAccessor.Spec.
Require Import PSCIAux2.Layer.
Require Import PSCI.Code.psci_features.

Require Import PSCI.LowSpecs.psci_features.

Local Open Scope Z_scope.

Section CodeProof.

  Context `{real_params: RealParams}.
  Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
  Context `{Hmwd: UseMemWithData memb}.

  Let mem := mwd (cdata RData).

  Context `{Hstencil: Stencil}.
  Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
  Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.

  Let L : compatlayer (cdata RData) :=
    _set_psci_result_x0 ↦ gensem set_psci_result_x0_spec
  .

  Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
  Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.

  Section BodyProof.

    Context `{Hwb: WritableBlockOps}.
    Variable (sc: stencil).
    Variables (ge: genv) (STENCIL_MATCHES: stencil_matches sc ge).

    Variable b_set_psci_result_x0: block.
    Hypothesis h_set_psci_result_x0_s : Genv.find_symbol ge _set_psci_result_x0 = Some b_set_psci_result_x0.
    Hypothesis h_set_psci_result_x0_p : Genv.find_funct_ptr ge b_set_psci_result_x0
                                        = Some (External (EF_external _set_psci_result_x0
                                                         (signature_of_type (Tcons tulong Tnil) tvoid cc_default))
                                               (Tcons tulong Tnil) tvoid cc_default).
    Local Opaque set_psci_result_x0_spec.

    Lemma psci_features_body_correct:
      forall m d d' env le rec_base rec_offset psci_func_id
             (Henv: env = PTree.empty _)
             (Hinv: high_level_invariant d)
             (HPTrec: PTree.get _rec le = Some (Vptr rec_base (Int.repr rec_offset)))
             (HPTpsci_func_id: PTree.get _psci_func_id le = Some (Vint psci_func_id))
             (Hspec: psci_features_spec0 (rec_base, rec_offset) (Int.unsigned psci_func_id) d = Some d'),
           exists le', (exec_stmt ge env le ((m, d): mem) psci_features_body E0 le' (m, d') Out_normal).
    Proof.
      solve_code_proof Hspec psci_features_body; eexists;
        repeat (repeat sstep; try big_vcgen;
                match goal with
                | [H: ?a = ?c |- context[zeq ?a ?b]] =>
                    destruct (zeq a b); try omega
                | _ => idtac
                end).
    Qed.

  End BodyProof.

End CodeProof.

author: columbia


text:
(** * Basic Attention Token contract *)
(** This implementation of the Basic Attention Token is a based on
    https://github.com/brave-intl/basic-attention-token-crowdsale/blob/66c886cc4bfb0493d9e7980f392ca7921ef1e7fc/contracts/BAToken.sol
    The implementation includes some minor changes that fixes bugs present in the original Solidity implementation.

    This file contains contract function definitions.
    All contract types and utility functions are defined in [ConCert.Examples.BAT.BATCommon].
    Proofs for this contract can be found in [ConCert.Examples.BAT.BATFixedCorrect].

    The BAT contract is a combination of a EIP20 token contract and a crowdsale contract.
    This implementation extends the EIP20 contract implemented in [ConCert.Examples.EIP20.EIP20Token].
*)
From Coq Require Import List. Import ListNotations.
From Coq Require Import ZArith_base.
From ConCert.Utils Require Import Extras.
From ConCert.Utils Require Import RecordUpdate.
From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import Containers.
From ConCert.Execution Require Import Monad.
From ConCert.Execution Require Import Serializable.
From ConCert.Execution Require Import ResultMonad.
From ConCert.Execution Require Import ContractCommon.
From ConCert.Examples.BAT Require Import BATCommon.
From ConCert.Examples.EIP20 Require EIP20Token.

(** * Contract functions *)
Section BATFixed.
  Context {BaseTypes : ChainBase}.

  Open Scope N_scope.
  (** ** Init *)
  (** This function only gets called once when contract is deployed.
      Will set up the initial storage state of the contract.
  *)
  Definition init (chain : Chain)
                  (ctx : ContractCallContext)
                  (setup : Setup)
                  : result State Error :=
    (** BAToken should not be deployable if one of the following conditions does not hold on [setup]
        - funding period is non-empty
        - funding period does not start before the slot where the contract is deployed
        - minimum tokens to fund should not be less than the maximum tokens allowed
        - the initial supply of tokens should be less than the maximum tokens allowed
        - token exchange rate must be larger than 0
        - it must be possible to get over minimum token bound without going over maximum
        For the last condition we check that [tokenExchangeRate <= tokenCreationCap - tokenCreationMin],
        however this does exclude a few possible configurations where the contract still works as intended.
        However, these are not likely to come up in real use cases.
    *)
    do _ <- throwIf ((setup.(_fundingEnd) <=? setup.(_fundingStart))%nat
            || (setup.(_fundingStart) <? chain.(current_slot))%nat
            || (setup.(_tokenCreationCap) <? setup.(_tokenCreationMin))
            || (setup.(_tokenCreationCap) <? setup.(_batFund))
            || (setup.(_tokenExchangeRate) =? 0)
            || ((setup.(_tokenCreationCap) - setup.(_tokenCreationMin)) <? setup.(_tokenExchangeRate))
            || address_eqb setup.(_batFundDeposit) ctx.(ctx_contract_address)
            || address_eqb setup.(_fundDeposit) ctx.(ctx_contract_address)) default_error;
    let token_state := {|
        EIP20Token.balances := FMap.add setup.(_batFundDeposit) setup.(_batFund) FMap.empty;
        EIP20Token.total_supply := setup.(_batFund);
        EIP20Token.allowances := FMap.empty;
      |} in
    Ok {|
      (** EIP20Token initialization: *)
      token_state := token_state;
      (** BAT initialization: *)
      initSupply := setup.(_batFund);
      isFinalized := false;
      fundDeposit := setup.(_fundDeposit);
      batFundDeposit := setup.(_batFundDeposit);
      fundingStart := setup.(_fundingStart);
      fundingEnd := setup.(_fundingEnd);
      tokenExchangeRate := setup.(_tokenExchangeRate);
      tokenCreationCap := setup.(_tokenCreationCap);
      tokenCreationMin := setup.(_tokenCreationMin);
    |}.

  (** ** Create Tokens *)
  (** This entrypoint allows users to fund the crowdsale in return for tokens *)
  Definition try_create_tokens (sender : Address)
                               (sender_payload : Amount)
                               (current_slot : nat)
                               (state : State)
                               : result State Error :=
  (** Early return if funding is finalized, funding period hasn't started yet,
      or funding period is over *)
    do _ <- throwIf (state.(isFinalized)
            || (Nat.ltb current_slot state.(fundingStart))
            || (Nat.ltb state.(fundingEnd) current_slot)
            || (address_eqb sender state.(batFundDeposit))) default_error;
    (** Here we deviate slightly from the reference implementation. They only check for = 0,
        but since ConCert's payloads may be negative numbers, we must extend this check to <= 0 *)
    do _ <- throwIf (Z.leb sender_payload 0) default_error;
    (** Note: this conversion from Z to N is safe because by assumption sender_payload > 0 *)
    let tokens := (Z.to_N sender_payload) * state.(tokenExchangeRate) in
    let checkedSupply := (total_supply state) + tokens in
    do _ <- throwIf (state.(tokenCreationCap) <? checkedSupply) default_error;
    let new_token_state : EIP20Token.State := {|
      EIP20Token.total_supply := checkedSupply;
      EIP20Token.balances := FMap.partial_alter (fun balance =>
        Some (with_default 0 balance + tokens)) sender (balances state);
      EIP20Token.allowances := allowances state;
    |} in
    Ok (state<|token_state := new_token_state|>).

  (** ** Refund *)
  (** This entrypoint can be called if crowdsale is not successfully funded.
      Users calling this entrypoint will have their tokens removed and get their money refunded.
  *)
  Definition try_refund (sender : Address)
                        (current_slot : nat)
                        (state : State)
                        : result (State * list ActionBody) Error :=
    (** Early return if funding is finalized, or funding period is NOT over,
        or if total supply exceeds or is equal to the minimum fund tokens. *)
    do _ <- throwIf (state.(isFinalized)
            || (Nat.leb current_slot state.(fundingEnd))
            || (state.(tokenCreationMin) <=? (total_supply state))) default_error;
    (** Don't allow the batFundDeposit account to refund *)
    do _ <- throwIf (address_eqb sender state.(batFundDeposit)) default_error;
    do sender_bats <- result_of_option (FMap.find sender (balances state)) default_error ;
    do _ <- throwIf (sender_bats =? 0) default_error;
    let new_total_supply := (total_supply) state - sender_bats in
    (** Convert tokens back to the currency of the blockchain, to be sent back to the sender address *)
    let amount_to_send := Z.of_N (sender_bats / state.(tokenExchangeRate)) in
    let new_token_state : EIP20Token.State := {|
      EIP20Token.total_supply := new_total_supply;
      EIP20Token.balances := FMap.add sender 0 (balances state);
      EIP20Token.allowances := allowances state;
    |} in
    let new_state := state<|token_state := new_token_state|> in
    let send_act := act_transfer sender amount_to_send in
      Ok (new_state, [send_act]).

  (** ** Finalize *)
  (** This entrypoint will end the crowdsale and pay out the money to the owner.
      Can only be called if funding was successful.
  *)
  Definition try_finalize (sender : Address)
                          (current_slot : nat)
                          (contract_balance : Amount)
                          (state : State)
                          : result (State * list ActionBody) Error :=
    (** Early return if funding is finalized, or if sender is NOT the fund deposit address,
        or if the total token supply is less than the minimum required amount,
        or if it is too early to end funding and the total token supply has not reached the cap.
        Note: the last requirement makes it possible to end a funding early if the cap has been reached.
    *)
    do _ <- throwIf (state.(isFinalized) ||
                    (address_neqb sender state.(fundDeposit)) ||
                    ((total_supply state) <? state.(tokenCreationMin))) default_error;
    do _ <- throwIf ((Nat.leb current_slot state.(fundingEnd)) &&
                      negb ((total_supply state) =? state.(tokenCreationCap)))
                      default_error;
    (** Send the currency of the contract back to the fund *)
    let send_act := act_transfer state.(fundDeposit) contract_balance in
    let new_state := state<|isFinalized := true|> in
    Ok (new_state, [send_act]).

  (** ** Receive *)
  (** This is the main entrypoint function.
      All contract calls will be handled by this function
  *)
  Open Scope Z_scope.
  Definition receive_bat (chain : Chain)
                         (ctx : ContractCallContext)
                         (state : State)
                         (maybe_msg : option Msg)
                         : result (State * list ActionBody) Error :=
    let sender := ctx.(ctx_from) in
    let sender_payload := ctx.(ctx_amount) in
    let slot := chain.(current_slot) in
    let contract_balance := ctx.(ctx_contract_balance) in
    match maybe_msg with
    | Some create_tokens =>
        without_actions (try_create_tokens sender sender_payload slot state)
    | Some refund =>
        not_payable ctx (try_refund sender slot state) default_error
    | Some finalize =>
        not_payable ctx (try_finalize sender slot contract_balance state) default_error
    | _ => Err default_error
    end.
  Close Scope Z_scope.

  (** Composes EIP20Token.receive and receive_bat by first executing
      EIP20Token.receive (if the message is an EIP20 message),
      and otherwise executes receive_bat *)
  Definition receive (chain : Chain)
                     (ctx : ContractCallContext)
                     (state : State)
                     (maybe_msg : option Msg)
                     : result (State * list ActionBody) Error :=
    match maybe_msg with
    | Some (tokenMsg msg) =>
        do _ <- throwIf (negb (isFinalized state)) default_error;
        do res <- EIP20Token.receive chain ctx state.(token_state) (Some msg) ;
        let new_state := state<|token_state := fst res|> in
            Ok (new_state, snd res)
    | _ => receive_bat chain ctx state maybe_msg
    end.

  Definition contract : Contract Setup Msg State Error :=
    build_contract init receive.

End BATFixed.

author: AU-COBRA

repo: ConCert

save_path: github-repos/coq/AU-COBRA-ConCert