Change name to Vericert

35 files changed, 135 insertions, 136 deletions

diff --git a/.gitignore b/.gitignore
index b2cf595..96ced2e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -41,7 +41,7 @@ src/extraction/STAMP
 
 *.exe
 *.ini
-bin/coqup
+bin/vericert
 
 # Ocaml
 _build
diff --git a/LICENSE b/LICENSE
index 0416644..fd6a7ce 100644
--- a/LICENSE
+++ b/LICENSE
@@ -631,7 +631,7 @@ to attach them to the start of each source file to most effectively
 state the exclusion of warranty; and each file should have at least
 the "copyright" line and a pointer to where the full notice is found.
 
-    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
@@ -652,7 +652,7 @@ Also add information on how to contact you by electronic and paper mail.
   If the program does terminal interaction, make it output a short
 notice like this when it starts in an interactive mode:
 
-    CoqUp Copyright (C) 2019-2020 Yann Herklotz
+    Vericert Copyright (C) 2019-2020 Yann Herklotz
     This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
     This is free software, and you are welcome to redistribute it
     under certain conditions; type `show c' for details.
diff --git a/Makefile b/Makefile
index 1303b13..518d4c9 100644
--- a/Makefile
+++ b/Makefile
@@ -9,9 +9,9 @@ endif
 COMPCERTRECDIRS := lib common x86_32 x86 backend cfrontend driver flocq exportclight \
   MenhirLib cparser
 
-COQINCLUDES := -R src/common coqup.common -R src/verilog coqup.verilog \
-               -R src/extraction coqup.extraction -R src/translation coqup.translation \
-               -R src coqup \
+COQINCLUDES := -R src/common vericert.common -R src/verilog vericert.verilog \
+               -R src/extraction vericert.extraction -R src/translation vericert.translation \
+               -R src vericert \
                $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d))
 
 COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source
@@ -35,7 +35,7 @@ lib/COMPCERTSTAMP:
 install:
 	install -d $(PREFIX)/bin
 	install -C _build/default/driver/compcert.ini $(PREFIX)/bin/.
-	install -C _build/default/driver/CoqupDriver.exe $(PREFIX)/bin/coqup
+	install -C _build/default/driver/VericertDriver.exe $(PREFIX)/bin/vericert
 
 proof: Makefile.coq
 	$(MAKE) -f Makefile.coq
@@ -47,9 +47,9 @@ test:
 	./test/test_all.sh ./test
 
 compile: src/extraction/STAMP
-	@echo "OCaml bin/coqup"
+	@echo "OCaml bin/vericert"
 	@mkdir -p bin
-	@dune build driver/CoqupDriver.exe
+	@dune build driver/VericertDriver.exe
 	@cp lib/CompCert/compcert.ini _build/default/driver/.
 
 src/extraction/STAMP:
diff --git a/README.md b/README.md
index 026266b..0f1041e 100644
--- a/README.md
+++ b/README.md
@@ -1,10 +1,10 @@
-# Coqup [![Build Status](https://travis-ci.com/ymherklotz/coqup.svg?token=qfBKKGwxeWkjDsy7e16x&branch=master)](https://travis-ci.com/ymherklotz/coqup)
+# Vericert [![Build Status](https://travis-ci.com/ymherklotz/vericert.svg?token=qfBKKGwxeWkjDsy7e16x&branch=master)](https://travis-ci.com/ymherklotz/vericert)
 
 A formally verified HLS tool in Coq, building on top of [CompCert](https://github.com/AbsInt/CompCert).
 
 ## Building
 
-To build coqup, the provided [Makefile](/Makefile) can be used. External dependencies are needed to build the project, which can be pulled in automatically with [nix](https://nixos.org/nix/) using the provided [default.nix](/default.nix) and [shell.nix](/shell.nix) files.
+To build vericert, the provided [Makefile](/Makefile) can be used. External dependencies are needed to build the project, which can be pulled in automatically with [nix](https://nixos.org/nix/) using the provided [default.nix](/default.nix) and [shell.nix](/shell.nix) files.
 
 The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following:
 
@@ -23,7 +23,7 @@ These dependencies can be installed manually, or automatically through Nix.
 CompCert is added as a submodule in the `lib/CompCert` directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, you can run:
 
 ``` shell
