simple test framework for Coq models

coq/Arbiter.v

+Set Warnings "-notation-overridden,-parsing".
+From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
+From sdram Require Export Trace.
+
+Section Arbiter.
+  Context {BANK_CFG : Bank_configuration}.
+
+  Definition Match (req : Request_t) (cmd : Command_t) : bool :=
+    match req.(Kind), cmd.(CKind) with
+      | RD, CRD
+      | WR, CWR => (cmd.(Request) == req)
+      | _, _    => false
+    end.
+
+  Class Arbiter_t := mkArbiter
+  {
+    Input  : Requests_t;
+
+    Arbitrate : Trace_t;
+
+    (* All Requests must handled *)
+    Req_handled : forall req,  exists cmd, req \in Requests -> cmd \in Arbitrate.(Commands) ->
+                    Match req cmd
+  }.
+End Arbiter.

coq/Bank.v

+Set Warnings "-notation-overridden,-parsing".
+From mathcomp Require Export ssreflect ssrnat ssrbool seq.
+
+
+Definition Bank_number_t := {B : nat | B <> 0}.
+Definition Timing_parameter_t := {T : nat | T <> 0}.
+
+Class Bank_configuration :=
+{
+  BANKS  : Bank_number_t;
+
+  T_RC   : Timing_parameter_t    (* ACT to ACT delay intra-bank *)
+}.
+
+Section Banks.
+  Context {BANK_CFG : Bank_configuration}.
+
+  Definition BANKS_NAT := proj1_sig BANKS.
+  Definition T_RC_NAT := proj1_sig T_RC.
+
+  Definition Bank_t := { a : nat | a < BANKS_NAT }.
+
+  Program Definition Nat_to_bank a : Bank_t :=
+    match a < BANKS_NAT with
+    | true  => (exist _ a _)
+    | false => (exist _ (BANKS_NAT - 1) _)
+    end.
+  Next Obligation.
+    unfold BANKS_NAT in *.
+    destruct BANKS. simpl in *.      
+    apply PeanoNat.Nat.lt_pred_l in n as H. move : H => /ltP H. by rewrite subn1.
+  Qed.
+
+  Definition Bank_to_nat (a : Bank_t) : nat :=
+    proj1_sig a.
+
+  Notation "'#B' b" := (Nat_to_bank b) (only parsing, at level 0).
+  Notation "'#B' b" := ((exist _ b  _) Bank_t) (only printing, at level 0).
+
+  Definition Banks_t := seq Bank_t.
+
+  Definition All_banks : Banks_t := 
+    map Nat_to_bank (iota 0 BANKS_NAT).
+End Banks.
+

coq/Commands.v

+Set Warnings "-notation-overridden,-parsing".
+From sdram Require Export Requests.
+
+Section Commands.
+  Context {BANK_CFG : Bank_configuration}.
+
+  Inductive Command_kind_t : Set :=
+    ACT |
+    PRE |
+    CRD |
+    CWR.
+
+  Local Definition Command_kind_eqdef (a b : Command_kind_t) :=
+    match a, b with
+      | ACT, ACT
+      | PRE, PRE 
+      | CRD, CRD
+      | CWR, CWR => true
+      | _, _     => false
+    end.
+
+  Lemma Command_kind_eqn : Equality.axiom Command_kind_eqdef.
+  Proof.
+    unfold Equality.axiom. intros.
+    destruct (Command_kind_eqdef x y) eqn:H; unfold Command_kind_eqdef in *.
+      apply ReflectT. destruct x, y; inversion H; auto.
+      apply ReflectF; destruct x, y; inversion H; unfold not; intros; inversion H0.
+  Qed.
+
+  Canonical Command_kind_eqMixin := EqMixin Command_kind_eqn.
+  Canonical Command_kind_eqType := Eval hnf in EqType Command_kind_t Command_kind_eqMixin.
+
+  Record Command_t : Set := mkCmd
+  {
+    CDate    : nat;
+    CKind    : Command_kind_t;
+    Request  : Request_t
+  }.
+
+  Local Definition Command_eqdef (a b : Command_t) :=
+    (a.(CDate) == b.(CDate)) &&
+    (a.(Request) == b.(Request)) &&
+    (a.(CKind) == b.(CKind)).
+
+  Lemma Command_eqn : Equality.axiom Command_eqdef.
+  Proof.
+    unfold Equality.axiom. intros. destruct Command_eqdef eqn:H; unfold Command_eqdef in *.
+    {
+      apply ReflectT.
+      move: H => /andP [/andP [/eqP CD /eqP R /eqP C]].
+      destruct x,y. simpl in *. subst. auto.
+    }
+    apply ReflectF. unfold not in *. intro BUG.
+    apply negbT in H; rewrite negb_and in H.
+    destruct x, y.
+      rewrite negb_and in H.
+      move: H => /orP [H | /eqP CK].
+      move: H => /orP [H | /eqP R].
+      move: H => /eqP CD.
+      by apply CD; inversion BUG.
+      by apply R; inversion BUG.
+      by apply CK; inversion BUG.
+  Qed.
+
+  Canonical Command_eqMixin := EqMixin Command_eqn.
+  Canonical Command_eqType := Eval hnf in EqType Command_t Command_eqMixin.
+
+  Definition Kind_of_req req :=
+    match req.(Kind) with
+      | RD => CRD
+      | WR => CWR
+    end.
+
+  Definition PRE_of_req req t :=
+    mkCmd t PRE req.
+
+  Definition ACT_of_req req t :=
+    mkCmd t ACT req.
+
+  Definition Cmd_of_req req t :=
+    mkCmd t (Kind_of_req req) req.
+
+  Definition Commands_t := seq Command_t.
+End Commands.

