Change name to Vericert

23 files changed, 52 insertions, 53 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index d716caa..7b17336 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * 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
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From coqup Require Import HTLgenproof.
+From vericert Require Import HTLgenproof.
 
 From compcert.common Require Import
     Errors
@@ -47,7 +47,7 @@ From compcert.cfrontend Require
 From compcert.driver Require
     Compiler.
 
-From coqup Require
+From vericert Require
      Verilog
      Veriloggen
      Veriloggenproof
diff --git a/src/CoqupClflags.ml b/src/CoqupClflags.ml
index 5b40ce6..ca591de 100644
--- a/src/CoqupClflags.ml
+++ b/src/CoqupClflags.ml
@@ -1,4 +1,4 @@
-(* Coqup flags *)
+(* Vericert flags *)
 let option_simulate = ref false
 let option_hls = ref true
 let option_debug_hls = ref false
diff --git a/src/Simulator.v b/src/Simulator.v
index 83d3e96..3df0c7f 100644
--- a/src/Simulator.v
+++ b/src/Simulator.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -20,8 +20,8 @@
 
 From compcert Require Import Errors.
 
-From coqup Require Compiler Verilog Value.
-From coqup Require Import Coquplib.
+From vericert Require Compiler Verilog Value.
+From vericert Require Import Vericertlib.
 
 Local Open Scope error_monad_scope.
 
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index 2295ff6..d9176db 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * 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
@@ -25,7 +25,7 @@ From Coq Require Export
 
 Require Import Lia.
 
-From coqup Require Import Show.
+From vericert Require Import Show.
 
 (* Depend on CompCert for the basic library, as they declare and prove some
    useful theorems. *)
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
index fe7d94f..c9b5dbd 100644
--- a/src/common/IntegerExtra.v
+++ b/src/common/IntegerExtra.v
@@ -5,7 +5,7 @@ Require Import ZBinary.
 From bbv Require Import ZLib.
 From compcert Require Import Integers Coqlib.
 
-Require Import Coquplib.
+Require Import Vericertlib.
 
 Local Open Scope Z_scope.
 
diff --git a/src/common/Maps.v b/src/common/Maps.v
index 3236417..b5a2fb2 100644
--- a/src/common/Maps.v
+++ b/src/common/Maps.v
@@ -1,4 +1,4 @@
-From coqup Require Import Coquplib.
+From vericert Require Import Vericertlib.
 
 From compcert Require Export Maps.
 From compcert Require Import Errors.
