diff --git a/.github/workflows/build-and-profile.yml b/.github/workflows/build-and-profile.yml index f06747f9..d2e651d8 100644 --- a/.github/workflows/build-and-profile.yml +++ b/.github/workflows/build-and-profile.yml @@ -45,12 +45,12 @@ jobs: - name: 'Run hybrid benchmarks' run: nix develop -L '.#bench-hybrid' --command ./bench-hybrid/test.sh + - name: 'Build Coq language examples' + run: nix build -L '.#languages-in-coq' + - name: 'Run Coq benchmarks' run: nix develop -L '.#bench-coq' --command ./bench-coq/build-and-profile.sh - - name: 'Build old Coq examples' - run: nix build -L '.#old-examples-coq' - - name: 'Build Docker image' run: nix build -L '.#minuska-docker' --out-link ./result-minuska-docker diff --git a/README.md b/README.md index 75415022..a421e58a 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ Minuska is a framework for defining operational semantics ("language definitions") of programming languages and deriving tools from them. Currently, the project is a research prototype, and the only tools derivable from language definitions are interpreters. Users looking for a mature programming language framework are advised to check out [K framework](https://kframework.org/) or [PLT-Redex](https://redex.racket-lang.org/). -(For a more detailed comparison to K framework, look [here](./doc/comparison-to-k-framework.md)) +(For a more detailed comparison to K framework, look [here](./doc/comparison-to-k-framework.md).) Minuska is built on top of the [Coq proof assistant](https://coq.inria.fr/). At its core is a simple language MinusLang for expressing programming language semantics in an exact, unambiguous way: MinusLang has a simple formal semantics (mechanized in [spec.v](https://h0nzzik.github.io/minuska/Minuska.spec.html)), @@ -52,9 +52,11 @@ In principle, many features could be implemented in Minuska that would make the These include support for concrete syntax of programming languages, formalization of the strictness declarations, symbolic execution, and deductive verification. See the [ideas document](./doc/ideas.md) - - # Troubleshooting -If your system does not support FUSE, or its configuration is broken, try `export APPIMAGE_EXTRACT_AND_RUN=1` before running any generated interpreters. +If your system does not support FUSE, or its configuration is broken, try `export APPIMAGE_EXTRACT_AND_RUN=1` before running any generated interpreters. +This needs to be done e.g., in Docker, or when running on Github-hosted runners. + +# Papers +An extended version of the preliminary 'Minuska: Towards a Formally Verified Programming Language Framework' paper is available [here](h0nzzik.github.io/papers/minuska-extended.pdf). diff --git a/bench-coq/README.md b/bench-coq/README.md new file mode 100644 index 00000000..25820aac --- /dev/null +++ b/bench-coq/README.md @@ -0,0 +1,83 @@ +# Benchmarks for languages specified directly in Coq + +To get some statistics about the languages defined in [../languages-in-coq](../languages-in-coq), run: +```sh +nix develop '.#bench-coq' --command ./build-and-profile.sh +``` +The first column is the name of the benchmark, second column is the time of the `Compute` inside Coq (measured by Coq's `Time` command), and the third columns is the total time of `coqc` as measured by the GNU `time` utility. + +The last two columns of Figure 3 of [this paper](h0nzzik.github.io/papers/minuska-extended.pdf) can be obtained by filtering the output of the above command. +For an illustrative example, a recent run on my "Intel(R) Core(TM) i7-10510U CPU @ 1.80GHz" laptop yield, among other, the following rows: +``` +two-counters(10), 0.015, 0.73 +two-counters(20), 0.01, 0.74 +two-counters(50), 0.014, 0.73 +two-counters(100), 0.008, 0.78 +unary-fib(5), 0.133, 0.81 +unary-fact(3), 0.285, 0.98 +``` + +Similarly, the right table of Figure 2 of that paper corresponds to the following part of the output: +``` +two-counters(10), 0.015, 0.73 +two-counters(100), 0.008, 0.78 +two-counters(1000), 0.011, 0.75 +two-counters(10000), 0.026, 0.74 +``` + +The middle two columns of Figure 4 of that paper are covered as well: +``` +imp-count-to(1), 0.642, 1.43 +imp-count-to(2), 1.078, 1.79 +imp-count-to(3), 1.453, 2.15 +imp-count-to(4), 1.911, 2.63 +imp-count-to(5), 2.322, 3.00 +imp-count-to(6), 2.569, 3.25 +imp-count-to(7), 3.004, 3.70 +``` +(For the last column of that figure, see [../bench-standalone](../bench-standalone)). + +Figure 5 of that paper is also contained in the output: +``` +native-fib(1), 0.01, 0.75 +native-fib(6), 0.015, 0.73 +native-fib(11), 0.017, 0.73 +native-fib(16), 0.021, 0.73 +native-fib(21), 0.034, 0.74 +native-fib(26), 0.038, 0.84 +native-fib(31), 0.039, 0.89 +native-fib(36), 0.038, 0.77 +native-fib(41), 0.041, 0.74 +native-fib(46), 0.044, 0.76 +native-fib(51), 0.05, 0.76 +native-fib(56), 0.047, 0.76 +native-fib(61), 0.06, 0.79 +native-fib(66), 0.059, 0.75 +native-fib(71), 0.058, 0.74 +native-fib(76), 0.072, 0.80 +native-fib(81), 0.071, 0.79 +native-fib(86), 0.102, 0.79 +native-fib(91), 0.105, 0.80 +native-fib(96), 0.095, 0.79 +native-fib(101), 0.107, 0.79 +native-fib(106), 0.115, 0.80 + +unary-fib(1), 0.074, 0.77 +unary-fib(2), 0.079, 0.78 +unary-fib(3), 0.093, 0.77 +unary-fib(4), 0.103, 0.78 +unary-fib(5), 0.137, 0.82 +unary-fib(6), 0.2, 0.90 +unary-fib(7), 0.311, 1.00 +unary-fib(8), 0.459, 1.20 +unary-fib(9), 0.882, 1.59 +unary-fib(10), 1.42, 2.12 +unary-fib(11), 2.471, 3.15 + +unary-fact(1), 0.108, 0.78 +unary-fact(2), 0.167, 0.85 +unary-fact(3), 0.285, 0.96 +unary-fact(4), 0.575, 1.35 +unary-fact(5), 2.102, 2.78 +unary-fact(6), 10.318, 10.97 +``` diff --git a/bench-hybrid/README.md b/bench-hybrid/README.md new file mode 100644 index 00000000..c5ef4bda --- /dev/null +++ b/bench-hybrid/README.md @@ -0,0 +1,18 @@ +## Hybrid Coq/`minuska` benchmarks + +To get some statistics about the languages defined in [../languages-in-coq](../languages-in-coq) converted into Coq and executed inside Coq, run: +```sh +nix develop '.#bench-hybrid' --command ./test.sh +``` +The output contains lines like +``` +coqc testCount7.v +Finished transaction in 1.814 secs (1.806u,0.002s) (successful) +2.45 +coqc testTC100.v +Finished transaction in 0.094 secs (0.093u,0.s) (successful) +0.68 +``` +where each three lines correspond to one benchmark: the first one the three contains the name of the benchmark, the second line the time required for Coq to execute the corresponding `Compute` command, and the third line is the execution time as measured by the GNU `time` utility. +This suite contains only two kind of benchmarks. The ones named `testCount${N}` run the `sum-to-${N}` program in the IMP language defined in [../languages/imp](../languages/imp), but do so inside Coq. The ones named `testTC${N}` run the `two-counters` language ([../languages/two-counters](../languages/two-counters)) on input `${N}`. + diff --git a/flake.nix b/flake.nix index 99c16f8f..0910f384 100644 --- a/flake.nix +++ b/flake.nix @@ -101,12 +101,12 @@ in { packages.minuska = minuskaFun { coqPackages = pkgs.coqPackages_8_19; } ; - packages.old-examples-coq + packages.languages-in-coq = pkgs.coqPackages_8_19.callPackage ( { coq, stdenv }: stdenv.mkDerivation { - name = "old-examples-coq"; - src = ./old-examples-coq; + name = "languages-in-coq"; + src = ./languages-in-coq; propagatedBuildInputs = [ self.outputs.packages.${system}.minuska @@ -163,7 +163,7 @@ propagatedBuildInputs = [ pkgs.time pkgs.python312 - self.outputs.packages.${system}.old-examples-coq + self.outputs.packages.${system}.languages-in-coq #self.outputs.packages.${system}.examples-coq.coqPackages.coq ]; enableParallelBuilding = true; diff --git a/old-examples-coq/Makefile b/languages-in-coq/Makefile similarity index 100% rename from old-examples-coq/Makefile rename to languages-in-coq/Makefile diff --git a/languages-in-coq/README.md b/languages-in-coq/README.md new file mode 100644 index 00000000..c7cfc41f --- /dev/null +++ b/languages-in-coq/README.md @@ -0,0 +1,13 @@ +## Language examples in Coq + +This directory contains a few language definitions encoded directly in Coq, as well as derived interpreters for those languages. Specifically: +- `examples.two_counters.interp` in [theories/examples.v](theories/examples.v) is an interpreter for the "two counters" language over unary-encoded natural numbers; +- `examples.two_counters_Z.interp` is the same but over built-in integers (that is, the `Z` type from Coq's standard library); +- `examples.arith.interp` is an interpreter for a simple language of arithmetic expressions; +- `examples.fib_native.interp` calculates a Fibonacci sequence (over built-in integers), in an imperative style +- `examples.imp.interp` interpretes a simple imperative language with arithmetic expressions, assignment, conditions, and loops; +- `examples_unary_nat.unary_nat.interp_fib` implements Fibonacci sequence in the same style, but over unary-encoded natural numbers; +- `examples_unary_nat.unary_nat.interp_fact` implements factorial in the imperative style, over unary-encoded natural numbers. + +No performance benchmarks for these are provided in this directory, but see [../bench-coq](../bench-coq) which uses this directory as a dependency. + diff --git a/old-examples-coq/_CoqProject b/languages-in-coq/_CoqProject similarity index 78% rename from old-examples-coq/_CoqProject rename to languages-in-coq/_CoqProject index 5a56ab4e..7dfaf5d6 100644 --- a/old-examples-coq/_CoqProject +++ b/languages-in-coq/_CoqProject @@ -1,7 +1,6 @@ -R theories MinuskaExamples theories/examples.v -theories/extraction.v theories/examples_unary_nat.v diff --git a/old-examples-coq/theories/dep.v b/languages-in-coq/theories/dep.v similarity index 100% rename from old-examples-coq/theories/dep.v rename to languages-in-coq/theories/dep.v diff --git a/old-examples-coq/theories/examples.v b/languages-in-coq/theories/examples.v similarity index 100% rename from old-examples-coq/theories/examples.v rename to languages-in-coq/theories/examples.v diff --git a/old-examples-coq/theories/examples_unary_nat.v b/languages-in-coq/theories/examples_unary_nat.v similarity index 100% rename from old-examples-coq/theories/examples_unary_nat.v rename to languages-in-coq/theories/examples_unary_nat.v diff --git a/old-examples-coq/src/example_lang_driver.ml b/old-examples-coq/src/example_lang_driver.ml deleted file mode 100644 index 112cd087..00000000 --- a/old-examples-coq/src/example_lang_driver.ml +++ /dev/null @@ -1,28 +0,0 @@ -open ExampleLang - -let usage_msg = "example_langdriver " - -let depth = ref 10 - -let number = ref 0 - - -let anon_fun mynum = - number := int_of_string mynum - -let speclist = - [ - ("-depth", Arg.Set_int depth, "Maximal execution depth") - ] - -let () = - Arg.parse speclist anon_fun usage_msg; - (* Main functionality here *) - print_string "Hello world!\n"; - print_string (string_of_int !number); - print_string (string_of_int !depth); - let result = ExampleLang.Coq_example_1.interp_loop_number !depth !number in - match result with - | None -> print_string "None" - | Some x -> print_string "Some"; print_string (string_of_int x) - \ No newline at end of file diff --git a/old-examples-coq/src/fib_native_driver.ml b/old-examples-coq/src/fib_native_driver.ml deleted file mode 100644 index 476f7650..00000000 --- a/old-examples-coq/src/fib_native_driver.ml +++ /dev/null @@ -1,36 +0,0 @@ -open Format -open FibNative -open Printexc - -module B = Big_int_Z - -let usage_msg = "fib_native_driver [-depth ] -n " - -let depth = ref 10000 -let n = ref 0 -let do_log = ref 0 - -let anon_fun mynum = () - -let speclist = - [ - ("-depth", Arg.Set_int depth, "Maximal execution depth"); - ("-log", Arg.Set_int do_log, "Print log?"); - ("-n", Arg.Set_int n, "N-th number to compute") - ] - -let main () = - Arg.parse speclist anon_fun usage_msg; - printf "Running for %d steps.\n" !depth; - let res = FibNative.Coq_fib_native.fib_interp_from_toint !depth (B.big_int_of_int !n) in - let fib_n = snd (fst res) in - printf "fib(%d) = %d\n" !n (B.int_of_big_int fib_n); - printf "Remaining fuel: %d\n" (fst (fst res)); - let log = String.of_seq (List.to_seq (snd res)) in - if !do_log > 0 then (printf "Log: %s.\n" log; ()) else (); - () - -let () = - Printexc.record_backtrace true; - try main() with Stack_overflow -> (printf "Stack overflow.\n%s" (Printexc.get_backtrace ()));; - diff --git a/old-examples-coq/src/generic_driver.ml b/old-examples-coq/src/generic_driver.ml deleted file mode 100644 index 694fb7f0..00000000 --- a/old-examples-coq/src/generic_driver.ml +++ /dev/null @@ -1,19 +0,0 @@ -open Format - -let usage_msg = "generic_driver [-depth ]" - -let depth = ref 10000 - -let anon_fun mynum = () - -let speclist = - [ - ("-depth", Arg.Set_int depth, "Maximal execution depth") - ] - -let () = - Arg.parse speclist anon_fun usage_msg; - printf "Running for %d steps.\n" !depth; - let res = result !depth in - printf "Remaining fuel: %d\n" (snd res) - diff --git a/old-examples-coq/src/imp.ml b/old-examples-coq/src/imp.ml deleted file mode 100644 index bfb35017..00000000 --- a/old-examples-coq/src/imp.ml +++ /dev/null @@ -1,36 +0,0 @@ -type token = - | TRUE - | FALSE - | ID of string - | INT of int - | LEFT_CURLY_BRACK - | RIGHT_CURLY_BRACK - | LEFT_ROUND_BRACK - | RIGHT_ROUND_BRACK - | COMMA - | COLONEQ - | EOF - -type id = - [ `Id of string - ] - -type aexpr = - [ `IntConstant of int - | `IntVariable of id - | `IntPlus of (aexpr * aexpr) - ] - -type bexpr = - [ `BoolConstant of bool - | `BoolAnd of (bexpr * bexpr) - | `BoolNot of bexpr - | `Leq of (aexpr * aexpr) - ] - -type stmt = - [ `AssignStmt of (string * expr) - | `AExprStmt of aexpr - | `SeqStmt of (stmt * stmt) - | `WhileStmt of (bexpr * stmt) - ] diff --git a/old-examples-coq/src/imp_lexer.mll b/old-examples-coq/src/imp_lexer.mll deleted file mode 100644 index 93bab953..00000000 --- a/old-examples-coq/src/imp_lexer.mll +++ /dev/null @@ -1,38 +0,0 @@ -{ -open Lexing -open Parser - -exception SyntaxError of string -} - -let int = '-'? ['0'-'9'] ['0'-'9']* - -let digit = ['0'-'9'] -let frac = '.' digit* -let exp = ['e' 'E'] ['-' '+']? digit+ -let float = digit* frac? exp? - -let white = [' ' '\t']+ -let newline = '\r' | '\n' | "\r\n" -let id = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_']* - - -rule read = - parse - | white { read lexbuf } - | newline { next_line lexbuf; read lexbuf } - | int { INT (int_of_string (Lexing.lexeme lexbuf)) } - | "true" { TRUE } - | "false" { FALSE } - | "and" { AND } - | "not" { NOT } - | ":=" { COLONEQ } - | '"' { read_string (Buffer.create 17) lexbuf } - | '{' { LEFT_CURLY_BRACK } - | '}' { RIGHT_CURLY_BRACK } - | '(' { LEFT_ROUND_BRACK } - | ')' { RIGHT_ROUND_BRACK } - | ':' { COLON } - | ',' { COMMA } - | _ { raise (SyntaxError ("Unexpected char: " ^ Lexing.lexeme lexbuf)) } - | eof { EOF } diff --git a/old-examples-coq/src/imp_parser.mly b/old-examples-coq/src/imp_parser.mly deleted file mode 100644 index 8dd92ded..00000000 --- a/old-examples-coq/src/imp_parser.mly +++ /dev/null @@ -1,68 +0,0 @@ -%token INT -%token ID -%token TRUE -%token FALSE -%token AND -%token NOT -%token LEFT_CURLY_BRACK -%token RIGHT_CURLY_BRACK -%token LEFT_ROUND_BRACK -%token RIGHT_ROUND_BRACK -%token WHILE -%token PLUS -%token SEMICOLON -%token COLONEQ -%token IF -%token LEQ -%token EOF - - -%start main - -%type aexpr -%type bexpr -%type stmt -%% - - -aexpr: - | n = INT { Some (IntConstant n) } - | x = ID { Some (IntVariable x) } - | e1 = aexpr; - PLUS; - e2 = aexpr { Some (IntPlus e1 e2) } - ; - -bexpr: - | TRUE { Some (BoolConstant true) } - | FALSE { Some (BoolConstant false) } - | e1 = bexpr; - AND; - e2 = bexpr { Some (BoolAnd e1 e2) } - | NOT; - e = bexpr { Some (BoolNot e) } - | e1 = aexpr; - LEQ; - e2 = aexpr { Some (Leq e1 e2) } - ; - -stmt: - | EOF { None } - | e = aexpr { Some e } - | x = ID; - COLONEQ; - e = aexpr { Some (AssignStmt x e) } - | WHILE; - LEFT_ROUND_BRACK; - b = bexpr; - RIGHT_ROUND_BRACK; - LEFT_CURLY_BRACK; - s = stmt; - RIGHT_CURLY_BRACK; - SEMICOLON { Some (WhileStmt b s) } - | s1 = stmt; s2 = stmt { Some (SeqStmt s1 s2) } - ; - -main: - | s = stmt; EOF { s } - ; diff --git a/old-examples-coq/src/sum_to_n_driver.ml b/old-examples-coq/src/sum_to_n_driver.ml deleted file mode 100644 index 264f8fc7..00000000 --- a/old-examples-coq/src/sum_to_n_driver.ml +++ /dev/null @@ -1,36 +0,0 @@ -open Format -open SumToN -open Printexc - -module B = Big_int_Z - -let usage_msg = "fib_native_driver [-depth ] -n " - -let depth = ref 10000 -let n = ref 0 -let do_log = ref 0 - -let anon_fun mynum = () - -let speclist = - [ - ("-depth", Arg.Set_int depth, "Maximal execution depth"); - ("-log", Arg.Set_int do_log, "Print log?"); - ("-n", Arg.Set_int n, "N-th number to compute") - ] - -let main () = - Arg.parse speclist anon_fun usage_msg; - printf "Running for %d steps.\n" !depth; - let res = SumToN.Coq_imp.interp_program_count_to !depth (B.big_int_of_int !n) in - let sum_n = snd (fst res) in - printf "sum_to_n(%d) = %d\n" !n (B.int_of_big_int sum_n); - printf "Remaining fuel: %d\n" (fst (fst res)); - let log = String.of_seq (List.to_seq (snd res)) in - if !do_log > 0 then (printf "Log: %s.\n" log; ()) else (); - () - -let () = - Printexc.record_backtrace true; - try main() with Stack_overflow -> (printf "Stack overflow.\n%s" (Printexc.get_backtrace ()));; - diff --git a/old-examples-coq/src/two_counters_driver.ml b/old-examples-coq/src/two_counters_driver.ml deleted file mode 100644 index a0e97879..00000000 --- a/old-examples-coq/src/two_counters_driver.ml +++ /dev/null @@ -1,29 +0,0 @@ -open Format -open TwoCounters - -let usage_msg = "two_counters_driver -m -n [-depth ]" - -let depth = ref 10 - -let number1 = ref 10 -let number2 = ref 0 - - -let anon_fun mynum = () - -let speclist = - [ - ("-depth", Arg.Set_int depth, "Maximal execution depth"); - ("-m", Arg.Set_int number1, "number1"); - ("-n", Arg.Set_int number2, "number2") - ] - -let () = - Arg.parse speclist anon_fun usage_msg; - printf "Running from (%d,%d) for %d steps.\n" !number1 !number2 !depth; - let result = TwoCounters.Coq_two_counters.interp_loop_number !depth !number1 !number2 in - match result with - | None -> print_string "None" - | Some x -> - printf "Some (%d,%d)\n" (fst x) (snd x) - diff --git a/old-examples-coq/theories/extraction.v b/old-examples-coq/theories/extraction.v deleted file mode 100644 index 16202ee8..00000000 --- a/old-examples-coq/theories/extraction.v +++ /dev/null @@ -1,47 +0,0 @@ -Require Extraction. -Extraction Language OCaml. -Require Import - Coq.extraction.ExtrOcamlString - Coq.extraction.ExtrOcamlZBigInt -. -From Coq Require Import Bool Arith ZArith List. - -From Minuska Require Import example. -From MinuskaExamples Require Import examples. - - -Extract Inductive nat => "int" - [ "0" "(fun x -> x + 1)" ] - "(fun zero succ n -> if n=0 then zero () else succ (n-1))" -. - - -Extraction - "ExampleLang.ml" - example_1.interp_loop_number -. - - -Extraction - "TwoCounters.ml" - two_counters.interp_loop_number -. - -Extraction - "FibNative.ml" - fib_native.fib_interp_from_toint -. - -Extraction - "SumToN.ml" - imp.interp_program_count_to -. - -Extraction - "Attempt.ml" - fib_native.interp_from -. - - - -(* Print DependGraph fib_native.interp_from. *) \ No newline at end of file diff --git a/old-examples-coq/trivial.m b/old-examples-coq/trivial.m deleted file mode 100644 index cf46c9bb..00000000 --- a/old-examples-coq/trivial.m +++ /dev/null @@ -1,18 +0,0 @@ -symbols : [s] ; - -value(X): (bool.or(bool.false(), bool.or(bool.false(), term.same_symbol(X, [unitValue[]])))) ; - -strictness: [] ; - -rule [stmt.ite.false]: - ite[B,X,Y] => Y where bool.eq(B, bool.false()) - ; - -rule [while.unfold]: - while[B,X] => ite[B, seq[X, while[B, X]], unitValue[]] - where bool.true() - ; - - - -