diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-07-14 16:08:58 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-14 16:08:58 +0100 |
commit | 450bda69837b02c20d2fb391bbe7827d1becaac4 (patch) | |
tree | 716c6d909fd18df3335080a0e00b4c79256c87ba /src | |
parent | 8486b4c046914b1388b68fe906fe267108f84267 (diff) | |
download | vericert-450bda69837b02c20d2fb391bbe7827d1becaac4.tar.gz vericert-450bda69837b02c20d2fb391bbe7827d1becaac4.zip |
Change name to Vericert
Diffstat (limited to 'src')
-rw-r--r-- | src/Compiler.v | 6 | ||||
-rw-r--r-- | src/CoqupClflags.ml | 2 | ||||
-rw-r--r-- | src/Simulator.v | 6 | ||||
-rw-r--r-- | src/common/Coquplib.v | 4 | ||||
-rw-r--r-- | src/common/IntegerExtra.v | 2 | ||||
-rw-r--r-- | src/common/Maps.v | 2 | ||||
-rw-r--r-- | src/common/Show.v | 2 | ||||
-rw-r--r-- | src/common/Statemonad.v | 2 | ||||
-rw-r--r-- | src/extraction/Extraction.v | 8 | ||||
-rw-r--r-- | src/translation/HTLgen.v | 4 | ||||
-rw-r--r-- | src/translation/HTLgenproof.v | 19 | ||||
-rw-r--r-- | src/translation/HTLgenspec.v | 4 | ||||
-rw-r--r-- | src/translation/Veriloggen.v | 4 | ||||
-rw-r--r-- | src/translation/Veriloggenproof.v | 6 | ||||
-rw-r--r-- | src/verilog/Array.v | 2 | ||||
-rw-r--r-- | src/verilog/AssocMap.v | 4 | ||||
-rw-r--r-- | src/verilog/HTL.v | 6 | ||||
-rw-r--r-- | src/verilog/PrintHTL.ml | 4 | ||||
-rw-r--r-- | src/verilog/PrintVerilog.ml | 4 | ||||
-rw-r--r-- | src/verilog/PrintVerilog.mli | 2 | ||||
-rw-r--r-- | src/verilog/Value.v | 4 | ||||
-rw-r--r-- | src/verilog/ValueInt.v | 4 | ||||
-rw-r--r-- | src/verilog/Verilog.v | 4 |
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. |