coq/FIFO.v

+Set Warnings "-notation-overridden,-parsing".
+From sdram Require Import  Arbiter.
+
+Section FIFO.
+  Context {BANK_CFG : Bank_configuration}.
+  Context {Input    : Requests_t}.
+
+  Local Record FIFO_state_t := mkFIFO
+  {
+    Cmds   : Commands_t;
+    Time   : nat;
+  }.
+
+  Definition FIFO_wait := T_RC.
+
+  Local Program Definition FIFO_req req State : FIFO_state_t :=
+    let PRE_date := State.(Time) + 1 in
+    let ACT_date := State.(Time) + 2 in
+    let CMD_date := State.(Time) + 3 in
+      let PRE := PRE_of_req req PRE_date in
+      let ACT := ACT_of_req req ACT_date in
+      let CMD := Cmd_of_req req CMD_date in
+        let Cmds := PRE::ACT::CMD::State.(Cmds) in
+          mkFIFO Cmds (State.(Time) + FIFO_wait).
+
+  Local Fixpoint FIFO_trace Reqs State : FIFO_state_t :=
+    match Reqs with
+      | [::]       => State
+      | req::Reqs' => FIFO_req req (FIFO_trace Reqs' State)
+    end.
+
+  Lemma FIFO_trace_time_monotone Reqs State:
+    State.(Time) <= (FIFO_trace Reqs State).(Time).
+   Proof.
+    induction Reqs.
+      auto.
+      {
+        simpl. destruct FIFO_wait. simpl. 
+        specialize (leq_addr x (Time (FIFO_trace Reqs State))) as H.
+        specialize leq_trans with (n := Time (FIFO_trace Reqs State)) (m := Time State) (p := Time (FIFO_trace Reqs State) + x) as H1. 
+        apply H1 in IHReqs; auto.
+      }
+  Qed.
+
+  Program Definition FIFO_arbitrate :=
+    let State := FIFO_trace Requests (mkFIFO [::] 0) in
+      mkTrace State.(Cmds) State.(Time) _ _ _.
+  Admit Obligations.
+
+  Program Instance FIFO_arbiter : Arbiter_t := 
+    mkArbiter Input FIFO_arbitrate _.
+  Admit Obligations.
+End FIFO.
+
+Section Test.
+  Program Instance BANK_CFG : Bank_configuration :=
+  {
+    BANKS := 1;
+    T_RC  := 2;
+  }.
+
+  Program Definition Req1 := mkReq 3 RD 0.
+  Program Definition Req2 := mkReq 4 RD 0.
+
+  Program Instance Input : Requests_t := mkReqs [:: Req1; Req2] _ _ _.
+  Admit Obligations.
+
+  Program Instance My_arbiter : Arbiter_t := 
+    mkArbiter Input FIFO_arbitrate _.
+  Admit Obligations.
+
+  Compute Arbitrate.(Commands).
+End Test.

coq/Requests.v

