Theory Munta_Certificate_Compile_Poly

section ‹Build and Test Exported Program With Poly/ML›
text_raw ‹\label{build-poly}›

theory Munta_Certificate_Compile_Poly
  imports Simple_Network_Language_Certificate_Code Munta_Certificate_Testing
begin

paragraph ‹Mock Compilation›

text ‹
Instead of using Poly/ML's ‹polyc›, we emulate compilation within Isabelle's Poly/ML environment.
Below we also show how ‹polyc› could be used alternatively.

We prepare a few pieces of code that will be passed to Poly/ML for mocking compilation.
This will be used for evaluating the code:›
ML ‹
― ‹from ‹HOL/Library/code_test.ML››
val flags = {environment = ML_Env.SML, redirect = false, verbose = false, catch_all = true,
          debug = NONE, writeln = writeln, warning = warning}
fun eval cmd = ML_Context.eval flags Position.none (ML_Lex.read_text (cmd, Position.none))
›

― ‹Redirecting output to file:›
ML ‹
val mock_print = ▩‹
val out_stream_ref = ref (NONE : BinIO.outstream option);
fun print s =
  BinIO.output (Option.valOf (!out_stream_ref), Byte.stringToBytes s)
›
›

― ‹Mocking command line arguments:›
ML ‹
val mock_cmd = ▩‹
structure CommandLine =
struct

