Verifying factorial for a simple assembly language

asm.v

Require Import Arith.PeanoNat.
Require Import List.
Import Nat.
Import ListNotations.

(** * Reflexive transitive closure of a relation *)
Definition relation (X : Type) := X -> X -> Prop.
Inductive multi {X : Type} (R : relation X) : relation X :=
  | multi_refl : forall (x : X), multi R x x
  | multi_step : forall (x y z : X),
                    R x y ->
                    multi R y z ->
                    multi R x z.

Hint Constructors multi : core.
Hint Resolve multi_refl : core.

Theorem multi_R : forall (X : Type) (R : relation X) (x y : X),
    R x y -> (multi R) x y.
Proof.
  econstructor; eauto.
Qed.

Theorem multi_trans :
  forall (X : Type) (R : relation X) (x y z : X),
      multi R x y  ->
      multi R y z ->
      multi R x z.
Proof.
  intros X R x y z G H.
  induction G; auto; econstructor; eauto.
Qed.

(* Opcode       Instruction     Meaning *)
(* 03           ld M            load accumulator with contents of memory location M *)
(* 04           st M            store contents of accumulator in location M *)
(* 05           add M           add contents of location M to accumulator *)
(* 06           sub M           subtract contents of location M from accumulator *)
(* 08           jz M            jump to location M if accumulator is zero *)
(* 09           j M             jump to location M *)
(* 10           halt            stop execution *)
(* 11           mul M           multiply contents of location M with accumulator *)
(* 14           inc             increment accumulator *)
(* 15           dec             decrement accumulator *)

(* Memory where default value is 0. *)
Module Type Memory.
  Parameter t : Set.
  Parameter get : t -> nat -> nat.
  (* set m i x == m[i] = x *)
  Parameter set : t -> nat -> nat -> t.
  Parameter empty : t.
  Axiom get_empty : forall i, get empty i = 0.
  Axiom get_set : forall m i x, get (set m i x) i = x.
  Axiom set_set : forall m i x y, set (set m i x) i y = set m i y.
  Axiom get_set' :
    forall m i i' x, i <> i' -> get (set m i x) i' = get m i'.
  Axiom set_set' :
    forall m i i' x y, i <> i' -> set (set m i x) i' y = set (set m i' y) i x.
End Memory.