+Set Warnings "-notation-overridden,-parsing".
+From mathcomp Require Export ssreflect eqtype.
+From sdram Require Export Bank Util.
+
+Section Requests.
+  Context {BANK_CFG : Bank_configuration}.
+
+  Inductive Request_kind_t : Set :=
+    RD |
+    WR.
+
+  Local Definition Request_kind_eqdef (a b : Request_kind_t) :=
+    match a, b with
+      | RD, RD
+      | WR, WR => true
+      | _, _   => false
+    end.
+
+  Lemma Request_kind_eqn : Equality.axiom Request_kind_eqdef.
+  Proof.
+    unfold Equality.axiom. intros.
+    destruct (Request_kind_eqdef x y) eqn:H; unfold Request_kind_eqdef in *.
+      apply ReflectT. destruct x, y; inversion H; auto.
+      apply ReflectF; destruct x, y; inversion H; unfold not; intros; inversion H0.
+  Qed.
+
+  Canonical Request_kind_eqMixin := EqMixin Request_kind_eqn.
+  Canonical Request_kind_eqType:= Eval hnf in EqType Request_kind_t Request_kind_eqMixin.
+
+  Record Request_t : Set := mkReq
+  {
+    Date : nat;
+    Kind : Request_kind_t;
+    Bank : Bank_t;
+  }.
+
+  Notation "'*R' b '@' id '->' cd" := (mkReq id (Some cd) true (exist _ b _)) (only printing, at level 0).
+  Notation "'*W' b '@' id '->' cd" := (mkReq id (Some cd) false (exist _ b _)) (only printing, at level 0).
+  Notation "'*R' b '@' id" := (mkReq id None true (exist _ b _)) (only printing, at level 0).
+  Notation "'*W' b '@' id" := (mkReq id None false (exist _ b _)) (only printing, at level 0).
+
+  Local Definition Request_eqdef (a b : Request_t) :=
+    (a.(Date) == b.(Date)) &&
+    (a.(Kind) == b.(Kind)) &&
+    (a.(Bank) == b.(Bank)).
+
+  Lemma Request_eqn : Equality.axiom Request_eqdef.
+  Proof.
+    unfold Equality.axiom. intros. destruct Request_eqdef eqn:H.
+    {
+      apply ReflectT. unfold Request_eqdef in *.
+      move: H => /andP [/andP [/eqP ID /eqP RD /eqP B]].
+      destruct x,y; simpl in *. subst. auto.
+    }
+    apply ReflectF. unfold Request_eqdef, not in *.
+    intro BUG.
+    apply negbT in H; rewrite negb_and in H.
+    destruct x, y.
+      rewrite negb_and in H.
+      move: H => /orP [H | /eqP B].
+      move: H => /orP [H | /eqP RD].
+      move: H => /eqP ID.
+      by apply ID; inversion BUG.
+      by apply RD; inversion BUG.
+      by apply B; inversion BUG.
+  Qed.
+
+  Canonical Request_eqMixin := EqMixin Request_eqn.
+  Canonical Request_eqType := Eval hnf in EqType Request_t Request_eqMixin.
+
+  Local Fixpoint sorted_ (Reqs : seq Request_t) a :=
+    match Reqs with
+      | [::]     => true
+      | b::Reqs' => (a.(Date) <= b.(Date)) &&
+                    sorted_ Reqs' b
+    end.
+
+  Local Definition sorted (Reqs : seq Request_t) :=
+    match Reqs with
+      | [::]     => true
+      | a::Reqs' => sorted_ Reqs' a
+    end.
+
+  Class Requests_t := mkReqs
+  {
+    Requests : seq Request_t; 
+
+    (* All Requests must be uniq *)
+    Reqs_uniq    : uniq Requests;
+
+    (* Requests are sorted by date. *)
+    Reqs_sorted  : sorted Requests;
+
+    (* A requestor may only issue a single request to a bank at a time *)
+    Reqs_issue   : forall a b, a \in Requests -> b \in Requests -> a != b ->
+                    a.(Date) == b.(Date) -> a.(Bank) != b.(Bank);
+  }.
+End Requests.

coq/Trace.v

+Set Warnings "-notation-overridden,-parsing".
+From mathcomp Require Import ssreflect ssrnat ssrbool seq eqtype.
+From sdram Require Export Commands Bank.
+
+Section Trace.
+  Context {BANK_CFG : Bank_configuration}.
+
+  Definition isACT (cmd : Command_t) :=
+    cmd.(CKind) == ACT.
+
+  Definition Same_Bank (a b : Command_t) :=
+    a.(Request).(Bank) == b.(Request).(Bank).
+
+  Definition ACT_to_ACT (a b : Command_t) :=
+    isACT a && isACT b.
+
+  Definition Before (a b : Command_t) :=
+    a.(CDate) < b.(CDate).
+
+  Definition Apart (a b : Command_t) t :=
+    a.(CDate) + t < b.(CDate).
+
+  Record Trace_t := mkTrace
+  {
+    Commands : Commands_t;
+    Time     : nat;
+
+    (* All commands must be uniq *)
+    Cmds_uniq    : uniq Commands;
+
+    (* All commands have to occur before the current time instant *)
+    Cmds_time_ok : forall cmd, cmd \in Commands -> cmd.(CDate) <= Time;
+
+    (* Ensure that the time between two ACT commands respects T_RC *)
+    Cmds_T_RC_ok : forall a b, a \in Commands -> b \in Commands ->
+                    ACT_to_ACT a b -> Same_Bank a b -> Before a b ->
+                    Apart a b T_RC_NAT;
+  }.
+
+  Program Definition Trace_empty := mkTrace [::] 0 _ _ _.
+End Trace.

