From 828bdcc6b92863e71d2355eec4c5412619ec3187 Mon Sep 17 00:00:00 2001 From: ascandone Date: Tue, 13 Oct 2026 18:06:38 +0200 Subject: [PATCH 1/2] feat(prove): prove properties of a script for every initial balance Adds `numscript prove`: the compiled IR (or a hand-written .ir file) is encoded into an SMT-LIB2 model of its run over free initial balances, a property written in a small boolean DSL is negated and checked with z3 (or any SMT-LIB2 solver), and a model is replayed on the real VM before being reported as a counterexample. - internal/prove/smt: Int/Bool term AST with constant folding, printer, script builder, solver subprocess driver, concrete evaluator - internal/prove/encode: one pass over the IR in text order with state copies per branch and ite merges at labels; balances as free Ints, the funds queue as one slot per pull, marks as candidate-guard frames, fail sites as guarded flags, portions as rational linear forms so the logic stays QF_LIA; VM replay and model/VM comparison - internal/prove/prop: the property language (before/after/sent/ received/moved/delta, success/fails, min/max, and/or/not/=>/<=>) - internal/prove: orchestration, reachability queries, pretty and JSON reports, exit codes - `numscript ir`: dumps the compiled textual IR; compiler.CompileToIR - fixtures under internal/prove/testdata/cases; a differential sweep that evaluates the model at concrete balances against the VM over the spec corpus and hand-written IR; a Prove CI job with z3 --- .github/workflows/main.yml | 15 + flake.nix | 1 + internal/cmd/ir.go | 89 +++ internal/cmd/ir_test.go | 42 ++ internal/cmd/prove.go | 214 ++++++ internal/cmd/prove_test.go | 73 ++ internal/cmd/root.go | 2 +- internal/compiler/compiler.go | 27 +- .../encode/__snapshots__/encode_test.snap | 27 + internal/prove/encode/encode.go | 630 ++++++++++++++++++ internal/prove/encode/encode_test.go | 123 ++++ internal/prove/encode/funds.go | 217 ++++++ internal/prove/encode/funds_ir_test.go | 222 ++++++ internal/prove/encode/problem.go | 245 +++++++ internal/prove/encode/replay.go | 282 ++++++++ internal/prove/encode/state.go | 318 +++++++++ internal/prove/encode/sweep_test.go | 157 +++++ internal/prove/encode/values.go | 159 +++++ internal/prove/prop/ast.go | 140 ++++ internal/prove/prop/dump.go | 87 +++ internal/prove/prop/dump_test.go | 93 +++ internal/prove/prop/eval.go | 97 +++ internal/prove/prop/eval_test.go | 79 +++ internal/prove/prop/helpers_test.go | 106 +++ internal/prove/prop/lexer.go | 265 ++++++++ internal/prove/prop/lower.go | 102 +++ internal/prove/prop/lower_test.go | 42 ++ internal/prove/prop/parser.go | 402 +++++++++++ internal/prove/prop/parser_test.go | 144 ++++ internal/prove/prop/typecheck.go | 244 +++++++ internal/prove/prop/typecheck_test.go | 105 +++ internal/prove/prove.go | 207 ++++++ internal/prove/prove_test.go | 159 +++++ internal/prove/report.go | 226 +++++++ internal/prove/result.go | 93 +++ internal/prove/smt/eval.go | 172 +++++ internal/prove/smt/print.go | 71 ++ internal/prove/smt/script.go | 109 +++ internal/prove/smt/sexpr.go | 156 +++++ internal/prove/smt/smt_test.go | 133 ++++ internal/prove/smt/solver.go | 174 +++++ internal/prove/smt/term.go | 383 +++++++++++ internal/prove/testdata/cases/allotment.num | 7 + .../testdata/cases/allotment.num.expected | 4 + .../prove/testdata/cases/allotment.num.props | 5 + .../prove/testdata/cases/capped-source.num | 7 + .../testdata/cases/capped-source.num.expected | 5 + .../testdata/cases/capped-source.num.props | 5 + internal/prove/testdata/cases/hand-written.ir | 11 + .../testdata/cases/hand-written.ir.expected | 3 + .../testdata/cases/hand-written.ir.props | 3 + internal/prove/testdata/cases/kept.num | 7 + .../prove/testdata/cases/kept.num.expected | 3 + internal/prove/testdata/cases/kept.num.props | 3 + .../prove/testdata/cases/negative-amount.num | 4 + .../cases/negative-amount.num.expected | 1 + .../testdata/cases/negative-amount.num.props | 1 + .../prove/testdata/cases/oneof-source.num | 6 + .../testdata/cases/oneof-source.num.expected | 5 + .../testdata/cases/oneof-source.num.props | 6 + .../prove/testdata/cases/save-then-send.num | 6 + .../cases/save-then-send.num.expected | 3 + .../testdata/cases/save-then-send.num.props | 3 + internal/prove/testdata/cases/send-all.num | 4 + .../testdata/cases/send-all.num.expected | 3 + .../prove/testdata/cases/send-all.num.props | 3 + internal/prove/testdata/cases/simple-send.num | 4 + .../testdata/cases/simple-send.num.expected | 7 + .../testdata/cases/simple-send.num.props | 9 + internal/prove/testdata/cases/uses-vars.num | 8 + .../testdata/cases/uses-vars.num.expected | 1 + .../prove/testdata/cases/uses-vars.num.props | 1 + internal/prove/testdata/cases/vacuous.num | 7 + .../prove/testdata/cases/vacuous.num.expected | 2 + .../prove/testdata/cases/vacuous.num.props | 4 + .../prove/testdata/cases/world-source.num | 4 + .../testdata/cases/world-source.num.expected | 3 + .../testdata/cases/world-source.num.props | 3 + 78 files changed, 6784 insertions(+), 9 deletions(-) create mode 100644 internal/cmd/ir.go create mode 100644 internal/cmd/ir_test.go create mode 100644 internal/cmd/prove.go create mode 100644 internal/cmd/prove_test.go create mode 100755 internal/prove/encode/__snapshots__/encode_test.snap create mode 100644 internal/prove/encode/encode.go create mode 100644 internal/prove/encode/encode_test.go create mode 100644 internal/prove/encode/funds.go create mode 100644 internal/prove/encode/funds_ir_test.go create mode 100644 internal/prove/encode/problem.go create mode 100644 internal/prove/encode/replay.go create mode 100644 internal/prove/encode/state.go create mode 100644 internal/prove/encode/sweep_test.go create mode 100644 internal/prove/encode/values.go create mode 100644 internal/prove/prop/ast.go create mode 100644 internal/prove/prop/dump.go create mode 100644 internal/prove/prop/dump_test.go create mode 100644 internal/prove/prop/eval.go create mode 100644 internal/prove/prop/eval_test.go create mode 100644 internal/prove/prop/helpers_test.go create mode 100644 internal/prove/prop/lexer.go create mode 100644 internal/prove/prop/lower.go create mode 100644 internal/prove/prop/lower_test.go create mode 100644 internal/prove/prop/parser.go create mode 100644 internal/prove/prop/parser_test.go create mode 100644 internal/prove/prop/typecheck.go create mode 100644 internal/prove/prop/typecheck_test.go create mode 100644 internal/prove/prove.go create mode 100644 internal/prove/prove_test.go create mode 100644 internal/prove/report.go create mode 100644 internal/prove/result.go create mode 100644 internal/prove/smt/eval.go create mode 100644 internal/prove/smt/print.go create mode 100644 internal/prove/smt/script.go create mode 100644 internal/prove/smt/sexpr.go create mode 100644 internal/prove/smt/smt_test.go create mode 100644 internal/prove/smt/solver.go create mode 100644 internal/prove/smt/term.go create mode 100644 internal/prove/testdata/cases/allotment.num create mode 100644 internal/prove/testdata/cases/allotment.num.expected create mode 100644 internal/prove/testdata/cases/allotment.num.props create mode 100644 internal/prove/testdata/cases/capped-source.num create mode 100644 internal/prove/testdata/cases/capped-source.num.expected create mode 100644 internal/prove/testdata/cases/capped-source.num.props create mode 100644 internal/prove/testdata/cases/hand-written.ir create mode 100644 internal/prove/testdata/cases/hand-written.ir.expected create mode 100644 internal/prove/testdata/cases/hand-written.ir.props create mode 100644 internal/prove/testdata/cases/kept.num create mode 100644 internal/prove/testdata/cases/kept.num.expected create mode 100644 internal/prove/testdata/cases/kept.num.props create mode 100644 internal/prove/testdata/cases/negative-amount.num create mode 100644 internal/prove/testdata/cases/negative-amount.num.expected create mode 100644 internal/prove/testdata/cases/negative-amount.num.props create mode 100644 internal/prove/testdata/cases/oneof-source.num create mode 100644 internal/prove/testdata/cases/oneof-source.num.expected create mode 100644 internal/prove/testdata/cases/oneof-source.num.props create mode 100644 internal/prove/testdata/cases/save-then-send.num create mode 100644 internal/prove/testdata/cases/save-then-send.num.expected create mode 100644 internal/prove/testdata/cases/save-then-send.num.props create mode 100644 internal/prove/testdata/cases/send-all.num create mode 100644 internal/prove/testdata/cases/send-all.num.expected create mode 100644 internal/prove/testdata/cases/send-all.num.props create mode 100644 internal/prove/testdata/cases/simple-send.num create mode 100644 internal/prove/testdata/cases/simple-send.num.expected create mode 100644 internal/prove/testdata/cases/simple-send.num.props create mode 100644 internal/prove/testdata/cases/uses-vars.num create mode 100644 internal/prove/testdata/cases/uses-vars.num.expected create mode 100644 internal/prove/testdata/cases/uses-vars.num.props create mode 100644 internal/prove/testdata/cases/vacuous.num create mode 100644 internal/prove/testdata/cases/vacuous.num.expected create mode 100644 internal/prove/testdata/cases/vacuous.num.props create mode 100644 internal/prove/testdata/cases/world-source.num create mode 100644 internal/prove/testdata/cases/world-source.num.expected create mode 100644 internal/prove/testdata/cases/world-source.num.props diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index cb7320eb..cef21501 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -74,3 +74,18 @@ jobs: - name: difftest regressions and differential sweep working-directory: internal/difftest run: go test ./... + + # The prover's solver-backed tests skip when z3 is missing, so they need a + # job that installs it and makes a missing solver a failure. + Prove: + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - uses: actions/checkout@v7 + - uses: actions/setup-go@v7 + with: + go-version-file: go.mod + - name: install z3 + run: sudo apt-get update && sudo apt-get install -y z3 + - name: prover tests + run: NUMSCRIPT_REQUIRE_Z3=1 go test ./internal/prove/... ./internal/cmd/... diff --git a/flake.nix b/flake.nix index 5d0fd199..2c1d1fde 100644 --- a/flake.nix +++ b/flake.nix @@ -47,6 +47,7 @@ goperf gotools just + z3 ]; unstablePackages = with pkgs-unstable; [ golangci-lint diff --git a/internal/cmd/ir.go b/internal/cmd/ir.go new file mode 100644 index 00000000..f11cfa67 --- /dev/null +++ b/internal/cmd/ir.go @@ -0,0 +1,89 @@ +package cmd + +import ( + "fmt" + "os" + + "github.com/formancehq/numscript/internal/compiler" + "github.com/formancehq/numscript/internal/ir" + "github.com/formancehq/numscript/internal/parser" + + "github.com/spf13/cobra" +) + +type IRArgs struct { + OutputPath string +} + +// compileScriptToIR reads a numscript source file and compiles it to IR, +// printing parse and compile errors on stderr the way `run` does. +func compileScriptToIR(scriptPath string) ([]ir.Instr, error) { + content, err := readIRSource(scriptPath) + if err != nil { + return nil, err + } + src := string(content) + + parseResult := parser.Parse(src) + if len(parseResult.Errors) != 0 { + fmt.Fprint(os.Stderr, parser.ParseErrorsToString(parseResult.Errors, src)) + return nil, fmt.Errorf("parsing failed") + } + + instrs, _, err := compiler.CompileToIR(parseResult.Value, nil) + if err != nil { + fmt.Fprintln(os.Stderr, err.Error()) + if ranged, ok := err.(parser.Ranged); ok { + fmt.Fprintln(os.Stderr, ranged.GetRange().ShowOnSource(src)) + } + return nil, fmt.Errorf("compilation failed") + } + return instrs, nil +} + +func dumpIR(scriptPath string, opts IRArgs) error { + instrs, err := compileScriptToIR(scriptPath) + if err != nil { + return err + } + + text := ir.Dump(instrs) + if opts.OutputPath == "" || opts.OutputPath == stdioPath { + _, err := os.Stdout.WriteString(text) + return err + } + return os.WriteFile(opts.OutputPath, []byte(text), 0o644) +} + +func getIRCmd() *cobra.Command { + opts := IRArgs{} + + cmd := cobra.Command{ + Use: "ir ", + Short: "Compile a numscript file and dump its textual IR", + Long: `Compile a numscript file and dump the textual IR the compiler produces, before +it is assembled into bytecode. The output goes to stdout unless --output says +otherwise, so it can be piped into assemble: +numscript ir folder/my-script.num | numscript assemble - > folder/my-script.numb + +Pass - as the path to read the script from stdin. + +The IR format tracks an unstable instruction set and is not a public interface. +`, + Args: cobra.ExactArgs(1), + RunE: func(cmd *cobra.Command, args []string) error { + err := dumpIR(args[0], opts) + if err != nil { + cmd.SilenceErrors = true + cmd.SilenceUsage = true + return err + } + + return nil + }, + } + + cmd.Flags().StringVarP(&opts.OutputPath, "output", "o", "", "Path where to write the IR ('-' for stdout)") + + return &cmd +} diff --git a/internal/cmd/ir_test.go b/internal/cmd/ir_test.go new file mode 100644 index 00000000..3d6fe6f6 --- /dev/null +++ b/internal/cmd/ir_test.go @@ -0,0 +1,42 @@ +package cmd + +import ( + "os" + "path/filepath" + "testing" + + "github.com/formancehq/numscript/internal/ir" + "github.com/stretchr/testify/require" +) + +func TestDumpIRRoundTrips(t *testing.T) { + dir := t.TempDir() + scriptPath := filepath.Join(dir, "x.num") + require.NoError(t, os.WriteFile(scriptPath, []byte(`send [USD/2 10] ( + source = @src + destination = @dest +)`), 0o644)) + + outPath := filepath.Join(dir, "x.ir") + require.NoError(t, dumpIR(scriptPath, IRArgs{OutputPath: outPath})) + + text, err := os.ReadFile(outPath) + require.NoError(t, err) + + instrs, errs := ir.Parse(string(text)) + require.Empty(t, errs) + require.Equal(t, string(text), ir.Dump(instrs)) + require.NoError(t, ir.Typecheck(instrs)) +} + +func TestDumpIRReportsCompileErrors(t *testing.T) { + dir := t.TempDir() + scriptPath := filepath.Join(dir, "x.num") + require.NoError(t, os.WriteFile(scriptPath, []byte(`send [USD/2 10] ( + source = @src + destination = $dest +)`), 0o644)) + + err := dumpIR(scriptPath, IRArgs{OutputPath: filepath.Join(dir, "x.ir")}) + require.EqualError(t, err, "compilation failed") +} diff --git a/internal/cmd/prove.go b/internal/cmd/prove.go new file mode 100644 index 00000000..609ec51d --- /dev/null +++ b/internal/cmd/prove.go @@ -0,0 +1,214 @@ +package cmd + +import ( + "context" + "errors" + "fmt" + "os" + "path/filepath" + "strings" + "time" + + "github.com/formancehq/numscript/internal/ir" + "github.com/formancehq/numscript/internal/prove" + "github.com/formancehq/numscript/internal/prove/encode" + "github.com/formancehq/numscript/internal/prove/prop" + "github.com/formancehq/numscript/internal/prove/smt" + + "github.com/spf13/cobra" +) + +type ProveArgs struct { + Props []string + PropsPath string + Solver string + Timeout time.Duration + EmitSMT string + OutFormatOpt string +} + +// exitCodeError carries the exit code the prove command ends with. +type exitCodeError struct { + code int +} + +func (e exitCodeError) Error() string { return fmt.Sprintf("exit %d", e.code) } + +func loadInstrs(scriptPath string) ([]ir.Instr, error) { + if !strings.HasSuffix(scriptPath, ".ir") { + return compileScriptToIR(scriptPath) + } + content, err := readIRSource(scriptPath) + if err != nil { + return nil, err + } + src := string(content) + instrs, irErrs := ir.Parse(src) + if len(irErrs) != 0 { + for _, irErr := range irErrs { + fmt.Fprintln(os.Stderr, irErr.Error()) + fmt.Fprintln(os.Stderr, irErr.Range.ShowOnSource(src)) + } + return nil, fmt.Errorf("parsing failed") + } + return instrs, nil +} + +func loadProps(scriptPath string, opts ProveArgs) ([]prop.Property, error) { + var props []prop.Property + for i, src := range opts.Props { + p, errs := prop.ParseInline(src) + if len(errs) != 0 { + for _, e := range errs { + fmt.Fprintf(os.Stderr, "--prop[%d]: %s\n", i+1, e.Error()) + fmt.Fprintln(os.Stderr, e.Range.ShowOnSource(src)) + } + return nil, fmt.Errorf("invalid property") + } + if p.Name == "" { + p.Name = fmt.Sprintf("prop%d", i+1) + } + props = append(props, p) + } + + path := opts.PropsPath + if path == "" && len(opts.Props) == 0 { + path = scriptPath + ".props" + if _, err := os.Stat(path); err != nil { + return nil, fmt.Errorf("no properties: pass --prop, or create '%s'", path) + } + } + if path != "" { + content, err := os.ReadFile(path) + if err != nil { + return nil, err + } + src := string(content) + parsed, errs := prop.ParseFile(src) + if len(errs) != 0 { + for _, e := range errs { + fmt.Fprintf(os.Stderr, "%s:%s\n", path, e.Error()) + fmt.Fprintln(os.Stderr, e.Range.ShowOnSource(src)) + } + return nil, fmt.Errorf("invalid properties file") + } + props = append(props, parsed...) + } + return props, nil +} + +func proveScript(scriptPath string, opts ProveArgs) error { + instrs, err := loadInstrs(scriptPath) + if err != nil { + return err + } + props, err := loadProps(scriptPath, opts) + if err != nil { + return err + } + + solver := smt.Solver{Path: opts.Solver, Timeout: opts.Timeout} + if err := solver.Available(); err != nil { + return err + } + + report, err := prove.Check(context.Background(), instrs, props, prove.Options{Solver: solver}) + if err != nil { + var unsupported encode.UnsupportedError + var propErr prove.PropertyError + switch { + case errors.As(err, &unsupported): + return fmt.Errorf("cannot prove: %w", err) + case errors.As(err, &propErr): + for _, e := range propErr.Errors { + fmt.Fprintf(os.Stderr, "property %q: %s\n", propErr.Property.Name, e.Error()) + } + return fmt.Errorf("invalid property") + } + return err + } + + if opts.EmitSMT != "" { + for _, res := range report.Results { + if opts.EmitSMT == stdioPath { + fmt.Printf("; ---- %s\n%s\n", res.Property.Name, res.SMT) + continue + } + if err := os.MkdirAll(opts.EmitSMT, 0o755); err != nil { + return err + } + if err := os.WriteFile(filepath.Join(opts.EmitSMT, res.Property.Name+".smt2"), []byte(res.SMT), 0o644); err != nil { + return err + } + } + } + + switch opts.OutFormatOpt { + case OutputFormatJson: + out, err := report.JSON(scriptPath) + if err != nil { + return err + } + if _, err := os.Stdout.Write(out); err != nil { + return err + } + case OutputFormatPretty: + if _, err := os.Stdout.WriteString(report.Pretty(scriptPath)); err != nil { + return err + } + default: + return fmt.Errorf("invalid output format: %s", opts.OutFormatOpt) + } + + if code := report.ExitCode(); code != 0 { + return exitCodeError{code} + } + return nil +} + +func getProveCmd() *cobra.Command { + opts := ProveArgs{} + + cmd := cobra.Command{ + Use: "prove ", + Short: "Prove properties of a script for every initial balance", + Long: `Compile a numscript file (or parse a textual IR file) and check properties +written in the property language against it, for every initial balance. Each +property is either proved, refuted with a counterexample (initial balances the +real vm confirms), or left unknown when the solver times out. + +Properties come from --prop (repeatable) and/or --props ; with neither, +'