diff --git a/src/common/Show.v b/src/common/Show.v
index c994df3..4c66725 100644
--- a/src/common/Show.v
+++ b/src/common/Show.v
@@ -1,5 +1,5 @@
 (* 
- * CoqUp: Verified high-level synthesis.
+ * 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
diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v
index ed1b9e7..2eada2f 100644
--- a/src/common/Statemonad.v
+++ b/src/common/Statemonad.v
@@ -1,5 +1,5 @@
 From compcert Require Errors.
-From coqup Require Import Monad.
+From vericert Require Import Monad.
 From Coq Require Import Lists.List.
 
 Module Type State.
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index df21dc4..b1a885e 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * 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
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From coqup Require Verilog Value Compiler.
+From vericert Require Verilog Value Compiler.
 
 From Coq Require DecidableClass.
 
@@ -134,7 +134,7 @@ Extract Constant Compiler.print_Mach => "PrintMach.print_if".
 Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x".
 Extract Constant Compiler.time  => "Timing.time_coq".
 
-Extract Constant Coquplib.debug_print => "print_newline".
+Extract Constant Vericertlib.debug_print => "print_newline".
 
 (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*)
 
@@ -167,7 +167,7 @@ Set Extraction AccessOpaque.
 
 Cd "src/extraction".
 Separate Extraction
-         Verilog.module Value.uvalueToZ coqup.Compiler.transf_hls
+         Verilog.module Value.uvalueToZ vericert.Compiler.transf_hls
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 1cc30c7..8245a06 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -1,5 +1,5 @@
 (* 
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -19,7 +19,7 @@
 From compcert Require Import Maps.
 From compcert Require Errors Globalenvs Integers.
 From compcert Require Import AST RTL.
-From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt Statemonad.
+From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt Statemonad.
 
 Hint Resolve AssocMap.gempty : htlh.
 Hint Resolve AssocMap.gso : htlh.
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index dd1d967..ddf8c3a 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -18,8 +18,8 @@
 
 From compcert Require RTL Registers AST.
 From compcert Require Import Integers Globalenvs Memory Linking.
-From coqup Require Import Coquplib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra.
-From coqup Require HTL Verilog.
+From vericert Require Import Vericertlib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra.
+From vericert Require HTL Verilog.
 
 Require Import Lia.
 
@@ -708,13 +708,12 @@ Section CORRECTNESS.
             Admitted.
 
   Lemma eval_cond_correct :
-    forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa,
-      translate_condition cond args s1 = OK c s' i ->
-      Op.eval_condition
-        cond
-        (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args)
-        m = Some b ->
-      Verilog.expr_runp f asr asa c (boolToValue b).
+    exists v' : value,
+      Verilog.expr_runp f' asr asa e v' /\
+      val_value_lessdef
+        (Values.Val.of_optbool
+           (Op.eval_condition cond
+                              (map (fun r : positive => Registers.Regmap.get r rs) args) m)) v'
   Admitted.
 
   (** The proof of semantic preservation for the translation of instructions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 71fb618..93d5612 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -18,7 +18,7 @@
 
 From compcert Require RTL Op Maps Errors.
 From compcert Require Import Maps Integers.
-From coqup Require Import Coquplib Verilog ValueInt HTL HTLgen AssocMap.
+From vericert Require Import Vericertlib Verilog ValueInt HTL HTLgen AssocMap.
 Require Import Lia.
 
 Hint Resolve Maps.PTree.elements_keys_norepet : htlspec.
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index f5d5fa7..a0be0fa 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -19,7 +19,7 @@
 From compcert Require Import Maps.
 From compcert Require Errors.
 From compcert Require Import AST.
-From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt.
+From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt.
 
 Definition transl_list_fun (a : node * Verilog.stmnt) :=
   let (n, stmnt) := a in
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
index 5b467a7..9abbd4b 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/translation/Veriloggenproof.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -17,8 +17,8 @@
  *)
 
 From compcert Require Import Smallstep Linking Integers Globalenvs.
-From coqup Require HTL.
-From coqup Require Import Coquplib Veriloggen Verilog ValueInt AssocMap.
+From vericert Require HTL.
+From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap.
 Require Import Lia.
 
 Local Open Scope assocmap.
diff --git a/src/verilog/Array.v b/src/verilog/Array.v
index be06541..02b6d33 100644
--- a/src/verilog/Array.v
+++ b/src/verilog/Array.v
@@ -1,7 +1,7 @@
 Set Implicit Arguments.
 
 Require Import Lia.
-Require Import Coquplib.
+Require Import Vericertlib.
 From Coq Require Import Lists.List Datatypes.
 
 Import ListNotations.
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
index c5cfa3f..8d8788a 100644
--- a/src/verilog/AssocMap.v
+++ b/src/verilog/AssocMap.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From coqup Require Import Coquplib ValueInt.
+From vericert Require Import Vericertlib ValueInt.
 From compcert Require Import Maps.
 
 Definition reg := positive.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index b3d1442..620ef14 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -17,8 +17,8 @@
  *)
 
 From Coq Require Import FSets.FMapPositive.
-From coqup Require Import Coquplib ValueInt AssocMap Array.
-From coqup Require Verilog.
+From vericert Require Import Vericertlib ValueInt AssocMap Array.
+From vericert Require Verilog.
 From compcert Require Events Globalenvs Smallstep Integers Values.
 From compcert Require Import Maps.
 
diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml
index 0bdba51..44f8b01 100644
--- a/src/verilog/PrintHTL.ml
+++ b/src/verilog/PrintHTL.ml
@@ -1,5 +1,5 @@
 (* -*- mode: tuareg -*-
- * CoqUp: Verified high-level synthesis.
+ * 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
@@ -27,7 +27,7 @@ open AST
 open HTL
 open PrintAST
 open PrintVerilog
-open CoqupClflags
+open VericertClflags
 
 let pstr pp = fprintf pp "%s"
 
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 5265c97..f348ee6 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -1,5 +1,5 @@
 (* -*- mode: tuareg -*-
- * CoqUp: Verified high-level synthesis.
+ * 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
@@ -26,7 +26,7 @@ open Clflags
 
 open Printf
 
-open CoqupClflags
+open VericertClflags
 
 let concat = String.concat ""
 
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index 62bf63f..47af3ef 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/verilog/PrintVerilog.mli
@@ -1,5 +1,5 @@
 (* 
- * CoqUp: Verified high-level synthesis.
+ * 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
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index af2b822..41a41b4 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -21,7 +21,7 @@ From bbv Require Import Word.
 From bbv Require HexNotation WordScope.
 From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
 From compcert Require Import lib.Integers common.Values.
-From coqup Require Import Coquplib.
+From vericert Require Import Vericertlib.
 (* end hide *)
 
 (** * Value
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v
index f0f6de6..c7f69a1 100644
--- a/src/verilog/ValueInt.v
+++ b/src/verilog/ValueInt.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
@@ -21,7 +21,7 @@ From bbv Require Import Word.
 From bbv Require HexNotation WordScope.
 From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
 From compcert Require Import lib.Integers common.Values.
-From coqup Require Import Coquplib.
+From vericert Require Import Vericertlib.
 (* end hide *)
 
 (** * Value
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 321bdc2..3b0dd0a 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -1,5 +1,5 @@
 (*
- * CoqUp: Verified high-level synthesis.
+ * 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
@@ -29,7 +29,7 @@ Require Import Lia.
 
 Import ListNotations.
 
-From coqup Require Import common.Coquplib common.Show verilog.ValueInt AssocMap Array.
+From vericert Require Import common.Vericertlib common.Show verilog.ValueInt AssocMap Array.
 From compcert Require Events.
 From compcert Require Import Integers Errors Smallstep Globalenvs.