coq/Util.v

+Set Warnings "-notation-overridden,-parsing".
+From mathcomp Require Import ssreflect ssrnat ssrbool seq eqtype.
+
+Lemma all_filter [T : eqType] a (p : pred T) S: 
+  all a S -> all a [seq x <- S | p x].
+Proof.
+  intros.
+  induction S.
+    auto.
+    simpl in *.
+    destruct (p a0).
+      simpl. apply /andP.
+      split. 
+        move : H => /andP /proj1 H. auto.
+        move : H => /andP /proj2 H. apply IHS in H. auto.
+      move : H => /andP /proj2 H. apply IHS in H. auto.
+Qed.
+
+(* TODO replace by generic definition *)
+Definition pred2_t (T : eqType) := T -> T -> bool.
+
+Definition all_pred2 [T : eqType] (p : pred2_t T) S x :=
+  all (p x) S.
+
+Lemma all_pred2_filter [T : eqType] (p2 : pred2_t T) (p : pred T) S (x : T): 
+  all_pred2 p2 S x -> all_pred2 p2 [seq y <- S | p y] x.
+Proof.
+  unfold pred2_t.
+  intros.
+  by apply all_filter.
+Qed.
+
+Fixpoint all_pred2_recursive [T : eqType] (p2 : pred2_t T) S :=
+  match S with
+    | [::]  => true
+    | x::S' => all_pred2 p2 S' x && 
+               all_pred2_recursive p2 S'
+  end.
+
+Lemma all_pred2_recursive_filter [T : eqType] (p2 : pred2_t T) (p : pred T) S: 
+  all_pred2_recursive p2 S -> all_pred2_recursive p2 [seq x <- S | p x].
+Proof.
+  induction S; intros; auto.
+    simpl in *. move : H => /andP H.
+     destruct (p a); simpl.
+      apply /andP. split.
+        apply proj1 in H. by apply all_filter.
+        apply proj2 in H. by apply IHS in H.
+      apply proj2 in H. by apply IHS in H.
+Qed.
+
+(* Lemma filter_forall_pred [T : eqType] S (p : pred T): forall z , z \in [seq y <- S | p y ] -> p z.
+  intros.
+  rewrite (mem_filter p z S) in H. by move : H => /andP /proj1.
+Qed.
+ *)

coq/makefile.conf

+# This configuration file was generated by running:
+# coq_makefile -o makefile Util.v Bank.v Requests.v Commands.v Trace.v Arbiter.v FIFO.v
+
+
+###############################################################################
+#                                                                             #
+# Project files.                                                              #
+#                                                                             #
+###############################################################################
+
+COQMF_VFILES = Util.v Bank.v Requests.v Commands.v Trace.v Arbiter.v FIFO.v
+COQMF_MLIFILES = 
+COQMF_MLFILES = 
+COQMF_MLGFILES = 
+COQMF_MLPACKFILES = 
+COQMF_MLLIBFILES = 
+COQMF_CMDLINE_VFILES = Util.v Bank.v Requests.v Commands.v Trace.v Arbiter.v FIFO.v
+
+###############################################################################
+#                                                                             #
+# Path directives (-I, -R, -Q).                                               #
+#                                                                             #
+###############################################################################
+
+COQMF_OCAMLLIBS = -I .
+COQMF_SRC_SUBDIRS = .
+COQMF_COQLIBS = -I .  -R . sdram
+COQMF_COQLIBS_NOML =  -R . sdram
+COQMF_CMDLINE_COQLIBS = -I .  -R . sdram
+
+###############################################################################
+#                                                                             #
+# Coq configuration.                                                          #
+#                                                                             #
+###############################################################################
+
+COQMF_LOCAL=0
+COQMF_COQLIB=/home/brandner/.opam/default/lib/coq/
+COQMF_DOCDIR=/home/brandner/.opam/default/doc/
+COQMF_OCAMLFIND=/home/brandner/.opam/default/bin/ocamlfind
+COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67   -safe-string -strict-sequence
+COQMF_WARN=-warn-error +a-3
+COQMF_HASNATDYNLINK=true
+COQMF_COQ_SRC_SUBDIRS=config lib clib kernel library engine pretyping interp gramlib gramlib/.pack parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/ssrsearch plugins/syntax
+COQMF_COQ_NATIVE_COMPILER_DEFAULT=no
+COQMF_WINDRIVE=
+
+###############################################################################
+#                                                                             #
+# Extra variables.                                                            #
+#                                                                             #
+###############################################################################
+
+COQMF_OTHERFLAGS = 
+COQMF_INSTALLCOQDOCROOT = Top