Require Import FunctionalExtensionality.
Require Import Bool.
Import Nat.
Module PureMemory <: Memory.
  Definition t : Set := nat -> nat.
  Definition empty := (fun (_ : nat) => 0).
  Definition get (m : t) i := m i.
  Definition set (m : t) i x := (fun i' => if i' =? i then x else m i').
  Theorem get_empty : forall i, get empty i = 0.
  Proof. reflexivity. Qed.
  Theorem get_set : forall m i x, get (set m i x) i = x.
  Proof. intros; unfold get, set. rewrite eqb_refl. reflexivity. Qed.

  Theorem set_set : forall m i x y, set (set m i x) i y = set m i y.
  Proof.
    intros; unfold get, set.
    apply functional_extensionality; intros i'.
    destruct (eqb_spec i' i); reflexivity.
  Qed.

  Theorem get_set' :
    forall m i i' x, i <> i' -> get (set m i x) i' = get m i'.
  Proof.
    intros; unfold get, set.
    destruct (eqb_spec i' i); congruence.
  Qed.
  Theorem set_set' :
    forall m i i' x y, i <> i' -> set (set m i x) i' y = set (set m i' y) i x.
  Proof.
    intros; unfold get, set.
    apply functional_extensionality; intros i''.
    destruct (eqb_spec i'' i'), (eqb_spec i'' i); congruence.
  Qed.
End PureMemory.

Module CPU.
  Import PureMemory.
  (* PC, accumulator, store *)
  Definition store := t.
  Definition state := (nat * nat * store)%type.
  Definition loc := nat.

  Inductive instr : Type :=
  | LD (n : loc) | ST (n : loc) | ADD (n : loc) | MUL (n : loc) | DEC | INC
  | SUB (n : loc) | JZ (n : loc) | J (n : loc) | HALT.

  Definition code := list instr.

  Fixpoint instr_at (C: code) (pc: loc) : option instr :=
  match C with
  | nil => None
  | i :: C' => if pc =? 0 then Some i else instr_at C' (pc - 1)
  end.

  Inductive step : instr -> state -> state -> Prop :=
  | s_j : forall pc acc a n,
      step (J n) (pc, acc, a)
                 (n, acc, a)
  | s_ld : forall pc acc a n,
      step (LD n) (pc, acc, a)
                  (pc + 1, get a n, a)
  | s_st : forall pc acc a n,
      step (ST n) (pc, acc, a)
                  (pc + 1, acc, set a n acc)
  | s_add : forall pc acc a n,
      step (ADD n) (pc, acc, a)
              (pc + 1, acc + get a n, a)
  | s_sub : forall pc acc a n,
      step (SUB n) (pc, acc, a)
                   (pc + 1, acc - get a n, a)
  | s_mul : forall pc acc a n,
      step (MUL n) (pc, acc, a)
                   (pc + 1, acc * get a n, a)
  | s_jz : forall pc acc a n,
      step (JZ n) (pc, acc, a)
                  (if acc =? 0 then n else pc + 1, acc, a)
  | s_dec : forall pc acc a,
      step DEC (pc, acc, a)
               (pc + 1, pred acc, a)
  | s_inc : forall pc acc a,
      step INC (pc, acc, a)
               (pc + 1, S acc, a)
  .

  Inductive cstep (C : code) : state -> state -> Prop :=
  | cstep_single : forall pc (src dst : state) opcode,
      pc = fst (fst src)
      -> instr_at C pc = Some opcode
      -> step opcode src dst
      -> cstep C src dst.
  Hint Constructors cstep : core.

  Definition csteps (C : code) : state -> state -> Prop := multi (cstep C).
  (* Hint Unfold csteps : core. *)

  Definition init_state : state := (0, 0, empty).
  Definition init_with_acc (n : nat) : state := (0, n, empty).

  Definition double_prog : code :=
    [ST 0; ADD 0; HALT].

  Lemma double_n : forall n, csteps double_prog (init_with_acc n) (2, n + n, set empty 0 n).
  Proof.
    intros n.
    repeat econstructor.
  Qed.

  Definition C := 0.
  Definition ACC := 1.
  Definition fact_prog : code :=
    [JZ 7; ST C; MUL ACC; ST ACC; LD C; DEC; J 0; LD ACC; HALT].

  Ltac step :=
    match goal with
    | |- csteps _ _ _ => econstructor; [(econstructor; econstructor) | idtac]
    | |- multi (cstep _) _ _ => econstructor; [(econstructor; econstructor) | idtac]
    end; cbn.

  Lemma fact_3 : { m : store | csteps fact_prog (0, 3, set empty ACC 1) (8, 6, m) }.
  Proof.
    eexists.
    repeat econstructor.
  Defined.

  Eval compute in (proj1_sig fact_3 ACC). (* => 6 *)
  Eval compute in (proj1_sig fact_3 C). (* => 1 *)

  Fixpoint fact (n : nat) :=
    match n with
    | 0 => 1
    | S n' => n * fact n'
    end.

  Hint Rewrite set_set get_set : memory.

  (* Let's prove factorial correct.  After playing with the statement
     for a bit one realizes that it follows from a more general
     statement: *)
  Lemma fact_n_aux (n : nat) :
    forall x y, { m : store | csteps fact_prog (0, n, set (set empty ACC y) C x) (8, fact n * y, m) }.
  Proof.
    unfold init_with_acc, fact_prog.
    induction n; intros x y.
    - eexists.
      do 2 step.
      rewrite add_0_r.
      auto.
    - destruct (IHn (S n) (S n * y)) as [m Hm].
      exists m.
      do 7 step.
      autorewrite with memory.
      rewrite set_set' by discriminate.
      autorewrite with memory.
      replace (y + n * y) with (S n * y) by auto.
      replace (fact n + n * fact n) with ((S n) * fact n) by auto.
      rewrite (mul_comm (S n) (fact n)).
      rewrite mul_assoc in Hm.
      apply Hm.
  Qed.

  (* Now we just instantiate ACC and C with the appropriate values. *)
  Lemma fact_n (n : nat) :
    { m : store | csteps fact_prog (0, n, set empty ACC 1) (8, fact n, m) }.
  Proof.
    replace empty with (set empty C 0).
    rewrite set_set' by discriminate.
    rewrite <- (mul_1_r (fact n)).
    apply fact_n_aux.
    unfold set.
    apply functional_extensionality; intros x.
    rewrite get_empty. destruct (_ =? _); reflexivity.
  Qed.

  (* Program logic*)
End CPU.