-git clone --recursive https://github.com/ymherklotz/coqup
+git clone --recursive https://github.com/ymherklotz/vericert
 ```
 
 If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded:
@@ -58,14 +58,14 @@ and installed locally, or under the `PREFIX` location using:
 make install
 ```
 
-Which will install the binary in `./bin/coqup` by default. However, this can be changed by changing the `PREFIX` environment variable, in which case the binary will be installed in `$PREFIX/bin/coqup`.
+Which will install the binary in `./bin/vericert` by default. However, this can be changed by changing the `PREFIX` environment variable, in which case the binary will be installed in `$PREFIX/bin/vericert`.
 
 ## Running
 
-To test out `coqup` you can try the following examples which are in the test folder using the following:
+To test out `vericert` you can try the following examples which are in the test folder using the following:
 
 ``` shell
-./bin/coqup test/loop.c -o loop.v
-./bin/coqup test/conditional.c -o conditional.v
-./bin/coqup test/add.c -o add.v
+./bin/vericert test/loop.c -o loop.v
+./bin/vericert test/conditional.c -o conditional.v
+./bin/vericert test/add.c -o add.v
 ```
diff --git a/_CoqProject b/_CoqProject
index 7965da9..e86312b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,8 +1,8 @@
--R src/common coqup.common
--R src/extraction coqup.extraction
--R src/translation coqup.translation
--R src/verilog coqup.verilog
--R src coqup
+-R src/common vericert.common
+-R src/extraction vericert.extraction
+-R src/translation vericert.translation
+-R src/verilog vericert.verilog
+-R src vericert
 
 -R lib/CompCert/MenhirLib compcert.MenhirLib
 -R lib/CompCert/backend compcert.backend
diff --git a/debug/CoqupTest.ml b/debug/CoqupTest.ml
index f961f64..2fe1389 100644
--- a/debug/CoqupTest.ml
+++ b/debug/CoqupTest.ml
@@ -1,4 +1,4 @@
-open Coqup
+open Vericert
 
 open Test
 open Camlcoq
