CN: Do translation validation of resource inference steps in Rocq [work in progress]

.github/workflows/ci-cn-coq.yml

@@ -6,8 +6,7 @@ on:
   push:
     branches:
       - master
-      - cn-logging
-      - cn-resource-logging
+      - resource-reasoning
 
 env:
   CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release
@@ -78,4 +77,4 @@ jobs:
       run: |
         opam switch ${{ matrix.version }}-with-coq
         eval $(opam env --switch=${{ matrix.version }}-with-coq )
-        ./tests/run-cn-coq.sh -p -v
+        ./tests/run-cn-coq.sh -v -p

Makefile

@@ -324,13 +324,13 @@ cn-coq-install: cn-coq
 	$(Q)dune install cn-coq
 
 .PHONY: cn-with-coq
-cn-with-coq:
+cn-with-coq: prelude-src
 	@echo "[DUNE] cerberus-lib,cn,cn-coq"
 	$(Q)dune build -p cerberus-lib,cn,cn-coq
 
 # Developement target to watch for changes in cn/lib and rebuild
 # e.g. to be used with vscode IDE
 .PHONY: cn-dev-watch
-cn-dev-watch:
+cn-dev-watch: prelude-src
 	@echo "[DUNE] cn-dev-watch"
 	$(Q)dune build --watch -p cerberus-lib,cn,cn-coq

_CoqProject

@@ -4,6 +4,7 @@
 # CN:
 -R _build/default/backend/cn/coq/Cerberus/ Cerberus
 -R _build/default/backend/cn/coq/Cn/ Cn
+-R _build/default/backend/cn/coq/Reasoning/ Reasoning
 # CHERI memory model
 -R _build/default/coq/Common/ Common
 -R _build/default/coq/Morello/ Morello

backend/cn/bin/main.ml

@@ -126,7 +126,9 @@ let with_well_formedness_check
   ~incl_dirs
   ~incl_files
   ~coq_export_file
+  ~coq_mucore
   ~coq_proof_log
+  ~coq_check_proof_log
   ~csv_times
   ~log_times
   ~astprints
@@ -174,14 +176,21 @@ let with_well_formedness_check
       in
       Result.iter_error handle_error (Typing.pause_to_result paused);
       let@ _ = f ~cabs_tunit ~prog5 ~ail_prog ~statement_locs ~paused in
-      let steps = Prooflog.get_proof_log () in
       Option.iter
         (fun path ->
-          Pp.print_file
-            path
-            (Pp_mucore_coq.pp_unit_file_with_resource_inference
-               prog5
-               (if coq_proof_log then Some steps else None)))
+          let prologue = Pp_mucore_coq.pp_prologue () in
+          let mucore =
+            if coq_mucore then Pp_mucore_coq.pp_unit_file prog5 else PPrint.empty
+          in
+          let proof =
+            if coq_proof_log then (
+              let steps = Prooflog.get_proof_log () in
+              Pp_mucore_coq.pp_proof_log steps coq_check_proof_log)
+            else
+              PPrint.empty
+          in
+          let doc = PPrint.( ^^ ) prologue (PPrint.( ^^ ) mucore proof) in
+          Pp.print_file path doc)
         coq_export_file;
       return ()
     in
@@ -259,7 +268,9 @@ let well_formed
     ~incl_dirs
     ~incl_files
     ~coq_export_file:None
+    ~coq_mucore:false
     ~coq_proof_log:false
+    ~coq_check_proof_log:false
     ~csv_times
     ~log_times
     ~astprints
@@ -286,7 +297,9 @@ let verify
   diag
   lemmata
   coq_export_file
+  coq_mucore
   coq_proof_log
+  coq_check_proof_log
   only
   skip
   csv_times
@@ -337,7 +350,9 @@ let verify
     ~incl_dirs
     ~incl_files
     ~coq_export_file
+    ~coq_mucore
     ~coq_proof_log
+    ~coq_check_proof_log
     ~csv_times
     ~log_times
     ~astprints
@@ -431,7 +446,9 @@ let generate_executable_specs
     ~incl_dirs
     ~incl_files
     ~coq_export_file:None
+    ~coq_mucore:false
     ~coq_proof_log:false
+    ~coq_check_proof_log:false
     ~csv_times
     ~log_times
     ~astprints
@@ -496,7 +513,9 @@ let run_seq_tests
     ~incl_files
     ~csv_times
     ~coq_export_file:None
+    ~coq_mucore:false
     ~coq_proof_log:false
+    ~coq_check_proof_log:false
     ~log_times
     ~astprints
     ~no_inherit_loc
@@ -610,7 +629,9 @@ let run_tests
     ~incl_files
     ~csv_times
     ~coq_export_file:None
+    ~coq_mucore:false
     ~coq_proof_log:false
+    ~coq_check_proof_log:false
     ~log_times
     ~astprints
     ~no_inherit_loc
@@ -944,14 +965,26 @@ end
 
 module CoqExport_flags = struct
   let coq_export =
-    let doc = "export to coq" in
+    let doc = "File to export to coq defintions" in
     Arg.(value & opt (some string) None & info [ "coq-export-file" ] ~docv:"FILE" ~doc)
 end
 
+module CoqMucore_flags = struct
+  let coq_mucore =
+    let doc = "include mu-core AST in coq export" in
+    Arg.(value & flag & info [ "coq-mucore" ] ~doc)
+end
+
 module CoqProofLog_flags = struct
   let coq_proof_log =
     let doc = "include proof log in coq export" in
-    Arg.(value & flag & info [ "coq-proof-log" ] ~docv:"FILE" ~doc)
+    Arg.(value & flag & info [ "coq-proof-log" ] ~doc)
+end
+
+module CoqCheckProofLog_flags = struct
+  let coq_check_proof_log =
+    let doc = "Include statements to check proof log in coq exported file" in
+    Arg.(value & flag & info [ "coq-check-proof-log" ] ~doc)
 end
 
 let wf_cmd =
@@ -1002,7 +1035,9 @@ let verify_t : unit Term.t =
   $ Verify_flags.diag
   $ Lemma_flags.lemmata
   $ CoqExport_flags.coq_export
+  $ CoqMucore_flags.coq_mucore
   $ CoqProofLog_flags.coq_proof_log
+  $ CoqCheckProofLog_flags.coq_check_proof_log
   $ Verify_flags.only
   $ Verify_flags.skip
   $ Common_flags.csv_times

backend/cn/coq/Cerberus/Utils.v

@@ -52,3 +52,9 @@ Qed.
  *)
 Definition split_at {A:Type} (n:nat) (l:list A)
   := (List.firstn n l, List.skipn n l).
+
+Definition option_map {A B:Type} (f: A -> B) (o: option A) : option B :=
+  match o with
+  | Some x => Some (f x)
+  | None => None
+  end.