diff options
-rw-r--r-- | README.org | 6 | ||||
-rw-r--r-- | default.nix | 6 | ||||
m--------- | docs | 0 | ||||
-rw-r--r-- | src/extraction/Extraction.v | 8 | ||||
-rw-r--r-- | src/hls/Sat.v | 4 |
5 files changed, 15 insertions, 9 deletions
@@ -1,3 +1,5 @@ +#+title: + #+html: <a href="https://vericert.ymhg.org"><img src="https://vericert.ymhg.org/vericert-main.svg" width="100%" height="144" /></a> #+html: <p align=center><a href="https://github.com/ymherklotz/vericert/actions"><img src="https://github.com/ymherklotz/vericert/workflows/CI/badge.svg" /></a> <a href="https://vericert.ymhg.org/"><img src="https://github.com/ymherklotz/vericert-docs/workflows/docs/badge.svg" /></a></p> @@ -11,8 +13,8 @@ correctness. :PROPERTIES: :CUSTOM_ID: features :END: -The project is currently a work in progress, so proofs remain to be finished. Currently, the -following C features are supported, but are not all proven correct yet: + +Currently all proofs of the following features have been completed. - all int operations, - non-recursive function calls, diff --git a/default.nix b/default.nix index 1121469..fa60637 100644 --- a/default.nix +++ b/default.nix @@ -1,4 +1,4 @@ -with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/8dd8bd8be74879f9f7919b16a4cb5ab2a75f18e5.tar.gz") {}; +with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/1a56d76d718afb6c47dd96602c915b6d23f7c45d.tar.gz") {}; let ncoq = coq_8_13; ncoqPackages = coqPackages_8_13; @@ -10,6 +10,10 @@ stdenv.mkDerivation { buildInputs = [ ncoq dune_2 gcc ncoq.ocaml ncoq.ocamlPackages.findlib ncoq.ocamlPackages.menhir ncoq.ocamlPackages.ocamlgraph + ncoqPackages.serapi + python3 python3Packages.docutils python3Packages.pygments + python3Packages.dominate + python3Packages.pelican ]; enableParallelBuilding = true; diff --git a/docs b/docs -Subproject 5508c21e064276aa4d5146b3af5b6f6e9a4c236 +Subproject 42e19f2b20c907505a28486a8071147ed6c610f diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 6abe4e0..6bbfc05 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -179,7 +179,7 @@ Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". Extract Constant Pipeline.pipeline => "SoftwarePipelining.pipeline". Extract Constant RTLBlockgen.partition => "Partition.partition". -(*Extract Constant RTLPargen.schedule => "Schedule.schedule_fn".*) +Extract Constant RTLPargen.schedule => "Schedule.schedule_fn". (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. @@ -187,11 +187,11 @@ Set Extraction AccessOpaque. Cd "src/extraction". Separate Extraction Verilog.module vericert.Compiler.transf_hls -(* vericert.Compiler.transf_hls_temp*) -(* RTLBlockgen.transl_program RTLBlockInstr.successors_instr*) + vericert.Compiler.transf_hls_temp + RTLBlockgen.transl_program RTLBlockInstr.successors_instr HTLgen.tbl_to_case_expr Pipeline.pipeline -(* RTLBlockInstr.sat_pred_temp*) + RTLBlockInstr.sat_pred_simple Verilog.stmnt_to_list Compiler.transf_c_program Compiler.transf_cminor_program diff --git a/src/hls/Sat.v b/src/hls/Sat.v index 9549947..679f5ec 100644 --- a/src/hls/Sat.v +++ b/src/hls/Sat.v @@ -202,9 +202,9 @@ Local Hint Resolve satLit_contra : core. obligations that it can't solve, or obligations that it takes 42 years to solve. However, if you think enough like me, each of the four definitions you fill in - should read like: [[ + should read like: refine some_expression_with_holes; clear function_name; magic_solver. -]] leaving out the [clear] invocation for non-recursive function definitions. + leaving out the [clear] invocation for non-recursive function definitions. *) Ltac magic_solver := simpl; intros; subst; intuition eauto; firstorder; match goal with |