From 09355fa5a22fe4ad47e35fe892e9dc36ad451571 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 23 Jan 2020 20:49:06 +0000 Subject: Add some proofs about values --- src/CoqUp/Verilog.v | 275 ++++++++++++++++++++++++++++++++++------------------ 1 file changed, 181 insertions(+), 94 deletions(-) (limited to 'src') diff --git a/src/CoqUp/Verilog.v b/src/CoqUp/Verilog.v index 52bf798..1ec95c1 100644 --- a/src/CoqUp/Verilog.v +++ b/src/CoqUp/Verilog.v @@ -1,105 +1,192 @@ From Coq Require Import Lists.List Strings.String. From Coq Require Import Structures.OrderedTypeEx - FSets.FMapList. - -From bbv Require Word. + FSets.FMapList + Program.Basics. From CoqUp Require Import Helper. -Module Verilog. - Import ListNotations. -Module Map := FMapList.Make String_as_OT. - -Definition state : Type := Map.t nat * Map.t nat. - -Inductive binop : Type := -| Plus -| Minus -| Times -| Divide -| LT -| GT -| LE -| GE -| Eq -| And -| Or -| Xor. - -Inductive expr : Type := -| Lit (n : nat) -| Var (s : string) -| Neg (a : expr) -| BinOp (op : binop) (a1 a2 : expr) -| Ternary (c t f : expr). - -Inductive stmnt : Type := -| Skip -| Block (s : list stmnt) -| Cond (c : expr) (st sf : stmnt) -| Case (c : expr) (b : list (expr * stmnt)) -| Blocking (a b : expr) -| Nonblocking (a b : expr). - -Inductive verilog : Type := Verilog (s : list stmnt). - -Coercion Lit : nat >-> expr. -Coercion Var : string >-> expr. - -Module VerilogNotation. - -Declare Scope verilog_scope. -Bind Scope verilog_scope with expr. -Bind Scope verilog_scope with stmnt. -Bind Scope verilog_scope with verilog. -Delimit Scope verilog_scope with verilog. - -Notation "x + y" := (BinOp Plus x y) (at level 50, left associativity) : verilog_scope. -Notation "x - y" := (BinOp Minus x y) (at level 50, left associativity) : verilog_scope. -Notation "x * y" := (BinOp Times x y) (at level 40, left associativity) : verilog_scope. -Notation "x / y" := (BinOp Divide x y) (at level 40, left associativity) : verilog_scope. -Notation "x < y" := (BinOp LT x y) (at level 70, no associativity) : verilog_scope. -Notation "x <= y" := (BinOp LE x y) (at level 70, no associativity) : verilog_scope. -Notation "x > y" := (BinOp GT x y) (at level 70, no associativity) : verilog_scope. -Notation "x >= y" := (BinOp GE x y) (at level 70, no associativity) : verilog_scope. -Notation "x == y" := (BinOp Eq x y) (at level 70, no associativity) : verilog_scope. -Notation "x & y" := (BinOp And x y) (at level 40, left associativity) : verilog_scope. -Notation "x | y" := (BinOp Eq x y) (at level 40, left associativity) : verilog_scope. -Notation "x ^ y" := (BinOp Eq x y) (at level 30, right associativity) : verilog_scope. -Notation "~ y" := (Neg y) (at level 75, right associativity) : verilog_scope. -Notation "c ? t : f" := (Ternary c t f) (at level 20, right associativity) : verilog_scope. - -Notation "a '<=!' b" := (Nonblocking a b) (at level 80, no associativity) : verilog_scope. -Notation "a '=!' b" := (Blocking a b) (at level 80, no associativity) : verilog_scope. -Notation "'IF' c 'THEN' a 'ELSE' b 'FI'" := (Cond c a b) (at level 80, right associativity) : verilog_scope. - -End VerilogNotation. - -Module VerilogEval. - -Definition state_find (k : string) (s : state) : nat := - opt_default 0 (Map.find k (fst s)). - -Definition eval_binop (op : binop) (a1 a2 : nat) : nat := - match op with - | Plus => a1 + a2 - | Minus => a1 - a2 - | Times => a1 * a2 - end. - -Fixpoint eval_expr (s : state) (e : expr) : nat := - match e with - | Lit n => n - | Var v => state_find v s - | Neg a => 0 - (eval_expr s a) - | BinOp op a1 a2 => eval_binop op a1 a2 - | Ternary c t f => if eval_expr s c then eval_expr s t else eval_expr s f - end. - -End VerilogEval. +Module Verilog. + + Module Map := FMapList.Make String_as_OT. + + Inductive value : Type := + | VBool (b : bool) + | VArray (l : list value). + + Definition cons_value (a b : value) : value := + match a, b with + | VBool _, VArray b' => VArray (a :: b') + | VArray a', VBool _ => VArray (List.concat [a'; [b]]) + | VArray a', VArray b' => VArray (List.concat [a'; b']) + | _, _ => VArray [a; b] + end. + + (** * Conversion to and from value *) + + Fixpoint nat_to_value (sz n : nat) : value := + match sz with + | 0 => VArray [] + | S sz' => + match Nat.modulo n 2 with + | 0 => cons_value (VBool false) (nat_to_value sz' (Nat.div n 2)) + | S _ => cons_value (VBool true) (nat_to_value sz' (Nat.div n 2)) + end + end. + + Coercion VBool : bool >-> value. + + Definition value_is_bool (v : value) : bool := + match v with + | VBool _ => true + | VArray _ => false + end. + + Definition value_is_array : value -> bool := compose negb value_is_bool. + + Definition flat_value (v : value) : bool := + match v with + | VBool _ => true + | VArray l => forallb value_is_bool l + end. + + Inductive value_is_boolP : value -> Prop := + | ValIsBool : forall b : bool, value_is_boolP (VBool b). + + Inductive value_is_arrayP : value -> Prop := + | ValIsArray : forall v : list value, value_is_arrayP (VArray v). + + Inductive flat_valueP : value -> Prop := + | FLV0 : forall b : value, value_is_boolP b -> flat_valueP b + | FLVA : forall l : list value, + Forall (value_is_boolP) l -> flat_valueP (VArray l). + + Lemma value_is_bool_equiv : + forall v, value_is_boolP v <-> value_is_bool v = true. + Proof. + split; intros. + - inversion H. trivial. + - destruct v. constructor. unfold value_is_bool in H. discriminate. + Qed. + + Lemma value_is_array_equiv : + forall v, value_is_arrayP v <-> value_is_array v = true. + Proof. + split; intros. + - inversion H. trivial. + - destruct v; try constructor. unfold value_is_array in H. + unfold compose, value_is_bool, negb in H. discriminate. + Qed. + + Lemma flat_value_equiv : + forall v, flat_valueP v <-> flat_value v = true. + Proof. + split; intros. + - unfold flat_value. inversion H. subst. + destruct v. + + trivial. + + inversion H0. + + subst. rewrite Forall_forall in H0. rewrite forallb_forall. + intros. apply value_is_bool_equiv. apply H0. assumption. + - unfold flat_value in H. destruct v. + + repeat constructor. + + constructor. apply value_is_bool_equiv. rewrite forallb_forall in H. + + Fixpoint value_to_nat (v : value) : option nat := + match v with + | VBool b => 0 + | VArray (l :: ls) => + + Definition state : Type := Map.t value * Map.t value. + + Inductive binop : Type := + | Plus + | Minus + | Times + | Divide + | LT + | GT + | LE + | GE + | Eq + | And + | Or + | Xor. + + Inductive expr : Type := + | Lit (n : value) + | Var (s : string) + | Neg (a : expr) + | BinOp (op : binop) (a1 a2 : expr) + | Ternary (c t f : expr). + + Inductive stmnt : Type := + | Skip + | Block (s : list stmnt) + | Cond (c : expr) (st sf : stmnt) + | Case (c : expr) (b : list (expr * stmnt)) + | Blocking (a b : expr) + | Nonblocking (a b : expr). + + Inductive verilog : Type := Verilog (s : list stmnt). + + Coercion VBool : bool >-> value. + Coercion Lit : value >-> expr. + Coercion Var : string >-> expr. + + Module VerilogNotation. + + Declare Scope verilog_scope. + Bind Scope verilog_scope with expr. + Bind Scope verilog_scope with stmnt. + Bind Scope verilog_scope with verilog. + Delimit Scope verilog_scope with verilog. + + Notation "x + y" := (BinOp Plus x y) (at level 50, left associativity) : verilog_scope. + Notation "x - y" := (BinOp Minus x y) (at level 50, left associativity) : verilog_scope. + Notation "x * y" := (BinOp Times x y) (at level 40, left associativity) : verilog_scope. + Notation "x / y" := (BinOp Divide x y) (at level 40, left associativity) : verilog_scope. + Notation "x < y" := (BinOp LT x y) (at level 70, no associativity) : verilog_scope. + Notation "x <= y" := (BinOp LE x y) (at level 70, no associativity) : verilog_scope. + Notation "x > y" := (BinOp GT x y) (at level 70, no associativity) : verilog_scope. + Notation "x >= y" := (BinOp GE x y) (at level 70, no associativity) : verilog_scope. + Notation "x == y" := (BinOp Eq x y) (at level 70, no associativity) : verilog_scope. + Notation "x & y" := (BinOp And x y) (at level 40, left associativity) : verilog_scope. + Notation "x | y" := (BinOp Eq x y) (at level 40, left associativity) : verilog_scope. + Notation "x ^ y" := (BinOp Eq x y) (at level 30, right associativity) : verilog_scope. + Notation "~ y" := (Neg y) (at level 75, right associativity) : verilog_scope. + Notation "c ? t : f" := (Ternary c t f) (at level 20, right associativity) : verilog_scope. + + Notation "a '<=!' b" := (Nonblocking a b) (at level 80, no associativity) : verilog_scope. + Notation "a '=!' b" := (Blocking a b) (at level 80, no associativity) : verilog_scope. + Notation "'IF' c 'THEN' a 'ELSE' b 'FI'" := (Cond c a b) (at level 80, right associativity) : verilog_scope. + + End VerilogNotation. + + Module VerilogEval. + + Definition state_find (k : string) (s : state) : value := + opt_default (VBool false) (Map.find k (fst s)). + + Definition eval_binop (op : binop) (a1 a2 : value) : value := + match op with + | Plus => a1 + a2 + | Minus => a1 - a2 + | Times => a1 * a2 + end. + + Fixpoint eval_expr (s : state) (e : expr) : nat := + match e with + | Lit n => n + | Var v => state_find v s + | Neg a => 0 - (eval_expr s a) + | BinOp op a1 a2 => eval_binop op a1 a2 + | Ternary c t f => if eval_expr s c then eval_expr s t else eval_expr s f + end. + + End VerilogEval. End Verilog. Export Verilog. -- cgit