val mock_args = ref [""]
fun arguments () = !mock_args
fun set_mock_args s =
  mock_args := String.tokens (fn c => c = #" ") s;

end
›
›

― ‹Set command line arguments, run ‹main›, and capture output›
ML ‹
fun run_cmd dir args =
  let
    val out_path = dir + Path.basic "out" |> Path.expand |> Path.implode
  in ▩‹
CommandLine.set_mock_args "› ^ args ^ ▩‹";
val out_stream = BinIO.openOut "› ^ out_path ^ ▩‹";
val _ = out_stream_ref := SOME out_stream;
main ();
BinIO.flushOut out_stream;
BinIO.closeOut out_stream
› end
›

― ‹This is essentially the content of ‹build_muntac.sml›:›
ML ‹
val files = [
  "Unsynchronized.sml",
  "Writeln.sml",
  "basics.ML",
  "library.ML",
  "parallel_task_queue.sml"
]
val mlunta_files = [
  "prelude.sml",
  "serializable.sml",
  "certificate.sml"
]
val final_files = [
  "Util.sml",
  "Muntac.sml"
]
›

― ‹Mock compiling›
ML ‹
fun mock_compile dir file_name =
  let
    val _ = eval mock_cmd
    val _ = eval mock_print
    fun mk_path file_name = Path.append dir (Path.explode file_name)
    fun mk_mlunta_path file_name =
      dir + Path.explode mlunta_certificate_path + Path.basic file_name |> Path.expand
    val _ = app (fn x => mk_path x |> ML_Context.eval_file flags) files
    val _ = ML_Context.eval_file flags (dir + Path.basic file_name)
    val _ = app (fn x => mk_mlunta_path x |> ML_Context.eval_file flags) mlunta_files
    val _ = app (fn x => mk_path x |> ML_Context.eval_file flags) final_files
  in () end
›

― ‹Also need to mock ‹check_cert›: simply pass the captured output to ‹check_benchmark.sh››
ML ‹
fun mock_exec_check_cert dir title muntac_path name =
  let
    fun check () =
      Generated_Files.execute dir title ▩‹./check_benchmark.sh cat out›
    fun mk_path name ext = dir + Path.basic name |> Path.ext ext |> Path.expand |> Path.implode
    val args = implode_space [
      muntac_path,
      "-certificate", mk_path name "cert",
      "-renaming", mk_path name "renaming",
      "-model", mk_path name "muntax"
    ]
    val cmd = run_cmd dir args
    val _ = eval cmd
  in
    check ()
  end
›


paragraph ‹Compilation and Testing›

text ‹Here is how to compile Munta Certifier with Poly/ML and then run some benchmarks:›

compile_generated_files "code/Certificate.ML" (in Simple_Network_Language_Certificate_Code)
  external_files
    ‹Writeln.sml›
    ‹Util.sml›
    ‹Muntac.sml›
    ‹Mlton_Main.sml›
    ‹Unsynchronized.sml›
    ‹sequential.sml›
    ‹parallel_task_queue.sml›
    ‹build_muntac.sml›
    ‹check_benchmark.sh›
    (in "ML")
  and
    ‹HDDI_02.muntax›
    ‹HDDI_02_broadcast.muntax›
    ‹HDDI_08_broadcast.muntax›
    ‹PM_all_1.muntax›
    ‹PM_all_2.muntax›
    ‹PM_all_3.muntax›
    ‹PM_all_4.muntax›
    ‹PM_all_5.muntax›
    ‹PM_all_6.muntax›
    ‹PM_all_urgent.muntax›
    ‹bridge.muntax›
    ‹csma_05.muntax›
    ‹csma_06.muntax›
    ‹fischer.muntax›
    ‹fischer_05.muntax›
    ‹hddi_08.muntax›
    ‹light_switch.muntax› (in "benchmarks")
  export_files ‹muntac_poly› (exe)
  where ‹fn dir =>
    let
      val mock = true ― ‹whether to eval in Poly/ML instead of using ‹polyc››

      val exec = Generated_Files.execute dir

      val _ = exec ‹Copy MLunta› ("cp -r '" ^  Path.implode mlunta_dir ^ "' .")
      val _ = exec ‹Compile MLunta› "cd mlunta && mlton=$ISABELLE_MLTON make build_checker && cd .."
      val mlunta_path = "mlunta/build/mluntac-mlton"

      val _ =
        exec ‹Copy Isabelle library files›
          ("cp '" ^ library_path ^ "' library.ML && cp '" ^ basics_path ^ "' basics.ML")

      val _ =
        exec ‹Preparation›
          "mv code/Certificate.ML Certificate.ML"
      val _ =
        exec ‹Replace int type›
          "sed -i -e 's/IntInf/Int/g' Certificate.ML"
      val _ =
        exec ‹set›
          "set -x"
      val _ =
        if mock then
          (mock_compile dir "Certificate.ML";
           exec ‹Compilation› "touch muntac_poly")
        else
          exec ‹Compilation›
            ("MLUNTA_CERT=" ^ mlunta_certificate_path ^ " " ^
             ▩‹$ML_HOME› ^
             "/polyc -o muntac_poly build_muntac.sml")

      val muntac_path = if mock then "" else "./muntac_poly"
      val muntac_path_n6 = muntac_path ^ " -n 6" ― ‹Parallel checking for larger certificates›
      val muntac_path_dc = muntac_path ^ " -dc" ― ‹For deadlock checking›

      val _ = writeln "Generating certificates."

      val _ = exec ‹Gen HDDI_02› (mk_cert mlunta_path "HDDI_02")
      val _ = exec ‹Gen HDDI_02_broadcast› (mk_cert mlunta_path "HDDI_02_broadcast")
      val _ = exec ‹Gen HDDI_08_broadcast› (mk_cert mlunta_path "HDDI_08_broadcast")
      val _ = exec ‹Gen hddi_08› (mk_cert mlunta_path "hddi_08")
      val _ = exec ‹Gen PM_all_1› (mk_cert mlunta_path "PM_all_1")
      val _ = exec ‹Gen PM_all_2› (mk_cert mlunta_path "PM_all_2")
      val _ = exec ‹Gen PM_all_3› (mk_cert mlunta_path "PM_all_3")
      val _ = exec ‹Gen PM_all_4› (mk_cert mlunta_path "PM_all_4")
      val _ = exec ‹Gen PM_all_5› (mk_cert mlunta_path "PM_all_5")
      val _ = exec ‹Gen csma_05› (mk_cert mlunta_path "csma_05")
      val _ = exec ‹Gen csma_06› (mk_cert mlunta_path "csma_06")
      val _ = exec ‹Gen fischer_05› (mk_cert mlunta_path "fischer_05")

      val _ = writeln "Finished generating certificates. Now checking.";

      fun exec_check_cert title muntac_path name =
        if mock then
          mock_exec_check_cert dir title muntac_path name
        else
          exec title (check_cert muntac_path name)

      val _ = exec_check_cert ‹Test HDDI_02› muntac_path "HDDI_02"
      val _ = exec_check_cert ‹Test HDDI_02_broadcast› muntac_path "HDDI_02_broadcast"
      val _ = exec_check_cert ‹Test HDDI_08_broadcast› muntac_path "HDDI_08_broadcast"
      val _ = exec_check_cert ‹Test PM_all_1› muntac_path "PM_all_1"
      val _ = exec_check_cert ‹Test PM_all_2› muntac_path "PM_all_2"
      val _ = exec_check_cert ‹Test PM_all_3› muntac_path "PM_all_3"
      val _ = exec_check_cert ‹Test csma_05› muntac_path_n6 "csma_05"
      ― ‹30 s on an M1 Mac›
      ⌦‹val _ = exec_check_cert ‹Test csma_06› muntac_path_n6 "csma_06"›
      val _ = exec_check_cert ‹Test fischer_05› muntac_path_n6 "fischer_05"
      val _ = exec_check_cert ‹Test hddi_08› muntac_path "hddi_08"
      val _ = exec_check_cert ‹Test PM_all_4› muntac_path "PM_all_4"
      ― ‹60 s on an M1 Mac›
      ⌦‹val _ = exec_check_cert ‹Test PM_all_5› muntac_path_n6 "PM_all_5"›

      val _ = exec_check_cert ‹Test deadlock HDDI_02› muntac_path_dc "HDDI_02"
    in () end›

end