diff --git a/debug/dune b/debug/dune
index 7f0c6a6..feee97c 100644
--- a/debug/dune
+++ b/debug/dune
@@ -1,5 +1,5 @@
 (include_subdirs no)
 
 (executable
- (name CoqupTest)
- (libraries coqup))
+ (name VericertTest)
+ (libraries vericert))
diff --git a/default.nix b/default.nix
index cd37308..a253285 100644
--- a/default.nix
+++ b/default.nix
@@ -25,7 +25,7 @@ let
       } ) { };
 in
 stdenv.mkDerivation {
-  name = "coqup";
+  name = "vericert";
   src = ./.;
 
   buildInputs = [ ncoq ocamlPackages.menhir dune
diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml
index 0b64f48..f500499 100644
--- a/driver/CoqupDriver.ml
+++ b/driver/CoqupDriver.ml
@@ -9,7 +9,7 @@
 (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
 (*                                                                     *)
 (* *********************************************************************)
-(* 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,16 +27,16 @@
  *)
 
 open Printf
-open Coqup.Commandline
-open Coqup.Clflags
-open Coqup.CommonOptions
-open Coqup.Timing
-open Coqup.Driveraux
-open Coqup.Frontend
-open Coqup.Assembler
-open Coqup.Linker
-open Coqup.Diagnostics
-open Coqup.CoqupClflags
+open Vericert.Commandline
+open Vericert.Clflags
+open Vericert.CommonOptions
+open Vericert.Timing
+open Vericert.Driveraux
+open Vericert.Frontend
+open Vericert.Assembler
+open Vericert.Linker
+open Vericert.Diagnostics
+open Vericert.VericertClflags
 
 (* Name used for version string etc. *)
 let tool_name = "C verified high-level synthesis"
@@ -60,45 +60,45 @@ let compile_c_file sourcename ifile ofile =
   let set_dest dst opt ext =
     dst := if !opt then Some (output_filename sourcename ".c" ext)
       else None in
-  set_dest Coqup.Cprint.destination option_dparse ".parsed.c";
-  set_dest Coqup.PrintCsyntax.destination option_dcmedium ".compcert.c";
-  set_dest Coqup.PrintClight.destination option_dclight ".light.c";
-  set_dest Coqup.PrintCminor.destination option_dcminor ".cm";
-  set_dest Coqup.PrintRTL.destination option_drtl ".rtl";
-  set_dest Coqup.PrintHTL.destination option_dhtl ".htl";
-  set_dest Coqup.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
-  set_dest Coqup.PrintLTL.destination option_dltl ".ltl";
-  set_dest Coqup.PrintMach.destination option_dmach ".mach";
-  set_dest Coqup.AsmToJSON.destination option_sdump !sdump_suffix;
+  set_dest Vericert.Cprint.destination option_dparse ".parsed.c";
+  set_dest Vericert.PrintCsyntax.destination option_dcmedium ".compcert.c";
+  set_dest Vericert.PrintClight.destination option_dclight ".light.c";
+  set_dest Vericert.PrintCminor.destination option_dcminor ".cm";
+  set_dest Vericert.PrintRTL.destination option_drtl ".rtl";
+  set_dest Vericert.PrintHTL.destination option_dhtl ".htl";
+  set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
+  set_dest Vericert.PrintLTL.destination option_dltl ".ltl";
+  set_dest Vericert.PrintMach.destination option_dmach ".mach";
+  set_dest Vericert.AsmToJSON.destination option_sdump !sdump_suffix;
   (* Parse the ast *)
   let csyntax = parse_c_file sourcename ifile in
   if not !option_hls then begin
     (* Convert to Asm *)
     let asm =
-      match Coqup.Compiler.apply_partial
-              (Coqup.Compiler.transf_c_program csyntax)
-              Coqup.Asmexpand.expand_program with
-      | Coqup.Errors.OK asm ->
+      match Vericert.Compiler.apply_partial
+              (Vericert.Compiler.transf_c_program csyntax)
+              Vericert.Asmexpand.expand_program with
+      | Vericert.Errors.OK asm ->
         asm
-      | Coqup.Errors.Error msg ->
+      | Vericert.Errors.Error msg ->
         let loc = file_loc sourcename in
         fatal_error loc "%a"  print_error msg in
     (* Dump Asm in binary and JSON format *)
-    Coqup.AsmToJSON.print_if asm sourcename;
+    Vericert.AsmToJSON.print_if asm sourcename;
     (* Print Asm in text form *)
     let oc = open_out ofile in
-    Coqup.PrintAsm.print_program oc asm;
+    Vericert.PrintAsm.print_program oc asm;
     close_out oc
   end else begin
     let verilog =
-      match Coqup.Compiler0.transf_hls csyntax with
-      | Coqup.Errors.OK v ->
+      match Vericert.Compiler0.transf_hls csyntax with
+      | Vericert.Errors.OK v ->
         v
-      | Coqup.Errors.Error msg ->
+      | Vericert.Errors.Error msg ->
         let loc = file_loc sourcename in
         fatal_error loc "%a"  print_error msg in
     let oc = open_out ofile in
-    Coqup.PrintVerilog.print_program !option_debug_hls oc verilog;
+    Vericert.PrintVerilog.print_program !option_debug_hls oc verilog;
     close_out oc
   end
 
@@ -106,9 +106,9 @@ let compile_c_file sourcename ifile ofile =
 
 let compile_i_file sourcename preproname =
   if !option_interp then begin
-    Coqup.Machine.config := Coqup.Machine.compcert_interpreter !Coqup.Machine.config;
+    Vericert.Machine.config := Vericert.Machine.compcert_interpreter !Vericert.Machine.config;
     let csyntax = parse_c_file sourcename preproname in
-    Coqup.Interp.execute csyntax;
+    Vericert.Interp.execute csyntax;
         ""
   end else if !option_hls then begin
     compile_c_file sourcename preproname
@@ -179,7 +179,7 @@ let process_h_file sourcename =
     fatal_error no_loc "input file %s ignored (not in -E mode)\n" sourcename
 
 let target_help =
-  if Coqup.Configuration.arch = "arm" && Coqup.Configuration.model <> "armv6" then
+  if Vericert.Configuration.arch = "arm" && Vericert.Configuration.model <> "armv6" then
 {|Target processor options:
   -mthumb        Use Thumb2 instruction encoding
   -marm          Use classic ARM instruction encoding
@@ -188,7 +188,7 @@ else
   ""
 
 let toolchain_help =
-  if not Coqup.Configuration.gnu_toolchain then begin
+  if not Vericert.Configuration.gnu_toolchain then begin
 {|Toolchain options:
   -t tof:env     Select target processor for the diab toolchain
 |} end else
@@ -216,7 +216,7 @@ Processing options:
 |} ^
   prepro_help ^
   language_support_help ^
- Coqup.DebugInit.debugging_help ^
+ Vericert.DebugInit.debugging_help ^
 {|Optimization options: (use -fno-<opt> to turn off -f<opt>)
   -O             Optimize the compiled code [on by default]
   -O0            Do not optimize the compiled code
@@ -263,7 +263,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)
 |} ^
   general_help ^
   warning_help ^
-  {|Coqup.Interpreter mode:
+  {|Vericert.Interpreter mode:
   -interp        Execute given .c files using the reference interpreter
   -quiet         Suppress diagnostic messages for the interpreter
   -trace         Have the interpreter produce a detailed trace of reductions
@@ -275,7 +275,7 @@ let print_usage_and_exit () =
   printf "%s" usage_string; exit 0
 
 let enforce_buildnr nr =
-  let build = int_of_string Coqup.Version.buildnr in
+  let build = int_of_string Vericert.Version.buildnr in
   if nr != build then
     fatal_error no_loc "Mismatching builds: This is CompCert build %d, but QSK requires build %d.\n\
 Please use matching builds of QSK and CompCert." build nr
@@ -283,7 +283,7 @@ Please use matching builds of QSK and CompCert." build nr
 let dump_mnemonics destfile =
   let oc = open_out_bin destfile in
   let pp = Format.formatter_of_out_channel oc in
-  Coqup.AsmToJSON.pp_mnemonics pp;
+  Vericert.AsmToJSON.pp_mnemonics pp;
   Format.pp_print_flush pp ();
   close_out oc;
   exit 0
@@ -320,7 +320,7 @@ let cmdline_actions =
 (* Getting version info *)
   @ version_options tool_name @
 (* Enforcing CompCert build numbers for QSKs and mnemonics dump *)
-  (if Coqup.Version.buildnr <> "" then
+  (if Vericert.Version.buildnr <> "" then
     [ Exact "-qsk-enforce-build", Integer enforce_buildnr;
       Exact "--qsk-enforce-build", Integer enforce_buildnr;
       Exact "-dump-mnemonics", String  dump_mnemonics;
@@ -338,7 +338,7 @@ let cmdline_actions =
   (* Language support options *)
     language_support_options
   (* Debugging options *)
-    @ Coqup.DebugInit.debugging_actions @
+    @ Vericert.DebugInit.debugging_actions @
 (* Code generation options -- more below *)
  [
   Exact "-O0", Unit (unset_all optimization_options);
@@ -354,15 +354,15 @@ let cmdline_actions =
   Exact "-falign-cond-branches", Integer(fun n -> check_align n; option_faligncondbranchs := n);] @
       f_opt "common" option_fcommon @
 (* Target processor options *)
-  (if Coqup.Configuration.arch = "arm" then
-    if Coqup.Configuration.model = "armv6" then
+  (if Vericert.Configuration.arch = "arm" then
+    if Vericert.Configuration.model = "armv6" then
       [ Exact "-marm", Ignore ] (* Thumb needs ARMv6T2 or ARMv7 *)
     else
       [ Exact "-mthumb", Set option_mthumb;
         Exact "-marm", Unset option_mthumb; ]
    else []) @
 (* Toolchain options *)
-    (if not Coqup.Configuration.gnu_toolchain then
+    (if not Vericert.Configuration.gnu_toolchain then
        [Exact "-t", String (fun arg -> push_linker_arg "-t"; push_linker_arg arg;
                              prepro_options := arg :: "-t" :: !prepro_options;
                              assembler_options := arg :: "-t" :: !assembler_options;)]
@@ -398,17 +398,17 @@ let cmdline_actions =
     option_dasm := true);
   Exact "-sdump", Set option_sdump;
   Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s);
-  Exact "-sdump-folder", String (fun s -> Coqup.AsmToJSON.sdump_folder := s);] @
+  Exact "-sdump-folder", String (fun s -> Vericert.AsmToJSON.sdump_folder := s);] @
 (* General options *)
    general_options @
 (* Diagnostic options *)
   warning_options @
-(* Coqup.Interpreter mode *)
+(* Vericert.Interpreter mode *)
  [ Exact "-interp", Set option_interp;
-  Exact "-quiet", Unit (fun () -> Coqup.Interp.trace := 0);
-  Exact "-trace", Unit (fun () -> Coqup.Interp.trace := 2);
-  Exact "-random", Unit (fun () -> Coqup.Interp.mode := Coqup.Interp.Random);
-  Exact "-all", Unit (fun () -> Coqup.Interp.mode := Coqup.Interp.All)
+  Exact "-quiet", Unit (fun () -> Vericert.Interp.trace := 0);
+  Exact "-trace", Unit (fun () -> Vericert.Interp.trace := 2);
+  Exact "-random", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.Random);
+  Exact "-all", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.All)
  ]
 (* Optimization options *)
 (* -f options: come in -f and -fno- variants *)
@@ -456,9 +456,9 @@ let _ =
                 Gc.major_heap_increment = 4194304 (* 4M *)
            };
     Printexc.record_backtrace true;
-    Coqup.Frontend.init ();
+    Vericert.Frontend.init ();
     parse_cmdline cmdline_actions;
-    Coqup.DebugInit.init (); (* Initialize the debug functions *)
+    Vericert.DebugInit.init (); (* Initialize the debug functions *)
     if nolink () && !option_o <> None && !num_source_files >= 2 then
       fatal_error no_loc "ambiguous '-o' option (multiple source files)";
     if !num_input_files = 0 then
diff --git a/driver/dune b/driver/dune
index 5dbfcad..b0c97bc 100644
--- a/driver/dune
+++ b/driver/dune
@@ -1,5 +1,5 @@
 (include_subdirs no)
 
 (executable
- (name CoqupDriver)
- (libraries coqup))
+ (name VericertDriver)
+ (libraries vericert))
diff --git a/dune b/dune
index 020ec08..92ac822 100644
--- a/dune
+++ b/dune
@@ -4,7 +4,7 @@
 (include_subdirs unqualified)
 
 (library
- (public_name coqup)
+ (public_name vericert)
  (modules_without_implementation c debugTypes dwarfTypes)
  (libraries menhirLib str unix)
  (flags (:standard -warn-error -A)))
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.
 
diff --git a/test/test_all.sh b/test/test_all.sh
index 371ed0e..d43e2ac 100755
--- a/test/test_all.sh
+++ b/test/test_all.sh
@@ -30,7 +30,7 @@ for cfile in $test_dir/*.c; do
     gcc -o $outbase.gcc $cfile
     $outbase.gcc
     expected=$?
-    ./bin/coqup -drtl -o $outbase.v $cfile
+    ./bin/vericert -drtl -o $outbase.v $cfile
     iverilog -o $outbase.iverilog $outbase.v
     actual=$($outbase.iverilog | sed -E -e 's/[^0-9]+([0-9]+)/\1/')
     if [[ $expected = $actual ]]; then