(* * Vericert: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by * the Free Software Foundation, either version 3 of the License, or * (at your option) any later version. * * This program is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with this program. If not, see <https://www.gnu.org/licenses/>. *) From Coq Require Import Structures.OrderedTypeEx FSets.FMapPositive Program.Basics PeanoNat ZArith Lists.List Program. Require Import Lia. Import ListNotations. From vericert Require Import Vericertlib Show ValueInt AssocMap Array. From compcert Require Events. From compcert Require Import Integers Errors Smallstep Globalenvs. Local Open Scope assocmap. Set Implicit Arguments. Definition reg : Type := positive. Definition node : Type := positive. Definition szreg : Type := reg * nat. Record associations (A : Type) : Type := mkassociations { assoc_blocking : AssocMap.t A; assoc_nonblocking : AssocMap.t A }. Definition arr := (Array (option value)). Definition reg_associations := associations value. Definition arr_associations := associations arr. Definition assocmap_reg := AssocMap.t value. Definition assocmap_arr := AssocMap.t arr. Definition merge_regs (new : assocmap_reg) (old : assocmap_reg) : assocmap_reg := AssocMapExt.merge value new old. Definition merge_cell (new : option value) (old : option value) : option value := match new, old with | Some _, _ => new | _, _ => old end. Definition merge_arr (new : option arr) (old : option arr) : option arr := match new, old with | Some new', Some old' => Some (combine merge_cell new' old') | Some new', None => Some new' | None, Some old' => Some old' | None, None => None end. Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr := AssocMap.combine merge_arr new old. Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value := match a ! r with | None => None | Some arr => Some (Option.default (NToValue 0) (Option.join (array_get_error i arr))) end. Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr := match a ! r with | None => a | Some arr => a # r <- (array_set i (Some v) arr) end. Definition block_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations := mkassociations (arr_assocmap_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking). Definition nonblock_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations := mkassociations asa.(assoc_blocking) (arr_assocmap_set r i v asa.(assoc_nonblocking)). Definition block_reg (r : reg) (asr : reg_associations) (v : value) := mkassociations (AssocMap.set r v asr.(assoc_blocking)) asr.(assoc_nonblocking). Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) := mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)). Inductive scl_decl : Type := VScalar (sz : nat). Inductive arr_decl : Type := VArray (sz : nat) (ln : nat). (** * Verilog AST The Verilog AST is defined here, which is the target language of the compilation. ** Value The Verilog [value] is a bitvector containg a size and the actual bitvector. In this case, the [Word.word] type is used as many theorems about that bitvector have already been proven. *) (** ** Binary Operators These are the binary operations that can be represented in Verilog. Ideally, multiplication and division would be done by custom modules which could al so be scheduled properly. However, for now every Verilog operator is assumed to take one clock cycle. *) Inductive binop : Type := | Vadd : binop (** addition (binary [+]) *) | Vsub : binop (** subtraction (binary [-]) *) | Vmul : binop (** multiplication (binary [*]) *) | Vdiv : binop (** division (binary [/]) *) | Vdivu : binop (** division unsigned (binary [/]) *) | Vmod : binop (** remainder ([%]) *) | Vmodu : binop (** remainder unsigned ([%]) *) | Vlt : binop (** less than ([<]) *) | Vltu : binop (** less than unsigned ([<]) *) | Vgt : binop (** greater than ([>]) *) | Vgtu : binop (** greater than unsigned ([>]) *) | Vle : binop (** less than or equal ([<=]) *) | Vleu : binop (** less than or equal unsigned ([<=]) *) | Vge : binop (** greater than or equal ([>=]) *) | Vgeu : binop (** greater than or equal unsigned ([>=]) *) | Veq : binop (** equal to ([==]) *) | Vne : binop (** not equal to ([!=]) *) | Vand : binop (** and (binary [&]) *) | Vor : binop (** or (binary [|]) *) | Vxor : binop (** xor (binary [^|]) *) | Vshl : binop (** shift left ([<<]) *) | Vshr : binop (** shift right ([>>>]) *) | Vshru : binop. (** shift right unsigned ([>>]) *)
Vror : binop (** shift right unsigned ([>>]) *)
(** ** Unary Operators *) Inductive unop : Type := | Vneg (** negation ([-]) *) | Vnot. (** not operation [!] *) (** ** Expressions *) Inductive expr : Type := | Vlit : value -> expr | Vvar : reg -> expr | Vvari : reg -> expr -> expr | Vinputvar : reg -> expr | Vbinop : binop -> expr -> expr -> expr | Vunop : unop -> expr -> expr | Vternary : expr -> expr -> expr -> expr. Definition posToExpr (p : positive) : expr := Vlit (posToValue p). (** ** Statements *) Inductive stmnt : Type := | Vskip : stmnt | Vseq : stmnt -> stmnt -> stmnt | Vcond : expr -> stmnt -> stmnt -> stmnt | Vcase : expr -> list (expr * stmnt) -> option stmnt -> stmnt | Vblock : expr -> expr -> stmnt | Vnonblock : expr -> expr -> stmnt. (** ** Edges These define when an always block should be triggered, for example if the always block should be triggered synchronously at the clock edge, or asynchronously for combinational logic. [edge] is not part of [stmnt] in this formalisation because is closer to the semantics that are used. *) Inductive edge : Type := | Vposedge : reg -> edge | Vnegedge : reg -> edge | Valledge : edge | Voredge : edge -> edge -> edge. (** ** Module Items Module items can either be declarations ([Vdecl]) or always blocks ([Valways]). The declarations are always register declarations as combinational logic can be done using combinational always block instead of continuous assignments. *) Inductive io : Type := | Vinput : io | Voutput : io | Vinout : io. Inductive declaration : Type := | Vdecl : option io -> reg -> nat -> declaration | Vdeclarr : option io -> reg -> nat -> nat -> declaration. Inductive module_item : Type := | Vdeclaration : declaration -> module_item | Valways : edge -> stmnt -> module_item | Valways_ff : edge -> stmnt -> module_item | Valways_comb : edge -> stmnt -> module_item. (** The main module type containing all the important control signals - [mod_start] If set, starts the computations in the module. - [mod_reset] If set, reset the state in the module. - [mod_clk] The clock that controls the computation in the module. - [mod_args] The arguments to the module. - [mod_finish] Bit that is set if the result is ready. - [mod_return] The return value that was computed. - [mod_body] The body of the module, including the state machine. *) Record module : Type := mkmodule { mod_start : reg; mod_reset : reg; mod_clk : reg; mod_finish : reg; mod_return : reg; mod_st : reg; (**r Variable that defines the current state, it should be internal. *) mod_stk : reg; mod_stk_len : nat; mod_args : list reg; mod_body : list module_item; mod_entrypoint : node; }. Definition fundef := AST.fundef module. Definition program := AST.program fundef unit. (** Convert a [positive] to an expression directly, setting it to the right size. *) Definition posToLit (p : positive) : expr := Vlit (posToValue p). Definition fext := unit. Definition fextclk := nat -> fext. (** ** State The [state] contains the following items: n - Current [module] that is being worked on, so that the state variable can be retrieved and set appropriately. - Current [module_item] which is being worked on. - A contiunation ([cont]) which defines what to do next. The option is to either evaluate another module item or go to the next clock cycle. Finally it could also end if the finish flag of the module goes high. - Association list containing the blocking assignments made, or assignments made in previous clock cycles. - Nonblocking association list containing all the nonblocking assignments made in the current module. - The environment containing values for the input. - The program counter which determines the value for the state in this version of Verilog, as the Verilog was generated by the RTL, which means that we have to make an assumption about how it looks. In this case, that it contains state which determines which part of the Verilog is executed. This is then the part of the Verilog that should match with the RTL. *) Inductive stackframe : Type := Stackframe : forall (res : reg) (m : module) (pc : node) (reg_assoc : assocmap_reg) (arr_assoc : assocmap_arr), stackframe. Inductive state : Type := | State : forall (stack : list stackframe) (m : module) (st : node) (reg_assoc : assocmap_reg) (arr_assoc : assocmap_arr), state | Returnstate : forall (res : list stackframe) (v : value), state | Callstate : forall (stack : list stackframe) (m : module) (args : list value), state. Definition binop_run (op : binop) (v1 v2 : value) : option value := match op with | Vadd => Some (Int.add v1 v2) | Vsub => Some (Int.sub v1 v2) | Vmul => Some (Int.mul v1 v2) | Vdiv => if Int.eq v2 Int.zero || Int.eq v1 (Int.repr Int.min_signed) && Int.eq v2 Int.mone then None else Some (Int.divs v1 v2) | Vdivu => if Int.eq v2 Int.zero then None else Some (Int.divu v1 v2) | Vmod => if Int.eq v2 Int.zero || Int.eq v1 (Int.repr Int.min_signed) && Int.eq v2 Int.mone then None else Some (Int.mods v1 v2) | Vmodu => if Int.eq v2 Int.zero then None else Some (Int.modu v1 v2) | Vlt => Some (boolToValue (Int.lt v1 v2)) | Vltu => Some (boolToValue (Int.ltu v1 v2)) | Vgt => Some (boolToValue (Int.lt v2 v1)) | Vgtu => Some (boolToValue (Int.ltu v2 v1)) | Vle => Some (boolToValue (negb (Int.lt v2 v1))) | Vleu => Some (boolToValue (negb (Int.ltu v2 v1))) | Vge => Some (boolToValue (negb (Int.lt v1 v2))) | Vgeu => Some (boolToValue (negb (Int.ltu v1 v2))) | Veq => Some (boolToValue (Int.eq v1 v2)) | Vne => Some (boolToValue (negb (Int.eq v1 v2))) | Vand => Some (Int.and v1 v2) | Vor => Some (Int.or v1 v2) | Vxor => Some (Int.xor v1 v2) | Vshl => Some (Int.shl v1 v2) | Vshr => Some (Int.shr v1 v2) | Vshru => Some (Int.shru v1 v2) end. Definition unop_run (op : unop) (v1 : value) : value := match op with | Vneg => Int.neg v1 | Vnot => Int.not v1 end. Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop := | erun_Vlit : forall fext reg stack v, expr_runp fext reg stack (Vlit v) v | erun_Vvar : forall fext reg stack v r, reg#r = v -> expr_runp fext reg stack (Vvar r) v | erun_Vvari : forall fext reg stack v iexp i r, expr_runp fext reg stack iexp i -> arr_assocmap_lookup stack r (valueToNat i) = Some v -> expr_runp fext reg stack (Vvari r iexp) v | erun_Vbinop : forall fext reg stack op l r lv rv resv, expr_runp fext reg stack l lv -> expr_runp fext reg stack r rv -> Some resv = binop_run op lv rv -> expr_runp fext reg stack (Vbinop op l r) resv | erun_Vunop : forall fext reg stack u vu op oper resv, expr_runp fext reg stack u vu -> oper = unop_run op -> resv = oper vu -> expr_runp fext reg stack (Vunop op u) resv | erun_Vternary_true : forall fext reg stack c ts fs vc vt, expr_runp fext reg stack c vc -> expr_runp fext reg stack ts vt -> valueToBool vc = true -> expr_runp fext reg stack (Vternary c ts fs) vt | erun_Vternary_false : forall fext reg stack c ts fs vc vf, expr_runp fext reg stack c vc -> expr_runp fext reg stack fs vf -> valueToBool vc = false -> expr_runp fext reg stack (Vternary c ts fs) vf. Hint Constructors expr_runp : verilog. Definition handle_opt {A : Type} (err : errmsg) (val : option A) : res A := match val with | Some a => OK a | None => Error err end. Definition handle_def {A : Type} (a : A) (val : option A) : res A := match val with | Some a' => OK a' | None => OK a end. Local Open Scope error_monad_scope. (*Definition access_fext (f : fext) (r : reg) : res value := match AssocMap.get r f with | Some v => OK v | _ => OK (ZToValue 0) end.*) (* TODO FIX Vvar case without default *) (*Fixpoint expr_run (assoc : assocmap) (e : expr) {struct e} : res value := match e with | Vlit v => OK v | Vvar r => match s with | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r | _ => Error (msg "Verilog: Wrong state") end | Vvari _ _ => Error (msg "Verilog: variable indexing not modelled") | Vinputvar r => access_fext s r | Vbinop op l r => let lv := expr_run s l in let rv := expr_run s r in let oper := binop_run op in do lv' <- lv; do rv' <- rv; handle_opt (msg "Verilog: sizes are not equal") (eq_to_opt lv' rv' (oper lv' rv')) | Vunop op e => let oper := unop_run op in do ev <- expr_run s e; OK (oper ev) | Vternary c te fe => do cv <- expr_run s c; if valueToBool cv then expr_run s te else expr_run s fe end.*) (** Return the location of the lhs of an assignment. *) Inductive location : Type := | LocReg (_ : reg) | LocArray (_ : reg) (_ : nat). Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop := | Base : forall f asr asa r, location_is f asr asa (Vvar r) (LocReg r) | Indexed : forall f asr asa r iexp iv, expr_runp f asr asa iexp iv -> location_is f asr asa (Vvari r iexp) (LocArray r (valueToNat iv)). (* Definition assign_name (f : fext) (asr: assocmap) (asa : assocmap_l) (e : expr) : res reg := *) (* match e with *) (* | Vvar r => OK r *) (* | _ => Error (msg "Verilog: expression not supported on lhs of assignment") *) (* end. *) (*Fixpoint stmnt_height (st : stmnt) {struct st} : nat := match st with | Vseq s1 s2 => S (stmnt_height s1 + stmnt_height s2) | Vcond _ s1 s2 => S (Nat.max (stmnt_height s1) (stmnt_height s2)) | Vcase _ ls (Some st) => S (fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls) | _ => 1 end. Fixpoint find_case_stmnt (s : state) (v : value) (cl : list (expr * stmnt)) {struct cl} : option (res stmnt) := match cl with | (e, st)::xs => match expr_run s e with | OK v' => match eq_to_opt v v' (veq v v') with | Some eq => if valueToBool eq then Some (OK st) else find_case_stmnt s v xs | None => Some (Error (msg "Verilog: equality check sizes not equal")) end | Error msg => Some (Error msg) end | _ => None end. Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state := match n with | S n' => match st with | Vskip => OK s | Vseq s1 s2 => do s' <- stmnt_run' n' s s1; stmnt_run' n' s' s2 | Vcond c st sf => do cv <- expr_run s c; if valueToBool cv then stmnt_run' n' s st else stmnt_run' n' s sf | Vcase e cl defst => do v <- expr_run s e; match find_case_stmnt s v cl with | Some (OK st') => stmnt_run' n' s st' | Some (Error msg) => Error msg | None => do s' <- handle_opt (msg "Verilog: no case was matched") (option_map (stmnt_run' n' s) defst); s' end | Vblock lhs rhs => match s with | State m assoc nbassoc f c => do name <- assign_name lhs; do rhse <- expr_run s rhs; OK (State m (PositiveMap.add name rhse assoc) nbassoc f c) | _ => Error (msg "Verilog: Wrong state") end | Vnonblock lhs rhs => match s with | State m assoc nbassoc f c => do name <- assign_name lhs; do rhse <- expr_run s rhs; OK (State m assoc (PositiveMap.add name rhse nbassoc) f c) | _ => Error (msg "Verilog: Wrong state") end end | _ => OK s end. Definition stmnt_run (s : state) (st : stmnt) : res state := stmnt_run' (stmnt_height st) s st. *) Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> stmnt -> reg_associations -> arr_associations -> Prop := | stmnt_runp_Vskip: forall f ar al, stmnt_runp f ar al Vskip ar al | stmnt_runp_Vseq: forall f st1 st2 asr0 asa0 asr1 asa1 asr2 asa2, stmnt_runp f asr0 asa0 st1 asr1 asa1 -> stmnt_runp f asr1 asa1 st2 asr2 asa2 -> stmnt_runp f asr0 asa0 (Vseq st1 st2) asr2 asa2 | stmnt_runp_Vcond_true: forall asr0 asa0 asr1 asa1 f c vc stt stf, expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc -> valueToBool vc = true -> stmnt_runp f asr0 asa0 stt asr1 asa1 -> stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1 | stmnt_runp_Vcond_false: forall asr0 asa0 asr1 asa1 f c vc stt stf, expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc -> valueToBool vc = false -> stmnt_runp f asr0 asa0 stf asr1 asa1 -> stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1 | stmnt_runp_Vcase_nomatch: forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def, expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve -> expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve -> mve <> ve -> stmnt_runp f asr0 asa0 (Vcase e cs def) asr1 asa1 -> stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1 | stmnt_runp_Vcase_match: forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def, expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve -> expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve -> mve = ve -> stmnt_runp f asr0 asa0 sc asr1 asa1 -> stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1 | stmnt_runp_Vcase_default: forall asr0 asa0 asr1 asa1 f st e ve, expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve -> stmnt_runp f asr0 asa0 st asr1 asa1 -> stmnt_runp f asr0 asa0 (Vcase e nil (Some st)) asr1 asa1 | stmnt_runp_Vblock_reg: forall lhs r rhs rhsval asr asa f, location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) -> expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> stmnt_runp f asr asa (Vblock lhs rhs) (block_reg r asr rhsval) asa | stmnt_runp_Vnonblock_reg: forall lhs r rhs rhsval asr asa f, location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) -> expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> stmnt_runp f asr asa (Vnonblock lhs rhs) (nonblock_reg r asr rhsval) asa | stmnt_runp_Vblock_arr: forall lhs r i rhs rhsval asr asa f, location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) -> expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> stmnt_runp f asr asa (Vblock lhs rhs) asr (block_arr r i asa rhsval) | stmnt_runp_Vnonblock_arr: forall lhs r i rhs rhsval asr asa f, location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) -> expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> stmnt_runp f asr asa (Vnonblock lhs rhs) asr (nonblock_arr r i asa rhsval). Hint Constructors stmnt_runp : verilog. (*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := let run := fun st ls => do s' <- stmnt_run s st; mi_step s' ls in match m with | (Valways _ st)::ls => run st ls | (Valways_ff _ st)::ls => run st ls | (Valways_comb _ st)::ls => run st ls | (Vdecl _ _)::ls => mi_step s ls | (Vdeclarr _ _ _)::ls => mi_step s ls | nil => OK s end.*) Inductive mi_stepp : fext -> reg_associations -> arr_associations -> module_item -> reg_associations -> arr_associations -> Prop := | mi_stepp_Valways : forall f sr0 sa0 st sr1 sa1 c, stmnt_runp f sr0 sa0 st sr1 sa1 -> mi_stepp f sr0 sa0 (Valways c st) sr1 sa1 | mi_stepp_Valways_ff : forall f sr0 sa0 st sr1 sa1 c, stmnt_runp f sr0 sa0 st sr1 sa1 -> mi_stepp f sr0 sa0 (Valways_ff c st) sr1 sa1 | mi_stepp_Valways_comb : forall f sr0 sa0 st sr1 sa1 c, stmnt_runp f sr0 sa0 st sr1 sa1 -> mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1 | mi_stepp_Vdecl : forall f sr sa d, mi_stepp f sr sa (Vdeclaration d) sr sa. Hint Constructors mi_stepp : verilog. Inductive mis_stepp : fext -> reg_associations -> arr_associations -> list module_item -> reg_associations -> arr_associations -> Prop := | mis_stepp_Cons : forall f mi mis sr0 sa0 sr1 sa1 sr2 sa2, mi_stepp f sr0 sa0 mi sr1 sa1 -> mis_stepp f sr1 sa1 mis sr2 sa2 -> mis_stepp f sr0 sa0 (mi :: mis) sr2 sa2 | mis_stepp_Nil : forall f sr sa, mis_stepp f sr sa nil sr sa. Hint Constructors mis_stepp : verilog. (*Definition mi_step_commit (s : state) (m : list module_item) : res state := match mi_step s m with | OK (State m assoc nbassoc f c) => OK (State m (merge_assocmap nbassoc assoc) empty_assocmap f c) | Error msg => Error msg | _ => Error (msg "Verilog: Wrong state") end. Fixpoint mi_run (f : fextclk) (assoc : assocmap) (m : list module_item) (n : nat) {struct n} : res assocmap := match n with | S n' => do assoc' <- mi_run f assoc m n'; match mi_step_commit (State assoc' empty_assocmap f (Pos.of_nat n')) m with | OK (State assoc _ _ _) => OK assoc | Error m => Error m end | O => OK assoc end.*) (** Resets the module into a known state, so that it can be executed. This is assumed to be the starting state of the module, and may have to be changed if other arguments to the module are also to be supported. *) (*Definition initial_fextclk (m : module) : fextclk := fun x => match x with | S O => (AssocMap.set (mod_reset m) (ZToValue 1) empty_assocmap) | _ => (AssocMap.set (mod_reset m) (ZToValue 0) empty_assocmap) end.*) (*Definition module_run (n : nat) (m : module) : res assocmap := mi_run (initial_fextclk m) empty_assocmap (mod_body m) n.*) Local Close Scope error_monad_scope. (*Theorem value_eq_size_if_eq: forall lv rv EQ, vsize lv = vsize rv -> value_eq_size lv rv = left EQ. Proof. intros. unfold value_eq_size. Theorem expr_run_same: forall assoc e v, expr_run assoc e = OK v <-> expr_runp assoc e v. Proof. split; generalize dependent v; generalize dependent assoc. - induction e. + intros. inversion H. constructor. + intros. inversion H. constructor. assumption. + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (expr_run assoc e2) eqn:?. unfold eq_to_opt in H1. destruct (value_eq_size v0 v1) eqn:?. inversion H1. constructor. apply IHe1. assumption. apply IHe2. assumption. reflexivity. discriminate. discriminate. discriminate. + intros. inversion H. destruct (expr_run assoc e) eqn:?. unfold option_map in H1. inversion H1. constructor. apply IHe. assumption. reflexivity. discriminate. + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (valueToBool v0) eqn:?. eapply erun_Vternary_true. apply IHe1. eassumption. apply IHe2. eassumption. assumption. eapply erun_Vternary_false. apply IHe1. eassumption. apply IHe3. eassumption. assumption. discriminate. - induction e. + intros. inversion H. reflexivity. + intros. inversion H. subst. simpl. assumption. + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. apply IHe2 in H6. rewrite H6. unfold eq_to_opt. assert (vsize lv = vsize rv). apply EQ. apply (value_eq_size_if_eq lv rv EQ) in H0. rewrite H0. reflexivity. + intros. inversion H. subst. simpl. destruct (expr_run assoc e) eqn:?. simpl. apply IHe in H3. rewrite Heqo in H3. inversion H3. subst. reflexivity. apply IHe in H3. rewrite Heqo in H3. discriminate. + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. apply IHe2 in H6. rewrite H6. reflexivity. subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. apply IHe3. assumption. Qed. *) Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} := match rl, vl with | r :: rl', v :: vl' => AssocMap.set r v (init_params vl' rl') | _, _ => empty_assocmap end. Definition genv := Globalenvs.Genv.t fundef unit. Definition empty_stack (m : module) : assocmap_arr := (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty arr)). Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist, asr!(m.(mod_reset)) = Some (ZToValue 0) -> asr!(m.(mod_finish)) = Some (ZToValue 0) -> asr!(m.(mod_st)) = Some ist -> valueToPos ist = st -> mis_stepp f (mkassociations asr empty_assocmap) (mkassociations asa (empty_stack m)) m.(mod_body) (mkassociations basr1 nasr1) (mkassociations basa1 nasa1)-> asr' = merge_regs nasr1 basr1 -> asa' = merge_arrs nasa1 basa1 -> asr'!(m.(mod_st)) = Some stval -> valueToPos stval = pstval -> step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') | step_finish : forall asr asa sf retval m st g, asr!(m.(mod_finish)) = Some (ZToValue 1) -> asr!(m.(mod_return)) = Some retval -> step g (State sf m st asr asa) Events.E0 (Returnstate sf retval) | step_call : forall g res m args, step g (Callstate res m args) Events.E0 (State res m m.(mod_entrypoint) (AssocMap.set (mod_reset m) (ZToValue 0) (AssocMap.set (mod_finish m) (ZToValue 0) (AssocMap.set m.(mod_st) (posToValue m.(mod_entrypoint)) (init_params args m.(mod_args))))) (empty_stack m)) | step_return : forall g m asr i r sf pc mst asa, mst = mod_st m -> step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa). Hint Constructors step : verilog. Inductive initial_state (p: program): state -> Prop := | initial_state_intro: forall b m0 m, let ge := Globalenvs.Genv.globalenv p in Globalenvs.Genv.init_mem p = Some m0 -> Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) -> initial_state p (Callstate nil m nil). Inductive final_state : state -> Integers.int -> Prop := | final_state_intro : forall retval retvali, retvali = valueToInt retval -> final_state (Returnstate nil retval) retvali. Definition semantics (m : program) := Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m).forall (f : fext) (e : expr) (asr : assocmap) (asa : assocmap_arr) (v : value), expr_runp f asr asa e v -> forall v' : value, expr_runp f asr asa e v' -> v' = vinduction e; intros; repeat (try match goal with | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vunop _ _) _ |- _ ] => invert H | [ H : expr_runp _ _ _ (Vternary _ _ _) _ |- _ ] => invert H | [ H1 : forall asr asa v, expr_runp _ asr asa ?e v -> _, H2 : expr_runp _ _ _ ?e _ |- _ ] => learn (H1 _ _ _ H2) | [ H1 : forall v, expr_runp _ ?asr ?asa ?e v -> _, H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => learn (H1 _ H2) end; crush). Qed. Hint Resolve expr_runp_determinate : verilog.forall (f : fext) (e : expr) (asr : assocmap) (asa : assocmap_arr) (v : value), expr_runp f asr asa e v -> forall v' : value, expr_runp f asr asa e v' -> v' = vforall (f : fext) (asr : assocmap) (asa : assocmap_arr) (e : expr) (l : location), location_is f asr asa e l -> forall l' : location, location_is f asr asa e l' -> l' = linduction 1; intros; repeat (try match goal with | [ H : location_is _ _ _ _ _ |- _ ] => invert H | [ H1 : expr_runp _ ?asr ?asa ?e _, H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => learn (expr_runp_determinate H1 H2) end; crush). Qed.forall (f : fext) (asr : assocmap) (asa : assocmap_arr) (e : expr) (l : location), location_is f asr asa e l -> forall l' : location, location_is f asr asa e l' -> l' = linduction 1; intros; repeat (try match goal with | [ H : stmnt_runp _ _ _ (Vseq _ _) _ _ |- _ ] => invert H | [ H : stmnt_runp _ _ _ (Vnonblock _ _) _ _ |- _ ] => invert H | [ H : stmnt_runp _ _ _ (Vblock _ _) _ _ |- _ ] => invert H | [ H : stmnt_runp _ _ _ Vskip _ _ |- _ ] => invert H | [ H : stmnt_runp _ _ _ (Vcond _ _ _) _ _ |- _ ] => invert H | [ H : stmnt_runp _ _ _ (Vcase _ (_ :: _) _) _ _ |- _ ] => invert H | [ H : stmnt_runp _ _ _ (Vcase _ [] _) _ _ |- _ ] => invert H | [ H1 : expr_runp _ ?asr ?asa ?e _, H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => learn (expr_runp_determinate H1 H2) | [ H1 : location_is _ ?asr ?asa ?e _, H2 : location_is _ ?asr ?asa ?e _ |- _ ] => learn (location_is_determinate H1 H2) | [ H1 : forall asr1 asa1, stmnt_runp _ ?asr0 ?asa0 ?s asr1 asa1 -> _, H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] => learn (H1 _ _ H2) end; crush). Qed. Hint Resolve stmnt_runp_determinate : verilog.forall (f : fext) (s : stmnt) (asr0 : reg_associations) (asa0 : arr_associations) (asr1 : reg_associations) (asa1 : arr_associations), stmnt_runp f asr0 asa0 s asr1 asa1 -> forall (asr1' : reg_associations) (asa1' : arr_associations), stmnt_runp f asr0 asa0 s asr1' asa1' -> asr1' = asr1 /\ asa1' = asa1forall (f : fext) (asr0 : reg_associations) (asa0 : arr_associations) (m : module_item) (asr1 : reg_associations) (asa1 : arr_associations), mi_stepp f asr0 asa0 m asr1 asa1 -> forall (asr1' : reg_associations) (asa1' : arr_associations), mi_stepp f asr0 asa0 m asr1' asa1' -> asr1' = asr1 /\ asa1' = asa1forall (f : fext) (asr0 : reg_associations) (asa0 : arr_associations) (m : module_item) (asr1 : reg_associations) (asa1 : arr_associations), mi_stepp f asr0 asa0 m asr1 asa1 -> forall (asr1' : reg_associations) (asa1' : arr_associations), mi_stepp f asr0 asa0 m asr1' asa1' -> asr1' = asr1 /\ asa1' = asa1destruct m; invert H; invert H0; repeat (try match goal with | [ H1 : stmnt_runp _ ?asr0 ?asa0 ?s _ _, H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] => learn (stmnt_runp_determinate H1 H2) end; crush). Qed.f:fextasr0:reg_associationsasa0:arr_associationsm:module_itemasr1:reg_associationsasa1:arr_associationsH:mi_stepp f asr0 asa0 m asr1 asa1asr1':reg_associationsasa1':arr_associationsH0:mi_stepp f asr0 asa0 m asr1' asa1'asr1' = asr1 /\ asa1' = asa1forall (f : fext) (asr0 : reg_associations) (asa0 : arr_associations) (m : list module_item) (asr1 : reg_associations) (asa1 : arr_associations), mis_stepp f asr0 asa0 m asr1 asa1 -> forall (asr1' : reg_associations) (asa1' : arr_associations), mis_stepp f asr0 asa0 m asr1' asa1' -> asr1' = asr1 /\ asa1' = asa1induction 1; intros; repeat (try match goal with | [ H : mis_stepp _ _ _ [] _ _ |- _ ] => invert H | [ H : mis_stepp _ _ _ ( _ :: _ ) _ _ |- _ ] => invert H | [ H1 : mi_stepp _ ?asr0 ?asa0 ?s _ _, H2 : mi_stepp _ ?asr0 ?asa0 ?s _ _ |- _ ] => learn (mi_stepp_determinate H1 H2) | [ H1 : forall asr1 asa1, mis_stepp _ ?asr0 ?asa0 ?m asr1 asa1 -> _, H2 : mis_stepp _ ?asr0 ?asa0 ?m _ _ |- _ ] => learn (H1 _ _ H2) end; crush). Qed.forall (f : fext) (asr0 : reg_associations) (asa0 : arr_associations) (m : list module_item) (asr1 : reg_associations) (asa1 : arr_associations), mis_stepp f asr0 asa0 m asr1 asa1 -> forall (asr1' : reg_associations) (asa1' : arr_associations), mis_stepp f asr0 asa0 m asr1' asa1' -> asr1' = asr1 /\ asa1' = asa1forall p : program, determinate (semantics p)forall p : program, determinate (semantics p)p:programdeterminate (semantics p)p:programge:=Genv.globalenv p:Genv.t fundef ()s:statet1:Events.traces1:statet2:Events.traces2:stateH:step (Genv.globalenv p) s t1 s1H0:step (Genv.globalenv p) s t2 s2Events.match_traces (Genv.globalenv p) t1 t2p:programge:=Genv.globalenv p:Genv.t fundef ()s:statet1:Events.traces1:statet2:Events.traces2:stateH:step (Genv.globalenv p) s t1 s1H0:step (Genv.globalenv p) s t2 s2t1 = t2 -> s1 = s2p:programge:=Genv.globalenv p:Genv.t fundef ()single_events (semantics p)p:programge:=Genv.globalenv p:Genv.t fundef ()s1, s2:stateH:initial_state p s1H0:initial_state p s2s1 = s2p:programge:=Genv.globalenv p:Genv.t fundef ()s:stater:intH:final_state s rnostep step (Genv.globalenv p) sp:programge:=Genv.globalenv p:Genv.t fundef ()s:stater1, r2:intH:final_state s r1H0:final_state s r2r1 = r2invert H; invert H0; constructor. (* Traces are always empty *)p:programge:=Genv.globalenv p:Genv.t fundef ()s:statet1:Events.traces1:statet2:Events.traces2:stateH:step (Genv.globalenv p) s t1 s1H0:step (Genv.globalenv p) s t2 s2Events.match_traces (Genv.globalenv p) t1 t2p:programge:=Genv.globalenv p:Genv.t fundef ()s:statet1:Events.traces1:statet2:Events.traces2:stateH:step (Genv.globalenv p) s t1 s1H0:step (Genv.globalenv p) s t2 s2t1 = t2 -> s1 = s2p:programge:=Genv.globalenv p:Genv.t fundef ()asr:AssocMap.t valueasa:AssocMap.t arrm:modulesf:list stackframeist:valuebasr0, nasr0:AssocMap.t valuebasa0, nasa0:AssocMap.t arrstval0:valuebasr1, nasr1:AssocMap.t valuebasa1, nasa1:AssocMap.t arrstval:valuef:fextH1:asr ! (mod_reset m) = Some (ZToValue 0)H2:asr ! (mod_finish m) = Some (ZToValue 0)H3:asr ! (mod_st m) = Some istH5:mis_stepp f {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |} {| assoc_blocking := asa; assoc_nonblocking := empty_stack m |} (mod_body m) {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |}H8:(merge_regs nasr1 basr1) ! (mod_st m) = Some stvalf0:fextH10:asr ! (mod_reset m) = Some (ZToValue 0)H11:asr ! (mod_finish m) = Some (ZToValue 0)H12:asr ! (mod_st m) = Some istH15:mis_stepp f0 {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |} {| assoc_blocking := asa; assoc_nonblocking := empty_stack m |} (mod_body m) {| assoc_blocking := basr0; assoc_nonblocking := nasr0 |} {| assoc_blocking := basa0; assoc_nonblocking := nasa0 |}H20:(merge_regs nasr0 basr0) ! (mod_st m) = Some stval0Learn:Learnt H3Learn0:Learnt H2Learn1:Learnt H1State sf m (valueToPos stval) (merge_regs nasr1 basr1) (merge_arrs nasa1 basa1) = State sf m (valueToPos stval0) (merge_regs nasr0 basr0) (merge_arrs nasa0 basa0)p:programge:=Genv.globalenv p:Genv.t fundef ()asr:AssocMap.t valueasa:AssocMap.t arrm:modulesf:list stackframeist:valuebasr0, nasr0:AssocMap.t valuebasa0, nasa0:AssocMap.t arrstval0:valuebasr1, nasr1:AssocMap.t valuebasa1, nasa1:AssocMap.t arrstval:valueH1:asr ! (mod_reset m) = Some (ZToValue 0)H2:asr ! (mod_finish m) = Some (ZToValue 0)H3:asr ! (mod_st m) = Some istf0:fextH5:mis_stepp f0 {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |} {| assoc_blocking := asa; assoc_nonblocking := empty_stack m |} (mod_body m) {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |}H8:(merge_regs nasr1 basr1) ! (mod_st m) = Some stvalH10:asr ! (mod_reset m) = Some (ZToValue 0)H11:asr ! (mod_finish m) = Some (ZToValue 0)H12:asr ! (mod_st m) = Some istH15:mis_stepp f0 {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |} {| assoc_blocking := asa; assoc_nonblocking := empty_stack m |} (mod_body m) {| assoc_blocking := basr0; assoc_nonblocking := nasr0 |} {| assoc_blocking := basa0; assoc_nonblocking := nasa0 |}H20:(merge_regs nasr0 basr0) ! (mod_st m) = Some stval0Learn:Learnt H3Learn0:Learnt H2Learn1:Learnt H1State sf m (valueToPos stval) (merge_regs nasr1 basr1) (merge_arrs nasa1 basa1) = State sf m (valueToPos stval0) (merge_regs nasr0 basr0) (merge_arrs nasa0 basa0)crush.p:programge:=Genv.globalenv p:Genv.t fundef ()asr:AssocMap.t valueasa:AssocMap.t arrm:modulesf:list stackframeist:valuebasr0, nasr0:AssocMap.t valuebasa0, nasa0:AssocMap.t arrstval0:valuebasr1, nasr1:AssocMap.t valuebasa1, nasa1:AssocMap.t arrstval:valueH1:asr ! (mod_reset m) = Some (ZToValue 0)H2:asr ! (mod_finish m) = Some (ZToValue 0)H3:asr ! (mod_st m) = Some istf0:fextH5:mis_stepp f0 {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |} {| assoc_blocking := asa; assoc_nonblocking := empty_stack m |} (mod_body m) {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |}H8:(merge_regs nasr1 basr1) ! (mod_st m) = Some stvalH10:asr ! (mod_reset m) = Some (ZToValue 0)H11:asr ! (mod_finish m) = Some (ZToValue 0)H12:asr ! (mod_st m) = Some istH15:mis_stepp f0 {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |} {| assoc_blocking := asa; assoc_nonblocking := empty_stack m |} (mod_body m) {| assoc_blocking := basr0; assoc_nonblocking := nasr0 |} {| assoc_blocking := basa0; assoc_nonblocking := nasa0 |}H20:(merge_regs nasr0 basr0) ! (mod_st m) = Some stval0Learn:Learnt H3Learn0:Learnt H2Learn1:Learnt H1H:{| assoc_blocking := basr0; assoc_nonblocking := nasr0 |} = {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} /\ {| assoc_blocking := basa0; assoc_nonblocking := nasa0 |} = {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |}State sf m (valueToPos stval) (merge_regs nasr1 basr1) (merge_arrs nasa1 basa1) = State sf m (valueToPos stval0) (merge_regs nasr0 basr0) (merge_arrs nasa0 basa0)p:programge:=Genv.globalenv p:Genv.t fundef ()single_events (semantics p)invert H; crush.p:programge:=Genv.globalenv p:Genv.t fundef ()s:Smallstep.state (semantics p)t:Events.traces':Smallstep.state (semantics p)H:Step (semantics p) s t s'(Datatypes.length t <= 0)%natinvert H; invert H0; unfold ge0, ge1 in *; crush.p:programge:=Genv.globalenv p:Genv.t fundef ()s1, s2:stateH:initial_state p s1H0:initial_state p s2s1 = s2red; simplify; intro; invert H0; invert H; crush.p:programge:=Genv.globalenv p:Genv.t fundef ()s:stater:intH:final_state s rnostep step (Genv.globalenv p) sinvert H; invert H0; crush. Qed.p:programge:=Genv.globalenv p:Genv.t fundef ()s:stater1, r2:intH:final_state s r1H0:final_state s r2r1 = r2