From ba61dfd69504ec6263a9dee9931d93adeb6f3142 Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Mon, 7 Jul 2025 21:52:08 +0200 Subject: Initialize repository --- .gitignore | 22 + .ocamlformat | 1 + .ocamlformat-ignore | 1 + COPYING | 564 ++++ Makefile | 55 + README.md | 383 +++ _CoqProject | 31 + axioms.nix | 22 + bin/dune | 14 + bin/main.ml | 26 + bin/repl.ml | 52 + bin/repl_cmd.ml | 178 ++ bin/run.ml | 163 ++ bin/settings.ml | 120 + cloc-rocq.sh | 150 ++ cloc.nix | 16 + coverage.nix | 19 + coverage.sh | 9 + default.nix | 27 + dune-project | 22 + explorer/.gitignore | 2 + explorer/generate.sh | 140 + explorer/tree.sh | 17 + explorer/upload-new.sh | 16 + importdef.sexp | 1 + lib/extraction/dune | 56 + lib/extraction/extraction.ml | 18 + lib/extraction/prelude.v | 52 + lib/mininix/builtins.ml | 77 + lib/mininix/builtins.nix | 302 +++ lib/mininix/conv.ml | 96 + lib/mininix/dune | 15 + lib/mininix/import.ml | 54 + lib/mininix/mininix.ml | 13 + lib/mininix/mininix2nix.ml | 54 + lib/mininix/nix2mininix.ml | 254 ++ lib/mininix/run.ml | 17 + lib/mininix/sexp.ml | 160 ++ lib/nix/dune | 15 + lib/nix/elaborator.ml | 208 ++ lib/nix/lexer.mll | 315 +++ lib/nix/nix.ml | 20 + lib/nix/parser.mly | 310 +++ lib/nix/printer.ml | 176 ++ lib/nix/tokens.ml | 64 + lib/nix/types.ml | 112 + mininix.opam | 39 + mininix.opam.locked | 131 + nixpkgs-pinned.nix | 7 + shell.nix | 21 + test/dune | 7 + test/test_mininix.ml | 319 +++ test/testdata/binary-data | Bin 0 -> 1024 bytes test/testdata/data | 1 + test/testdata/dir1/a.nix | 1 + test/testdata/dir2/a.nix | 1 + test/testdata/dir2/b.nix | 1 + test/testdata/dir3/a.nix | 1 + test/testdata/dir3/b.nix | 1 + test/testdata/dir3/c.nix | 1 + test/testdata/dir4/a.nix | 1 + test/testdata/dir4/c.nix | 1 + test/testdata/eval-fail-abort.err.exp | 8 + test/testdata/eval-fail-abort.nix | 1 + ...-addDrvOutputDependencies-empty-context.err.exp | 8 + ...fail-addDrvOutputDependencies-empty-context.nix | 1 + ...rvOutputDependencies-multi-elem-context.err.exp | 9 + ...addDrvOutputDependencies-multi-elem-context.nix | 18 + ...rvOutputDependencies-wrong-element-kind.err.exp | 9 + ...addDrvOutputDependencies-wrong-element-kind.nix | 9 + .../eval-fail-addErrorContext-example.err.exp | 24 + .../eval-fail-addErrorContext-example.flags | 1 + .../testdata/eval-fail-addErrorContext-example.nix | 9 + .../eval-fail-assert-equal-attrs-names-2.err.exp | 8 + .../eval-fail-assert-equal-attrs-names-2.nix | 2 + .../eval-fail-assert-equal-attrs-names.err.exp | 8 + .../eval-fail-assert-equal-attrs-names.nix | 2 + ...val-fail-assert-equal-derivations-extra.err.exp | 26 + .../eval-fail-assert-equal-derivations-extra.nix | 5 + .../eval-fail-assert-equal-derivations.err.exp | 26 + .../eval-fail-assert-equal-derivations.nix | 5 + .../testdata/eval-fail-assert-equal-floats.err.exp | 22 + test/testdata/eval-fail-assert-equal-floats.nix | 2 + .../eval-fail-assert-equal-function-direct.err.exp | 9 + .../eval-fail-assert-equal-function-direct.nix | 7 + .../eval-fail-assert-equal-int-float.err.exp | 8 + test/testdata/eval-fail-assert-equal-int-float.nix | 2 + test/testdata/eval-fail-assert-equal-ints.err.exp | 22 + test/testdata/eval-fail-assert-equal-ints.nix | 2 + .../eval-fail-assert-equal-list-length.err.exp | 8 + .../eval-fail-assert-equal-list-length.nix | 2 + test/testdata/eval-fail-assert-equal-paths.err.exp | 8 + test/testdata/eval-fail-assert-equal-paths.nix | 2 + .../eval-fail-assert-equal-type-nested.err.exp | 22 + .../eval-fail-assert-equal-type-nested.nix | 2 + test/testdata/eval-fail-assert-equal-type.err.exp | 8 + test/testdata/eval-fail-assert-equal-type.nix | 2 + test/testdata/eval-fail-assert-nested-bool.err.exp | 74 + test/testdata/eval-fail-assert-nested-bool.nix | 6 + test/testdata/eval-fail-assert.err.exp | 30 + test/testdata/eval-fail-assert.nix | 5 + test/testdata/eval-fail-attr-name-type.err.exp | 21 + test/testdata/eval-fail-attr-name-type.nix | 7 + .../eval-fail-bad-string-interpolation-1.err.exp | 8 + .../eval-fail-bad-string-interpolation-1.nix | 1 + .../eval-fail-bad-string-interpolation-2.err.exp | 1 + .../eval-fail-bad-string-interpolation-2.nix | 1 + .../eval-fail-bad-string-interpolation-3.err.exp | 8 + .../eval-fail-bad-string-interpolation-3.nix | 1 + .../eval-fail-bad-string-interpolation-4.err.exp | 9 + .../eval-fail-bad-string-interpolation-4.nix | 9 + test/testdata/eval-fail-blackhole.err.exp | 14 + test/testdata/eval-fail-blackhole.nix | 5 + test/testdata/eval-fail-call-primop.err.exp | 10 + test/testdata/eval-fail-call-primop.nix | 1 + test/testdata/eval-fail-deepseq.err.exp | 20 + test/testdata/eval-fail-deepseq.nix | 1 + test/testdata/eval-fail-derivation-name.err.exp | 26 + test/testdata/eval-fail-derivation-name.nix | 5 + .../testdata/eval-fail-derivation-name.postprocess | 9 + test/testdata/eval-fail-dup-dynamic-attrs.err.exp | 14 + test/testdata/eval-fail-dup-dynamic-attrs.nix | 4 + test/testdata/eval-fail-duplicate-traces.err.exp | 51 + test/testdata/eval-fail-duplicate-traces.nix | 9 + test/testdata/eval-fail-eol-1.err.exp | 6 + test/testdata/eval-fail-eol-1.nix | 3 + test/testdata/eval-fail-eol-2.err.exp | 6 + test/testdata/eval-fail-eol-2.nix | 2 + test/testdata/eval-fail-eol-3.err.exp | 6 + test/testdata/eval-fail-eol-3.nix | 3 + test/testdata/eval-fail-fetchTree-negative.err.exp | 8 + test/testdata/eval-fail-fetchTree-negative.nix | 5 + .../eval-fail-fetchurl-baseName-attrs-name.err.exp | 8 + .../eval-fail-fetchurl-baseName-attrs-name.nix | 1 + .../eval-fail-fetchurl-baseName-attrs.err.exp | 8 + .../testdata/eval-fail-fetchurl-baseName-attrs.nix | 1 + test/testdata/eval-fail-fetchurl-baseName.err.exp | 8 + test/testdata/eval-fail-fetchurl-baseName.nix | 1 + ...il-flake-ref-to-string-negative-integer.err.exp | 14 + ...l-fail-flake-ref-to-string-negative-integer.nix | 7 + ...-fail-foldlStrict-strict-op-application.err.exp | 37 + ...eval-fail-foldlStrict-strict-op-application.nix | 5 + .../eval-fail-fromJSON-overflowing.err.exp | 8 + test/testdata/eval-fail-fromJSON-overflowing.nix | 1 + .../testdata/eval-fail-fromTOML-timestamps.err.exp | 8 + test/testdata/eval-fail-fromTOML-timestamps.nix | 130 + test/testdata/eval-fail-hashfile-missing.err.exp | 13 + test/testdata/eval-fail-hashfile-missing.nix | 5 + .../eval-fail-infinite-recursion-lambda.err.exp | 38 + .../eval-fail-infinite-recursion-lambda.flags | 1 + .../eval-fail-infinite-recursion-lambda.nix | 1 + test/testdata/eval-fail-list.err.exp | 8 + test/testdata/eval-fail-list.nix | 1 + test/testdata/eval-fail-missing-arg.err.exp | 12 + test/testdata/eval-fail-missing-arg.nix | 1 + test/testdata/eval-fail-mutual-recursion.err.exp | 64 + test/testdata/eval-fail-mutual-recursion.nix | 36 + test/testdata/eval-fail-nested-list-items.err.exp | 9 + test/testdata/eval-fail-nested-list-items.nix | 11 + test/testdata/eval-fail-nonexist-path.err.exp | 1 + test/testdata/eval-fail-nonexist-path.nix | 4 + test/testdata/eval-fail-not-throws.err.exp | 14 + test/testdata/eval-fail-not-throws.nix | 1 + test/testdata/eval-fail-overflowing-add.err.exp | 6 + test/testdata/eval-fail-overflowing-add.nix | 4 + test/testdata/eval-fail-overflowing-div.err.exp | 23 + test/testdata/eval-fail-overflowing-div.nix | 7 + test/testdata/eval-fail-overflowing-mul.err.exp | 16 + test/testdata/eval-fail-overflowing-mul.nix | 3 + test/testdata/eval-fail-overflowing-sub.err.exp | 9 + test/testdata/eval-fail-overflowing-sub.nix | 4 + test/testdata/eval-fail-path-slash.err.exp | 6 + test/testdata/eval-fail-path-slash.nix | 6 + test/testdata/eval-fail-pipe-operators.err.exp | 5 + test/testdata/eval-fail-pipe-operators.nix | 1 + test/testdata/eval-fail-recursion.err.exp | 12 + test/testdata/eval-fail-recursion.nix | 1 + test/testdata/eval-fail-remove.err.exp | 15 + test/testdata/eval-fail-remove.nix | 5 + test/testdata/eval-fail-scope-5.err.exp | 28 + test/testdata/eval-fail-scope-5.nix | 10 + test/testdata/eval-fail-seq.err.exp | 14 + test/testdata/eval-fail-seq.nix | 1 + test/testdata/eval-fail-set-override.err.exp | 4 + test/testdata/eval-fail-set-override.nix | 1 + test/testdata/eval-fail-set.err.exp | 5 + test/testdata/eval-fail-set.nix | 1 + test/testdata/eval-fail-substring.err.exp | 8 + test/testdata/eval-fail-substring.nix | 1 + test/testdata/eval-fail-to-path.err.exp | 10 + test/testdata/eval-fail-to-path.nix | 1 + test/testdata/eval-fail-toJSON.err.exp | 50 + test/testdata/eval-fail-toJSON.nix | 10 + test/testdata/eval-fail-undeclared-arg.err.exp | 13 + test/testdata/eval-fail-undeclared-arg.nix | 1 + .../eval-fail-using-set-as-attr-name.err.exp | 14 + test/testdata/eval-fail-using-set-as-attr-name.nix | 5 + test/testdata/eval-okay-any-all.exp | 1 + test/testdata/eval-okay-any-all.nix | 11 + test/testdata/eval-okay-arithmetic.exp | 1 + test/testdata/eval-okay-arithmetic.nix | 59 + test/testdata/eval-okay-attrnames.exp | 1 + test/testdata/eval-okay-attrnames.nix | 11 + test/testdata/eval-okay-attrs.exp | 1 + test/testdata/eval-okay-attrs.nix | 5 + test/testdata/eval-okay-attrs2.exp | 1 + test/testdata/eval-okay-attrs2.nix | 10 + test/testdata/eval-okay-attrs3.exp | 1 + test/testdata/eval-okay-attrs3.nix | 22 + test/testdata/eval-okay-attrs4.exp | 1 + test/testdata/eval-okay-attrs4.nix | 7 + test/testdata/eval-okay-attrs5.exp | 1 + test/testdata/eval-okay-attrs5.nix | 21 + test/testdata/eval-okay-attrs6.exp | 1 + test/testdata/eval-okay-attrs6.nix | 4 + test/testdata/eval-okay-autoargs.exp | 1 + test/testdata/eval-okay-autoargs.flags | 1 + test/testdata/eval-okay-autoargs.nix | 15 + test/testdata/eval-okay-backslash-newline-1.exp | 1 + test/testdata/eval-okay-backslash-newline-1.nix | 2 + test/testdata/eval-okay-backslash-newline-2.exp | 1 + test/testdata/eval-okay-backslash-newline-2.nix | 2 + test/testdata/eval-okay-baseNameOf.exp | 1 + test/testdata/eval-okay-baseNameOf.nix | 32 + test/testdata/eval-okay-builtins-add.exp | 1 + test/testdata/eval-okay-builtins-add.nix | 8 + test/testdata/eval-okay-builtins.exp | 1 + test/testdata/eval-okay-builtins.nix | 12 + test/testdata/eval-okay-callable-attrs.exp | 1 + test/testdata/eval-okay-callable-attrs.nix | 1 + test/testdata/eval-okay-catattrs.exp | 1 + test/testdata/eval-okay-catattrs.nix | 1 + test/testdata/eval-okay-closure.exp | 1 + test/testdata/eval-okay-closure.exp.xml | 343 +++ test/testdata/eval-okay-closure.nix | 13 + test/testdata/eval-okay-comments.exp | 1 + test/testdata/eval-okay-comments.nix | 59 + test/testdata/eval-okay-concat.exp | 1 + test/testdata/eval-okay-concat.nix | 1 + test/testdata/eval-okay-concatmap.exp | 1 + test/testdata/eval-okay-concatmap.nix | 5 + test/testdata/eval-okay-concatstringssep.exp | 1 + test/testdata/eval-okay-concatstringssep.nix | 8 + test/testdata/eval-okay-context-introspection.exp | 1 + test/testdata/eval-okay-context-introspection.nix | 59 + test/testdata/eval-okay-context.exp | 1 + test/testdata/eval-okay-context.nix | 6 + test/testdata/eval-okay-convertHash.err.exp | 108 + test/testdata/eval-okay-convertHash.exp | 1 + test/testdata/eval-okay-convertHash.nix | 33 + test/testdata/eval-okay-curpos.exp | 1 + test/testdata/eval-okay-curpos.nix | 5 + test/testdata/eval-okay-deepseq.exp | 1 + test/testdata/eval-okay-deepseq.nix | 1 + test/testdata/eval-okay-delayed-with-inherit.exp | 1 + test/testdata/eval-okay-delayed-with-inherit.nix | 24 + test/testdata/eval-okay-delayed-with.exp | 1 + test/testdata/eval-okay-delayed-with.nix | 29 + test/testdata/eval-okay-derivation-legacy.err.exp | 6 + test/testdata/eval-okay-derivation-legacy.exp | 1 + test/testdata/eval-okay-derivation-legacy.nix | 12 + test/testdata/eval-okay-dynamic-attrs-2.exp | 1 + test/testdata/eval-okay-dynamic-attrs-2.nix | 1 + test/testdata/eval-okay-dynamic-attrs-bare.exp | 1 + test/testdata/eval-okay-dynamic-attrs-bare.nix | 17 + test/testdata/eval-okay-dynamic-attrs.exp | 1 + test/testdata/eval-okay-dynamic-attrs.nix | 17 + test/testdata/eval-okay-elem.exp | 1 + test/testdata/eval-okay-elem.nix | 6 + test/testdata/eval-okay-empty-args.exp | 1 + test/testdata/eval-okay-empty-args.nix | 1 + test/testdata/eval-okay-eq-derivations.exp | 1 + test/testdata/eval-okay-eq-derivations.nix | 10 + test/testdata/eval-okay-eq.exp | 1 + test/testdata/eval-okay-eq.nix | 3 + test/testdata/eval-okay-filter.exp | 1 + test/testdata/eval-okay-filter.nix | 5 + test/testdata/eval-okay-flake-ref-to-string.exp | 1 + test/testdata/eval-okay-flake-ref-to-string.nix | 7 + test/testdata/eval-okay-flatten.exp | 1 + test/testdata/eval-okay-flatten.nix | 8 + test/testdata/eval-okay-float.exp | 1 + test/testdata/eval-okay-float.nix | 6 + test/testdata/eval-okay-floor-ceil.exp | 1 + test/testdata/eval-okay-floor-ceil.nix | 9 + .../eval-okay-foldlStrict-lazy-elements.exp | 1 + .../eval-okay-foldlStrict-lazy-elements.nix | 9 + ...l-okay-foldlStrict-lazy-initial-accumulator.exp | 1 + ...l-okay-foldlStrict-lazy-initial-accumulator.nix | 6 + test/testdata/eval-okay-foldlStrict.exp | 1 + test/testdata/eval-okay-foldlStrict.nix | 3 + test/testdata/eval-okay-fromTOML-timestamps.exp | 1 + test/testdata/eval-okay-fromTOML-timestamps.flags | 1 + test/testdata/eval-okay-fromTOML-timestamps.nix | 130 + test/testdata/eval-okay-fromTOML.exp | 1 + test/testdata/eval-okay-fromTOML.nix | 208 ++ test/testdata/eval-okay-fromjson-escapes.exp | 1 + test/testdata/eval-okay-fromjson-escapes.nix | 3 + test/testdata/eval-okay-fromjson.exp | 1 + test/testdata/eval-okay-fromjson.nix | 41 + test/testdata/eval-okay-functionargs.exp | 1 + test/testdata/eval-okay-functionargs.exp.xml | 15 + test/testdata/eval-okay-functionargs.nix | 80 + .../testdata/eval-okay-getattrpos-functionargs.exp | 1 + .../testdata/eval-okay-getattrpos-functionargs.nix | 4 + test/testdata/eval-okay-getattrpos-undefined.exp | 1 + test/testdata/eval-okay-getattrpos-undefined.nix | 1 + test/testdata/eval-okay-getattrpos.exp | 1 + test/testdata/eval-okay-getattrpos.nix | 6 + test/testdata/eval-okay-getenv.exp | 1 + test/testdata/eval-okay-getenv.nix | 1 + test/testdata/eval-okay-groupBy.exp | 1 + test/testdata/eval-okay-groupBy.nix | 5 + test/testdata/eval-okay-hash.exp | 0 test/testdata/eval-okay-hashfile.exp | 1 + test/testdata/eval-okay-hashfile.nix | 4 + test/testdata/eval-okay-hashstring.exp | 1 + test/testdata/eval-okay-hashstring.nix | 4 + test/testdata/eval-okay-if.exp | 1 + test/testdata/eval-okay-if.nix | 1 + test/testdata/eval-okay-import.exp | 1 + test/testdata/eval-okay-import.nix | 11 + test/testdata/eval-okay-ind-string.exp | 1 + test/testdata/eval-okay-ind-string.nix | 128 + test/testdata/eval-okay-inherit-attr-pos.exp | 1 + test/testdata/eval-okay-inherit-attr-pos.nix | 12 + test/testdata/eval-okay-inherit-from.err.exp | 1 + test/testdata/eval-okay-inherit-from.exp | 1 + test/testdata/eval-okay-inherit-from.nix | 16 + test/testdata/eval-okay-intersectAttrs.exp | 1 + test/testdata/eval-okay-intersectAttrs.nix | 50 + test/testdata/eval-okay-let.exp | 1 + test/testdata/eval-okay-let.nix | 5 + test/testdata/eval-okay-list.exp | 1 + test/testdata/eval-okay-list.nix | 7 + test/testdata/eval-okay-listtoattrs.exp | 1 + test/testdata/eval-okay-listtoattrs.nix | 11 + test/testdata/eval-okay-logic.exp | 1 + test/testdata/eval-okay-logic.nix | 1 + test/testdata/eval-okay-map.exp | 1 + test/testdata/eval-okay-map.nix | 3 + test/testdata/eval-okay-mapattrs.exp | 1 + test/testdata/eval-okay-mapattrs.nix | 3 + test/testdata/eval-okay-merge-dynamic-attrs.exp | 1 + test/testdata/eval-okay-merge-dynamic-attrs.nix | 13 + test/testdata/eval-okay-nested-with.exp | 1 + test/testdata/eval-okay-nested-with.nix | 3 + test/testdata/eval-okay-new-let.exp | 1 + test/testdata/eval-okay-new-let.nix | 14 + test/testdata/eval-okay-null-dynamic-attrs.exp | 1 + test/testdata/eval-okay-null-dynamic-attrs.nix | 1 + test/testdata/eval-okay-overrides.exp | 1 + test/testdata/eval-okay-overrides.nix | 9 + test/testdata/eval-okay-parse-flake-ref.exp | 1 + test/testdata/eval-okay-parse-flake-ref.nix | 1 + test/testdata/eval-okay-partition.exp | 1 + test/testdata/eval-okay-partition.nix | 5 + .../eval-okay-path-string-interpolation.exp | 1 + .../eval-okay-path-string-interpolation.nix | 12 + test/testdata/eval-okay-path.exp | 1 + test/testdata/eval-okay-path.nix | 15 + test/testdata/eval-okay-pathexists.exp | 1 + test/testdata/eval-okay-pathexists.nix | 34 + test/testdata/eval-okay-patterns.exp | 1 + test/testdata/eval-okay-patterns.nix | 16 + test/testdata/eval-okay-print.err.exp | 1 + test/testdata/eval-okay-print.exp | 1 + test/testdata/eval-okay-print.nix | 1 + test/testdata/eval-okay-readDir.exp | 1 + test/testdata/eval-okay-readDir.nix | 1 + test/testdata/eval-okay-readFileType.exp | 1 + test/testdata/eval-okay-readFileType.nix | 6 + test/testdata/eval-okay-readfile.exp | 1 + test/testdata/eval-okay-readfile.nix | 1 + test/testdata/eval-okay-redefine-builtin.exp | 1 + test/testdata/eval-okay-redefine-builtin.nix | 3 + test/testdata/eval-okay-regex-match.exp | 1 + test/testdata/eval-okay-regex-match.nix | 29 + test/testdata/eval-okay-regex-split.exp | 1 + test/testdata/eval-okay-regex-split.nix | 48 + test/testdata/eval-okay-regression-20220122.exp | 1 + test/testdata/eval-okay-regression-20220122.nix | 1 + test/testdata/eval-okay-regression-20220125.exp | 1 + test/testdata/eval-okay-regression-20220125.nix | 2 + test/testdata/eval-okay-remove.exp | 1 + test/testdata/eval-okay-remove.nix | 5 + test/testdata/eval-okay-repeated-empty-attrs.exp | 1 + test/testdata/eval-okay-repeated-empty-attrs.nix | 2 + test/testdata/eval-okay-repeated-empty-list.exp | 1 + test/testdata/eval-okay-repeated-empty-list.nix | 1 + test/testdata/eval-okay-replacestrings.exp | 1 + test/testdata/eval-okay-replacestrings.nix | 12 + test/testdata/eval-okay-scope-1.exp | 1 + test/testdata/eval-okay-scope-1.nix | 6 + test/testdata/eval-okay-scope-2.exp | 1 + test/testdata/eval-okay-scope-2.nix | 6 + test/testdata/eval-okay-scope-3.exp | 1 + test/testdata/eval-okay-scope-3.nix | 6 + test/testdata/eval-okay-scope-4.exp | 1 + test/testdata/eval-okay-scope-4.nix | 10 + test/testdata/eval-okay-scope-6.exp | 1 + test/testdata/eval-okay-scope-6.nix | 7 + test/testdata/eval-okay-scope-7.exp | 1 + test/testdata/eval-okay-scope-7.nix | 6 + test/testdata/eval-okay-search-path.exp | 1 + test/testdata/eval-okay-search-path.flags | 1 + test/testdata/eval-okay-search-path.nix | 10 + test/testdata/eval-okay-seq.exp | 1 + test/testdata/eval-okay-seq.nix | 1 + test/testdata/eval-okay-sort.exp | 1 + test/testdata/eval-okay-sort.nix | 20 + test/testdata/eval-okay-splitversion.exp | 1 + test/testdata/eval-okay-splitversion.nix | 1 + test/testdata/eval-okay-string.exp | 1 + test/testdata/eval-okay-string.nix | 12 + test/testdata/eval-okay-strings-as-attrs-names.exp | 1 + test/testdata/eval-okay-strings-as-attrs-names.nix | 20 + test/testdata/eval-okay-substring-context.exp | 1 + test/testdata/eval-okay-substring-context.nix | 11 + test/testdata/eval-okay-substring.exp | 1 + test/testdata/eval-okay-substring.nix | 23 + test/testdata/eval-okay-symlink-resolution.exp | 1 + test/testdata/eval-okay-symlink-resolution.nix | 1 + test/testdata/eval-okay-tail-call-1.exp-disabled | 1 + test/testdata/eval-okay-tail-call-1.nix | 3 + test/testdata/eval-okay-tojson.exp | 1 + test/testdata/eval-okay-tojson.nix | 13 + test/testdata/eval-okay-toxml.exp | 1 + test/testdata/eval-okay-toxml.nix | 3 + test/testdata/eval-okay-toxml2.exp | 1 + test/testdata/eval-okay-toxml2.nix | 1 + test/testdata/eval-okay-tryeval.exp | 1 + test/testdata/eval-okay-tryeval.nix | 5 + test/testdata/eval-okay-types.exp | 1 + test/testdata/eval-okay-types.nix | 37 + test/testdata/eval-okay-versions.exp | 1 + test/testdata/eval-okay-versions.nix | 43 + test/testdata/eval-okay-with.exp | 1 + test/testdata/eval-okay-with.nix | 19 + test/testdata/eval-okay-xml.exp.xml | 52 + test/testdata/eval-okay-xml.nix | 21 + test/testdata/eval-okay-zipAttrsWith.exp | 1 + test/testdata/eval-okay-zipAttrsWith.nix | 9 + test/testdata/importdef.sexp | 1 + test/testdata/imported.nix | 3 + test/testdata/imported2.nix | 1 + test/testdata/lib.nix | 61 + test/testdata/non-eval-fail-bad-drvPath.nix | 14 + test/testdata/parse-fail-dup-attrs-1.err.exp | 6 + test/testdata/parse-fail-dup-attrs-1.nix | 4 + test/testdata/parse-fail-dup-attrs-2.err.exp | 6 + test/testdata/parse-fail-dup-attrs-2.nix | 13 + test/testdata/parse-fail-dup-attrs-3.err.exp | 6 + test/testdata/parse-fail-dup-attrs-3.nix | 13 + test/testdata/parse-fail-dup-attrs-4.err.exp | 6 + test/testdata/parse-fail-dup-attrs-4.nix | 4 + test/testdata/parse-fail-dup-attrs-7.err.exp | 6 + test/testdata/parse-fail-dup-attrs-7.nix | 9 + test/testdata/parse-fail-dup-formals.err.exp | 4 + test/testdata/parse-fail-dup-formals.nix | 1 + test/testdata/parse-fail-eof-in-string.err.exp | 5 + test/testdata/parse-fail-eof-in-string.nix | 3 + test/testdata/parse-fail-eof-pos.err.exp | 5 + test/testdata/parse-fail-eof-pos.nix | 2 + .../parse-fail-mixed-nested-attrs1.err.exp | 6 + test/testdata/parse-fail-mixed-nested-attrs1.nix | 4 + .../parse-fail-mixed-nested-attrs2.err.exp | 6 + test/testdata/parse-fail-mixed-nested-attrs2.nix | 4 + test/testdata/parse-fail-patterns-1.err.exp | 5 + test/testdata/parse-fail-patterns-1.nix | 1 + .../parse-fail-regression-20060610.err.exp | 6 + test/testdata/parse-fail-regression-20060610.nix | 11 + test/testdata/parse-fail-undef-var-2.err.exp | 6 + test/testdata/parse-fail-undef-var-2.nix | 7 + test/testdata/parse-fail-undef-var.err.exp | 5 + test/testdata/parse-fail-undef-var.nix | 1 + test/testdata/parse-fail-utf8.err.exp | 5 + test/testdata/parse-fail-utf8.nix | 1 + test/testdata/parse-okay-1.exp | 1 + test/testdata/parse-okay-1.nix | 1 + test/testdata/parse-okay-crlf.exp | 1 + test/testdata/parse-okay-crlf.nix | 17 + test/testdata/parse-okay-dup-attrs-5.exp | 1 + test/testdata/parse-okay-dup-attrs-5.nix | 4 + test/testdata/parse-okay-dup-attrs-6.exp | 1 + test/testdata/parse-okay-dup-attrs-6.nix | 4 + test/testdata/parse-okay-ind-string.exp | 1 + test/testdata/parse-okay-ind-string.nix | 31 + test/testdata/parse-okay-inherits.exp | 1 + test/testdata/parse-okay-inherits.nix | 9 + test/testdata/parse-okay-mixed-nested-attrs-1.exp | 1 + test/testdata/parse-okay-mixed-nested-attrs-1.nix | 4 + test/testdata/parse-okay-mixed-nested-attrs-2.exp | 1 + test/testdata/parse-okay-mixed-nested-attrs-2.nix | 4 + test/testdata/parse-okay-mixed-nested-attrs-3.exp | 1 + test/testdata/parse-okay-mixed-nested-attrs-3.nix | 7 + test/testdata/parse-okay-regression-20041027.exp | 1 + test/testdata/parse-okay-regression-20041027.nix | 11 + test/testdata/parse-okay-regression-751.exp | 1 + test/testdata/parse-okay-regression-751.nix | 2 + test/testdata/parse-okay-subversion.exp | 1 + test/testdata/parse-okay-subversion.nix | 43 + test/testdata/parse-okay-url.exp | 1 + test/testdata/parse-okay-url.nix | 8 + test/testdata/readDir/bar | 0 test/testdata/readDir/foo/git-hates-directories | 0 test/testdata/readDir/ldir | 1 + test/testdata/readDir/linked | 1 + test/testdata/symlink-resolution/broken | 1 + .../symlink-resolution/foo/lib/default.nix | 1 + test/testdata/symlink-resolution/foo/overlays | 1 + .../symlink-resolution/overlays/overlay.nix | 1 + theories/dune | 8 + theories/dynlang/equiv.v | 154 ++ theories/dynlang/interp.v | 49 + theories/dynlang/interp_proofs.v | 426 ++++ theories/dynlang/operational.v | 41 + theories/dynlang/operational_props.v | 33 + theories/evallang/interp.v | 52 + theories/evallang/interp_proofs.v | 478 ++++ theories/evallang/operational.v | 140 + theories/evallang/operational_props.v | 33 + theories/evallang/tests.v | 33 + theories/lambda/interp.v | 44 + theories/lambda/interp_proofs.v | 614 +++++ theories/lambda/operational.v | 38 + theories/lambda/operational_props.v | 29 + theories/nix/floats.v | 85 + theories/nix/interp.v | 351 +++ theories/nix/interp_proofs.v | 2690 ++++++++++++++++++++ theories/nix/notations.v | 43 + theories/nix/operational.v | 527 ++++ theories/nix/operational_props.v | 680 +++++ theories/nix/tests.v | 185 ++ theories/nix/wp.v | 143 ++ theories/nix/wp_examples.v | 164 ++ theories/res.v | 75 + theories/utils.v | 275 ++ 538 files changed, 16716 insertions(+) create mode 100644 .gitignore create mode 100644 .ocamlformat create mode 100644 .ocamlformat-ignore create mode 100644 COPYING create mode 100644 Makefile create mode 100644 README.md create mode 100644 _CoqProject create mode 100644 axioms.nix create mode 100644 bin/dune create mode 100644 bin/main.ml create mode 100644 bin/repl.ml create mode 100644 bin/repl_cmd.ml create mode 100644 bin/run.ml create mode 100644 bin/settings.ml create mode 100755 cloc-rocq.sh create mode 100644 cloc.nix create mode 100644 coverage.nix create mode 100755 coverage.sh create mode 100644 default.nix create mode 100644 dune-project create mode 100644 explorer/.gitignore create mode 100755 explorer/generate.sh create mode 100755 explorer/tree.sh create mode 100755 explorer/upload-new.sh create mode 100644 importdef.sexp create mode 100644 lib/extraction/dune create mode 100644 lib/extraction/extraction.ml create mode 100644 lib/extraction/prelude.v create mode 100644 lib/mininix/builtins.ml create mode 100644 lib/mininix/builtins.nix create mode 100644 lib/mininix/conv.ml create mode 100644 lib/mininix/dune create mode 100644 lib/mininix/import.ml create mode 100644 lib/mininix/mininix.ml create mode 100644 lib/mininix/mininix2nix.ml create mode 100644 lib/mininix/nix2mininix.ml create mode 100644 lib/mininix/run.ml create mode 100644 lib/mininix/sexp.ml create mode 100644 lib/nix/dune create mode 100644 lib/nix/elaborator.ml create mode 100644 lib/nix/lexer.mll create mode 100644 lib/nix/nix.ml create mode 100644 lib/nix/parser.mly create mode 100644 lib/nix/printer.ml create mode 100644 lib/nix/tokens.ml create mode 100644 lib/nix/types.ml create mode 100644 mininix.opam create mode 100644 mininix.opam.locked create mode 100644 nixpkgs-pinned.nix create mode 100644 shell.nix create mode 100644 test/dune create mode 100644 test/test_mininix.ml create mode 100644 test/testdata/binary-data create mode 100644 test/testdata/data create mode 100644 test/testdata/dir1/a.nix create mode 100644 test/testdata/dir2/a.nix create mode 100644 test/testdata/dir2/b.nix create mode 100644 test/testdata/dir3/a.nix create mode 100644 test/testdata/dir3/b.nix create mode 100644 test/testdata/dir3/c.nix create mode 100644 test/testdata/dir4/a.nix create mode 100644 test/testdata/dir4/c.nix create mode 100644 test/testdata/eval-fail-abort.err.exp create mode 100644 test/testdata/eval-fail-abort.nix create mode 100644 test/testdata/eval-fail-addDrvOutputDependencies-empty-context.err.exp create mode 100644 test/testdata/eval-fail-addDrvOutputDependencies-empty-context.nix create mode 100644 test/testdata/eval-fail-addDrvOutputDependencies-multi-elem-context.err.exp create mode 100644 test/testdata/eval-fail-addDrvOutputDependencies-multi-elem-context.nix create mode 100644 test/testdata/eval-fail-addDrvOutputDependencies-wrong-element-kind.err.exp create mode 100644 test/testdata/eval-fail-addDrvOutputDependencies-wrong-element-kind.nix create mode 100644 test/testdata/eval-fail-addErrorContext-example.err.exp create mode 100644 test/testdata/eval-fail-addErrorContext-example.flags create mode 100644 test/testdata/eval-fail-addErrorContext-example.nix create mode 100644 test/testdata/eval-fail-assert-equal-attrs-names-2.err.exp create mode 100644 test/testdata/eval-fail-assert-equal-attrs-names-2.nix create mode 100644 test/testdata/eval-fail-assert-equal-attrs-names.err.exp create mode 100644 test/testdata/eval-fail-assert-equal-attrs-names.nix create mode 100644 test/testdata/eval-fail-assert-equal-derivations-extra.err.exp create mode 100644 test/testdata/eval-fail-assert-equal-derivations-extra.nix create mode 100644 test/testdata/eval-fail-assert-equal-derivations.err.exp create mode 100644 test/testdata/eval-fail-assert-equal-derivations.nix create mode 100644 test/testdata/eval-fail-assert-equal-floats.err.exp create mode 100644 test/testdata/eval-fail-assert-equal-floats.nix create mode 100644 test/testdata/eval-fail-assert-equal-function-direct.err.exp create mode 100644 test/testdata/eval-fail-assert-equal-function-direct.nix create mode 100644 test/testdata/eval-fail-assert-equal-int-float.err.exp create mode 100644 test/testdata/eval-fail-assert-equal-int-float.nix create mode 100644 test/testdata/eval-fail-assert-equal-ints.err.exp create mode 100644 test/testdata/eval-fail-assert-equal-ints.nix create mode 100644 test/testdata/eval-fail-assert-equal-list-length.err.exp create mode 100644 test/testdata/eval-fail-assert-equal-list-length.nix create mode 100644 test/testdata/eval-fail-assert-equal-paths.err.exp create mode 100644 test/testdata/eval-fail-assert-equal-paths.nix create mode 100644 test/testdata/eval-fail-assert-equal-type-nested.err.exp create mode 100644 test/testdata/eval-fail-assert-equal-type-nested.nix create mode 100644 test/testdata/eval-fail-assert-equal-type.err.exp create mode 100644 test/testdata/eval-fail-assert-equal-type.nix create mode 100644 test/testdata/eval-fail-assert-nested-bool.err.exp create mode 100644 test/testdata/eval-fail-assert-nested-bool.nix create mode 100644 test/testdata/eval-fail-assert.err.exp create mode 100644 test/testdata/eval-fail-assert.nix create mode 100644 test/testdata/eval-fail-attr-name-type.err.exp create mode 100644 test/testdata/eval-fail-attr-name-type.nix create mode 100644 test/testdata/eval-fail-bad-string-interpolation-1.err.exp create mode 100644 test/testdata/eval-fail-bad-string-interpolation-1.nix create mode 100644 test/testdata/eval-fail-bad-string-interpolation-2.err.exp create mode 100644 test/testdata/eval-fail-bad-string-interpolation-2.nix create mode 100644 test/testdata/eval-fail-bad-string-interpolation-3.err.exp create mode 100644 test/testdata/eval-fail-bad-string-interpolation-3.nix create mode 100644 test/testdata/eval-fail-bad-string-interpolation-4.err.exp create mode 100644 test/testdata/eval-fail-bad-string-interpolation-4.nix create mode 100644 test/testdata/eval-fail-blackhole.err.exp create mode 100644 test/testdata/eval-fail-blackhole.nix create mode 100644 test/testdata/eval-fail-call-primop.err.exp create mode 100644 test/testdata/eval-fail-call-primop.nix create mode 100644 test/testdata/eval-fail-deepseq.err.exp create mode 100644 test/testdata/eval-fail-deepseq.nix create mode 100644 test/testdata/eval-fail-derivation-name.err.exp create mode 100644 test/testdata/eval-fail-derivation-name.nix create mode 100644 test/testdata/eval-fail-derivation-name.postprocess create mode 100644 test/testdata/eval-fail-dup-dynamic-attrs.err.exp create mode 100644 test/testdata/eval-fail-dup-dynamic-attrs.nix create mode 100644 test/testdata/eval-fail-duplicate-traces.err.exp create mode 100644 test/testdata/eval-fail-duplicate-traces.nix create mode 100644 test/testdata/eval-fail-eol-1.err.exp create mode 100644 test/testdata/eval-fail-eol-1.nix create mode 100644 test/testdata/eval-fail-eol-2.err.exp create mode 100644 test/testdata/eval-fail-eol-2.nix create mode 100644 test/testdata/eval-fail-eol-3.err.exp create mode 100644 test/testdata/eval-fail-eol-3.nix create mode 100644 test/testdata/eval-fail-fetchTree-negative.err.exp create mode 100644 test/testdata/eval-fail-fetchTree-negative.nix create mode 100644 test/testdata/eval-fail-fetchurl-baseName-attrs-name.err.exp create mode 100644 test/testdata/eval-fail-fetchurl-baseName-attrs-name.nix create mode 100644 test/testdata/eval-fail-fetchurl-baseName-attrs.err.exp create mode 100644 test/testdata/eval-fail-fetchurl-baseName-attrs.nix create mode 100644 test/testdata/eval-fail-fetchurl-baseName.err.exp create mode 100644 test/testdata/eval-fail-fetchurl-baseName.nix create mode 100644 test/testdata/eval-fail-flake-ref-to-string-negative-integer.err.exp create mode 100644 test/testdata/eval-fail-flake-ref-to-string-negative-integer.nix create mode 100644 test/testdata/eval-fail-foldlStrict-strict-op-application.err.exp create mode 100644 test/testdata/eval-fail-foldlStrict-strict-op-application.nix create mode 100644 test/testdata/eval-fail-fromJSON-overflowing.err.exp create mode 100644 test/testdata/eval-fail-fromJSON-overflowing.nix create mode 100644 test/testdata/eval-fail-fromTOML-timestamps.err.exp create mode 100644 test/testdata/eval-fail-fromTOML-timestamps.nix create mode 100644 test/testdata/eval-fail-hashfile-missing.err.exp create mode 100644 test/testdata/eval-fail-hashfile-missing.nix create mode 100644 test/testdata/eval-fail-infinite-recursion-lambda.err.exp create mode 100644 test/testdata/eval-fail-infinite-recursion-lambda.flags create mode 100644 test/testdata/eval-fail-infinite-recursion-lambda.nix create mode 100644 test/testdata/eval-fail-list.err.exp create mode 100644 test/testdata/eval-fail-list.nix create mode 100644 test/testdata/eval-fail-missing-arg.err.exp create mode 100644 test/testdata/eval-fail-missing-arg.nix create mode 100644 test/testdata/eval-fail-mutual-recursion.err.exp create mode 100644 test/testdata/eval-fail-mutual-recursion.nix create mode 100644 test/testdata/eval-fail-nested-list-items.err.exp create mode 100644 test/testdata/eval-fail-nested-list-items.nix create mode 100644 test/testdata/eval-fail-nonexist-path.err.exp create mode 100644 test/testdata/eval-fail-nonexist-path.nix create mode 100644 test/testdata/eval-fail-not-throws.err.exp create mode 100644 test/testdata/eval-fail-not-throws.nix create mode 100644 test/testdata/eval-fail-overflowing-add.err.exp create mode 100644 test/testdata/eval-fail-overflowing-add.nix create mode 100644 test/testdata/eval-fail-overflowing-div.err.exp create mode 100644 test/testdata/eval-fail-overflowing-div.nix create mode 100644 test/testdata/eval-fail-overflowing-mul.err.exp create mode 100644 test/testdata/eval-fail-overflowing-mul.nix create mode 100644 test/testdata/eval-fail-overflowing-sub.err.exp create mode 100644 test/testdata/eval-fail-overflowing-sub.nix create mode 100644 test/testdata/eval-fail-path-slash.err.exp create mode 100644 test/testdata/eval-fail-path-slash.nix create mode 100644 test/testdata/eval-fail-pipe-operators.err.exp create mode 100644 test/testdata/eval-fail-pipe-operators.nix create mode 100644 test/testdata/eval-fail-recursion.err.exp create mode 100644 test/testdata/eval-fail-recursion.nix create mode 100644 test/testdata/eval-fail-remove.err.exp create mode 100644 test/testdata/eval-fail-remove.nix create mode 100644 test/testdata/eval-fail-scope-5.err.exp create mode 100644 test/testdata/eval-fail-scope-5.nix create mode 100644 test/testdata/eval-fail-seq.err.exp create mode 100644 test/testdata/eval-fail-seq.nix create mode 100644 test/testdata/eval-fail-set-override.err.exp create mode 100644 test/testdata/eval-fail-set-override.nix create mode 100644 test/testdata/eval-fail-set.err.exp create mode 100644 test/testdata/eval-fail-set.nix create mode 100644 test/testdata/eval-fail-substring.err.exp create mode 100644 test/testdata/eval-fail-substring.nix create mode 100644 test/testdata/eval-fail-to-path.err.exp create mode 100644 test/testdata/eval-fail-to-path.nix create mode 100644 test/testdata/eval-fail-toJSON.err.exp create mode 100644 test/testdata/eval-fail-toJSON.nix create mode 100644 test/testdata/eval-fail-undeclared-arg.err.exp create mode 100644 test/testdata/eval-fail-undeclared-arg.nix create mode 100644 test/testdata/eval-fail-using-set-as-attr-name.err.exp create mode 100644 test/testdata/eval-fail-using-set-as-attr-name.nix create mode 100644 test/testdata/eval-okay-any-all.exp create mode 100644 test/testdata/eval-okay-any-all.nix create mode 100644 test/testdata/eval-okay-arithmetic.exp create mode 100644 test/testdata/eval-okay-arithmetic.nix create mode 100644 test/testdata/eval-okay-attrnames.exp create mode 100644 test/testdata/eval-okay-attrnames.nix create mode 100644 test/testdata/eval-okay-attrs.exp create mode 100644 test/testdata/eval-okay-attrs.nix create mode 100644 test/testdata/eval-okay-attrs2.exp create mode 100644 test/testdata/eval-okay-attrs2.nix create mode 100644 test/testdata/eval-okay-attrs3.exp create mode 100644 test/testdata/eval-okay-attrs3.nix create mode 100644 test/testdata/eval-okay-attrs4.exp create mode 100644 test/testdata/eval-okay-attrs4.nix create mode 100644 test/testdata/eval-okay-attrs5.exp create mode 100644 test/testdata/eval-okay-attrs5.nix create mode 100644 test/testdata/eval-okay-attrs6.exp create mode 100644 test/testdata/eval-okay-attrs6.nix create mode 100644 test/testdata/eval-okay-autoargs.exp create mode 100644 test/testdata/eval-okay-autoargs.flags create mode 100644 test/testdata/eval-okay-autoargs.nix create mode 100644 test/testdata/eval-okay-backslash-newline-1.exp create mode 100644 test/testdata/eval-okay-backslash-newline-1.nix create mode 100644 test/testdata/eval-okay-backslash-newline-2.exp create mode 100644 test/testdata/eval-okay-backslash-newline-2.nix create mode 100644 test/testdata/eval-okay-baseNameOf.exp create mode 100644 test/testdata/eval-okay-baseNameOf.nix create mode 100644 test/testdata/eval-okay-builtins-add.exp create mode 100644 test/testdata/eval-okay-builtins-add.nix create mode 100644 test/testdata/eval-okay-builtins.exp create mode 100644 test/testdata/eval-okay-builtins.nix create mode 100644 test/testdata/eval-okay-callable-attrs.exp create mode 100644 test/testdata/eval-okay-callable-attrs.nix create mode 100644 test/testdata/eval-okay-catattrs.exp create mode 100644 test/testdata/eval-okay-catattrs.nix create mode 100644 test/testdata/eval-okay-closure.exp create mode 100644 test/testdata/eval-okay-closure.exp.xml create mode 100644 test/testdata/eval-okay-closure.nix create mode 100644 test/testdata/eval-okay-comments.exp create mode 100644 test/testdata/eval-okay-comments.nix create mode 100644 test/testdata/eval-okay-concat.exp create mode 100644 test/testdata/eval-okay-concat.nix create mode 100644 test/testdata/eval-okay-concatmap.exp create mode 100644 test/testdata/eval-okay-concatmap.nix create mode 100644 test/testdata/eval-okay-concatstringssep.exp create mode 100644 test/testdata/eval-okay-concatstringssep.nix create mode 100644 test/testdata/eval-okay-context-introspection.exp create mode 100644 test/testdata/eval-okay-context-introspection.nix create mode 100644 test/testdata/eval-okay-context.exp create mode 100644 test/testdata/eval-okay-context.nix create mode 100644 test/testdata/eval-okay-convertHash.err.exp create mode 100644 test/testdata/eval-okay-convertHash.exp create mode 100644 test/testdata/eval-okay-convertHash.nix create mode 100644 test/testdata/eval-okay-curpos.exp create mode 100644 test/testdata/eval-okay-curpos.nix create mode 100644 test/testdata/eval-okay-deepseq.exp create mode 100644 test/testdata/eval-okay-deepseq.nix create mode 100644 test/testdata/eval-okay-delayed-with-inherit.exp create mode 100644 test/testdata/eval-okay-delayed-with-inherit.nix create mode 100644 test/testdata/eval-okay-delayed-with.exp create mode 100644 test/testdata/eval-okay-delayed-with.nix create mode 100644 test/testdata/eval-okay-derivation-legacy.err.exp create mode 100644 test/testdata/eval-okay-derivation-legacy.exp create mode 100644 test/testdata/eval-okay-derivation-legacy.nix create mode 100644 test/testdata/eval-okay-dynamic-attrs-2.exp create mode 100644 test/testdata/eval-okay-dynamic-attrs-2.nix create mode 100644 test/testdata/eval-okay-dynamic-attrs-bare.exp create mode 100644 test/testdata/eval-okay-dynamic-attrs-bare.nix create mode 100644 test/testdata/eval-okay-dynamic-attrs.exp create mode 100644 test/testdata/eval-okay-dynamic-attrs.nix create mode 100644 test/testdata/eval-okay-elem.exp create mode 100644 test/testdata/eval-okay-elem.nix create mode 100644 test/testdata/eval-okay-empty-args.exp create mode 100644 test/testdata/eval-okay-empty-args.nix create mode 100644 test/testdata/eval-okay-eq-derivations.exp create mode 100644 test/testdata/eval-okay-eq-derivations.nix create mode 100644 test/testdata/eval-okay-eq.exp create mode 100644 test/testdata/eval-okay-eq.nix create mode 100644 test/testdata/eval-okay-filter.exp create mode 100644 test/testdata/eval-okay-filter.nix create mode 100644 test/testdata/eval-okay-flake-ref-to-string.exp create mode 100644 test/testdata/eval-okay-flake-ref-to-string.nix create mode 100644 test/testdata/eval-okay-flatten.exp create mode 100644 test/testdata/eval-okay-flatten.nix create mode 100644 test/testdata/eval-okay-float.exp create mode 100644 test/testdata/eval-okay-float.nix create mode 100644 test/testdata/eval-okay-floor-ceil.exp create mode 100644 test/testdata/eval-okay-floor-ceil.nix create mode 100644 test/testdata/eval-okay-foldlStrict-lazy-elements.exp create mode 100644 test/testdata/eval-okay-foldlStrict-lazy-elements.nix create mode 100644 test/testdata/eval-okay-foldlStrict-lazy-initial-accumulator.exp create mode 100644 test/testdata/eval-okay-foldlStrict-lazy-initial-accumulator.nix create mode 100644 test/testdata/eval-okay-foldlStrict.exp create mode 100644 test/testdata/eval-okay-foldlStrict.nix create mode 100644 test/testdata/eval-okay-fromTOML-timestamps.exp create mode 100644 test/testdata/eval-okay-fromTOML-timestamps.flags create mode 100644 test/testdata/eval-okay-fromTOML-timestamps.nix create mode 100644 test/testdata/eval-okay-fromTOML.exp create mode 100644 test/testdata/eval-okay-fromTOML.nix create mode 100644 test/testdata/eval-okay-fromjson-escapes.exp create mode 100644 test/testdata/eval-okay-fromjson-escapes.nix create mode 100644 test/testdata/eval-okay-fromjson.exp create mode 100644 test/testdata/eval-okay-fromjson.nix create mode 100644 test/testdata/eval-okay-functionargs.exp create mode 100644 test/testdata/eval-okay-functionargs.exp.xml create mode 100644 test/testdata/eval-okay-functionargs.nix create mode 100644 test/testdata/eval-okay-getattrpos-functionargs.exp create mode 100644 test/testdata/eval-okay-getattrpos-functionargs.nix create mode 100644 test/testdata/eval-okay-getattrpos-undefined.exp create mode 100644 test/testdata/eval-okay-getattrpos-undefined.nix create mode 100644 test/testdata/eval-okay-getattrpos.exp create mode 100644 test/testdata/eval-okay-getattrpos.nix create mode 100644 test/testdata/eval-okay-getenv.exp create mode 100644 test/testdata/eval-okay-getenv.nix create mode 100644 test/testdata/eval-okay-groupBy.exp create mode 100644 test/testdata/eval-okay-groupBy.nix create mode 100644 test/testdata/eval-okay-hash.exp create mode 100644 test/testdata/eval-okay-hashfile.exp create mode 100644 test/testdata/eval-okay-hashfile.nix create mode 100644 test/testdata/eval-okay-hashstring.exp create mode 100644 test/testdata/eval-okay-hashstring.nix create mode 100644 test/testdata/eval-okay-if.exp create mode 100644 test/testdata/eval-okay-if.nix create mode 100644 test/testdata/eval-okay-import.exp create mode 100644 test/testdata/eval-okay-import.nix create mode 100644 test/testdata/eval-okay-ind-string.exp create mode 100644 test/testdata/eval-okay-ind-string.nix create mode 100644 test/testdata/eval-okay-inherit-attr-pos.exp create mode 100644 test/testdata/eval-okay-inherit-attr-pos.nix create mode 100644 test/testdata/eval-okay-inherit-from.err.exp create mode 100644 test/testdata/eval-okay-inherit-from.exp create mode 100644 test/testdata/eval-okay-inherit-from.nix create mode 100644 test/testdata/eval-okay-intersectAttrs.exp create mode 100644 test/testdata/eval-okay-intersectAttrs.nix create mode 100644 test/testdata/eval-okay-let.exp create mode 100644 test/testdata/eval-okay-let.nix create mode 100644 test/testdata/eval-okay-list.exp create mode 100644 test/testdata/eval-okay-list.nix create mode 100644 test/testdata/eval-okay-listtoattrs.exp create mode 100644 test/testdata/eval-okay-listtoattrs.nix create mode 100644 test/testdata/eval-okay-logic.exp create mode 100644 test/testdata/eval-okay-logic.nix create mode 100644 test/testdata/eval-okay-map.exp create mode 100644 test/testdata/eval-okay-map.nix create mode 100644 test/testdata/eval-okay-mapattrs.exp create mode 100644 test/testdata/eval-okay-mapattrs.nix create mode 100644 test/testdata/eval-okay-merge-dynamic-attrs.exp create mode 100644 test/testdata/eval-okay-merge-dynamic-attrs.nix create mode 100644 test/testdata/eval-okay-nested-with.exp create mode 100644 test/testdata/eval-okay-nested-with.nix create mode 100644 test/testdata/eval-okay-new-let.exp create mode 100644 test/testdata/eval-okay-new-let.nix create mode 100644 test/testdata/eval-okay-null-dynamic-attrs.exp create mode 100644 test/testdata/eval-okay-null-dynamic-attrs.nix create mode 100644 test/testdata/eval-okay-overrides.exp create mode 100644 test/testdata/eval-okay-overrides.nix create mode 100644 test/testdata/eval-okay-parse-flake-ref.exp create mode 100644 test/testdata/eval-okay-parse-flake-ref.nix create mode 100644 test/testdata/eval-okay-partition.exp create mode 100644 test/testdata/eval-okay-partition.nix create mode 100644 test/testdata/eval-okay-path-string-interpolation.exp create mode 100644 test/testdata/eval-okay-path-string-interpolation.nix create mode 100644 test/testdata/eval-okay-path.exp create mode 100644 test/testdata/eval-okay-path.nix create mode 100644 test/testdata/eval-okay-pathexists.exp create mode 100644 test/testdata/eval-okay-pathexists.nix create mode 100644 test/testdata/eval-okay-patterns.exp create mode 100644 test/testdata/eval-okay-patterns.nix create mode 100644 test/testdata/eval-okay-print.err.exp create mode 100644 test/testdata/eval-okay-print.exp create mode 100644 test/testdata/eval-okay-print.nix create mode 100644 test/testdata/eval-okay-readDir.exp create mode 100644 test/testdata/eval-okay-readDir.nix create mode 100644 test/testdata/eval-okay-readFileType.exp create mode 100644 test/testdata/eval-okay-readFileType.nix create mode 100644 test/testdata/eval-okay-readfile.exp create mode 100644 test/testdata/eval-okay-readfile.nix create mode 100644 test/testdata/eval-okay-redefine-builtin.exp create mode 100644 test/testdata/eval-okay-redefine-builtin.nix create mode 100644 test/testdata/eval-okay-regex-match.exp create mode 100644 test/testdata/eval-okay-regex-match.nix create mode 100644 test/testdata/eval-okay-regex-split.exp create mode 100644 test/testdata/eval-okay-regex-split.nix create mode 100644 test/testdata/eval-okay-regression-20220122.exp create mode 100644 test/testdata/eval-okay-regression-20220122.nix create mode 100644 test/testdata/eval-okay-regression-20220125.exp create mode 100644 test/testdata/eval-okay-regression-20220125.nix create mode 100644 test/testdata/eval-okay-remove.exp create mode 100644 test/testdata/eval-okay-remove.nix create mode 100644 test/testdata/eval-okay-repeated-empty-attrs.exp create mode 100644 test/testdata/eval-okay-repeated-empty-attrs.nix create mode 100644 test/testdata/eval-okay-repeated-empty-list.exp create mode 100644 test/testdata/eval-okay-repeated-empty-list.nix create mode 100644 test/testdata/eval-okay-replacestrings.exp create mode 100644 test/testdata/eval-okay-replacestrings.nix create mode 100644 test/testdata/eval-okay-scope-1.exp create mode 100644 test/testdata/eval-okay-scope-1.nix create mode 100644 test/testdata/eval-okay-scope-2.exp create mode 100644 test/testdata/eval-okay-scope-2.nix create mode 100644 test/testdata/eval-okay-scope-3.exp create mode 100644 test/testdata/eval-okay-scope-3.nix create mode 100644 test/testdata/eval-okay-scope-4.exp create mode 100644 test/testdata/eval-okay-scope-4.nix create mode 100644 test/testdata/eval-okay-scope-6.exp create mode 100644 test/testdata/eval-okay-scope-6.nix create mode 100644 test/testdata/eval-okay-scope-7.exp create mode 100644 test/testdata/eval-okay-scope-7.nix create mode 100644 test/testdata/eval-okay-search-path.exp create mode 100644 test/testdata/eval-okay-search-path.flags create mode 100644 test/testdata/eval-okay-search-path.nix create mode 100644 test/testdata/eval-okay-seq.exp create mode 100644 test/testdata/eval-okay-seq.nix create mode 100644 test/testdata/eval-okay-sort.exp create mode 100644 test/testdata/eval-okay-sort.nix create mode 100644 test/testdata/eval-okay-splitversion.exp create mode 100644 test/testdata/eval-okay-splitversion.nix create mode 100644 test/testdata/eval-okay-string.exp create mode 100644 test/testdata/eval-okay-string.nix create mode 100644 test/testdata/eval-okay-strings-as-attrs-names.exp create mode 100644 test/testdata/eval-okay-strings-as-attrs-names.nix create mode 100644 test/testdata/eval-okay-substring-context.exp create mode 100644 test/testdata/eval-okay-substring-context.nix create mode 100644 test/testdata/eval-okay-substring.exp create mode 100644 test/testdata/eval-okay-substring.nix create mode 100644 test/testdata/eval-okay-symlink-resolution.exp create mode 100644 test/testdata/eval-okay-symlink-resolution.nix create mode 100644 test/testdata/eval-okay-tail-call-1.exp-disabled create mode 100644 test/testdata/eval-okay-tail-call-1.nix create mode 100644 test/testdata/eval-okay-tojson.exp create mode 100644 test/testdata/eval-okay-tojson.nix create mode 100644 test/testdata/eval-okay-toxml.exp create mode 100644 test/testdata/eval-okay-toxml.nix create mode 100644 test/testdata/eval-okay-toxml2.exp create mode 100644 test/testdata/eval-okay-toxml2.nix create mode 100644 test/testdata/eval-okay-tryeval.exp create mode 100644 test/testdata/eval-okay-tryeval.nix create mode 100644 test/testdata/eval-okay-types.exp create mode 100644 test/testdata/eval-okay-types.nix create mode 100644 test/testdata/eval-okay-versions.exp create mode 100644 test/testdata/eval-okay-versions.nix create mode 100644 test/testdata/eval-okay-with.exp create mode 100644 test/testdata/eval-okay-with.nix create mode 100644 test/testdata/eval-okay-xml.exp.xml create mode 100644 test/testdata/eval-okay-xml.nix create mode 100644 test/testdata/eval-okay-zipAttrsWith.exp create mode 100644 test/testdata/eval-okay-zipAttrsWith.nix create mode 100644 test/testdata/importdef.sexp create mode 100644 test/testdata/imported.nix create mode 100644 test/testdata/imported2.nix create mode 100644 test/testdata/lib.nix create mode 100644 test/testdata/non-eval-fail-bad-drvPath.nix create mode 100644 test/testdata/parse-fail-dup-attrs-1.err.exp create mode 100644 test/testdata/parse-fail-dup-attrs-1.nix create mode 100644 test/testdata/parse-fail-dup-attrs-2.err.exp create mode 100644 test/testdata/parse-fail-dup-attrs-2.nix create mode 100644 test/testdata/parse-fail-dup-attrs-3.err.exp create mode 100644 test/testdata/parse-fail-dup-attrs-3.nix create mode 100644 test/testdata/parse-fail-dup-attrs-4.err.exp create mode 100644 test/testdata/parse-fail-dup-attrs-4.nix create mode 100644 test/testdata/parse-fail-dup-attrs-7.err.exp create mode 100644 test/testdata/parse-fail-dup-attrs-7.nix create mode 100644 test/testdata/parse-fail-dup-formals.err.exp create mode 100644 test/testdata/parse-fail-dup-formals.nix create mode 100644 test/testdata/parse-fail-eof-in-string.err.exp create mode 100644 test/testdata/parse-fail-eof-in-string.nix create mode 100644 test/testdata/parse-fail-eof-pos.err.exp create mode 100644 test/testdata/parse-fail-eof-pos.nix create mode 100644 test/testdata/parse-fail-mixed-nested-attrs1.err.exp create mode 100644 test/testdata/parse-fail-mixed-nested-attrs1.nix create mode 100644 test/testdata/parse-fail-mixed-nested-attrs2.err.exp create mode 100644 test/testdata/parse-fail-mixed-nested-attrs2.nix create mode 100644 test/testdata/parse-fail-patterns-1.err.exp create mode 100644 test/testdata/parse-fail-patterns-1.nix create mode 100644 test/testdata/parse-fail-regression-20060610.err.exp create mode 100644 test/testdata/parse-fail-regression-20060610.nix create mode 100644 test/testdata/parse-fail-undef-var-2.err.exp create mode 100644 test/testdata/parse-fail-undef-var-2.nix create mode 100644 test/testdata/parse-fail-undef-var.err.exp create mode 100644 test/testdata/parse-fail-undef-var.nix create mode 100644 test/testdata/parse-fail-utf8.err.exp create mode 100644 test/testdata/parse-fail-utf8.nix create mode 100644 test/testdata/parse-okay-1.exp create mode 100644 test/testdata/parse-okay-1.nix create mode 100644 test/testdata/parse-okay-crlf.exp create mode 100644 test/testdata/parse-okay-crlf.nix create mode 100644 test/testdata/parse-okay-dup-attrs-5.exp create mode 100644 test/testdata/parse-okay-dup-attrs-5.nix create mode 100644 test/testdata/parse-okay-dup-attrs-6.exp create mode 100644 test/testdata/parse-okay-dup-attrs-6.nix create mode 100644 test/testdata/parse-okay-ind-string.exp create mode 100644 test/testdata/parse-okay-ind-string.nix create mode 100644 test/testdata/parse-okay-inherits.exp create mode 100644 test/testdata/parse-okay-inherits.nix create mode 100644 test/testdata/parse-okay-mixed-nested-attrs-1.exp create mode 100644 test/testdata/parse-okay-mixed-nested-attrs-1.nix create mode 100644 test/testdata/parse-okay-mixed-nested-attrs-2.exp create mode 100644 test/testdata/parse-okay-mixed-nested-attrs-2.nix create mode 100644 test/testdata/parse-okay-mixed-nested-attrs-3.exp create mode 100644 test/testdata/parse-okay-mixed-nested-attrs-3.nix create mode 100644 test/testdata/parse-okay-regression-20041027.exp create mode 100644 test/testdata/parse-okay-regression-20041027.nix create mode 100644 test/testdata/parse-okay-regression-751.exp create mode 100644 test/testdata/parse-okay-regression-751.nix create mode 100644 test/testdata/parse-okay-subversion.exp create mode 100644 test/testdata/parse-okay-subversion.nix create mode 100644 test/testdata/parse-okay-url.exp create mode 100644 test/testdata/parse-okay-url.nix create mode 100644 test/testdata/readDir/bar create mode 100644 test/testdata/readDir/foo/git-hates-directories create mode 120000 test/testdata/readDir/ldir create mode 120000 test/testdata/readDir/linked create mode 120000 test/testdata/symlink-resolution/broken create mode 100644 test/testdata/symlink-resolution/foo/lib/default.nix create mode 120000 test/testdata/symlink-resolution/foo/overlays create mode 100644 test/testdata/symlink-resolution/overlays/overlay.nix create mode 100644 theories/dune create mode 100644 theories/dynlang/equiv.v create mode 100644 theories/dynlang/interp.v create mode 100644 theories/dynlang/interp_proofs.v create mode 100644 theories/dynlang/operational.v create mode 100644 theories/dynlang/operational_props.v create mode 100644 theories/evallang/interp.v create mode 100644 theories/evallang/interp_proofs.v create mode 100644 theories/evallang/operational.v create mode 100644 theories/evallang/operational_props.v create mode 100644 theories/evallang/tests.v create mode 100644 theories/lambda/interp.v create mode 100644 theories/lambda/interp_proofs.v create mode 100644 theories/lambda/operational.v create mode 100644 theories/lambda/operational_props.v create mode 100644 theories/nix/floats.v create mode 100644 theories/nix/interp.v create mode 100644 theories/nix/interp_proofs.v create mode 100644 theories/nix/notations.v create mode 100644 theories/nix/operational.v create mode 100644 theories/nix/operational_props.v create mode 100644 theories/nix/tests.v create mode 100644 theories/nix/wp.v create mode 100644 theories/nix/wp_examples.v create mode 100644 theories/res.v create mode 100644 theories/utils.v diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..00ce93e --- /dev/null +++ b/.gitignore @@ -0,0 +1,22 @@ +*.aux +*.glob +*.vio +*.vo +*.vok +*.vos +.CoqMakefile.d +.Makefile.coq.d +.direnv +.lia.cache +Makefile.coq +Makefile.coq.conf +*#*.v# +*~ +_build/ +_coverage/ +_opam/ +result +mininix_history +.vscode/ +.envrc +mininix.install diff --git a/.ocamlformat b/.ocamlformat new file mode 100644 index 0000000..9ed4c26 --- /dev/null +++ b/.ocamlformat @@ -0,0 +1 @@ +version = 0.27.0 diff --git a/.ocamlformat-ignore b/.ocamlformat-ignore new file mode 100644 index 0000000..fb55689 --- /dev/null +++ b/.ocamlformat-ignore @@ -0,0 +1 @@ +lib/mininix/extraction.* diff --git a/COPYING b/COPYING new file mode 100644 index 0000000..412a78c --- /dev/null +++ b/COPYING @@ -0,0 +1,564 @@ +License information for this artifact +===================================== + +This artifact consists of a few parts. We choose to license most of +our code under the 3-clause BSD license (SPDX: BSD-3-Clause), with an +exception of the Nix test suite that we have adopted, which remains +licensed under LGPL 2.1 (SPDX: LGPL-2.1-or-later). + +Specifically: +- The following files in lib/nix/ are derived from nixformat [1] by + Denis Korzunov: + lexer.ml, nix.ml, parser.mly, printer.ml and types.ml + nixformat is licensed under ISC (SPDX: ISC). For consistency, we + choose to relicense these files under the 3-clause BSD license (as + it subsumes the ISC license). We also include a copy of the ISC + license as required. +- The files in test/testdata/ come from Nix [2] and remain licensed + under version 2.1 of the LGPL license. We also include a copy of + this license below. The only exception here is the file + test/testdata/importdef.sexp + which was created by us (and is therefore licensed under the 3-clause BSD + license). +- Any files not described by the preceding items is licensed under the + 3-clause BSD license. + +[1]: https://github.com/d2km/nixformat +[2]: https://github.com/NixOs/nix + + +The 3-clause BSD license (BSD-3-Clause) +--------------------------------------- + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + + 1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + 2. Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + 3. Neither the name of the copyright holder nor the names of its + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + + +The ISC license (ISC) +--------------------- + +Permission to use, copy, modify, and /or distribute this software for +any purpose with or without fee is hereby granted, provided that the +above copyright notice and this permission notice appear in all +copies. + +THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL +WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE +AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL +DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR +PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER +TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR +PERFORMANCE OF THIS SOFTWARE. + + +Version 2.1 of the LGPL license (LGPL-2.1-or-later) +--------------------------------------------------- + +Copyright (C) 1991, 1999 Free Software Foundation, Inc. +51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA + +Everyone is permitted to copy and distribute verbatim copies of this +license document, but changing it is not allowed. + +[This is the first released version of the Lesser GPL. It also counts +as the successor of the GNU Library Public License, version 2, hence +the version number 2.1.] + +Preamble + +The licenses for most software are designed to take away your freedom +to share and change it. By contrast, the GNU General Public Licenses +are intended to guarantee your freedom to share and change free +software--to make sure the software is free for all its users. + +This license, the Lesser General Public License, applies to some +specially designated software packages--typically libraries--of the +Free Software Foundation and other authors who decide to use it. You +can use it too, but we suggest you first think carefully about whether +this license or the ordinary General Public License is the better +strategy to use in any particular case, based on the explanations +below. + +When we speak of free software, we are referring to freedom of use, +not price. Our General Public Licenses are designed to make sure that +you have the freedom to distribute copies of free software (and charge +for this service if you wish); that you receive source code or can get +it if you want it; that you can change the software and use pieces of +it in new free programs; and that you are informed that you can do +these things. + +To protect your rights, we need to make restrictions that forbid +distributors to deny you these rights or to ask you to surrender these +rights. These restrictions translate to certain responsibilities for +you if you distribute copies of the library or if you modify it. + +For example, if you distribute copies of the library, whether gratis +or for a fee, you must give the recipients all the rights that we gave +you. You must make sure that they, too, receive or can get the source +code. If you link other code with the library, you must provide +complete object files to the recipients, so that they can relink them +with the library after making changes to the library and recompiling +it. And you must show them these terms so they know their rights. + +We protect your rights with a two-step method: (1) we copyright the +library, and (2) we offer you this license, which gives you legal +permission to copy, distribute and/or modify the library. + +To protect each distributor, we want to make it very clear that there +is no warranty for the free library. Also, if the library is modified +by someone else and passed on, the recipients should know that what +they have is not the original version, so that the original author's +reputation will not be affected by problems that might be introduced +by others. + +Finally, software patents pose a constant threat to the existence of +any free program. We wish to make sure that a company cannot +effectively restrict the users of a free program by obtaining a +restrictive license from a patent holder. Therefore, we insist that +any patent license obtained for a version of the library must be +consistent with the full freedom of use specified in this license. + +Most GNU software, including some libraries, is covered by the +ordinary GNU General Public License. This license, the GNU Lesser +General Public License, applies to certain designated libraries, and +is quite different from the ordinary General Public License. We use +this license for certain libraries in order to permit linking those +libraries into non-free programs. + +When a program is linked with a library, whether statically or using a +shared library, the combination of the two is legally speaking a +combined work, a derivative of the original library. The ordinary +General Public License therefore permits such linking only if the +entire combination fits its criteria of freedom. The Lesser General +Public License permits more lax criteria for linking other code with +the library. + +We call this license the "Lesser" General Public License because it +does Less to protect the user's freedom than the ordinary General +Public License. It also provides other free software developers Less +of an advantage over competing non-free programs. These disadvantages +are the reason we use the ordinary General Public License for many +libraries. However, the Lesser license provides advantages in certain +special circumstances. + +For example, on rare occasions, there may be a special need to +encourage the widest possible use of a certain library, so that it +becomes a de-facto standard. To achieve this, non-free programs must +be allowed to use the library. A more frequent case is that a free +library does the same job as widely used non-free libraries. In this +case, there is little to gain by limiting the free library to free +software only, so we use the Lesser General Public License. + +In other cases, permission to use a particular library in non-free +programs enables a greater number of people to use a large body of +free software. For example, permission to use the GNU C Library in +non-free programs enables many more people to use the whole GNU +operating system, as well as its variant, the GNU/Linux operating +system. + +Although the Lesser General Public License is Less protective of the +users' freedom, it does ensure that the user of a program that is +linked with the Library has the freedom and the wherewithal to run +that program using a modified version of the Library. + +The precise terms and conditions for copying, distribution and +modification follow. Pay close attention to the difference between a +"work based on the library" and a "work that uses the library". The +former contains code derived from the library, whereas the latter must +be combined with the library in order to run. + +GNU LESSER GENERAL PUBLIC LICENSE + +TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + + 0. This License Agreement applies to any software library or + other program which contains a notice placed by the copyright + holder or other authorized party saying it may be distributed + under the terms of this Lesser General Public License (also + called "this License"). Each licensee is addressed as "you". + + A "library" means a collection of software functions and/or + data prepared so as to be conveniently linked with application + programs (which use some of those functions and data) to form + executables. + + The "Library", below, refers to any such software library or + work which has been distributed under these terms. A "work + based on the Library" means either the Library or any + derivative work under copyright law: that is to say, a work + containing the Library or a portion of it, either verbatim or + with modifications and/or translated straightforwardly into + another language. (Hereinafter, translation is included + without limitation in the term "modification".) + + "Source code" for a work means the preferred form of the work + for making modifications to it. For a library, complete source + code means all the source code for all modules it contains, + plus any associated interface definition files, plus the + scripts used to control compilation and installation of the + library. + + Activities other than copying, distribution and modification + are not covered by this License; they are outside its scope. + The act of running a program using the Library is not + restricted, and output from such a program is covered only if + its contents constitute a work based on the Library + (independent of the use of the Library in a tool for writing + it). Whether that is true depends on what the Library does and + what the program that uses the Library does. 1. You may copy + and distribute verbatim copies of the Library's complete + source code as you receive it, in any medium, provided that + you conspicuously and appropriately publish on each copy an + appropriate copyright notice and disclaimer of warranty; keep + intact all the notices that refer to this License and to the + absence of any warranty; and distribute a copy of this License + along with the Library. + + You may charge a fee for the physical act of transferring a + copy, and you may at your option offer warranty protection in + exchange for a fee. + + 2. You may modify your copy or copies of the Library or any + portion of it, thus forming a work based on the Library, and + copy and distribute such modifications or work under the terms + of Section 1 above, provided that you also meet all of these + conditions: + + a) The modified work must itself be a software library. + b) You must cause the files modified to carry prominent + notices stating that you changed the files and the date of + any change. + c) You must cause the whole of the work to be licensed at no + charge to all third parties under the terms of this + License. + d) If a facility in the modified Library refers to a function + or a table of data to be supplied by an application + program that uses the facility, other than as an argument + passed when the facility is invoked, then you must make a + good faith effort to ensure that, in the event an + application does not supply such function or table, the + facility still operates, and performs whatever part of its + purpose remains meaningful. + + (For example, a function in a library to compute square roots + has a purpose that is entirely well-defined independent of the + application. Therefore, Subsection 2d requires that any + application-supplied function or table used by this function + must be optional: if the application does not supply it, the + square root function must still compute square roots.) + + These requirements apply to the modified work as a whole. If + identifiable sections of that work are not derived from the + Library, and can be reasonably considered independent and + separate works in themselves, then this License, and its + terms, do not apply to those sections when you distribute them + as separate works. But when you distribute the same sections + as part of a whole which is a work based on the Library, the + distribution of the whole must be on the terms of this + License, whose permissions for other licensees extend to the + entire whole, and thus to each and every part regardless of + who wrote it. + + Thus, it is not the intent of this section to claim rights or + contest your rights to work written entirely by you; rather, + the intent is to exercise the right to control the + distribution of derivative or collective works based on the + Library. + + In addition, mere aggregation of another work not based on the + Library with the Library (or with a work based on the Library) + on a volume of a storage or distribution medium does not bring + the other work under the scope of this License. + + 3. You may opt to apply the terms of the ordinary GNU General + Public License instead of this License to a given copy of the + Library. To do this, you must alter all the notices that refer + to this License, so that they refer to the ordinary GNU + General Public License, version 2, instead of to this License. + (If a newer version than version 2 of the ordinary GNU General + Public License has appeared, then you can specify that version + instead if you wish.) Do not make any other change in these + notices. + + Once this change is made in a given copy, it is irreversible + for that copy, so the ordinary GNU General Public License + applies to all subsequent copies and derivative works made + from that copy. + + This option is useful when you wish to copy part of the code + of the Library into a program that is not a library. + + 4. You may copy and distribute the Library (or a portion or + derivative of it, under Section 2) in object code or + executable form under the terms of Sections 1 and 2 above + provided that you accompany it with the complete corresponding + machine-readable source code, which must be distributed under + the terms of Sections 1 and 2 above on a medium customarily + used for software interchange. + + If distribution of object code is made by offering access to + copy from a designated place, then offering equivalent access + to copy the source code from the same place satisfies the + requirement to distribute the source code, even though third + parties are not compelled to copy the source along with the + object code. + + 5. A program that contains no derivative of any portion of the + Library, but is designed to work with the Library by being + compiled or linked with it, is called a "work that uses the + Library". Such a work, in isolation, is not a derivative work + of the Library, and therefore falls outside the scope of this + License. + + However, linking a "work that uses the Library" with the + Library creates an executable that is a derivative of the + Library (because it contains portions of the Library), rather + than a "work that uses the library". The executable is + therefore covered by this License. Section 6 states terms for + distribution of such executables. + + When a "work that uses the Library" uses material from a + header file that is part of the Library, the object code for + the work may be a derivative work of the Library even though + the source code is not. Whether this is true is especially + significant if the work can be linked without the Library, or + if the work is itself a library. The threshold for this to be + true is not precisely defined by law. + + If such an object file uses only numerical parameters, data + structure layouts and accessors, and small macros and small + inline functions (ten lines or less in length), then the use + of the object file is unrestricted, regardless of whether it + is legally a derivative work. (Executables containing this + object code plus portions of the Library will still fall under + Section 6.) + + Otherwise, if the work is a derivative of the Library, you may + distribute the object code for the work under the terms of + Section 6. Any executables containing that work also fall + under Section 6, whether or not they are linked directly with + the Library itself. + + 6. As an exception to the Sections above, you may also combine or + link a "work that uses the Library" with the Library to + produce a work containing portions of the Library, and + distribute that work under terms of your choice, provided that + the terms permit modification of the work for the customer's + own use and reverse engineering for debugging such + modifications. + + You must give prominent notice with each copy of the work that + the Library is used in it and that the Library and its use are + covered by this License. You must supply a copy of this + License. If the work during execution displays copyright + notices, you must include the copyright notice for the Library + among them, as well as a reference directing the user to the + copy of this License. Also, you must do one of these things: + + a) Accompany the work with the complete corresponding + machine-readable source code for the Library including + whatever changes were used in the work (which must be + distributed under Sections 1 and 2 above); and, if the + work is an executable linked with the Library, with the + complete machine-readable "work that uses the Library", as + object code and/or source code, so that the user can + modify the Library and then relink to produce a modified + executable containing the modified Library. (It is + understood that the user who changes the contents of + definitions files in the Library will not necessarily be + able to recompile the application to use the modified + definitions.) + b) Use a suitable shared library mechanism for linking with + the Library. A suitable mechanism is one that (1) uses at + run time a copy of the library already present on the + user's computer system, rather than copying library + functions into the executable, and (2) will operate + properly with a modified version of the library, if the + user installs one, as long as the modified version is + interface-compatible with the version that the work was + made with. + c) Accompany the work with a written offer, valid for at + least three years, to give the same user the materials + specified in Subsection 6a, above, for a charge no more + than the cost of performing this distribution. + d) If distribution of the work is made by offering access to + copy from a designated place, offer equivalent access to + copy the above specified materials from the same place. + e) Verify that the user has already received a copy of these + materials or that you have already sent this user a copy. + + For an executable, the required form of the "work that uses + the Library" must include any data and utility programs needed + for reproducing the executable from it. However, as a special + exception, the materials to be distributed need not include + anything that is normally distributed (in either source or + binary form) with the major components (compiler, kernel, and + so on) of the operating system on which the executable runs, + unless that component itself accompanies the executable. + + It may happen that this requirement contradicts the license + restrictions of other proprietary libraries that do not + normally accompany the operating system. Such a contradiction + means you cannot use both them and the Library together in an + executable that you distribute. + + 7. You may place library facilities that are a work based on the + Library side-by-side in a single library together with other + library facilities not covered by this License, and distribute + such a combined library, provided that the separate + distribution of the work based on the Library and of the other + library facilities is otherwise permitted, and provided that + you do these two things: + + a) Accompany the combined library with a copy of the same + work based on the Library, uncombined with any other + library facilities. This must be distributed under the + terms of the Sections above. + b) Give prominent notice with the combined library of the + fact that part of it is a work based on the Library, and + explaining where to find the accompanying uncombined form + of the same work. + + 8. You may not copy, modify, sublicense, link with, or distribute + the Library except as expressly provided under this License. + Any attempt otherwise to copy, modify, sublicense, link with, + or distribute the Library is void, and will automatically + terminate your rights under this License. However, parties who + have received copies, or rights, from you under this License + will not have their licenses terminated so long as such + parties remain in full compliance. + + 9. You are not required to accept this License, since you have + not signed it. However, nothing else grants you permission to + modify or distribute the Library or its derivative works. + These actions are prohibited by law if you do not accept this + License. Therefore, by modifying or distributing the Library + (or any work based on the Library), you indicate your + acceptance of this License to do so, and all its terms and + conditions for copying, distributing or modifying the Library + or works based on it. + + 10. Each time you redistribute the Library (or any work based on + the Library), the recipient automatically receives a license + from the original licensor to copy, distribute, link with or + modify the Library subject to these terms and conditions. You + may not impose any further restrictions on the recipients' + exercise of the rights granted herein. You are not responsible + for enforcing compliance by third parties with this License. + + 11. If, as a consequence of a court judgment or allegation of + patent infringement or for any other reason (not limited to + patent issues), conditions are imposed on you (whether by + court order, agreement or otherwise) that contradict the + conditions of this License, they do not excuse you from the + conditions of this License. If you cannot distribute so as to + satisfy simultaneously your obligations under this License and + any other pertinent obligations, then as a consequence you may + not distribute the Library at all. For example, if a patent + license would not permit royalty-free redistribution of the + Library by all those who receive copies directly or indirectly + through you, then the only way you could satisfy both it and + this License would be to refrain entirely from distribution of + the Library. + + If any portion of this section is held invalid or + unenforceable under any particular circumstance, the balance + of the section is intended to apply, and the section as a + whole is intended to apply in other circumstances. + + It is not the purpose of this section to induce you to + infringe any patents or other property right claims or to + contest validity of any such claims; this section has the sole + purpose of protecting the integrity of the free software + distribution system which is implemented by public license + practices. Many people have made generous contributions to the + wide range of software distributed through that system in + reliance on consistent application of that system; it is up to + the author/donor to decide if he or she is willing to + distribute software through any other system and a licensee + cannot impose that choice. + + This section is intended to make thoroughly clear what is + believed to be a consequence of the rest of this License. + + 12. If the distribution and/or use of the Library is restricted in + certain countries either by patents or by copyrighted + interfaces, the original copyright holder who places the + Library under this License may add an explicit geographical + distribution limitation excluding those countries, so that + distribution is permitted only in or among countries not thus + excluded. In such case, this License incorporates the + limitation as if written in the body of this License. + + 13. The Free Software Foundation may publish revised and/or new + versions of the Lesser General Public License from time to + time. Such new versions will be similar in spirit to the + present version, but may differ in detail to address new + problems or concerns. + + Each version is given a distinguishing version number. If the + Library specifies a version number of this License which + applies to it and "any later version", you have the option of + following the terms and conditions either of that version or + of any later version published by the Free Software + Foundation. If the Library does not specify a license version + number, you may choose any version ever published by the Free + Software Foundation. + + 14. If you wish to incorporate parts of the Library into other + free programs whose distribution conditions are incompatible + with these, write to the author to ask for permission. For + software which is copyrighted by the Free Software Foundation, + write to the Free Software Foundation; we sometimes make + exceptions for this. Our decision will be guided by the two + goals of preserving the free status of all derivatives of our + free software and of promoting the sharing and reuse of + software generally. + + NO WARRANTY + 15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO + WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY + APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE + COPYRIGHT HOLDERS AND/OR OTHER PARTIES PROVIDE THE LIBRARY "AS + IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED OR IMPLIED, + INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF + MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE + ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE LIBRARY + IS WITH YOU. SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME + THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN + WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY + MODIFY AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE + LIABLE TO YOU FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, + INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR + INABILITY TO USE THE LIBRARY (INCLUDING BUT NOT LIMITED TO + LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES + SUSTAINED BY YOU OR THIRD PARTIES OR A FAILURE OF THE LIBRARY + TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF SUCH HOLDER OR + OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH + DAMAGES. diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..ac8dba0 --- /dev/null +++ b/Makefile @@ -0,0 +1,55 @@ +# Default target +all: Makefile.coq + +@$(MAKE) -f Makefile.coq all +.PHONY: all + +# Permit local customization +-include Makefile.local + +# Forward most targets to Coq makefile (with some trick to make this phony) +%: Makefile.coq phony + @#echo "Forwarding $@" + +@$(MAKE) -f Makefile.coq $@ +phony: ; +.PHONY: phony + +clean: Makefile.coq + +@$(MAKE) -f Makefile.coq clean + @# Make sure not to enter the `_opam` folder. + find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true + rm -f Makefile.coq .lia.cache builddep/* +.PHONY: clean + +# Create Coq Makefile. +Makefile.coq: _CoqProject Makefile + "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES) + +# Install build-dependencies +OPAMFILES=$(wildcard *.opam) +BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES)))) + +builddep/%-builddep.opam: %.opam Makefile + @echo "# Creating builddep package for $<." + @mkdir -p builddep + @sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@ + +builddep-opamfiles: $(BUILDDEPFILES) +.PHONY: builddep-opamfiles + +builddep: builddep-opamfiles + @# We want opam to not just install the build-deps now, but to also keep satisfying these + @# constraints. Otherwise, `opam upgrade` may well update some packages to versions + @# that are incompatible with our build requirements. + @# To achieve this, we create a fake opam package that has our build-dependencies as + @# dependencies, but does not actually install anything itself. + @echo "# Installing builddep packages." + @opam install $(OPAMFLAGS) $(BUILDDEPFILES) +.PHONY: builddep + +# Backwards compatibility target +build-dep: builddep +.PHONY: build-dep + +# Some files that do *not* need to be forwarded to Makefile.coq. +# ("::" lets Makefile.local overwrite this.) +Makefile Makefile.local _CoqProject $(OPAMFILES):: ; diff --git a/README.md b/README.md new file mode 100644 index 0000000..ad7b1b7 --- /dev/null +++ b/README.md @@ -0,0 +1,383 @@ +Artifact for "Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language" +=========================================================================================================== + +This is the accompanying artifact for the following paper: +> Rutger Broekhoff and Robbert Krebbers. 2025. Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language. _Proc. ACM Program. Lang._ 9, ICFP, Article 268 (August 2025), 29 pages. https://doi.org/10.1145/3747537 + +This artifact primarily consists of two components: +1. A Rocq formalization of the languages presented in the paper (LambdaLang; § 2, DynLang; § 3, EvalLang; § 3.4, NixLang; § 4). + This includes operational semantics and properties, an interpreter and correctness proof, plus some tests and examples. +2. An OCaml front-end for NixLang (§ 5), which elaborates Nix source files into NixLang. + These are then evaluated using the NixLang interpreter, which is derived from the Rocq sources using Rocq's program extraction functionality. + +> N.B.: If you are using the VM image that we provide for evaluating the artifact, then all necessary dependencies will already be installed using `opam`. +> You can directly proceed with using the [Dune project and Makefile](#dune-project-and-makefile) or [using the CLI](#usage-of-the-cli). + +For the purposes of evaluating the artifact, we suggest the following steps: +1. [Building](#building) (this must certainly be done first). +2. Comparing that the mechanized semantics and interpreters of the defined languages match those presented in the paper. + The mechanization of all languages follows a [common structure](#structure-of-the-mechanization), but we also have a [table](#index-of-definitions-and-theories) that points you directly to the relevant definitions. +3. Comparing that the mechanized theorems correspond to those presented in the paper. + We have a [table](#index-of-definitions-and-theories) that lists all theorems in the paper and their corresponding version in the formalization. + The paper mentions some properties/proofs in passing, we list the corresponding mechanized versions for these as well (but it may be less relevant to verify these, as they are primarily used as stepping stones for the major theorems presented in the paper). +4. Exercising the Nix test suite on our interpreter and verifying that this gives the same results as presented in the paper (§ 5). +5. Trying out some Nix programs in our REPL. + The paper (§ 1, § 4.1, § 5) contains some examples that might be interesting to try out. + +You may also be interested in the [axioms used](#use-of-axioms) by the mechanization, or in reproducing the interpreter coverage number (91.77%, § 5, p. 22) and Table 1 (§ 5 p. 22). +How to do this depends on the build method that you are using, see the followings section. + +> N.B.: We have only verified this artifact to function on Linux (Arch Linux, Debian) and macOS. It does not work on Windows. + +## Building + +As mentioned at the start, this project consists of two parts: the Rocq mechanization and the front-end of the Nix interpreter. +The front-end of the Nix interpreter, which uses the makes use of the NixLang interpreter (written in Rocq, extracted to OCaml), is built using [Dune](https://dune.build/). +The Dune project also takes care of checking all of the parts of the Rocq mechanization, and extracting the NixLang interpreter to OCaml. +However, for convenience, we have a separate (classic) `Makefile` which checks only the Rocq sources (this may be more familiar to some, and will explicitly print the files being checked). +(Do note that Dune will refuse to build if the `.vo` files resulting from the checking process are not cleaned up; this can be done using `make clean`.) + +*Both parts require dependencies.* +We have two main ways of managing the dependencies of the project: either using Nix or `opam`. + +If you are familiar with Nix and have it available to you, it will likely be most easy to use. +If you are just interested in using Nix to build the project (so not directly interacting with the Dune project / Makefile), look [here](#building-with-nix). +If you are instead interested in interacting with `dune`, Makefile and/or other scripts in this repository, you should probably use the Nix devshell instead. +For that, look [here](#managing-dependencies-nix-devshell). +With the devshell set up, you can then proceed with using the [Dune project and Makefile](#dune-project-and-makefile). + +If you cannot or do not want to use Nix, there is always still `opam`. +Look [here](#managing-dependencies-opam) to see how to install project dependencies with `opam`. +With the dependencies installed using `opam`, you can then proceed with using the [Dune project and Makefile](#dune-project-and-makefile). + +### Building with Nix + +> N.B.: Only do this if you are solely interested in building/testing and/or using the artifact. If you are interested in being able to manually use the `Makefile` and Dune project, you should use a Nix devshell instead; look [here](#nix-devshell) for instructions. + +Run `nix-build` (or equivalently `nix-build ./default.nix`) to build and test the artifact. This will take a few minutes. +The resulting CLI should then be available as `./result/bin/mininix`. +See how to use the CLI [below](#usage-of-the-cli). +For some more details on the test suite, look [here](#use-of-the-nix-language-tests). + +Run `nix-build ./axioms.nix` to generate the list of axioms used by the formalization. +This is equivalent to running `make validate`. +The output of `coqchk` should be printed directly, but will also be stored at `./result/coqchk-output`. +See [below](#use-of-axioms) for more information on the axioms used. + +In the paper, we report a 91.77% coverage for the interpreter code extracted from Rocq. +To generate the coverage report, run `nix-build ./coverage.nix`. +The coverage report should then be available as `./result/coverage/report-plain` (a text file, look for `lib/extraction/interp.ml` for the interpreter coverage). +A HTML version is also generated, the report for the interpreter should then be available under `./result/coverage/html/lib/extraction/interp.ml.html`. + +To generate the line counts for the Rocq development (for comparison with Table 1 in the article), run `nix-build ./cloc.nix`. +The resulting report should be available as a text file `./result/formalization-loc-report`. + +### Managing dependencies: Nix devshell + +The Nix devshell gives you a shell where all required dependencies are installed for you, so you do not have to fiddle with `opam`, but can still use the Dune project and Makefile that we provide. +There are a few ways that you can use the devshell. + +Enter the devshell by running `nix-shell`. +You can then proceed with using the [Dune project and Makefile](#dune-project-and-makefile) *inside of the Nix devshell*. + +### Managing dependencies: opam + +First, ensure that your `opam` repositories are up-to-date: +```sh +opam update +``` + +For maximum flexibility and reproducibility, we recommend running the following +command to create a new opam switch in which the pinned dependencies are +installed (this includes the required Rocq, Flocq, Rocq-std++ versions etc.): + +```sh +# Leave out the --locked flag if not on Linux! +opam switch create ./ --repos default,rocq-released=https://rocq-prover.org/opam/released --deps-only --locked +``` + +It may be necessary to activate the newly set up opam switch as follows (if +you are not sure and opam instructs you to run this after creating the switch: +_do_ run it): + +```sh +eval $(opam env) +``` + +The [Dune project `Makefile`](#dune-project-and-makefile) can then be used as usual. + +### Dune project and `Makefile` + +#### The Makefile (just the formalization) + +If you are solely interested in the Rocq sources, you may make use of the `Makefile` to check and build Rocq sources and dependencies, provided that you have the appropriate [Rocq](https://rocq-prover.org/), [Flocq](https://flocq.gitlabpages.inria.fr/) and [Rocq-std++](https://gitlab.mpi-sws.org/iris/stdpp) versions available (8.20.1, 4.2.0/4.2.1 and 1.11.0 resp.). +When using a Nix devshell or an `opam` switch with the required dependencies installed (instructions above), this should work automatically. + +Run `make` to check all files in the formalization. +Run `make validate` to print the axioms used. +See [below](#use-of-axioms) for more information on the axioms used. + +#### The Dune project (formalization + front-end) + +> N.B.: Dune will produce errors if `.vo` files generated by the `Makefile` are present. +> Remove these by running `make clean`. +> The Dune project will then build. + +This step assumes that you have dependencies installed and available, either using `opam` or a Nix devshell. +See the relevant sections above. + +To check all proofs and build the CLI, use `dune build -p mininix`. +To then run the CLI, use `./_build/default/bin/main.exe` (see how to use it [below](#usage-of-the-cli)). +To execute the test suite, use `dune test` (this may take a few minutes). +For some more details on the test suite, look [here](#use-of-the-nix-language-tests). + +To generate the coverage report, run `./coverage.sh` (this will take a few minutes). +The report will then be printed directly (look for `lib/extraction/interp.ml`). +A detailed HTML report should also be available under `_coverage/html/lib/extraction/interp.ml.html`. + +To generate the line counts for the Rocq development (for comparison with Table 1 in the article), make sure that `cloc` and `jq` are installed (if not using the provided Nix shell). +Then run `./cloc-rocq.sh` to print the report. + +## Usage of the CLI + +Depending on how you built the CLI, it will be available to you as `./_build/default/bin/main.exe` (Dune) or `./result/bin/mininix` (Nix). +In these examples, replace `` with the actual path of the CLI binary. + +- As a Nix REPL: ` repl`. + Various meta-commands are available: `:quit`, `:run`, `:set` and `:settings`. + Autocomplete for these meta-commands is available; it is possible to cycle through suggestions using TAB. + Input can be canceled using Ctrl+C and the REPL can be quit using `:quit` or Ctrl+D. + The REPL evaluates in deep mode by default. + This can be changed by using `:set eval_strategy shallow`. + The REPL does not handle newlines in user input (a newline is processed as a request to process input). + + The expected format of user input is the Nix language (although, as mentioned in the paper, e.g. derivations are not supported). + The paper (§ 1, § 4.1, § 5) contains some examples that might be interesting to try out. +- For evaluating single files: ` eval FILENAME`. + This command evaluates in shallow mode by default. + You can change to deep mode by using the flag `-strict`. + An import tree definition file can be passed using the `-importsdef` flag. + See [below](#import-tree-definitions). + +## The Rocq mechanization + +See how to check/build the mechanization [here](#build). +This section describes the different parts of the mechanization, and how it relates to the different parts of the article. + +### Use of axioms + +See how to list the axioms used [above](#build) (look for the dependency management / build method that you are using). +(In case that you are using the Makefile (so dependencies are managed using `opam` / the Nix devshell): run `make validate`. If you are using Nix but not the devshell: use `nix-build ./axioms.nix` (the axioms used will also be written to `result/coqchk-output`).) + +Use of four axioms will be reported, namely: +``` +Coq.Logic.FunctionalExtensionality.functional_extensionality_dep +Coq.Reals.ClassicalDedekindReals.sig_not_dec +Coq.Reals.ClassicalDedekindReals.sig_forall_dec +Coq.Logic.Classical_Prop.classic +``` +*These are not axioms that we directly make use of.* +Instead, they are marked as used because we import [Flocq](https://flocq.gitlabpages.inria.fr/) (so NixLang can support IEEE 754 floating point numbers, see `theories/nix/floats.v`), which imports the classical `Reals` module from the standard library. +Running `coqchk` on the `Reals` module from the standard library gives the same list of axioms as shown above. + +### Structure of the mechanization + +There are two files that are shared by all four languages: +- `theories/res.v`: contains the `res` monad. See also Fig 2. on p. 6. +- `theories/utils.v`: contains some generic lemmas that are useful for all languages. + A decent amount of these are about finite maps, which we use heavily. + +There is a general structure for all four languages that we formalize: +- `operational.v`: the definition of the operational semantics. + + Contains an inductive type `expr` for expressions. + + Contains a `step` relation that describes the small-step op. sem. + + Contains a `subst` function that gives parallel substitution (as used by `step`). +- `operational_props.v`: properties of the operational semantics. + + Contains a lemma `step_det`, proving that the small-step op. sem. is deterministic. +- `interp.v`: the definition of the interpreter. + + Contains the definition of values `val`, thunks `thunk` and environments `env`. + + Contains an `interp` function that takes some expression, environment and amount of fuel, and returns a result (timeout, fail or some value). + (In NixLang, we end up not using `interp` directly, but instead use `interp'` which wraps `interp` and allows specifying whether to evaluate in shallow/deep mode, cf. `⟦e⟧^{δ,E}_μ` (§ 4.4, p. 19).) +- `interp_proofs.v`: soundness and completeness of interpreter w.r.t. operational semantics, in three main theorems: + + `interp_sound_complete_ret_string` (or `interp_sound_complete_ret_lit` for NixLang) proving the soundness and completeness for programs that reduce to strings (or literals in general in NixLang). + + `interp_sound_complete_fail` proving the soundness and completeness for programs that fault. + + `interp_sound_complete_no_fuel` proving the soundness and completeness for programs that loop. + For LambdaLang, an extra condition here is that the programs that we are considering must be closed. + + There is also always a generalized version of `interp_sound_complete_ret_string/lit`, namely `interp_sound_complete_ret`, which states that the interpreter is sound and complete w.r.t. the operational semantics for (in case of LambdaLang closed) programs that reduce to a value. + +Specific to the different languages are the following files: +- In `theories/dynlang` (for DynLang, § 3): + + `equiv.v`, the equivalence of LambdaLang and DynLang for closed LambdaLang terms. +- In `theories/evallang` (for EvalLang, § 3.4): + + `tests.v`, some tests of the EvalLang expression parser and interpreter. +- In `theories/nix` (for NixLang, § 4): + + `floats.v`: our Flocq instantiation with some helper functions. + + `notations.v`: some notations to make writing NixLang programs in Rocq easier. + + `tests.v`: some example NixLang programs to test the functionality of the interpreter with. + + `wp.v`: the definition of our proof-of-concept weakest precondition-based program logic, derived rules (see § 5). + + `wp_examples.v`: examples of use of our WP-based program logic (see § 5). + +### Index of definitions and theories + +**Relevant definitions.** + +| In paper | File and line number | Name | +|----------------------------------------------------|---------------------------------------|--------------------------------| +| Shared result monad (p. 6) | `theories/res.v:4` | `res` | +| LambdaLang syntax (p. 6) | `theories/lambda/operational.v:6` | `expr` | +| LambdaLang operational semantics (p. 6) | `theories/lambda/operational.v:21` | `step` | +| LambdaLang final expressions (p. 6) | `theories/lambda/operational.v:28` | `final` | +| LambdaLang parallel substitution (p. 6) | `theories/lambda/operational.v:12` | `subst` | +| LambdaLang interpreter (p. 6) | `theories/lambda/interp.v:34` | `interp` | +| LambdaLang interpreter data structures (p. 6) | `theories/lambda/interp.v:7-14` | `thunk`, `env`, `val` | +| DynLang syntax (p. 9) | `theories/dynlang/operational.v:6` | `expr` | +| DynLang operational semantics (p. 9) | `theories/dynlang/operational.v:21` | `step` | +| DynLang final expressions (p. 9) | `theories/dynlang/operational.v:31` | `final` | +| DynLang parallel substitution (p. 9) | `theories/dynlang/operational.v:12` | `subst` | +| DynLang interpreter (p. 9) | `theories/dynlang/interp.v:39` | `interp` | +| DynLang interpreter data structures (p. 9) | `theories/dynlang/interp.v:7-13` | `thunk`, `env`, `val` | +| EvalLang syntax (p. 11) | `theories/evallang/operational.v:7` | `expr` | +| EvalLang expression parser (p. 11) | `theories/evallang/operational.v:103` | `parse` | +| EvalLang operational semantics (p. 11) | `theories/evallang/operational.v:119` | `step` | +| EvalLang final expressions (p. 11) | `theories/evallang/operational.v:130` | `final` | +| EvalLang interpreter (p. 11) | `theories/evallang/interp.v:42` | `interp` | +| EvalLang interpreter data structures (p. 11) | `theories/evallang/interp.v:7-13` | `thunk`, `env`, `val` | +| NixLang syntax (p. 14) | `theories/nix/operational.v:67` | `expr` | +| NixLang operational semantics (p. 14) | `theories/nix/operational.v:444` | `step` | +| NixLang evaluation contexts (p. 14) | `theories/nix/operational.v:418` | `ctx1` | +| NixLang final expressions (p. 14) | `theories/nix/operational.v:139` | `final` | +| NixLang binary operator semantics (p. 15) | `theories/nix/operational.v:297` | `sem_bin_op` | +| NixLang argument matching (p. 15) | `theories/nix/operational.v:398` | `matches` | +| NixLang substitution (p. 15) | `theories/nix/operational.v:112` | `subst` | +| NixLang interpreter (p. 18) | `theories/nix/interp.v:329` | `interp` | +| NixLang interpreter data structures (p. 18) | `theories/nix/interp.v:5-21` | `val`, `thunk`, `tattr`, `env` | +| NixLang interpreter variant with mode arg. (p. 19) | `theories/nix/interp.v:348` | `interp'` | + +**Corresponding theorems.** + +| Theorem in paper | File and line number | Name | +|---------------------------------|---------------------------------------|------------------------------------| +| Theorem 2.1, Item 1 (p. 7) | `theories/lambda/interp_proofs.v:575` | `interp_sound_complete_ret_string` | +| Theorem 2.1, Item 2 (p. 7) | `theories/lambda/interp_proofs.v:585` | `interp_sound_complete_fail` | +| Theorem 2.1, Item 3 (p. 7) | `theories/lambda/interp_proofs.v:594` | `interp_sound_complete_no_fuel` | +| Lemma 2.2 (p. 8) | `theories/lambda/interp_proofs.v:516` | `interp_sound_open` | +| Lemma 2.3 (p. 8) | `theories/lambda/interp_proofs.v:402` | `interp_step` | +| Lemma 2.4 (p. 8) | `theories/lambda/interp_proofs.v:297` | `interp_proper` | +| Theorem 3.1, Item 1 (p. 11) | `theories/dynlang/equiv.v:120` | `interp_equiv_ret_string` | +| Theorem 3.1, Item 2 (p. 11) | `theories/dynlang/equiv.v:131` | `interp_equiv_fail` | +| Theorem 3.1, Item 3 (p. 11) | `theories/dynlang/equiv.v:142` | `interp_equiv_no_fuel` | +| Theorem 4.1, Item 1 (p. 20) (*) | `theories/nix/interp_proofs.v:2655` | `interp_sound_complete_ret_lit` | +| Theorem 4.1, Item 2 (p. 20) | `theories/nix/interp_proofs.v:2665` | `interp_sound_complete_fail` | +| Theorem 4.1, Item 3 (p. 20) | `theories/nix/interp_proofs.v:2673` | `interp_sound_complete_no_fuel` | +| Lemma 4.2 (p. 20) | `theories/nix/interp_proofs.v:2619` | `interp_sound_open'` | +| Lemma 4.3 (p. 20) | `theories/nix/interp_proofs.v:2029` | `interp_step'` | + +(*): The theorem in the formalization is stronger than the theorem presented in the paper. The latter is a trivial specialization of the former. + +**Other claims in the paper.** + +- § 2, LambdaLang: + + p. 7: Theorem 2.1, Item 1 generalizes to any final value. + See `theories/lambda/interp_proofs.v:563`, `interp_sound_complete_ret`. + This also holds for DynLang, EvalLang and NixLang. + These languages have a theory `interp_sound_complete_ret` in their respective `interp_proofs.v` files as well. + + p. 7: LambdaLang has a deterministic operational semantics. See `theories/lambda/operational_props.v:19`, `step_det`. + This also holds for DynLang, EvalLang and NixLang. + These languages have a theory `step_det` in their respective `operational_props.v` files as well. +- § 3, DynLang: + + p. 10: A variant of the main theorem of DynLang (Theorem 2.1) also holds for DynLang. + The primary difference here is that the closedness conditions are not needed for DynLang. + For a variant of Theorem 2.1, Item 1, see `theories/dynlang/interp_proofs.v:391`, `interp_sound_complete_ret_string`. + For a variant of Theorem 2.1, Item 2, see `theories/dynlang/interp_proofs.v:400`, `interp_sound_complete_fail`. + For a variant of Theorem 2.1, Item 3, see `theories/dynlang/interp_proofs.v:408`, `interp_sound_complete_no_fuel`. + A variant of the generalized version of Theorem 2.1, Item 1 also holds for DynLang. + See `theories/dynlang/interp_proofs.v:381`, `interp_sound_complete_ret`. +- § 4, NixLang: + + p. 19/20: Theorem 4.1, Item 1 generalizes to any final value. + + p. 20: Lemma 4.2 follows from mutual induction on four properties. + For these four properties and their corresponding proof, see `theories/nix/interp_proofs.v:2267-2282` (`interp_sound_open`, `interp_thunk_sound`, `interp_app_sound`, `force_deep_sound`). + + p. 20: Lemma 4.3 follows from mutual induction on two properties. + For these two properties and their corresponding proof, see `theories/nix/interp_proofs.v:1519`, `interp_step`. +- § 5, Evaluation (Program logic, p. 22): + + We can derive structural rules for WP (the application rule is presented). + See `theories/nix/wp.v:55`, `App_wp` for the presented application rule. + In general, `theories/nix/wp.v` contains all derived rules for WP. + + We prove the total correctness of three variants of the recursive program from § 4.1: + * See `theories/nix/wp_examples.v:84`, `even_rec_attr_wp'` for + ```nix + rec { f = x: if x = 0 then true else !(f (x - 1)); }.f n + ``` + * See `theories/nix/wp_examples.v:132`, `even_rec_functor_wp'` for + ```nix + { "__functor " = r: x: if x == 0 then true else !(r (x - 1)); } n + ``` + * See `theories/nix/wp_examples.v:157`, `even_rec_default_wp'` for + ```nix + ({ f ? (x: if x == 0 then true else !(f (x - 1))) }: f) {} n + ``` + + We prove the total correctness of the following program for any non-recursive attribute set `e`: + ```nix + let x = 1; in with e; with { y = 2; }; x == y + ``` + See `theories/nix/wp_examples.v:11`, `test_wp`. + +## Import tree definitions + +We do not claim to have (proper) support the `import` feature of Nix, but we do support it in a bare-bones fashion in order to be able to run the test suite. +In the test suite, there is a file `lib.nix`, which a few test cases load by using `with import ./lib.nix; ...` (or something similar). +To support this, we use a so-called import tree definition file, which pre-declares all files that may be imported. +In the test suite, for example, we have created a `test/testdata/importdef.sexp` file, which looks like this: +``` +(deps ./lib.nix) +``` +This means that the file `lib.nix` should be available to be imported for all files in the `test/testdata` folder. +Such `importdef.sexp` files are discovered automatically by walking up the directory tree from the path of the file to be evaluated (or in case of the REPL, from the current working directory). +The general syntax (``) is as follows: `(deps )`, where `` is either `` or `( )` + +In general, the primitive imports mechanism works as follows: + +- All path expressions (_e.g.,_ `./lib.nix`) in the Nix source file are converted to strings representing their absolute path. +- We load all dependencies and evaluate them to NixLang values. +- We put all of these values in a NixLang attribute set (`VAttr`, see `theories/nix/interp.v:14`), where we associate the NixLang value of each imported file with the original filename (as an absolute path). +- We then create a NixLang function `import ` (using `VClo`, see `theories/nix/interp.v:9`) that takes a string and returns the value for that file (if indeed forward-declared in the import tree definition). +- This function is then inserted into the global environment of the file that we want to evaluate. + +This process is performed recursively, hence recursive imports are also supported. + +## Use of the Nix language tests + +When exercising the official Nix language tests on our extracted interpreter, we do not exactly consider all tests in the Nix test suite. +Since we are only interested in tests for the interpreter, and not so much in tests for the parser, we only consider the `eval-*` test files in the `test/testdata` folder. +There are two types of tests that we have here: tests where evaluation should succeed, and tests where evaluation should fail. +This is simply marked in the filename; Nix files that should fail to evaluate are named `eval-fail-*.nix` and files that should evaluate successfully are named `eval-okay-*.nix`. +For the former, there are expected error outputs that the interpreter should produce, but we are not interested in reproducing these (nor would this be realistic with our setup). + +For the latter, there are also expected output expressions, which can be found in matching `eval-okay-*.exp`. +However, there are two `eval-okay-*.nix` files for which no such matching `eval-okay-*.exp` file exists: +- `eval-okay-tail-call-1.nix`: a file `eval-okay-tail-call-1.exp-disabled` exists; we hence do not consider this test. +- `eval-okay-xml.nix`: a file `eval-okay-xml.exp.xml` exists, but we are not interested in converting the resulting term to XML to validate the result of this test. + +The total amount of `eval-fail-*.nix` files and pairs of `eval-okay-*.nix` and `eval-okay-*.exp` files informs our total count of interpreter tests that we consider to begin with, namely 182 (§ 5, p. 21). +For these tests again, we explicitly list 74 tests that should be ignored in `./test/test_mininix.ml`, since they cover functionality of Nix that is out of scope for our paper. +We end up with 108 tests that we exercise our interpreter on. +Our interpreter passes 103 of these tests, and times out for five tests due to its call-by-name nature. +Some more details can be found in the paper, in § 5. + +## General project structure + +- The `theories` folder contains the Rocq formalization. See the [structure of the mechanization](#structure-of-the-mechanization). +- The `bin` folder contains the entrypoint for the command-line interface. +- The `lib` folder contains the Nix parser, elaborator and interpreter extraction + + The `nix` subfolder contains an adapted version of the parser and pretty-printer from nixformat (licensed under ISC) by Denis Korzunov. + See https://github.com/d2km/nixformat. + Some improvements were made to the parser and pretty-printer. + The file `elaborator.ml`, not part of nixformat, in this folder is concerned with desugaring attribute paths among other things; you may consider this a 'normalizing' stage, which allows the elaborator to our core language to be more concise. + + The `mininix` subfolder is the most important here. It contains, among + other files: + - `nix2mininix.ml`, elaboration of Nix into our core language + - `builtins.nix`, our implementation of builtins in Nix, in our core Nix language, where we liberally use 'core' builtins (available as binary operations) that are specific to the core language + - `conv.ml`, conversion between numeric types in OCaml and Rocq/Flocq + - `import.ml`, very bare-bones support for imports, used in the test suite + + The `extraction` folder contains a file that extracts the core language interpreter and some auxiliary functions to OCaml +- The `explorer` folder contains some utilities for converting the Rocq Mechanization to a static site. diff --git a/_CoqProject b/_CoqProject new file mode 100644 index 0000000..49e7e24 --- /dev/null +++ b/_CoqProject @@ -0,0 +1,31 @@ +-Q theories mininix + +theories/utils.v +theories/res.v + +theories/lambda/operational.v +theories/lambda/operational_props.v +theories/lambda/interp.v +theories/lambda/interp_proofs.v + +theories/dynlang/operational.v +theories/dynlang/operational_props.v +theories/dynlang/interp.v +theories/dynlang/interp_proofs.v +theories/dynlang/equiv.v + +theories/evallang/operational.v +theories/evallang/operational_props.v +theories/evallang/interp.v +theories/evallang/interp_proofs.v +theories/evallang/tests.v + +theories/nix/floats.v +theories/nix/operational.v +theories/nix/operational_props.v +theories/nix/interp.v +theories/nix/notations.v +theories/nix/tests.v +theories/nix/interp_proofs.v +theories/nix/wp.v +theories/nix/wp_examples.v diff --git a/axioms.nix b/axioms.nix new file mode 100644 index 0000000..1bdbefb --- /dev/null +++ b/axioms.nix @@ -0,0 +1,22 @@ +{ pkgs ? import ./nixpkgs-pinned.nix {} }: with pkgs; + +stdenv.mkDerivation { + name = "mininix-axioms"; + + src = ./.; + + nativeBuildInputs = [ coq_8_20 ]; + buildInputs = (with coqPackages_8_20; [ + flocq + stdpp + ]); + + buildPhase = '' + make validate 2>&1 | tee coqchk-output + ''; + + installPhase = '' + mkdir -p $out + mv coqchk-output $out + ''; +} diff --git a/bin/dune b/bin/dune new file mode 100644 index 0000000..2a56b29 --- /dev/null +++ b/bin/dune @@ -0,0 +1,14 @@ +(executable + (public_name mininix) + (name main) + (preprocess + (pps ppx_let)) + (libraries + nix + core + core_unix.command_unix + linenoise + mininix + sexp_pretty + stdio + ppx_let)) diff --git a/bin/main.ml b/bin/main.ml new file mode 100644 index 0000000..e4ca4b9 --- /dev/null +++ b/bin/main.ml @@ -0,0 +1,26 @@ +open Core + +let repl = + Command.basic ~summary:"run the Mininix REPL" (Command.Param.return Repl.run) + +let eval = + Command.basic ~summary:"run a Nix file" + (let%map_open.Command filename = anon ("FILENAME" %: string) + and strict = flag "strict" no_arg ~doc:"use deep evaluation strategy" + and importsdef = + flag "importsdef" (optional string) ~doc:"import tree definition file" + in + fun () -> + Settings.opts.eval_strategy := if strict then `Deep else `Shallow; + Settings.opts.imports_def_file := importsdef; + let ok = + if String.(filename = "-") then Run.eval_stdin () + else Run.eval_file filename + in + if ok then exit 0 else exit 1) + +let main = + Command.group ~summary:"the Mininix interpreter" + [ ("repl", repl); ("eval", eval) ] + +let () = Command_unix.run main diff --git a/bin/repl.ml b/bin/repl.ml new file mode 100644 index 0000000..092c503 --- /dev/null +++ b/bin/repl.ml @@ -0,0 +1,52 @@ +open Core +open Option.Let_syntax + +let ok = ref true +let opts = Settings.opts + +let rec user_input cb = + let prompt = (if !ok then "[okay]" else "[fail]") ^ " (mini)nix> " in + try + match LNoise.linenoise prompt with + | None -> () + | Some v -> + cb v; + user_input cb + with Sys_unix.Break -> + printf "\n%!"; + user_input cb + +let split_cmd_prefix cmd = + let%bind cmd = String.chop_prefix ~prefix:":" cmd in + let cmd' = Repl_cmd.lstrip_space cmd in + let space = String.chop_suffix_exn cmd ~suffix:cmd' in + return (":" ^ space, cmd') + +let handle_cmd cmd = + let cmd = Repl_cmd.strip_space cmd in + (match split_cmd_prefix cmd with + | Some (_, cmd) -> ok := Repl_cmd.invoke cmd + | None -> + if String.(strip cmd <> "") then + ok := Run.eval_expr cmd ~origin:Interactive); + printf "\n%!" + +let run () = + LNoise.set_multiline true; + LNoise.history_load ~filename:"mininix_history" |> ignore; + LNoise.history_set ~max_length:500 |> ignore; + LNoise.set_hints_callback (fun line -> + let%bind _, cmd = split_cmd_prefix line in + let%bind hint = Repl_cmd.hint cmd in + return (hint, LNoise.Yellow, true)); + LNoise.set_completion_callback (fun line_so_far completions -> + match split_cmd_prefix line_so_far with + | Some (prefix, cmd_so_far) -> + Repl_cmd.complete cmd_so_far + |> List.map ~f:(String.append prefix) + |> List.iter ~f:(LNoise.add_completion completions) + | None -> ()); + user_input (fun from_user -> + LNoise.history_add from_user |> ignore; + LNoise.history_save ~filename:"mininix_history" |> ignore; + handle_cmd from_user) diff --git a/bin/repl_cmd.ml b/bin/repl_cmd.ml new file mode 100644 index 0000000..9ebeae7 --- /dev/null +++ b/bin/repl_cmd.ml @@ -0,0 +1,178 @@ +open Core +open Option.Let_syntax + +let join_str_list ~sep = function + | [] -> "" + | s :: ss -> List.fold ss ~init:s ~f:(fun acc s -> acc ^ sep ^ s) + +type cmd = { + args : string; + opts : unit -> string list; + next : (string -> (string, cmd) Either.t) option; + call : string list -> bool; +} + +let set_opt_cmd opt setting = + { + args = "