From f716a48f271a5cfa2ff3c26f7e4dfb75180800a8 Mon Sep 17 00:00:00 2001 From: David Pearce Date: Fri, 13 Dec 2024 15:37:35 +1300 Subject: [PATCH] feat: implement corset type checker (#431) * Add Tests for Typing This adds a small number of valid and invalid tests for checking typing. * Distinguish loobean / boolean semantics Whilst this is a fairly esoteric part of the corset language, it is nevertheless necessary to implement in order to faithly recreate the language's semantics. * Support primitive type inference This puts in place a fairly primitive form of type inference, which doesn't really do anything at this time. However, most of the machinery is now in place... * Enable Resolution of If This puts in place the ability to resolve an if as either an if-zero or an if-notzero depending on whether the condition is loobean or boolean. In the case that it is neither, then an error is reported. At this stage, however, the mechanism for infering the type of an arbitrary expression remains somewhat limited. * Enable checking guards are boolean This adds support for checking that guards have boolean semantics. For now, checking constraints have loobean semantics is implemented but not enabled. The problem is that it breaks a lot of the existing tests! * Fix (now broken) tests This fixes a number of tests which have been broken as a result of the introduced type checking process. The biggest issue here is that we really need the ability to put return types on functions in order to resolve some situations. * Support Function Return Types This adds support for function return types, and updates a larger number of tests to use "vanishes!" to meet the loobean requirements for a constraint. This also relaxes the rules for combining types for addition and subtraction, following what corset does. In addition, this introduces a very minimal standard library which (at this time) includes only the "vanishes" declaration. * Rework Memory Example This reworks the memory example so that it now: (a) compiles; (b) makes use of the stdlib (what there is of it) to improve the overall look. There is an outstanding issue related to the return types of functions. Specifically, it seems that corset infers the return type when it is not specified. * Implement type inference This puts in place a naive algorithm for type inference of function invocations. Its somewhat awkward, but it reflects the original corset language. * Support type inference through invocations The corset language supports an interesting notion of type inference in the case that a function is declared without an explicit return type being given. Specifically, it types it polymorphically at the call site based on the types of the given arguments. * Fix Declaration Finalisation This fixes some problems with the existing finalisation algorithm. Firstly, it was sometimes finalising things more than once (which is wasteful). Secondly, it was not finalising at a fine-enough granularity (which caused problems for constant definitions which referred to themself). Finally, there were still some gremlins related to binding. * Fixes for Quick Tests This puts through various minor fixes for the quick tests. What remains now is to update the larger tests. At this stage, performance may be starting to become an issue. * Update standard library This pulls over as much of the original corset standard library as possible at the moment (which is actually most of it). There are a couple of outstanding issues to be resolved around overloading, etc. * Update Slow Tests This updates the slow test to be almost exactly as they were original defined (i.e. using the full corset syntax). At this stage, there are a number of outstanding issues which remain, and some of the tests have parts commented out. --- cmd/testgen/main.go | 2 +- pkg/cmd/check.go | 7 +- pkg/cmd/debug.go | 4 +- pkg/cmd/test.go | 4 +- pkg/cmd/util.go | 9 +- pkg/corset/binding.go | 76 +++- pkg/corset/compiler.go | 27 +- pkg/corset/{ast.go => declaration.go} | 210 +++++++++- pkg/corset/{expr.go => expression.go} | 44 +- pkg/corset/parser.go | 183 ++++++--- pkg/corset/resolver.go | 290 ++++++++----- pkg/corset/scope.go | 32 +- pkg/corset/stdlib.lisp | 137 ++++++ pkg/corset/symbol.go | 15 +- pkg/corset/translator.go | 33 +- pkg/corset/type.go | 173 ++++++++ pkg/schema/type.go | 2 +- pkg/sexp/parser.go | 2 + pkg/test/invalid_corset_test.go | 43 +- pkg/test/valid_corset_test.go | 306 +++++++------- testdata/add.lisp | 99 ++++- testdata/alias_01.lisp | 4 +- testdata/alias_02.lisp | 19 +- testdata/alias_03.lisp | 18 +- testdata/alias_04.lisp | 4 +- testdata/alias_05.lisp | 4 +- testdata/alias_06.lisp | 4 +- testdata/basic_01.lisp | 2 +- testdata/basic_02.lisp | 6 +- testdata/basic_03.lisp | 6 +- testdata/basic_04.lisp | 6 +- testdata/basic_05.lisp | 18 +- testdata/basic_06.lisp | 4 +- testdata/basic_07.lisp | 6 +- testdata/basic_08.lisp | 8 +- testdata/basic_09.lisp | 5 +- testdata/basic_10.lisp | 4 +- testdata/bin-dynamic.lisp | 230 ++++++++++- testdata/bin-static.lisp | 241 ++++++++++- testdata/bit_decomposition.lisp | 2 +- testdata/block_01.lisp | 7 +- testdata/block_02.lisp | 10 +- testdata/block_03.lisp | 19 +- testdata/byte_decomposition.lisp | 60 +-- testdata/byte_sorting.lisp | 2 +- testdata/constant_01.lisp | 18 +- testdata/constant_02.lisp | 4 +- testdata/constant_03.lisp | 6 +- testdata/constant_04.lisp | 8 +- testdata/constant_05.lisp | 6 +- testdata/constant_06.lisp | 4 +- testdata/constant_07.lisp | 4 +- testdata/constexpr_01.lisp | 11 +- testdata/constexpr_02.lisp | 24 +- testdata/constexpr_03.lisp | 22 +- testdata/constexpr_04.lisp | 18 +- testdata/constexpr_05.lisp | 7 +- testdata/counter.lisp | 15 +- testdata/domain_01.lisp | 4 +- testdata/domain_02.lisp | 4 +- testdata/domain_03.lisp | 18 +- testdata/fun_01.lisp | 2 +- testdata/fun_02.lisp | 2 +- testdata/fun_03.lisp | 5 +- testdata/fun_04.lisp | 5 +- testdata/fun_05.lisp | 2 +- testdata/fun_06.lisp | 10 +- testdata/funalias_01.lisp | 4 +- testdata/funalias_02.lisp | 4 +- testdata/funalias_03.lisp | 4 +- testdata/guard_01.lisp | 5 +- testdata/guard_02.lisp | 8 +- testdata/guard_03.lisp | 9 +- testdata/guard_04.lisp | 9 +- testdata/guard_05.lisp | 8 +- testdata/if_01.lisp | 8 +- testdata/if_02.lisp | 9 +- testdata/if_03.lisp | 9 +- testdata/if_04.lisp | 9 +- testdata/if_05.lisp | 9 +- testdata/if_06.lisp | 13 +- testdata/if_07.lisp | 9 +- testdata/if_08.lisp | 11 +- testdata/if_09.lisp | 7 +- testdata/if_10.accepts | 36 ++ testdata/if_10.lisp | 5 + testdata/if_10.rejects | 45 ++ testdata/interleave_01.lisp | 2 +- testdata/interleave_02.lisp | 6 +- testdata/interleave_03.lisp | 2 +- testdata/memory.lisp | 46 ++- testdata/module_01.lisp | 2 +- testdata/module_02.lisp | 3 +- testdata/module_03.lisp | 4 +- testdata/module_04.lisp | 2 +- testdata/module_05.lisp | 2 +- testdata/module_06.lisp | 4 +- testdata/module_07.lisp | 3 +- testdata/module_09.lisp | 3 +- testdata/module_10.accepts | 11 + testdata/module_10.lisp | 15 + testdata/module_10.rejects | 7 + testdata/mxp.lisp | 571 ++++++++++++++++++++------ testdata/norm_01.lisp | 4 +- testdata/norm_02.lisp | 4 +- testdata/norm_03.lisp | 4 +- testdata/norm_04.lisp | 4 +- testdata/norm_05.lisp | 4 +- testdata/norm_06.lisp | 4 +- testdata/norm_07.lisp | 4 +- testdata/permute_01.lisp | 3 +- testdata/permute_02.lisp | 2 +- testdata/permute_03.lisp | 5 +- testdata/permute_04.lisp | 4 +- testdata/permute_05.lisp | 4 +- testdata/permute_06.lisp | 4 +- testdata/permute_07.lisp | 5 +- testdata/permute_08.lisp | 4 +- testdata/permute_09.lisp | 5 +- testdata/property_01.lisp | 4 +- testdata/purefun_01.lisp | 4 +- testdata/purefun_02.lisp | 2 +- testdata/purefun_04.lisp | 2 +- testdata/purefun_invalid_08.lisp | 5 + testdata/shift_01.lisp | 4 +- testdata/shift_02.lisp | 4 +- testdata/shift_03.lisp | 4 +- testdata/shift_04.lisp | 4 +- testdata/shift_05.lisp | 4 +- testdata/shift_06.lisp | 4 +- testdata/shift_07.lisp | 2 +- testdata/shift_08.lisp | 6 +- testdata/spillage_01.lisp | 6 +- testdata/spillage_02.lisp | 6 +- testdata/spillage_03.lisp | 6 +- testdata/spillage_04.lisp | 6 +- testdata/spillage_05.lisp | 8 +- testdata/spillage_06.lisp | 6 +- testdata/spillage_07.lisp | 8 +- testdata/spillage_08.lisp | 8 +- testdata/spillage_09.lisp | 8 +- testdata/type_03.lisp | 5 +- testdata/type_05.accepts | 42 ++ testdata/type_05.lisp | 5 + testdata/type_05.rejects | 20 + testdata/type_06.accepts | 34 ++ testdata/type_06.lisp | 5 + testdata/type_06.rejects | 20 + testdata/type_07.accepts | 44 ++ testdata/type_07.lisp | 5 + testdata/type_08.accepts | 27 ++ testdata/type_08.lisp | 3 + testdata/type_08.rejects | 20 + testdata/type_09.accepts | 27 ++ testdata/type_09.lisp | 2 + testdata/type_09.rejects | 29 ++ testdata/type_invalid_01.lisp | 5 + testdata/type_invalid_02.lisp | 5 + testdata/type_invalid_03.lisp | 5 + testdata/type_invalid_04.lisp | 5 + testdata/type_invalid_05.lisp | 5 + testdata/type_invalid_06.lisp | 3 + testdata/type_invalid_07.lisp | 5 + testdata/type_invalid_08.lisp | 5 + testdata/type_invalid_09.lisp | 5 + testdata/type_invalid_10.lisp | 5 + testdata/type_invalid_11.lisp | 5 + testdata/type_invalid_12.lisp | 5 + testdata/type_invalid_13.lisp | 5 + testdata/wcp.lisp | 236 +++++++++-- testdata/word_sorting.lisp | 4 +- 171 files changed, 3419 insertions(+), 837 deletions(-) rename pkg/corset/{ast.go => declaration.go} (79%) rename pkg/corset/{expr.go => expression.go} (96%) create mode 100644 pkg/corset/stdlib.lisp create mode 100644 pkg/corset/type.go create mode 100644 testdata/if_10.accepts create mode 100644 testdata/if_10.lisp create mode 100644 testdata/if_10.rejects create mode 100644 testdata/module_10.accepts create mode 100644 testdata/module_10.lisp create mode 100644 testdata/module_10.rejects create mode 100644 testdata/purefun_invalid_08.lisp create mode 100644 testdata/type_05.accepts create mode 100644 testdata/type_05.lisp create mode 100644 testdata/type_05.rejects create mode 100644 testdata/type_06.accepts create mode 100644 testdata/type_06.lisp create mode 100644 testdata/type_06.rejects create mode 100644 testdata/type_07.accepts create mode 100644 testdata/type_07.lisp create mode 100644 testdata/type_08.accepts create mode 100644 testdata/type_08.lisp create mode 100644 testdata/type_08.rejects create mode 100644 testdata/type_09.accepts create mode 100644 testdata/type_09.lisp create mode 100644 testdata/type_09.rejects create mode 100644 testdata/type_invalid_01.lisp create mode 100644 testdata/type_invalid_02.lisp create mode 100644 testdata/type_invalid_03.lisp create mode 100644 testdata/type_invalid_04.lisp create mode 100644 testdata/type_invalid_05.lisp create mode 100644 testdata/type_invalid_06.lisp create mode 100644 testdata/type_invalid_07.lisp create mode 100644 testdata/type_invalid_08.lisp create mode 100644 testdata/type_invalid_09.lisp create mode 100644 testdata/type_invalid_10.lisp create mode 100644 testdata/type_invalid_11.lisp create mode 100644 testdata/type_invalid_12.lisp create mode 100644 testdata/type_invalid_13.lisp diff --git a/cmd/testgen/main.go b/cmd/testgen/main.go index db4d362..c657c0a 100644 --- a/cmd/testgen/main.go +++ b/cmd/testgen/main.go @@ -190,7 +190,7 @@ func readSchemaFile(filename string) *hir.Schema { // Package up as source file srcfile := sexp.NewSourceFile(filename, bytes) // Attempt to parse schema - schema, err2 := corset.CompileSourceFile(srcfile) + schema, err2 := corset.CompileSourceFile(false, srcfile) // Check whether parsed successfully or not if err2 == nil { // Ok diff --git a/pkg/cmd/check.go b/pkg/cmd/check.go index a1b7c26..03fa86a 100644 --- a/pkg/cmd/check.go +++ b/pkg/cmd/check.go @@ -44,6 +44,7 @@ var checkCmd = &cobra.Command{ cfg.reportCellWidth = GetUint(cmd, "report-cellwidth") cfg.spillage = GetInt(cmd, "spillage") cfg.strict = !GetFlag(cmd, "warn") + cfg.stdlib = !GetFlag(cmd, "no-stdlib") cfg.quiet = GetFlag(cmd, "quiet") cfg.padding.Right = GetUint(cmd, "padding") cfg.parallelExpansion = !GetFlag(cmd, "sequential") @@ -58,7 +59,7 @@ var checkCmd = &cobra.Command{ // stats := util.NewPerfStats() // Parse constraints - hirSchema = readSchema(args[1:]) + hirSchema = readSchema(cfg.stdlib, args[1:]) // stats.Log("Reading constraints file") // Parse trace file @@ -97,6 +98,9 @@ type checkConfig struct { // not required when a "raw" trace is given which already includes all // implied columns. expand bool + // Specifies whether or not to include the standard library. The default is + // to include it. + stdlib bool // Specifies whether or not to report details of the failure (e.g. for // debugging purposes). report bool @@ -312,6 +316,7 @@ func init() { checkCmd.Flags().Bool("air", false, "check at AIR level") checkCmd.Flags().BoolP("warn", "w", false, "report warnings instead of failing for certain errors"+ "(e.g. unknown columns in the trace)") + checkCmd.Flags().Bool("no-stdlib", false, "prevents the standard library from being included") checkCmd.Flags().BoolP("debug", "d", false, "report debug logs") checkCmd.Flags().BoolP("quiet", "q", false, "suppress output (e.g. warnings)") checkCmd.Flags().Bool("sequential", false, "perform sequential trace expansion") diff --git a/pkg/cmd/debug.go b/pkg/cmd/debug.go index 2541182..42d11c8 100644 --- a/pkg/cmd/debug.go +++ b/pkg/cmd/debug.go @@ -28,8 +28,9 @@ var debugCmd = &cobra.Command{ mir := GetFlag(cmd, "mir") air := GetFlag(cmd, "air") stats := GetFlag(cmd, "stats") + stdlib := !GetFlag(cmd, "no-stdlib") // Parse constraints - hirSchema := readSchema(args) + hirSchema := readSchema(stdlib, args) // Print constraints if stats { printStats(hirSchema, hir, mir, air) @@ -45,6 +46,7 @@ func init() { debugCmd.Flags().Bool("mir", false, "Print constraints at MIR level") debugCmd.Flags().Bool("air", false, "Print constraints at AIR level") debugCmd.Flags().Bool("stats", false, "Print summary information") + debugCmd.Flags().Bool("no-stdlib", false, "prevents the standard library from being included") } func printSchemas(hirSchema *hir.Schema, hir bool, mir bool, air bool) { diff --git a/pkg/cmd/test.go b/pkg/cmd/test.go index c483e8a..2578d83 100644 --- a/pkg/cmd/test.go +++ b/pkg/cmd/test.go @@ -38,6 +38,7 @@ var testCmd = &cobra.Command{ cfg.mir = GetFlag(cmd, "mir") cfg.hir = GetFlag(cmd, "hir") cfg.expand = !GetFlag(cmd, "raw") + cfg.stdlib = !GetFlag(cmd, "no-stdlib") cfg.report = GetFlag(cmd, "report") cfg.reportPadding = GetUint(cmd, "report-context") // cfg.strict = !GetFlag(cmd, "warn") @@ -56,7 +57,7 @@ var testCmd = &cobra.Command{ // stats := util.NewPerfStats() // Parse constraints - hirSchema = readSchema(args) + hirSchema = readSchema(cfg.stdlib, args) // stats.Log("Reading constraints file") // @@ -140,6 +141,7 @@ func init() { // testCmd.Flags().BoolP("warn", "w", false, "report warnings instead of failing for certain errors"+ // "(e.g. unknown columns in the trace)") testCmd.Flags().BoolP("debug", "d", false, "report debug logs") + testCmd.Flags().Bool("no-stdlib", false, "prevents the standard library from being included") //testCmd.Flags().BoolP("quiet", "q", false, "suppress output (e.g. warnings)") testCmd.Flags().Bool("sequential", false, "perform sequential trace expansion") testCmd.Flags().Uint("padding", 0, "specify amount of (front) padding to apply") diff --git a/pkg/cmd/util.go b/pkg/cmd/util.go index c6cb699..12bf106 100644 --- a/pkg/cmd/util.go +++ b/pkg/cmd/util.go @@ -134,7 +134,8 @@ func readTraceFile(filename string) []trace.RawColumn { return nil } -func readSchema(filenames []string) *hir.Schema { +// Read the constraints file, whilst optionally including the standard library. +func readSchema(stdlib bool, filenames []string) *hir.Schema { if len(filenames) == 0 { fmt.Println("source or binary constraint(s) file required.") os.Exit(5) @@ -143,7 +144,7 @@ func readSchema(filenames []string) *hir.Schema { return readBinaryFile(filenames[0]) } // Must be source files - return readSourceFiles(filenames) + return readSourceFiles(stdlib, filenames) } // Read a "bin" file. @@ -168,7 +169,7 @@ func readBinaryFile(filename string) *hir.Schema { // Parse a set of source files and compile them into a single schema. This can // result, for example, in a syntax error, etc. -func readSourceFiles(filenames []string) *hir.Schema { +func readSourceFiles(stdlib bool, filenames []string) *hir.Schema { srcfiles := make([]*sexp.SourceFile, len(filenames)) // Read each file for i, n := range filenames { @@ -183,7 +184,7 @@ func readSourceFiles(filenames []string) *hir.Schema { srcfiles[i] = sexp.NewSourceFile(n, bytes) } // Parse and compile source files - schema, errs := corset.CompileSourceFiles(srcfiles) + schema, errs := corset.CompileSourceFiles(stdlib, srcfiles) // Check for any errors if len(errs) == 0 { return schema diff --git a/pkg/corset/binding.go b/pkg/corset/binding.go index e7af4f1..5af03eb 100644 --- a/pkg/corset/binding.go +++ b/pkg/corset/binding.go @@ -3,7 +3,6 @@ package corset import ( "math" - sc "github.com/consensys/go-corset/pkg/schema" tr "github.com/consensys/go-corset/pkg/trace" ) @@ -42,12 +41,24 @@ type ColumnBinding struct { // Column's length multiplier multiplier uint // Column's datatype - dataType sc.Type + dataType Type } -// NewColumnBinding constructs a new column binding in a given module. -func NewColumnBinding(module string, computed bool, mustProve bool, multiplier uint, datatype sc.Type) *ColumnBinding { - return &ColumnBinding{math.MaxUint, module, computed, mustProve, multiplier, datatype} +// NewInputColumnBinding constructs a new column binding in a given module. +// This is for the case where all information about the column is already known, +// and will not be inferred from elsewhere. +func NewInputColumnBinding(module string, mustProve bool, multiplier uint, datatype Type) *ColumnBinding { + return &ColumnBinding{math.MaxUint, module, false, mustProve, multiplier, datatype} +} + +// NewComputedColumnBinding constructs a new column binding in a given +// module. This is for the case where not all information is yet known about +// the column and, hence, it must be finalised later on. For example, in a +// definterleaved constraint the target column information (e.g. its type) is +// not immediately available and must be determined from those columns from +// which it is constructed. +func NewComputedColumnBinding(module string) *ColumnBinding { + return &ColumnBinding{math.MaxUint, module, true, false, 0, nil} } // IsFinalised checks whether this binding has been finalised yet or not. @@ -55,6 +66,12 @@ func (p *ColumnBinding) IsFinalised() bool { return p.multiplier != 0 } +// Finalise this binding by providing the necessary missing information. +func (p *ColumnBinding) Finalise(multiplier uint, datatype Type) { + p.multiplier = multiplier + p.dataType = datatype +} + // Context returns the of this column. That is, the module in which this colunm // was declared and also the length multiplier of that module it requires. func (p *ColumnBinding) Context() Context { @@ -84,11 +101,24 @@ func (p *ColumnBinding) ColumnId() uint { type ConstantBinding struct { // Constant expression which, when evaluated, produces a constant value. value Expr + // Inferred type of the given expression + datatype Type +} + +// NewConstantBinding creates a new constant binding (which is initially not +// finalised). +func NewConstantBinding(value Expr) ConstantBinding { + return ConstantBinding{value, nil} } // IsFinalised checks whether this binding has been finalised yet or not. func (p *ConstantBinding) IsFinalised() bool { - return true + return p.datatype != nil +} + +// Finalise this binding by providing the necessary missing information. +func (p *ConstantBinding) Finalise(datatype Type) { + p.datatype = datatype } // Context returns the of this constant, noting that constants (by definition) @@ -105,33 +135,38 @@ func (p *ConstantBinding) Context() Context { type ParameterBinding struct { // Identifies the variable or column index (as appropriate). index uint + // Type to use for this parameter. + datatype Type } -// ============================================================================ -// FunctionBinding -// ============================================================================ - // IsFinalised checks whether this binding has been finalised yet or not. func (p *ParameterBinding) IsFinalised() bool { - panic("") + panic("should be unreachable?") } +// ============================================================================ +// FunctionBinding +// ============================================================================ + // FunctionBinding represents the binding of a function application to its // physical definition. type FunctionBinding struct { // Flag whether or not is pure function pure bool - // Types of parameters - paramTypes []sc.Type - // Type of return - returnType sc.Type + // Types of parameters (optional) + paramTypes []Type + // Type of return (optional) + returnType Type + // Inferred type of the body. This is used to compare against the declared + // type (if there is one) to check for any descrepencies. + bodyType Type // body of the function in question. body Expr } // NewFunctionBinding constructs a new function binding. -func NewFunctionBinding(pure bool, paramTypes []sc.Type, returnType sc.Type, body Expr) FunctionBinding { - return FunctionBinding{pure, paramTypes, returnType, body} +func NewFunctionBinding(pure bool, paramTypes []Type, returnType Type, body Expr) FunctionBinding { + return FunctionBinding{pure, paramTypes, returnType, nil, body} } // IsPure checks whether this is a defpurefun or not @@ -141,7 +176,7 @@ func (p *FunctionBinding) IsPure() bool { // IsFinalised checks whether this binding has been finalised yet or not. func (p *FunctionBinding) IsFinalised() bool { - return p.returnType != nil + return p.bodyType != nil } // Arity returns the number of parameters that this function accepts. @@ -149,6 +184,11 @@ func (p *FunctionBinding) Arity() uint { return uint(len(p.paramTypes)) } +// Finalise this binding by providing the necessary missing information. +func (p *FunctionBinding) Finalise(bodyType Type) { + p.bodyType = bodyType +} + // Apply a given set of arguments to this function binding. func (p *FunctionBinding) Apply(args []Expr) Expr { return p.body.Substitute(args) diff --git a/pkg/corset/compiler.go b/pkg/corset/compiler.go index 2b048ec..de44c69 100644 --- a/pkg/corset/compiler.go +++ b/pkg/corset/compiler.go @@ -1,10 +1,17 @@ package corset import ( + _ "embed" + "github.com/consensys/go-corset/pkg/hir" "github.com/consensys/go-corset/pkg/sexp" ) +// STDLIB is an import of the standard library. +// +//go:embed stdlib.lisp +var STDLIB []byte + // SyntaxError defines the kind of errors that can be reported by this compiler. // Syntax errors are always associated with some line in one of the original // source files. For simplicity, we reuse existing notion of syntax error from @@ -14,7 +21,10 @@ type SyntaxError = sexp.SyntaxError // CompileSourceFiles compiles one or more source files into a schema. This // process can fail if the source files are mal-formed, or contain syntax errors // or other forms of error (e.g. type errors). -func CompileSourceFiles(srcfiles []*sexp.SourceFile) (*hir.Schema, []SyntaxError) { +func CompileSourceFiles(stdlib bool, srcfiles []*sexp.SourceFile) (*hir.Schema, []SyntaxError) { + // Include the standard library (if requested) + srcfiles = includeStdlib(stdlib, srcfiles) + // Parse all source files (inc stdblib if applicable). circuit, srcmap, errs := ParseSourceFiles(srcfiles) // Check for parsing errors if errs != nil { @@ -28,8 +38,8 @@ func CompileSourceFiles(srcfiles []*sexp.SourceFile) (*hir.Schema, []SyntaxError // really helper function for e.g. the testing environment. This process can // fail if the source file is mal-formed, or contains syntax errors or other // forms of error (e.g. type errors). -func CompileSourceFile(srcfile *sexp.SourceFile) (*hir.Schema, []SyntaxError) { - schema, errs := CompileSourceFiles([]*sexp.SourceFile{srcfile}) +func CompileSourceFile(stdlib bool, srcfile *sexp.SourceFile) (*hir.Schema, []SyntaxError) { + schema, errs := CompileSourceFiles(stdlib, []*sexp.SourceFile{srcfile}) // Check for errors if errs != nil { return nil, errs @@ -73,3 +83,14 @@ func (p *Compiler) Compile() (*hir.Schema, []SyntaxError) { // Finally, translate everything and add it to the schema. return TranslateCircuit(environment, p.srcmap, &p.circuit) } + +func includeStdlib(stdlib bool, srcfiles []*sexp.SourceFile) []*sexp.SourceFile { + if stdlib { + // Include stdlib file + srcfile := sexp.NewSourceFile("stdlib.lisp", STDLIB) + // Append to srcfile list + srcfiles = append(srcfiles, srcfile) + } + // Not included + return srcfiles +} diff --git a/pkg/corset/ast.go b/pkg/corset/declaration.go similarity index 79% rename from pkg/corset/ast.go rename to pkg/corset/declaration.go index 5660390..3db55f5 100644 --- a/pkg/corset/ast.go +++ b/pkg/corset/declaration.go @@ -4,7 +4,6 @@ import ( "fmt" "github.com/consensys/gnark-crypto/ecc/bls12-377/fr" - sc "github.com/consensys/go-corset/pkg/schema" "github.com/consensys/go-corset/pkg/sexp" "github.com/consensys/go-corset/pkg/util" ) @@ -43,6 +42,11 @@ type Declaration interface { Definitions() util.Iterator[SymbolDefinition] // Return set of columns on which this declaration depends. Dependencies() util.Iterator[Symbol] + // Check whether this declaration defines a given symbol. The symbol in + // question needs to have been resolved already for this to make sense. + Defines(Symbol) bool + // Check whether this declaration is finalised already. + IsFinalised() bool } // ============================================================================ @@ -71,6 +75,20 @@ func (p *DefAliases) Definitions() util.Iterator[SymbolDefinition] { return util.NewArrayIterator[SymbolDefinition](nil) } +// Defines checks whether this declaration defines the given symbol. The symbol +// in question needs to have been resolved already for this to make sense. +func (p *DefAliases) Defines(symbol Symbol) bool { + // fine beause defaliases gets special treatement. + return false +} + +// IsFinalised checks whether this declaration has already been finalised. If +// so, then we don't need to finalise it again. +func (p *DefAliases) IsFinalised() bool { + // Fine because defaliases doesn't really do anything with its symbols. + return true +} + // Lisp converts this node into its lisp representation. This is primarily used // for debugging purposes. // @@ -131,6 +149,24 @@ func (p *DefColumns) Definitions() util.Iterator[SymbolDefinition] { return util.NewCastIterator[*DefColumn, SymbolDefinition](iter) } +// Defines checks whether this declaration defines the given symbol. The symbol +// in question needs to have been resolved already for this to make sense. +func (p *DefColumns) Defines(symbol Symbol) bool { + for _, sym := range p.Columns { + if &sym.binding == symbol.Binding() { + return true + } + } + // + return false +} + +// IsFinalised checks whether this declaration has already been finalised. If +// so, then we don't need to finalise it again. +func (p *DefColumns) IsFinalised() bool { + return true +} + // Lisp converts this node into its lisp representation. This is primarily used // for debugging purposes. func (p *DefColumns) Lisp() sexp.SExp { @@ -171,7 +207,7 @@ func (e *DefColumn) Name() string { // DataType returns the type of this column. If this column have not yet been // finalised, then this will panic. -func (e *DefColumn) DataType() sc.Type { +func (e *DefColumn) DataType() Type { if !e.binding.IsFinalised() { panic("unfinalised column") } @@ -259,10 +295,42 @@ func (p *DefConst) Dependencies() util.Iterator[Symbol] { return util.NewArrayIterator[Symbol](deps) } +// Defines checks whether this declaration defines the given symbol. The symbol +// in question needs to have been resolved already for this to make sense. +func (p *DefConst) Defines(symbol Symbol) bool { + for _, sym := range p.constants { + if &sym.binding == symbol.Binding() { + return true + } + } + // + return false +} + +// IsFinalised checks whether this declaration has already been finalised. If +// so, then we don't need to finalise it again. +func (p *DefConst) IsFinalised() bool { + for _, c := range p.constants { + if !c.binding.IsFinalised() { + return false + } + } + // + return true +} + // Lisp converts this node into its lisp representation. This is primarily used // for debugging purposes. func (p *DefConst) Lisp() sexp.SExp { - panic("got here") + def := sexp.EmptyList() + def.Append(sexp.NewSymbol("defconst")) + // + for _, c := range p.constants { + def.Append(sexp.NewSymbol(c.name)) + def.Append(c.binding.value.Lisp()) + } + // Done + return def } // DefConstUnit represents the definition of exactly one constant value. As @@ -331,6 +399,8 @@ type DefConstraint struct { // The constraint itself which (when active) should evaluate to zero for the // relevant set of rows. Constraint Expr + // + finalised bool } // Definitions returns the set of symbols defined by this declaration. Observe @@ -352,6 +422,24 @@ func (p *DefConstraint) Dependencies() util.Iterator[Symbol] { return util.NewArrayIterator[Symbol](append(guard_deps, body_deps...)) } +// Defines checks whether this declaration defines the given symbol. The symbol +// in question needs to have been resolved already for this to make sense. +func (p *DefConstraint) Defines(symbol Symbol) bool { + return false +} + +// IsFinalised checks whether this declaration has already been finalised. If +// so, then we don't need to finalise it again. +func (p *DefConstraint) IsFinalised() bool { + return p.finalised +} + +// Finalise this declaration, which means that its guard (if applicable) and +// body have been resolved. +func (p *DefConstraint) Finalise() { + p.finalised = true +} + // Lisp converts this node into its lisp representation. This is primarily used // for debugging purposes. func (p *DefConstraint) Lisp() sexp.SExp { @@ -392,6 +480,8 @@ type DefInRange struct { // an fr.Element is used here to store the bound simply to make the // necessary comparison against table data more direct. Bound fr.Element + // Indicates whether or not the expression has been resolved. + finalised bool } // Definitions returns the set of symbols defined by this declaration. Observe @@ -405,6 +495,23 @@ func (p *DefInRange) Dependencies() util.Iterator[Symbol] { return util.NewArrayIterator[Symbol](p.Expr.Dependencies()) } +// Defines checks whether this declaration defines the given symbol. The symbol +// in question needs to have been resolved already for this to make sense. +func (p *DefInRange) Defines(symbol Symbol) bool { + return false +} + +// IsFinalised checks whether this declaration has already been finalised. If +// so, then we don't need to finalise it again. +func (p *DefInRange) IsFinalised() bool { + return p.finalised +} + +// Finalise this declaration, meaning that the expression has been resolved. +func (p *DefInRange) Finalise() { + p.finalised = true +} + // Lisp converts this node into its lisp representation. This is primarily used // for debugging purposes. func (p *DefInRange) Lisp() sexp.SExp { @@ -446,6 +553,18 @@ func (p *DefInterleaved) Dependencies() util.Iterator[Symbol] { return util.NewArrayIterator(p.Sources) } +// Defines checks whether this declaration defines the given symbol. The symbol +// in question needs to have been resolved already for this to make sense. +func (p *DefInterleaved) Defines(symbol Symbol) bool { + return &p.Target.binding == symbol.Binding() +} + +// IsFinalised checks whether this declaration has already been finalised. If +// so, then we don't need to finalise it again. +func (p *DefInterleaved) IsFinalised() bool { + return p.Target.binding.IsFinalised() +} + // Lisp converts this node into its lisp representation. This is primarily used // for debugging purposes. func (p *DefInterleaved) Lisp() sexp.SExp { @@ -488,6 +607,8 @@ type DefLookup struct { // Target expressions for lookup (i.e. these values must contain all of the // source values, but may contain more). Targets []Expr + // Indicates whether or not target and source expressions have been resolved. + finalised bool } // Definitions returns the set of symbols defined by this declaration. Observe @@ -504,6 +625,24 @@ func (p *DefLookup) Dependencies() util.Iterator[Symbol] { return util.NewArrayIterator(append(sourceDeps, targetDeps...)) } +// Defines checks whether this declaration defines the given symbol. The symbol +// in question needs to have been resolved already for this to make sense. +func (p *DefLookup) Defines(symbol Symbol) bool { + return false +} + +// IsFinalised checks whether this declaration has already been finalised. If +// so, then we don't need to finalise it again. +func (p *DefLookup) IsFinalised() bool { + return p.finalised +} + +// Finalise this declaration, which means that all source and target expressions +// have been resolved. +func (p *DefLookup) Finalise() { + p.finalised = true +} + // Lisp converts this node into its lisp representation. This is primarily used // for debugging purposes. func (p *DefLookup) Lisp() sexp.SExp { @@ -552,6 +691,30 @@ func (p *DefPermutation) Dependencies() util.Iterator[Symbol] { return util.NewArrayIterator(p.Sources) } +// Defines checks whether this declaration defines the given symbol. The symbol +// in question needs to have been resolved already for this to make sense. +func (p *DefPermutation) Defines(symbol Symbol) bool { + for _, col := range p.Targets { + if &col.binding == symbol.Binding() { + return true + } + } + // Done + return false +} + +// IsFinalised checks whether this declaration has already been finalised. If +// so, then we don't need to finalise it again. +func (p *DefPermutation) IsFinalised() bool { + for _, col := range p.Targets { + if !col.binding.IsFinalised() { + return false + } + } + // Done + return true +} + // Lisp converts this node into its lisp representation. This is primarily used // for debugging purposes. func (p *DefPermutation) Lisp() sexp.SExp { @@ -599,6 +762,8 @@ type DefProperty struct { // The assertion itself which (when active) should evaluate to zero for the // relevant set of rows. Assertion Expr + // Indicates whether or not the assertion has been resolved. + finalised bool } // Definitions returns the set of symbols defined by this declaration. Observe that @@ -612,6 +777,23 @@ func (p *DefProperty) Dependencies() util.Iterator[Symbol] { return util.NewArrayIterator(p.Assertion.Dependencies()) } +// Defines checks whether this declaration defines the given symbol. The symbol +// in question needs to have been resolved already for this to make sense. +func (p *DefProperty) Defines(symbol Symbol) bool { + return false +} + +// IsFinalised checks whether this declaration has already been finalised. If +// so, then we don't need to finalise it again. +func (p *DefProperty) IsFinalised() bool { + return p.finalised +} + +// Finalise this property, meaning that the assertion has been resolved. +func (p *DefProperty) Finalise() { + p.finalised = true +} + // Lisp converts this node into its lisp representation. This is primarily used // for debugging purposes. func (p *DefProperty) Lisp() sexp.SExp { @@ -696,10 +878,26 @@ func (p *DefFun) Dependencies() util.Iterator[Symbol] { return util.NewArrayIterator(ndeps) } +// Defines checks whether this declaration defines the given symbol. The symbol +// in question needs to have been resolved already for this to make sense. +func (p *DefFun) Defines(symbol Symbol) bool { + return &p.binding == symbol.Binding() +} + +// IsFinalised checks whether this declaration has already been finalised. If +// so, then we don't need to finalise it again. +func (p *DefFun) IsFinalised() bool { + return p.binding.IsFinalised() +} + // Lisp converts this node into its lisp representation. This is primarily used // for debugging purposes. func (p *DefFun) Lisp() sexp.SExp { - panic("got here") + return sexp.NewList([]sexp.SExp{ + sexp.NewSymbol("defun"), + sexp.NewSymbol(p.name), + sexp.NewSymbol("..."), // todo + }) } // hasParameter checks whether this function has a parameter with the given @@ -720,11 +918,11 @@ type DefParameter struct { // Column name Name string // The datatype which all values in this parameter should inhabit. - DataType sc.Type + DataType Type } // Lisp converts this node into its lisp representation. This is primarily used // for debugging purposes. func (p *DefParameter) Lisp() sexp.SExp { - panic("got here") + return sexp.NewSymbol(p.Name) } diff --git a/pkg/corset/expr.go b/pkg/corset/expression.go similarity index 96% rename from pkg/corset/expr.go rename to pkg/corset/expression.go index adb02fd..ef414e5 100644 --- a/pkg/corset/expr.go +++ b/pkg/corset/expression.go @@ -190,9 +190,13 @@ func (e *Exp) Dependencies() []Symbol { // IfZero // ============================================================================ -// IfZero returns the (optional) true branch when the condition evaluates to zero, and +// If returns the (optional) true branch when the condition evaluates to zero, and // the (optional false branch otherwise. -type IfZero struct { +type If struct { + // Indicates whether this is an if-zero (kind==1) or an if-notzero + // (kind==2). Any other kind value implies this has not yet been + // determined. + kind uint8 // Elements contained within this list. Condition Expr // True branch (optional). @@ -201,9 +205,31 @@ type IfZero struct { FalseBranch Expr } +// IsIfZero determines whether or not this has been determined as an IfZero +// condition. +func (e *If) IsIfZero() bool { + return e.kind == 1 +} + +// IsIfNotZero determines whether or not this has been determined as an +// IfNotZero condition. +func (e *If) IsIfNotZero() bool { + return e.kind == 2 +} + +// FixSemantics fixes the semantics for this condition to be either "if-zero" or +// "if-notzero". +func (e *If) FixSemantics(ifzero bool) { + if ifzero { + e.kind = 1 + } else { + e.kind = 2 + } +} + // AsConstant attempts to evaluate this expression as a constant (signed) value. // If this expression is not constant, then nil is returned. -func (e *IfZero) AsConstant() *big.Int { +func (e *If) AsConstant() *big.Int { if condition := e.Condition.AsConstant(); condition != nil { // Determine whether condition holds true (or not). holds := condition.Cmp(big.NewInt(0)) == 0 @@ -220,20 +246,20 @@ func (e *IfZero) AsConstant() *big.Int { // Multiplicity determines the number of values that evaluating this expression // can generate. -func (e *IfZero) Multiplicity() uint { +func (e *If) Multiplicity() uint { return determineMultiplicity([]Expr{e.Condition, e.TrueBranch, e.FalseBranch}) } // Context returns the context for this expression. Observe that the // expression must have been resolved for this to be defined (i.e. it may // panic if it has not been resolved yet). -func (e *IfZero) Context() Context { +func (e *If) Context() Context { return ContextOfExpressions([]Expr{e.Condition, e.TrueBranch, e.FalseBranch}) } // Lisp converts this schema element into a simple S-Expression, for example // so it can be printed. -func (e *IfZero) Lisp() sexp.SExp { +func (e *If) Lisp() sexp.SExp { if e.FalseBranch != nil { return sexp.NewList([]sexp.SExp{ sexp.NewSymbol("if"), @@ -248,15 +274,15 @@ func (e *IfZero) Lisp() sexp.SExp { // Substitute all variables (such as for function parameters) arising in // this expression. -func (e *IfZero) Substitute(args []Expr) Expr { - return &IfZero{e.Condition.Substitute(args), +func (e *If) Substitute(args []Expr) Expr { + return &If{e.kind, e.Condition.Substitute(args), SubstituteOptionalExpression(e.TrueBranch, args), SubstituteOptionalExpression(e.FalseBranch, args), } } // Dependencies needed to signal declaration. -func (e *IfZero) Dependencies() []Symbol { +func (e *If) Dependencies() []Symbol { return DependenciesOfExpressions([]Expr{e.Condition, e.TrueBranch, e.FalseBranch}) } diff --git a/pkg/corset/parser.go b/pkg/corset/parser.go index b667543..085ae27 100644 --- a/pkg/corset/parser.go +++ b/pkg/corset/parser.go @@ -10,7 +10,6 @@ import ( "unicode" "github.com/consensys/gnark-crypto/ecc/bls12-377/fr" - sc "github.com/consensys/go-corset/pkg/schema" "github.com/consensys/go-corset/pkg/sexp" ) @@ -317,7 +316,8 @@ func (p *Parser) parseDefColumns(module string, l *sexp.List) (Declaration, []Sy var errors []SyntaxError // Process column declarations one by one. for i := 1; i < len(l.Elements); i++ { - decl, err := p.parseColumnDeclaration(module, l.Elements[i]) + binding := NewInputColumnBinding(module, false, 1, NewFieldType()) + decl, err := p.parseColumnDeclaration(l.Elements[i], binding) // Extract column name if err != nil { errors = append(errors, *err) @@ -333,10 +333,11 @@ func (p *Parser) parseDefColumns(module string, l *sexp.List) (Declaration, []Sy return &DefColumns{columns}, nil } -func (p *Parser) parseColumnDeclaration(module string, e sexp.SExp) (*DefColumn, *SyntaxError) { - var name string - // - binding := NewColumnBinding(module, false, false, 1, &sc.FieldType{}) +func (p *Parser) parseColumnDeclaration(e sexp.SExp, binding *ColumnBinding) (*DefColumn, *SyntaxError) { + var ( + name string + error *SyntaxError + ) // Check whether extended declaration or not. if l := e.AsList(); l != nil { // Check at least the name provided. @@ -348,14 +349,8 @@ func (p *Parser) parseColumnDeclaration(module string, e sexp.SExp) (*DefColumn, // Column name is always first name = l.Elements[0].String(false) // Parse type (if applicable) - if len(l.Elements) == 2 { - var err *SyntaxError - if binding.dataType, binding.mustProve, err = p.parseType(l.Elements[1]); err != nil { - return nil, err - } - } else if len(l.Elements) > 2 { - // For now. - return nil, p.translator.SyntaxError(l, "unknown column declaration attributes") + if binding.dataType, binding.mustProve, error = p.parseColumnDeclarationAttributes(l.Elements[1:]); error != nil { + return nil, error } } else { name = e.String(false) @@ -368,6 +363,33 @@ func (p *Parser) parseColumnDeclaration(module string, e sexp.SExp) (*DefColumn, return def, nil } +func (p *Parser) parseColumnDeclarationAttributes(attrs []sexp.SExp) (Type, bool, *SyntaxError) { + var ( + dataType Type = NewFieldType() + mustProve bool = false + err *SyntaxError + ) + + for _, attr := range attrs { + symbol := attr.AsSymbol() + // Sanity check + if symbol == nil { + return nil, false, p.translator.SyntaxError(attr, "unknown column attribute") + } + // + switch symbol.Value { + case ":display", ":opcode": + // skip these for now, as they are only relevant to the inspector. + default: + if dataType, mustProve, err = p.parseType(attr); err != nil { + return nil, false, err + } + } + } + // Done + return dataType, mustProve, nil +} + // Parse a constant declaration func (p *Parser) parseDefConst(elements []sexp.SExp) (Declaration, []SyntaxError) { var ( @@ -401,7 +423,7 @@ func (p *Parser) parseDefConstUnit(name string, value sexp.SExp) (*DefConstUnit, return nil, []SyntaxError{*err} } // Looks good - def := &DefConstUnit{name, ConstantBinding{expr}} + def := &DefConstUnit{name, NewConstantBinding(expr)} // Map to source node p.mapSourceNode(value, def) // Done @@ -433,7 +455,7 @@ func (p *Parser) parseDefConstraint(elements []sexp.SExp) (Declaration, []Syntax return nil, errors } // Done - return &DefConstraint{elements[1].AsSymbol().Value, domain, guard, expr}, nil + return &DefConstraint{elements[1].AsSymbol().Value, domain, guard, expr, false}, nil } // Parse a interleaved declaration @@ -458,7 +480,7 @@ func (p *Parser) parseDefInterleaved(module string, elements []sexp.SExp) (Decla p.mapSourceNode(ith, sources[i]) } // - binding := NewColumnBinding(module, false, false, 1, &sc.FieldType{}) + binding := NewComputedColumnBinding(module) target := &DefColumn{elements[1].AsSymbol().Value, *binding} // Updating mapping for target definition p.mapSourceNode(elements[1], target) @@ -500,7 +522,7 @@ func (p *Parser) parseDefLookup(elements []sexp.SExp) (Declaration, *SyntaxError } } // Done - return &DefLookup{handle, sources, targets}, nil + return &DefLookup{handle, sources, targets, false}, nil } // Parse a permutation declaration @@ -526,7 +548,8 @@ func (p *Parser) parseDefPermutation(module string, elements []sexp.SExp) (Decla // for i := 0; i < len(targets); i++ { // Parse target column - if targets[i], err = p.parseColumnDeclaration(module, sexpTargets.Get(i)); err != nil { + binding := NewComputedColumnBinding(module) + if targets[i], err = p.parseColumnDeclaration(sexpTargets.Get(i), binding); err != nil { return nil, err } // Parse source column @@ -596,14 +619,14 @@ func (p *Parser) parseDefProperty(elements []sexp.SExp) (Declaration, *SyntaxErr return nil, err } // Done - return &DefProperty{handle, expr}, nil + return &DefProperty{handle, expr, false}, nil } // Parse a permutation declaration func (p *Parser) parseDefFun(pure bool, elements []sexp.SExp) (Declaration, []SyntaxError) { var ( name string - ret sc.Type + ret Type params []*DefParameter errors []SyntaxError signature *sexp.List = elements[1].AsList() @@ -625,7 +648,7 @@ func (p *Parser) parseDefFun(pure bool, elements []sexp.SExp) (Declaration, []Sy return nil, errors } // Extract parameter types - paramTypes := make([]sc.Type, len(params)) + paramTypes := make([]Type, len(params)) for i, p := range params { paramTypes[i] = p.DataType } @@ -635,17 +658,12 @@ func (p *Parser) parseDefFun(pure bool, elements []sexp.SExp) (Declaration, []Sy return &DefFun{name, params, binding}, nil } -func (p *Parser) parseFunctionSignature(elements []sexp.SExp) (string, sc.Type, []*DefParameter, []SyntaxError) { +func (p *Parser) parseFunctionSignature(elements []sexp.SExp) (string, Type, []*DefParameter, []SyntaxError) { var ( params []*DefParameter = make([]*DefParameter, len(elements)-1) - ret sc.Type = &sc.FieldType{} - errors []SyntaxError ) - // Parse name - if !isIdentifier(elements[0]) { - err := p.translator.SyntaxError(elements[1], "expected function name") - errors = append(errors, *err) - } + // Parse name and (optional) return type + name, ret, _, errors := p.parseFunctionNameReturn(elements[0]) // Parse parameters for i := 0; i < len(params); i = i + 1 { var errs []SyntaxError @@ -659,12 +677,56 @@ func (p *Parser) parseFunctionSignature(elements []sexp.SExp) (string, sc.Type, return "", nil, nil, errors } // - return elements[0].AsSymbol().Value, ret, params, nil + return name, ret, params, nil +} + +func (p *Parser) parseFunctionNameReturn(element sexp.SExp) (string, Type, bool, []SyntaxError) { + var ( + err *SyntaxError + name sexp.SExp + ret Type = nil + forced bool + symbol *sexp.Symbol = element.AsSymbol() + list *sexp.List = element.AsList() + ) + // + if symbol != nil { + name = symbol + } else { + // Check all modifiers + for i, element := range list.Elements { + symbol := element.AsSymbol() + // Check what we have + if symbol == nil { + err := p.translator.SyntaxError(element, "modifier expected") + return "", nil, false, []SyntaxError{*err} + } else if i == 0 { + name = symbol + } else { + switch symbol.Value { + case ":force": + forced = true + default: + if ret, _, err = p.parseType(element); err != nil { + return "", nil, false, []SyntaxError{*err} + } + } + } + } + } + // + if isIdentifier(name) { + return name.AsSymbol().Value, ret, forced, nil + } else { + // Must be non-identifier symbol + err = p.translator.SyntaxError(element, "expected function name") + return "", nil, false, []SyntaxError{*err} + } } func (p *Parser) parseFunctionParameter(element sexp.SExp) (*DefParameter, []SyntaxError) { if isIdentifier(element) { - return &DefParameter{element.AsSymbol().Value, &sc.FieldType{}}, nil + return &DefParameter{element.AsSymbol().Value, NewFieldType()}, nil } // Construct error message (for now) err := p.translator.SyntaxError(element, "malformed parameter declaration") @@ -751,38 +813,59 @@ func (p *Parser) parseDomainAttribute(attribute sexp.SExp) (domain *int, err *Sy return nil, p.translator.SyntaxError(attribute, "multiple values not supported") } -func (p *Parser) parseType(term sexp.SExp) (sc.Type, bool, *SyntaxError) { +func (p *Parser) parseType(term sexp.SExp) (Type, bool, *SyntaxError) { symbol := term.AsSymbol() if symbol == nil { return nil, false, p.translator.SyntaxError(term, "malformed type") } // Access string of symbol parts := strings.Split(symbol.Value, "@") - if len(parts) > 2 || (len(parts) == 2 && parts[1] != "prove") { - return nil, false, p.translator.SyntaxError(term, "malformed type") - } // Determine whether type should be proven or not. - proven := len(parts) == 2 + var datatype Type // See what we've got. switch parts[0] { case ":binary": - return sc.NewUintType(1), proven, nil + datatype = NewUintType(1) case ":byte": - return sc.NewUintType(8), proven, nil + datatype = NewUintType(8) + case ":": + if len(parts) == 1 { + return nil, false, p.translator.SyntaxError(symbol, "unknown type") + } + // + datatype = NewFieldType() default: // Handle generic types like i16, i128, etc. str := parts[0] - if strings.HasPrefix(str, ":i") { - n, err := strconv.Atoi(str[2:]) - if err != nil { - return nil, false, p.translator.SyntaxError(symbol, err.Error()) - } - // Done - return sc.NewUintType(uint(n)), proven, nil + if !strings.HasPrefix(str, ":i") { + return nil, false, p.translator.SyntaxError(symbol, "unknown type") + } + // Parse bitwidth + n, err := strconv.Atoi(str[2:]) + if err != nil { + return nil, false, p.translator.SyntaxError(symbol, err.Error()) + } + // Done + datatype = NewUintType(uint(n)) + } + // Types not proven unless explicitly requested + var proven bool = false + // Process type modifiers + for i := 1; i < len(parts); i++ { + switch parts[i] { + case "prove": + proven = true + case "loob": + datatype = datatype.WithLoobeanSemantics() + case "bool": + datatype = datatype.WithBooleanSemantics() + default: + msg := fmt.Sprintf("unknown modifier \"%s\"", parts[i]) + return nil, false, p.translator.SyntaxError(symbol, msg) } } - // Error - return nil, false, p.translator.SyntaxError(symbol, "unknown type") + // Done + return datatype, proven, nil } func beginParserRule(_ string, args []Expr) (Expr, error) { @@ -847,9 +930,9 @@ func mulParserRule(_ string, args []Expr) (Expr, error) { func ifParserRule(_ string, args []Expr) (Expr, error) { if len(args) == 2 { - return &IfZero{args[0], args[1], nil}, nil + return &If{0, args[0], args[1], nil}, nil } else if len(args) == 3 { - return &IfZero{args[0], args[1], args[2]}, nil + return &If{0, args[0], args[1], args[2]}, nil } return nil, errors.New("incorrect number of arguments") diff --git a/pkg/corset/resolver.go b/pkg/corset/resolver.go index 898d050..a2611e9 100644 --- a/pkg/corset/resolver.go +++ b/pkg/corset/resolver.go @@ -3,9 +3,7 @@ package corset import ( "fmt" - "github.com/consensys/go-corset/pkg/schema" "github.com/consensys/go-corset/pkg/sexp" - "github.com/consensys/go-corset/pkg/util" ) // ResolveCircuit resolves all symbols declared and used within a circuit, @@ -184,20 +182,24 @@ func (r *resolver) finaliseDeclarationsInModule(scope *ModuleScope, decls []Decl complete = true // for _, d := range decls { - ready, errs := r.declarationDependenciesAreFinalised(scope, d.Dependencies()) - // See what arosed - if errs != nil { - errors = append(errors, errs...) - } else if ready { - // Finalise declaration and handle errors - errs := r.finaliseDeclaration(scope, d) - errors = append(errors, errs...) - // Record that a new assignment is available. - changed = changed || len(errs) == 0 - } else { - // Declaration not ready yet - complete = false - incomplete = d + // Check whether already finalised + if !d.IsFinalised() { + // No, so attempt to finalise + ready, errs := r.declarationDependenciesAreFinalised(scope, d) + // Check what we found + if errs != nil { + errors = append(errors, errs...) + } else if ready { + // Finalise declaration and handle errors + errs := r.finaliseDeclaration(scope, d) + errors = append(errors, errs...) + // Record that a new assignment is available. + changed = changed || len(errs) == 0 + } else { + // Declaration not ready yet + complete = false + incomplete = d + } } } // Sanity check for any errors caught during this iteration. @@ -221,26 +223,34 @@ func (r *resolver) finaliseDeclarationsInModule(scope *ModuleScope, decls []Decl return nil } -// Check that a given set of source columns have been finalised. This is -// important, since we cannot finalise a declaration until all of its -// dependencies have themselves been finalised. +// Check that a given set of symbols have been finalised. This is important, +// since we cannot finalise a declaration until all of its dependencies have +// themselves been finalised. func (r *resolver) declarationDependenciesAreFinalised(scope *ModuleScope, - symbols util.Iterator[Symbol]) (bool, []SyntaxError) { + decl Declaration) (bool, []SyntaxError) { var ( errors []SyntaxError finalised bool = true ) // - for iter := symbols; iter.HasNext(); { + for iter := decl.Dependencies(); iter.HasNext(); { symbol := iter.Next() // Attempt to resolve if !symbol.IsResolved() && !scope.Bind(symbol) { errors = append(errors, *r.srcmap.SyntaxError(symbol, "unknown symbol")) // not finalised yet finalised = false - } else if symbol.IsResolved() && !symbol.Binding().IsFinalised() { - // no, not finalised - finalised = false + } else { + // Check whether this declaration defines this symbol (because if it + // does, we cannot expect it to be finalised yet :) + selfdefinition := decl.Defines(symbol) + // Check whether this symbol is already finalised. + symbol_finalised := symbol.Binding().IsFinalised() + // Final check + if !selfdefinition && !symbol_finalised { + // Ok, not ready for finalisation yet. + finalised = false + } } } // @@ -279,11 +289,16 @@ func (r *resolver) finaliseDefConstInModule(enclosing Scope, decl *DefConst) []S for _, c := range decl.constants { scope := NewLocalScope(enclosing, false, true) // Resolve constant body - errors = append(errors, r.finaliseExpressionInModule(scope, c.binding.value)...) + datatype, errs := r.finaliseExpressionInModule(scope, c.binding.value) + // Accumulate errors + errors = append(errors, errs...) // Check it is indeed constant! if constant := c.binding.value.AsConstant(); constant == nil { err := r.srcmap.SyntaxError(c, "definition not constant") errors = append(errors, *err) + } else { + // Finalise constant binding + c.binding.Finalise(datatype) } } // @@ -295,17 +310,32 @@ func (r *resolver) finaliseDefConstInModule(enclosing Scope, decl *DefConst) []S // expressions are well-typed. func (r *resolver) finaliseDefConstraintInModule(enclosing Scope, decl *DefConstraint) []SyntaxError { var ( - errors []SyntaxError - scope = NewLocalScope(enclosing, false, false) + guard_errors []SyntaxError + guard_t Type + scope = NewLocalScope(enclosing, false, false) ) // Resolve guard if decl.Guard != nil { - errors = r.finaliseExpressionInModule(scope, decl.Guard) + guard_t, guard_errors = r.finaliseExpressionInModule(scope, decl.Guard) + // + if guard_t != nil && guard_t.HasLoobeanSemantics() { + err := r.srcmap.SyntaxError(decl.Guard, "unexpected loobean guard") + guard_errors = append(guard_errors, *err) + } } // Resolve constraint body - errors = append(errors, r.finaliseExpressionInModule(scope, decl.Constraint)...) + constraint_t, errors := r.finaliseExpressionInModule(scope, decl.Constraint) + // + if constraint_t != nil && !constraint_t.HasLoobeanSemantics() { + msg := fmt.Sprintf("expected loobean constraint (found %s)", constraint_t.String()) + err := r.srcmap.SyntaxError(decl.Constraint, msg) + errors = append(errors, *err) + } else if len(errors) == 0 { + // Finalise declaration. + decl.Finalise() + } // Done - return errors + return append(guard_errors, errors...) } // Finalise an interleaving assignment. Since the assignment would already been @@ -318,7 +348,7 @@ func (r *resolver) finaliseDefInterleavedInModule(decl *DefInterleaved) []Syntax // Length multiplier being determined length_multiplier uint // Column type being determined - datatype schema.Type + datatype Type // Errors discovered errors []SyntaxError ) @@ -336,7 +366,7 @@ func (r *resolver) finaliseDefInterleavedInModule(decl *DefInterleaved) []Syntax errors = append(errors, *err) } // Combine datatypes. - datatype = schema.Join(datatype, binding.dataType) + datatype = GreatestLowerBound(datatype, binding.dataType) } // Finalise details only if no errors if len(errors) == 0 { @@ -344,9 +374,8 @@ func (r *resolver) finaliseDefInterleavedInModule(decl *DefInterleaved) []Syntax length_multiplier *= uint(len(decl.Sources)) // Lookup existing declaration binding := decl.Target.Binding().(*ColumnBinding) - // Update with completed information - binding.multiplier = length_multiplier - binding.dataType = datatype + // Finalise column binding + binding.Finalise(length_multiplier, datatype) } // Done return errors @@ -365,7 +394,7 @@ func (r *resolver) finaliseDefPermutationInModule(decl *DefPermutation) []Syntax // Lookup source of column being permuted source := ith.Binding().(*ColumnBinding) // Sanity check length multiplier - if i == 0 && source.dataType.AsUint() == nil { + if i == 0 && source.dataType.AsUnderlying().AsUint() == nil { errors = append(errors, *r.srcmap.SyntaxError(ith, "fixed-width type required")) } else if i == 0 { multiplier = source.multiplier @@ -388,11 +417,10 @@ func (r *resolver) finaliseDefPermutationInModule(decl *DefPermutation) []Syntax // expressions are well-typed. func (r *resolver) finaliseDefInRangeInModule(enclosing Scope, decl *DefInRange) []SyntaxError { var ( - errors []SyntaxError - scope = NewLocalScope(enclosing, false, false) + scope = NewLocalScope(enclosing, false, false) ) // Resolve property body - errors = append(errors, r.finaliseExpressionInModule(scope, decl.Expr)...) + _, errors := r.finaliseExpressionInModule(scope, decl.Expr) // Done return errors } @@ -404,15 +432,18 @@ func (r *resolver) finaliseDefInRangeInModule(enclosing Scope, decl *DefInRange) // function. func (r *resolver) finaliseDefFunInModule(enclosing Scope, decl *DefFun) []SyntaxError { var ( - errors []SyntaxError - scope = NewLocalScope(enclosing, false, decl.IsPure()) + scope = NewLocalScope(enclosing, false, decl.IsPure()) ) // Declare parameters in local scope for _, p := range decl.Parameters() { - scope.DeclareLocal(p.Name) + scope.DeclareLocal(p.Name, p.DataType) } // Resolve property body - errors = append(errors, r.finaliseExpressionInModule(scope, decl.Body())...) + datatype, errors := r.finaliseExpressionInModule(scope, decl.Body()) + // Finalise declaration + if len(errors) == 0 { + decl.binding.Finalise(datatype) + } // Done return errors } @@ -420,43 +451,45 @@ func (r *resolver) finaliseDefFunInModule(enclosing Scope, decl *DefFun) []Synta // Resolve those variables appearing in the body of this lookup constraint. func (r *resolver) finaliseDefLookupInModule(enclosing Scope, decl *DefLookup) []SyntaxError { var ( - errors []SyntaxError sourceScope = NewLocalScope(enclosing, true, false) targetScope = NewLocalScope(enclosing, true, false) ) // Resolve source expressions - errors = append(errors, r.finaliseExpressionsInModule(sourceScope, decl.Sources)...) + _, source_errors := r.finaliseExpressionsInModule(sourceScope, decl.Sources) // Resolve target expressions - errors = append(errors, r.finaliseExpressionsInModule(targetScope, decl.Targets)...) - // Done - return errors + _, target_errors := r.finaliseExpressionsInModule(targetScope, decl.Targets) + // + return append(source_errors, target_errors...) } // Resolve those variables appearing in the body of this property assertion. func (r *resolver) finaliseDefPropertyInModule(enclosing Scope, decl *DefProperty) []SyntaxError { var ( - errors []SyntaxError - scope = NewLocalScope(enclosing, false, false) + scope = NewLocalScope(enclosing, false, false) ) - // Resolve property body - errors = append(errors, r.finaliseExpressionInModule(scope, decl.Assertion)...) + // Resolve assertion + _, errors := r.finaliseExpressionInModule(scope, decl.Assertion) // Done return errors } // Resolve a sequence of zero or more expressions within a given module. This // simply resolves each of the arguments in turn, collecting any errors arising. -func (r *resolver) finaliseExpressionsInModule(scope LocalScope, args []Expr) []SyntaxError { - var errors []SyntaxError +func (r *resolver) finaliseExpressionsInModule(scope LocalScope, args []Expr) ([]Type, []SyntaxError) { + var ( + errs []SyntaxError + errors []SyntaxError + types []Type = make([]Type, len(args)) + ) // Visit each argument - for _, arg := range args { + for i, arg := range args { if arg != nil { - errs := r.finaliseExpressionInModule(scope, arg) + types[i], errs = r.finaliseExpressionInModule(scope, arg) errors = append(errors, errs...) } } // Done - return errors + return types, errors } // Resolve any variable accesses with this expression (which is declared in a @@ -464,91 +497,142 @@ func (r *resolver) finaliseExpressionsInModule(scope LocalScope, args []Expr) [] // variable accesses. As above, the goal is ensure variable refers to something // that was declared and, more specifically, what kind of access it is (e.g. // column access, constant access, etc). -func (r *resolver) finaliseExpressionInModule(scope LocalScope, expr Expr) []SyntaxError { - if _, ok := expr.(*Constant); ok { - return nil +// +//nolint:staticcheck +func (r *resolver) finaliseExpressionInModule(scope LocalScope, expr Expr) (Type, []SyntaxError) { + if v, ok := expr.(*Constant); ok { + nbits := v.Val.BitLen() + return NewUintType(uint(nbits)), nil } else if v, ok := expr.(*Add); ok { - return r.finaliseExpressionsInModule(scope, v.Args) + types, errs := r.finaliseExpressionsInModule(scope, v.Args) + return LeastUpperBoundAll(types), errs } else if v, ok := expr.(*Exp); ok { purescope := scope.NestedPureScope() - arg_errs := r.finaliseExpressionInModule(scope, v.Arg) - pow_errs := r.finaliseExpressionInModule(purescope, v.Pow) + arg_types, arg_errs := r.finaliseExpressionInModule(scope, v.Arg) + _, pow_errs := r.finaliseExpressionInModule(purescope, v.Pow) // combine errors - return append(arg_errs, pow_errs...) - } else if v, ok := expr.(*IfZero); ok { - return r.finaliseExpressionsInModule(scope, []Expr{v.Condition, v.TrueBranch, v.FalseBranch}) + return arg_types, append(arg_errs, pow_errs...) + } else if v, ok := expr.(*If); ok { + return r.finaliseIfInModule(scope, v) } else if v, ok := expr.(*Invoke); ok { return r.finaliseInvokeInModule(scope, v) } else if v, ok := expr.(*List); ok { - return r.finaliseExpressionsInModule(scope, v.Args) + types, errs := r.finaliseExpressionsInModule(scope, v.Args) + return GreatestLowerBoundAll(types), errs } else if v, ok := expr.(*Mul); ok { - return r.finaliseExpressionsInModule(scope, v.Args) + types, errs := r.finaliseExpressionsInModule(scope, v.Args) + return GreatestLowerBoundAll(types), errs } else if v, ok := expr.(*Normalise); ok { return r.finaliseExpressionInModule(scope, v.Arg) } else if v, ok := expr.(*Shift); ok { purescope := scope.NestedPureScope() - arg_errs := r.finaliseExpressionInModule(scope, v.Arg) - shf_errs := r.finaliseExpressionInModule(purescope, v.Shift) + arg_types, arg_errs := r.finaliseExpressionInModule(scope, v.Arg) + _, shf_errs := r.finaliseExpressionInModule(purescope, v.Shift) // combine errors - return append(arg_errs, shf_errs...) + return arg_types, append(arg_errs, shf_errs...) } else if v, ok := expr.(*Sub); ok { - return r.finaliseExpressionsInModule(scope, v.Args) + types, errs := r.finaliseExpressionsInModule(scope, v.Args) + return LeastUpperBoundAll(types), errs } else if v, ok := expr.(*VariableAccess); ok { return r.finaliseVariableInModule(scope, v) } else { - return r.srcmap.SyntaxErrors(expr, "unknown expression") + return nil, r.srcmap.SyntaxErrors(expr, "unknown expression") + } +} + +// Resolve an if condition contained within some expression which, in turn, is +// contained within some module. An important step occurrs here where, based on +// the semantics of the condition, this is inferred as an "if-zero" or an +// "if-notzero". +func (r *resolver) finaliseIfInModule(scope LocalScope, expr *If) (Type, []SyntaxError) { + types, errs := r.finaliseExpressionsInModule(scope, []Expr{expr.Condition, expr.TrueBranch, expr.FalseBranch}) + // Sanity check + if len(errs) != 0 { + return nil, errs + } + // Check & Resolve Condition + if types[0].HasLoobeanSemantics() { + // if-zero + expr.FixSemantics(true) + } else if types[0].HasBooleanSemantics() { + // if-notzero + expr.FixSemantics(false) + } else { + return nil, r.srcmap.SyntaxErrors(expr.Condition, "invalid condition (neither loobean nor boolean)") } + // Join result types + return GreatestLowerBoundAll(types[1:]), errs } // Resolve a specific invocation contained within some expression which, in // turn, is contained within some module. Note, qualified accesses are only // permitted in a global context. -func (r *resolver) finaliseInvokeInModule(scope LocalScope, expr *Invoke) []SyntaxError { +func (r *resolver) finaliseInvokeInModule(scope LocalScope, expr *Invoke) (Type, []SyntaxError) { // Resolve arguments - if errors := r.finaliseExpressionsInModule(scope, expr.Args()); errors != nil { - return errors + if _, errors := r.finaliseExpressionsInModule(scope, expr.Args()); errors != nil { + return nil, errors } // Lookup the corresponding function definition. if !scope.Bind(expr) { - return r.srcmap.SyntaxErrors(expr, "unknown function") + return nil, r.srcmap.SyntaxErrors(expr, "unknown function") } else if scope.IsPure() && !expr.binding.IsPure() { - return r.srcmap.SyntaxErrors(expr, "not permitted in pure context") + return nil, r.srcmap.SyntaxErrors(expr, "not permitted in pure context") + } else if binding := expr.binding; binding.Arity() != uint(len(expr.Args())) { + msg := fmt.Sprintf("incorrect number of arguments (expected %d, found %d)", binding.Arity(), len(expr.Args())) + return nil, r.srcmap.SyntaxErrors(expr, msg) } - // Success - return nil + // Check whether need to infer return type + if expr.binding.returnType != nil { + // no need, it was provided + return expr.binding.returnType, nil + } + // TODO: this is potentially expensive, and it would likely be good if we + // could avoid it. Realistically, this is just about determining the right + // type information. Potentially, we could adjust the local scope to + // provide the required type information. Or we could have a separate pass + // which just determines the type. + body := expr.binding.Apply(expr.Args()) + // Dig out the type + return r.finaliseExpressionInModule(scope, body) } // Resolve a specific variable access contained within some expression which, in // turn, is contained within some module. Note, qualified accesses are only // permitted in a global context. func (r *resolver) finaliseVariableInModule(scope LocalScope, - expr *VariableAccess) []SyntaxError { + expr *VariableAccess) (Type, []SyntaxError) { // Check whether this is a qualified access, or not. if !scope.IsGlobal() && expr.IsQualified() { - return r.srcmap.SyntaxErrors(expr, "qualified access not permitted here") + return nil, r.srcmap.SyntaxErrors(expr, "qualified access not permitted here") } else if expr.IsQualified() && !scope.HasModule(expr.Module()) { - return r.srcmap.SyntaxErrors(expr, fmt.Sprintf("unknown module %s", expr.Module())) + return nil, r.srcmap.SyntaxErrors(expr, fmt.Sprintf("unknown module %s", expr.Module())) } - // Symbol should be resolved at this point, but we still need to check the - // context. - if expr.IsResolved() { - // Update context - if binding, ok := expr.Binding().(*ColumnBinding); ok { - if !scope.FixContext(binding.Context()) { - return r.srcmap.SyntaxErrors(expr, "conflicting context") - } else if scope.IsPure() { - return r.srcmap.SyntaxErrors(expr, "not permitted in pure context") - } - } else if _, ok := expr.Binding().(*ConstantBinding); !ok { - // Unable to resolve variable - return r.srcmap.SyntaxErrors(expr, "refers to a function") + // Symbol should be resolved at this point, but we'd better sanity check this. + if !expr.IsResolved() && !scope.Bind(expr) { + // Unable to resolve variable + return nil, r.srcmap.SyntaxErrors(expr, "unresolved symbol") + } + // + if binding, ok := expr.Binding().(*ColumnBinding); ok { + // For column bindings, we still need to sanity check the context is + // compatible. + if !scope.FixContext(binding.Context()) { + return nil, r.srcmap.SyntaxErrors(expr, "conflicting context") + } else if scope.IsPure() { + return nil, r.srcmap.SyntaxErrors(expr, "not permitted in pure context") } - // Done - return nil - } else if scope.Bind(expr) { - // Must be a local variable or parameter access, so we're all good. - return nil + // Use column's datatype + return binding.dataType, nil + } else if binding, ok := expr.Binding().(*ConstantBinding); ok { + // Constant + return binding.datatype, nil + } else if binding, ok := expr.Binding().(*ParameterBinding); ok { + // Parameter + return binding.datatype, nil + } else if _, ok := expr.Binding().(*FunctionBinding); ok { + // Function doesn't makes sense here. + return nil, r.srcmap.SyntaxErrors(expr, "refers to a function") } - // Unable to resolve variable - return r.srcmap.SyntaxErrors(expr, "unresolved symbol") + // Should be unreachable. + return nil, r.srcmap.SyntaxErrors(expr, "unknown symbol kind") } diff --git a/pkg/corset/scope.go b/pkg/corset/scope.go index 7f5388c..3d042af 100644 --- a/pkg/corset/scope.go +++ b/pkg/corset/scope.go @@ -64,7 +64,8 @@ func (p *GlobalScope) HasModule(module string) bool { // root context, this is either a column, an alias or a function declaration. func (p *GlobalScope) Bind(symbol Symbol) bool { if !symbol.IsQualified() { - panic("cannot bind unqualified symbol in the global scope") + // Search for symbol in root module. + return p.Module("").Bind(symbol) } else if !p.HasModule(symbol.Module()) { // Pontially, it might be better to report a more useful error message. return false @@ -134,9 +135,13 @@ func (p *ModuleScope) Bind(symbol Symbol) bool { binding := p.bindings[bid] // Resolve symbol return symbol.Resolve(binding) + } else if !symbol.IsQualified() && p.module != "" { + // Attempt to lookup in parent (unless we are the root module, in which + // case we have no parent) + return p.enclosing.Bind(symbol) + } else { + return false } - // failed - return false } // Binding returns information about the binding of a particular symbol defined @@ -215,6 +220,8 @@ type LocalScope struct { context *Context // Maps inputs parameters to the declaration index. locals map[string]uint + // Actual parameter bindings + bindings []*ParameterBinding } // NewLocalScope constructs a new local scope within a given enclosing scope. A @@ -224,31 +231,38 @@ type LocalScope struct { func NewLocalScope(enclosing Scope, global bool, pure bool) LocalScope { context := tr.VoidContext[string]() locals := make(map[string]uint) + bindings := make([]*ParameterBinding, 0) // - return LocalScope{global, pure, enclosing, &context, locals} + return LocalScope{global, pure, enclosing, &context, locals, bindings} } // NestedScope creates a nested scope within this local scope. func (p LocalScope) NestedScope() LocalScope { nlocals := make(map[string]uint) + nbindings := make([]*ParameterBinding, len(p.bindings)) // Clone allocated variables for k, v := range p.locals { nlocals[k] = v } + // Copy over bindings. + copy(nbindings, p.bindings) // Done - return LocalScope{p.global, p.pure, p, p.context, nlocals} + return LocalScope{p.global, p.pure, p, p.context, nlocals, nbindings} } // NestedPureScope creates a nested scope within this local scope which, in // addition, is always pure. func (p LocalScope) NestedPureScope() LocalScope { nlocals := make(map[string]uint) + nbindings := make([]*ParameterBinding, len(p.bindings)) // Clone allocated variables for k, v := range p.locals { nlocals[k] = v } + // Copy over bindings. + copy(nbindings, p.bindings) // Done - return LocalScope{p.global, true, p, p.context, nlocals} + return LocalScope{p.global, true, p, p.context, nlocals, nbindings} } // IsGlobal determines whether symbols can be accessed in modules other than the @@ -284,16 +298,18 @@ func (p LocalScope) Bind(symbol Symbol) bool { // Check whether this is a local variable access. if id, ok := p.locals[symbol.Name()]; ok && !symbol.IsFunction() && !symbol.IsQualified() { // Yes, this is a local variable access. - return symbol.Resolve(&ParameterBinding{id}) + return symbol.Resolve(p.bindings[id]) } // No, this is not a local variable access. return p.enclosing.Bind(symbol) } // DeclareLocal registers a new local variable (e.g. a parameter). -func (p LocalScope) DeclareLocal(name string) uint { +func (p *LocalScope) DeclareLocal(name string, datatype Type) uint { index := uint(len(p.locals)) + binding := ParameterBinding{index, datatype} p.locals[name] = index + p.bindings = append(p.bindings, &binding) // Return variable index return index } diff --git a/pkg/corset/stdlib.lisp b/pkg/corset/stdlib.lisp new file mode 100644 index 0000000..97fff76 --- /dev/null +++ b/pkg/corset/stdlib.lisp @@ -0,0 +1,137 @@ +;; [TODO] (defunalias debug-assert debug) + +(defpurefun (if-zero cond then) (if (vanishes! cond) then)) +;; [TODO] (defpurefun (if-zero cond then else) (if (vanishes! cond) then else)) +(defpurefun (if-zero-else cond then else) (if (vanishes! cond) then else)) + +(defpurefun (if-not-zero cond then) (if (force-bool cond) then)) +;; [TODO] (defpurefun (if-not-zero cond then else) (if (force-bool cond) then else)) + +(defpurefun ((force-bool :@bool :force) x) x) +(defpurefun ((is-binary :@loob :force) e0) (* e0 (- 1 e0))) + +(defpurefun ((force-bin :binary :force) x) x) + +;; +;; Boolean functions +;; +;; !-suffix denotes loobean algebra (i.e. 0 == true) +;; ~-prefix denotes normalized-functions (i.e. output is 0/1) +(defpurefun (and a b) (* a b)) +;; [TODO] (defpurefun ((~and :binary@bool) a b) (~ (and a b))) +(defpurefun ((or! :@loob) a b) (* a b)) +;; [TODO] (defpurefun ((~or! :binary@loob) a b) (~ (or! a b))) + +;; [TODO] (defpurefun ((not :binary@bool :force) (x :binary)) (- 1 x)) + +(defpurefun ((eq! :@loob) x y) (- x y)) +;; [TODO] (defpurefun ((neq! :binary@loob :force) x y) (not (~ (eq! x y)))) +;; [TODO] (defunalias = eq!) + +;; [TODO] (defpurefun ((eq :binary@bool :force) (x :binary) (y :binary)) (^ (- x y) 2)) +(defpurefun ((eq :binary@bool :force) x y) (- 1 (~ (eq! x y)))) +(defpurefun ((neq :binary@bool :force) x y) (eq! x y)) + +;; Variadic variations on and/or +;; [TODO] (defunalias any! *) +;; [TODO] (defunalias all *) + +;; Boolean functions +(defpurefun ((is-not-zero :binary@bool) x) (~ x)) +(defpurefun ((is-not-zero! :binary@loob :force) x) (- 1 (is-not-zero x))) +(defpurefun ((is-zero :binary@bool :force) x) (- 1 (~ x))) + +;; Chronological functions +(defpurefun (next X) (shift X 1)) +(defpurefun (prev X) (shift X -1)) + +;; Ensure that e0 has (resp. will) increase (resp. decrease) of offset +;; w.r.t. the previous (resp. next) row. +(defpurefun (did-inc! e0 offset) (eq! e0 (+ (prev e0) offset))) +(defpurefun (did-dec! e0 offset) (eq! e0 (- (prev e0) offset))) +(defpurefun (will-inc! e0 offset) (will-eq! e0 (+ e0 offset))) +(defpurefun (will-dec! e0 offset) (eq! (next e0) (- e0 offset))) + +(defpurefun (did-inc e0 offset) (eq e0 (+ (prev e0) offset))) +(defpurefun (did-dec e0 offset) (eq e0 (- (prev e0) offset))) +(defpurefun (will-inc e0 offset) (will-eq e0 (+ e0 offset))) +(defpurefun (will-dec e0 offset) (eq (next e0) (- e0 offset))) + +;; Ensure that e0 remained (resp. will be) constant +;; with regards to the previous (resp. next) row. +(defpurefun (remained-constant! e0) (eq! e0 (prev e0))) +(defpurefun (will-remain-constant! e0) (will-eq! e0 e0)) + +(defpurefun (remained-constant e0) (eq e0 (prev e0))) +(defpurefun (will-remain-constant e0) (will-eq e0 e0)) + +;; Ensure (in loobean logic) that e0 has changed (resp. will change) its value +;; with regards to the previous (resp. next) row. +;; [TODO] (defpurefun (did-change! e0) (neq! e0 (prev e0))) +;; [TODO] (defpurefun (will-change! e0) (neq! e0 (next e0))) + +(defpurefun (did-change e0) (neq e0 (prev e0))) +(defpurefun (will-change e0) (neq e0 (next e0))) + +;; Ensure (in loobean logic) that e0 was (resp. will be) equal to e1 in the +;; previous (resp. next) row. +(defpurefun (was-eq! e0 e1) (eq! (prev e0) e1)) +(defpurefun (will-eq! e0 e1) (eq! (next e0) e1)) + +(defpurefun (was-eq e0 e1) (eq (prev e0) e1)) +(defpurefun (will-eq e0 e1) (eq (next e0) e1)) + + +;; Helpers +(defpurefun ((vanishes! :@loob :force) e0) e0) +(defpurefun (if-eq x val then) (if (eq! x val) then)) +(defpurefun (if-eq-else x val then else) (if (eq! x val) then else)) + +;; counter constancy constraint +(defpurefun ((counter-constancy :@loob) ct X) + (if-not-zero ct + (remained-constant! X))) + +;; perspective constancy constraint +(defpurefun ((perspective-constancy :@loob) PERSPECTIVE_SELECTOR X) + (if-not-zero (* PERSPECTIVE_SELECTOR (prev PERSPECTIVE_SELECTOR)) + (remained-constant! X))) + +;; base-X decomposition constraints +(defpurefun (base-X-decomposition ct base acc digits) + (if-zero-else ct + (eq! acc digits) + (eq! acc (+ (* base (prev acc)) digits)))) + +;; byte decomposition constraint +(defpurefun (byte-decomposition ct acc bytes) (base-X-decomposition ct 256 acc bytes)) + +;; bit decomposition constraint +(defpurefun (bit-decomposition ct acc bits) (base-X-decomposition ct 2 acc bits)) + +;; plateau constraints +;; [TODO] (defpurefun (plateau-constraint CT (X :binary) C) +;; (begin (debug-assert (stamp-constancy CT C)) +;; (if-zero C +;; (eq! X 1) +;; (if (eq! CT 0) +;; (vanishes! X) +;; (if (eq! CT C) +;; (did-inc! X 1) +;; (remained-constant! X)))))) + +;; stamp constancy imposes that the column C may only +;; change at rows where the STAMP column changes. +(defpurefun (stamp-constancy STAMP C) + (if (will-remain-constant! STAMP) + (will-remain-constant! C))) + +;; ============================================================================= +;; Add +;; ============================================================================= +(defpurefun (if-not-eq X Y then) + (if (eq! X Y) + ;; True branch + (vanishes! 0) + ;; False branch + then)) diff --git a/pkg/corset/symbol.go b/pkg/corset/symbol.go index c8a7ed5..d1109b7 100644 --- a/pkg/corset/symbol.go +++ b/pkg/corset/symbol.go @@ -1,6 +1,10 @@ package corset -import "github.com/consensys/go-corset/pkg/sexp" +import ( + "fmt" + + "github.com/consensys/go-corset/pkg/sexp" +) // Symbol represents a variable or function access within a declaration. // Initially, such the proper interpretation of such accesses is unclear and it @@ -30,6 +34,15 @@ type Symbol interface { Resolve(Binding) bool } +// QualifiedName returns the qualified name of a given symbol +func QualifiedName(symbol Symbol) string { + if symbol.IsQualified() { + return fmt.Sprintf("%s.%s", symbol.Module(), symbol.Name()) + } + // + return symbol.Name() +} + // SymbolDefinition represents a declaration (or part thereof) which defines a // particular symbol. For example, "defcolumns" will define one or more symbols // representing columns, etc. diff --git a/pkg/corset/translator.go b/pkg/corset/translator.go index 2e7cf61..6dcd63b 100644 --- a/pkg/corset/translator.go +++ b/pkg/corset/translator.go @@ -93,10 +93,10 @@ func (t *translator) translateDefColumns(decl *DefColumns, module string) []Synt // Add each column to schema for _, c := range decl.Columns { context := t.env.ContextFrom(module, c.LengthMultiplier()) - cid := t.schema.AddDataColumn(context, c.Name(), c.DataType()) + cid := t.schema.AddDataColumn(context, c.Name(), c.DataType().AsUnderlying()) // Prove type (if requested) if c.MustProve() { - bound := c.DataType().AsUint().Bound() + bound := c.DataType().AsUnderlying().AsUint().Bound() t.schema.AddRangeConstraint(c.Name(), context, &hir.ColumnAccess{Column: cid, Shift: 0}, bound) } // Sanity check column identifier @@ -240,8 +240,10 @@ func (t *translator) translateDefInterleaved(decl *DefInterleaved, module string } // Construct context for this assignment context := t.env.ContextFrom(module, info.multiplier) + // Extract underlying datatype + datatype := info.dataType.AsUnderlying() // Register assignment - cid := t.schema.AddAssignment(assignment.NewInterleaving(context, decl.Target.Name(), sources, info.dataType)) + cid := t.schema.AddAssignment(assignment.NewInterleaving(context, decl.Target.Name(), sources, datatype)) // Sanity check column identifiers align. if cid != info.ColumnId() { errors = append(errors, *t.srcmap.SyntaxError(decl, "invalid column identifier")) @@ -265,7 +267,10 @@ func (t *translator) translateDefPermutation(decl *DefPermutation, module string for i := 0; i < len(decl.Sources); i++ { target := t.env.Column(module, decl.Targets[i].Name()) context = t.env.ContextFrom(module, target.multiplier) - targets[i] = sc.NewColumn(context, decl.Targets[i].Name(), target.dataType) + // Extract underlying datatype + datatype := target.dataType.AsUnderlying() + // Construct columns + targets[i] = sc.NewColumn(context, decl.Targets[i].Name(), datatype) sources[i] = t.env.Column(module, decl.Sources[i].Name()).ColumnId() signs[i] = decl.Signs[i] // Record first CID @@ -358,9 +363,16 @@ func (t *translator) translateExpressionInModule(expr Expr, module string, shift return &hir.Add{Args: args}, errs } else if e, ok := expr.(*Exp); ok { return t.translateExpInModule(e, module, shift) - } else if v, ok := expr.(*IfZero); ok { + } else if v, ok := expr.(*If); ok { args, errs := t.translateExpressionsInModule([]Expr{v.Condition, v.TrueBranch, v.FalseBranch}, module) - return &hir.IfZero{Condition: args[0], TrueBranch: args[1], FalseBranch: args[2]}, errs + if v.IsIfZero() { + return &hir.IfZero{Condition: args[0], TrueBranch: args[1], FalseBranch: args[2]}, errs + } else if v.IsIfNotZero() { + // In this case, switch the ordering. + return &hir.IfZero{Condition: args[0], TrueBranch: args[2], FalseBranch: args[1]}, errs + } + // Should be unreachable + return nil, t.srcmap.SyntaxErrors(expr, "unresolved conditional") } else if e, ok := expr.(*Invoke); ok { return t.translateInvokeInModule(e, module, shift) } else if v, ok := expr.(*List); ok { @@ -403,13 +415,8 @@ func (t *translator) translateExpInModule(expr *Exp, module string, shift int) ( func (t *translator) translateInvokeInModule(expr *Invoke, module string, shift int) (hir.Expr, []SyntaxError) { if binding, ok := expr.Binding().(*FunctionBinding); ok { - if binding.Arity() == uint(len(expr.Args())) { - body := binding.Apply(expr.Args()) - return t.translateExpressionInModule(body, module, shift) - } else { - msg := fmt.Sprintf("incorrect number of arguments (expected %d, found %d)", binding.Arity(), len(expr.Args())) - return nil, t.srcmap.SyntaxErrors(expr, msg) - } + body := binding.Apply(expr.Args()) + return t.translateExpressionInModule(body, module, shift) } // return nil, t.srcmap.SyntaxErrors(expr, "unbound function") diff --git a/pkg/corset/type.go b/pkg/corset/type.go new file mode 100644 index 0000000..813a294 --- /dev/null +++ b/pkg/corset/type.go @@ -0,0 +1,173 @@ +package corset + +import ( + "fmt" + + sc "github.com/consensys/go-corset/pkg/schema" +) + +// Type embodies a richer notion of type found at the Corset level, compared +// with that found at lower levels (e.g. HIR). below. +type Type interface { + // Determines whether or not this type supports "loobean" semantics. If so, + // this means that 0 is treated as true, with anything else being false. + HasLoobeanSemantics() bool + + // Determines whether or not this type supports "boolean" semantics. If so, + // this means that 0 is treated as false, with anything else being true. + HasBooleanSemantics() bool + + // Construct a variant of this type which employs loobean semantics. This + // will panic if the type has already been given boolean semantics. + WithLoobeanSemantics() Type + + // Construct a variant of this type which employs boolean semantics. This + // will panic if the type has already been given loobean semantics. + WithBooleanSemantics() Type + + // Access an underlying representation of this type (should one exist). If + // this doesn't exist, then nil is returned. + AsUnderlying() sc.Type + + // Produce a string representation of this type. + String() string +} + +// NewFieldType constructs a native field type which, initially, has no semantic +// specified. +func NewFieldType() Type { + return &NativeType{&sc.FieldType{}, false, false} +} + +// NewUintType constructs a native uint type of the given width which, +// initially, has no semantic specified. +func NewUintType(nbits uint) Type { + return &NativeType{sc.NewUintType(nbits), false, false} +} + +// GreatestLowerBoundAll joins zero or more types together using the GLB +// operator. +func GreatestLowerBoundAll(types []Type) Type { + var datatype Type + // + for _, t := range types { + if datatype == nil { + datatype = t + } else if t != nil { + datatype = GreatestLowerBound(datatype, t) + } + } + // + return datatype +} + +// GreatestLowerBound computes the Greatest Lower Bound of two types. For +// example, the lub of u16 and u128 is u128, etc. This means that, when joining +// the bottom type with a type that has semantics, you get the former. +func GreatestLowerBound(lhs Type, rhs Type) Type { + var ( + l_loobean bool = lhs.HasLoobeanSemantics() + r_loobean bool = rhs.HasLoobeanSemantics() + l_boolean bool = lhs.HasBooleanSemantics() + r_boolean bool = rhs.HasBooleanSemantics() + ) + // Determine join of underlying types + underlying := sc.Join(lhs.AsUnderlying(), rhs.AsUnderlying()) + // + return &NativeType{underlying, l_loobean && r_loobean, l_boolean && r_boolean} +} + +// LeastUpperBoundAll joins zero or more types together using the LUB operator. +func LeastUpperBoundAll(types []Type) Type { + var datatype Type + // + for _, t := range types { + if datatype == nil { + datatype = t + } else if t != nil { + datatype = LeastUpperBound(datatype, t) + } + } + // + return datatype +} + +// LeastUpperBound computes the Least Upper Bound of two types. For example, +// the lub of u16 and u128 is u128, etc. This means that, when joining the +// bottom type with a type that has semantics, you get the latter. +func LeastUpperBound(lhs Type, rhs Type) Type { + var ( + l_loobean bool = lhs.HasLoobeanSemantics() + r_loobean bool = rhs.HasLoobeanSemantics() + l_boolean bool = lhs.HasBooleanSemantics() + r_boolean bool = rhs.HasBooleanSemantics() + ) + // Determine join of underlying types + underlying := sc.Join(lhs.AsUnderlying(), rhs.AsUnderlying()) + // + return &NativeType{underlying, l_loobean || r_loobean, l_boolean || r_boolean} +} + +// NativeType simply wraps one of the types available at the HIR level (and below). +type NativeType struct { + // The underlying type + datatype sc.Type + // Determines whether or not this type supports "loobean" semantics. If so, + // this means that 0 is treated as true, with anything else being false. + loobean bool + // Determines whether or not this type supports "boolean" semantics. If so, + // this means that 0 is treated as false, with anything else being true. + boolean bool +} + +// HasLoobeanSemantics indicates whether or not this type supports "loobean" +// semantics or not. If so, this means that 0 is treated as true, with anything +// else being false. +func (p *NativeType) HasLoobeanSemantics() bool { + return p.loobean && !p.boolean +} + +// HasBooleanSemantics indicates whether or not this type supports "boolean" +// semantics. If so, this means that 0 is treated as false, with anything else +// being true. +func (p *NativeType) HasBooleanSemantics() bool { + return p.boolean && !p.loobean +} + +// WithLoobeanSemantics constructs a variant of this type which employs loobean +// semantics. This will panic if the type has already been given boolean +// semantics. +func (p *NativeType) WithLoobeanSemantics() Type { + if p.HasBooleanSemantics() { + panic("type already given boolean semantics") + } + // Done + return &NativeType{p.datatype, true, false} +} + +// WithBooleanSemantics constructs a variant of this type which employs boolean +// semantics. This will panic if the type has already been given boolean +// semantics. +func (p *NativeType) WithBooleanSemantics() Type { + if p.HasLoobeanSemantics() { + panic("type already given loobean semantics") + } + // Done + return &NativeType{p.datatype, false, true} +} + +// AsUnderlying attempts to convert this type into an underlying type. If this +// is not possible, then nil is returned. +func (p *NativeType) AsUnderlying() sc.Type { + return p.datatype +} + +func (p *NativeType) String() string { + if p.loobean { + return fmt.Sprintf("%s@loob", p.datatype.String()) + } else if p.boolean { + return fmt.Sprintf("%s@bool", p.datatype.String()) + } + // + return p.datatype.String() +} diff --git a/pkg/schema/type.go b/pkg/schema/type.go index 1801fd6..ce9b5f9 100644 --- a/pkg/schema/type.go +++ b/pkg/schema/type.go @@ -140,7 +140,7 @@ func (p *FieldType) String() string { return "𝔽" } -// Join compute the Least Upper Bound of two types. For example, the lub of u16 +// Join computes the Least Upper Bound of two types. For example, the lub of u16 // and u128 is u128, etc. func Join(lhs Type, rhs Type) Type { if lhs.AsField() != nil || rhs.AsField() != nil { diff --git a/pkg/sexp/parser.go b/pkg/sexp/parser.go index 617eef6..276455c 100644 --- a/pkg/sexp/parser.go +++ b/pkg/sexp/parser.go @@ -173,6 +173,8 @@ func (p *Parser) parseSequence(terminator rune) ([]SExp, *SyntaxError) { } // Continue around! elements = append(elements, element) + // Skip whitespace + p.SkipWhiteSpace() } // Consume terminator p.Next() diff --git a/pkg/test/invalid_corset_test.go b/pkg/test/invalid_corset_test.go index c75ac1c..b992d4e 100644 --- a/pkg/test/invalid_corset_test.go +++ b/pkg/test/invalid_corset_test.go @@ -233,6 +233,42 @@ func Test_Invalid_If_02(t *testing.T) { CheckInvalid(t, "if_invalid_02") } +// =================================================================== +// Types +// =================================================================== + +func Test_Invalid_Type_01(t *testing.T) { + CheckInvalid(t, "type_invalid_01") +} + +func Test_Invalid_Type_02(t *testing.T) { + CheckInvalid(t, "type_invalid_02") +} + +func Test_Invalid_Type_03(t *testing.T) { + CheckInvalid(t, "type_invalid_03") +} + +func Test_Invalid_Type_04(t *testing.T) { + CheckInvalid(t, "type_invalid_04") +} + +func Test_Invalid_Type_05(t *testing.T) { + CheckInvalid(t, "type_invalid_05") +} + +func Test_Invalid_Type_06(t *testing.T) { + CheckInvalid(t, "type_invalid_06") +} + +func Test_Invalid_Type_07(t *testing.T) { + CheckInvalid(t, "type_invalid_07") +} + +func Test_Invalid_Type_08(t *testing.T) { + CheckInvalid(t, "type_invalid_08") +} + // =================================================================== // Range Constraints // =================================================================== @@ -438,6 +474,11 @@ func Test_Invalid_PureFun_07(t *testing.T) { CheckInvalid(t, "purefun_invalid_07") } +func Test_Invalid_PureFun_08(t *testing.T) { + // tricky one + CheckInvalid(t, "purefun_invalid_08") +} + // =================================================================== // Test Helpers // =================================================================== @@ -456,7 +497,7 @@ func CheckInvalid(t *testing.T, test string) { // Package up as source file srcfile := sexp.NewSourceFile(filename, bytes) // Parse terms into an HIR schema - _, errs := corset.CompileSourceFile(srcfile) + _, errs := corset.CompileSourceFile(false, srcfile) // Check program did not compile! if len(errs) == 0 { t.Fatalf("Error %s should not have compiled\n", filename) diff --git a/pkg/test/valid_corset_test.go b/pkg/test/valid_corset_test.go index bcda248..88b663c 100644 --- a/pkg/test/valid_corset_test.go +++ b/pkg/test/valid_corset_test.go @@ -27,111 +27,111 @@ const TestDir = "../../testdata" // =================================================================== func Test_Basic_01(t *testing.T) { - Check(t, "basic_01") + Check(t, false, "basic_01") } func Test_Basic_02(t *testing.T) { - Check(t, "basic_02") + Check(t, false, "basic_02") } func Test_Basic_03(t *testing.T) { - Check(t, "basic_03") + Check(t, false, "basic_03") } func Test_Basic_04(t *testing.T) { - Check(t, "basic_04") + Check(t, false, "basic_04") } func Test_Basic_05(t *testing.T) { - Check(t, "basic_05") + Check(t, false, "basic_05") } func Test_Basic_06(t *testing.T) { - Check(t, "basic_06") + Check(t, false, "basic_06") } func Test_Basic_07(t *testing.T) { - Check(t, "basic_07") + Check(t, false, "basic_07") } func Test_Basic_08(t *testing.T) { - Check(t, "basic_08") + Check(t, false, "basic_08") } func Test_Basic_09(t *testing.T) { - Check(t, "basic_09") + Check(t, false, "basic_09") } func Test_Basic_10(t *testing.T) { - Check(t, "basic_10") + Check(t, false, "basic_10") } // =================================================================== // Constants Tests // =================================================================== func Test_Constant_01(t *testing.T) { - Check(t, "constant_01") + Check(t, false, "constant_01") } func Test_Constant_02(t *testing.T) { - Check(t, "constant_02") + Check(t, false, "constant_02") } func Test_Constant_03(t *testing.T) { - Check(t, "constant_03") + Check(t, false, "constant_03") } func Test_Constant_04(t *testing.T) { - Check(t, "constant_04") + Check(t, false, "constant_04") } func Test_Constant_05(t *testing.T) { - Check(t, "constant_05") + Check(t, false, "constant_05") } func Test_Constant_06(t *testing.T) { - Check(t, "constant_06") + Check(t, false, "constant_06") } func Test_Constant_07(t *testing.T) { - Check(t, "constant_07") + Check(t, false, "constant_07") } // =================================================================== // Alias Tests // =================================================================== func Test_Alias_01(t *testing.T) { - Check(t, "alias_01") + Check(t, false, "alias_01") } func Test_Alias_02(t *testing.T) { - Check(t, "alias_02") + Check(t, false, "alias_02") } func Test_Alias_03(t *testing.T) { - Check(t, "alias_03") + Check(t, false, "alias_03") } func Test_Alias_04(t *testing.T) { - Check(t, "alias_04") + Check(t, false, "alias_04") } func Test_Alias_05(t *testing.T) { - Check(t, "alias_05") + Check(t, false, "alias_05") } func Test_Alias_06(t *testing.T) { - Check(t, "alias_06") + Check(t, false, "alias_06") } // =================================================================== // Function Alias Tests // =================================================================== func Test_FunAlias_01(t *testing.T) { - Check(t, "funalias_01") + Check(t, false, "funalias_01") } func Test_FunAlias_02(t *testing.T) { - Check(t, "funalias_02") + Check(t, false, "funalias_02") } func Test_FunAlias_03(t *testing.T) { - Check(t, "funalias_03") + Check(t, false, "funalias_03") } // =================================================================== @@ -139,15 +139,15 @@ func Test_FunAlias_03(t *testing.T) { // =================================================================== func Test_Domain_01(t *testing.T) { - Check(t, "domain_01") + Check(t, false, "domain_01") } func Test_Domain_02(t *testing.T) { - Check(t, "domain_02") + Check(t, false, "domain_02") } func Test_Domain_03(t *testing.T) { - Check(t, "domain_03") + Check(t, false, "domain_03") } // =================================================================== @@ -155,15 +155,15 @@ func Test_Domain_03(t *testing.T) { // =================================================================== func Test_Block_01(t *testing.T) { - Check(t, "block_01") + Check(t, false, "block_01") } func Test_Block_02(t *testing.T) { - Check(t, "block_02") + Check(t, false, "block_02") } func Test_Block_03(t *testing.T) { - Check(t, "block_03") + Check(t, false, "block_03") } // =================================================================== @@ -171,7 +171,7 @@ func Test_Block_03(t *testing.T) { // =================================================================== func Test_Property_01(t *testing.T) { - Check(t, "property_01") + Check(t, false, "property_01") } // =================================================================== @@ -179,35 +179,35 @@ func Test_Property_01(t *testing.T) { // =================================================================== func Test_Shift_01(t *testing.T) { - Check(t, "shift_01") + Check(t, false, "shift_01") } func Test_Shift_02(t *testing.T) { - Check(t, "shift_02") + Check(t, false, "shift_02") } func Test_Shift_03(t *testing.T) { - Check(t, "shift_03") + Check(t, false, "shift_03") } func Test_Shift_04(t *testing.T) { - Check(t, "shift_04") + Check(t, false, "shift_04") } func Test_Shift_05(t *testing.T) { - Check(t, "shift_05") + Check(t, false, "shift_05") } func Test_Shift_06(t *testing.T) { - Check(t, "shift_06") + Check(t, false, "shift_06") } func Test_Shift_07(t *testing.T) { - Check(t, "shift_07") + Check(t, false, "shift_07") } func Test_Shift_08(t *testing.T) { - Check(t, "shift_08") + Check(t, false, "shift_08") } // =================================================================== @@ -215,39 +215,39 @@ func Test_Shift_08(t *testing.T) { // =================================================================== func Test_Spillage_01(t *testing.T) { - Check(t, "spillage_01") + Check(t, false, "spillage_01") } func Test_Spillage_02(t *testing.T) { - Check(t, "spillage_02") + Check(t, false, "spillage_02") } func Test_Spillage_03(t *testing.T) { - Check(t, "spillage_03") + Check(t, false, "spillage_03") } func Test_Spillage_04(t *testing.T) { - Check(t, "spillage_04") + Check(t, false, "spillage_04") } func Test_Spillage_05(t *testing.T) { - Check(t, "spillage_05") + Check(t, false, "spillage_05") } func Test_Spillage_06(t *testing.T) { - Check(t, "spillage_06") + Check(t, false, "spillage_06") } func Test_Spillage_07(t *testing.T) { - Check(t, "spillage_07") + Check(t, false, "spillage_07") } func Test_Spillage_08(t *testing.T) { - Check(t, "spillage_08") + Check(t, false, "spillage_08") } func Test_Spillage_09(t *testing.T) { - Check(t, "spillage_09") + Check(t, false, "spillage_09") } // =================================================================== @@ -255,31 +255,31 @@ func Test_Spillage_09(t *testing.T) { // =================================================================== func Test_Norm_01(t *testing.T) { - Check(t, "norm_01") + Check(t, false, "norm_01") } func Test_Norm_02(t *testing.T) { - Check(t, "norm_02") + Check(t, false, "norm_02") } func Test_Norm_03(t *testing.T) { - Check(t, "norm_03") + Check(t, false, "norm_03") } func Test_Norm_04(t *testing.T) { - Check(t, "norm_04") + Check(t, false, "norm_04") } func Test_Norm_05(t *testing.T) { - Check(t, "norm_05") + Check(t, false, "norm_05") } func Test_Norm_06(t *testing.T) { - Check(t, "norm_06") + Check(t, false, "norm_06") } func Test_Norm_07(t *testing.T) { - Check(t, "norm_07") + Check(t, false, "norm_07") } // =================================================================== @@ -287,39 +287,43 @@ func Test_Norm_07(t *testing.T) { // =================================================================== func Test_If_01(t *testing.T) { - Check(t, "if_01") + Check(t, false, "if_01") } func Test_If_02(t *testing.T) { - Check(t, "if_02") + Check(t, false, "if_02") } func Test_If_03(t *testing.T) { - Check(t, "if_03") + Check(t, false, "if_03") } func Test_If_04(t *testing.T) { - Check(t, "if_04") + Check(t, false, "if_04") } func Test_If_05(t *testing.T) { - Check(t, "if_05") + Check(t, false, "if_05") } func Test_If_06(t *testing.T) { - Check(t, "if_06") + Check(t, false, "if_06") } func Test_If_07(t *testing.T) { - Check(t, "if_07") + Check(t, false, "if_07") } func Test_If_08(t *testing.T) { - Check(t, "if_08") + Check(t, false, "if_08") } func Test_If_09(t *testing.T) { - Check(t, "if_09") + Check(t, false, "if_09") +} + +func Test_If_10(t *testing.T) { + Check(t, false, "if_10") } // =================================================================== @@ -327,43 +331,59 @@ func Test_If_09(t *testing.T) { // =================================================================== func Test_Guard_01(t *testing.T) { - Check(t, "guard_01") + Check(t, false, "guard_01") } func Test_Guard_02(t *testing.T) { - Check(t, "guard_02") + Check(t, false, "guard_02") } func Test_Guard_03(t *testing.T) { - Check(t, "guard_03") + Check(t, false, "guard_03") } func Test_Guard_04(t *testing.T) { - Check(t, "guard_04") + Check(t, false, "guard_04") } func Test_Guard_05(t *testing.T) { - Check(t, "guard_05") + Check(t, false, "guard_05") } // =================================================================== -// Column Types +// Types // =================================================================== func Test_Type_01(t *testing.T) { - Check(t, "type_01") + Check(t, false, "type_01") } func Test_Type_02(t *testing.T) { - Check(t, "type_02") + Check(t, false, "type_02") } func Test_Type_03(t *testing.T) { - Check(t, "type_03") + Check(t, false, "type_03") } func Test_Type_04(t *testing.T) { - Check(t, "type_04") + Check(t, false, "type_04") +} + +func Test_Type_05(t *testing.T) { + Check(t, false, "type_04") +} + +func Test_Type_06(t *testing.T) { + Check(t, false, "type_06") +} + +func Test_Type_07(t *testing.T) { + Check(t, false, "type_07") +} + +func Test_Type_08(t *testing.T) { + Check(t, false, "type_08") } // =================================================================== @@ -371,23 +391,23 @@ func Test_Type_04(t *testing.T) { // =================================================================== func Test_Range_01(t *testing.T) { - Check(t, "range_01") + Check(t, false, "range_01") } func Test_Range_02(t *testing.T) { - Check(t, "range_02") + Check(t, false, "range_02") } func Test_Range_03(t *testing.T) { - Check(t, "range_03") + Check(t, false, "range_03") } func Test_Range_04(t *testing.T) { - Check(t, "range_04") + Check(t, false, "range_04") } func Test_Range_05(t *testing.T) { - Check(t, "range_05") + Check(t, false, "range_05") } // =================================================================== @@ -395,23 +415,23 @@ func Test_Range_05(t *testing.T) { // =================================================================== func Test_ConstExpr_01(t *testing.T) { - Check(t, "constexpr_01") + Check(t, false, "constexpr_01") } func Test_ConstExpr_02(t *testing.T) { - Check(t, "constexpr_02") + Check(t, false, "constexpr_02") } func Test_ConstExpr_03(t *testing.T) { - Check(t, "constexpr_03") + Check(t, false, "constexpr_03") } func Test_ConstExpr_04(t *testing.T) { - Check(t, "constexpr_04") + Check(t, false, "constexpr_04") } func Test_ConstExpr_05(t *testing.T) { - Check(t, "constexpr_05") + Check(t, false, "constexpr_05") } // =================================================================== @@ -419,39 +439,43 @@ func Test_ConstExpr_05(t *testing.T) { // =================================================================== func Test_Module_01(t *testing.T) { - Check(t, "module_01") + Check(t, false, "module_01") } func Test_Module_02(t *testing.T) { - Check(t, "module_02") + Check(t, false, "module_02") } func Test_Module_03(t *testing.T) { - Check(t, "module_03") + Check(t, false, "module_03") } func Test_Module_04(t *testing.T) { - Check(t, "module_04") + Check(t, false, "module_04") } func Test_Module_05(t *testing.T) { - Check(t, "module_05") + Check(t, false, "module_05") } func Test_Module_06(t *testing.T) { - Check(t, "module_06") + Check(t, false, "module_06") } func Test_Module_07(t *testing.T) { - Check(t, "module_07") + Check(t, false, "module_07") } func Test_Module_08(t *testing.T) { - Check(t, "module_08") + Check(t, false, "module_08") } func Test_Module_09(t *testing.T) { - Check(t, "module_09") + Check(t, false, "module_09") +} + +func Test_Module_10(t *testing.T) { + Check(t, false, "module_10") } // =================================================================== @@ -459,39 +483,39 @@ func Test_Module_09(t *testing.T) { // =================================================================== func Test_Permute_01(t *testing.T) { - Check(t, "permute_01") + Check(t, false, "permute_01") } func Test_Permute_02(t *testing.T) { - Check(t, "permute_02") + Check(t, false, "permute_02") } func Test_Permute_03(t *testing.T) { - Check(t, "permute_03") + Check(t, false, "permute_03") } func Test_Permute_04(t *testing.T) { - Check(t, "permute_04") + Check(t, false, "permute_04") } func Test_Permute_05(t *testing.T) { - Check(t, "permute_05") + Check(t, false, "permute_05") } func Test_Permute_06(t *testing.T) { - Check(t, "permute_06") + Check(t, false, "permute_06") } func Test_Permute_07(t *testing.T) { - Check(t, "permute_07") + Check(t, false, "permute_07") } func Test_Permute_08(t *testing.T) { - Check(t, "permute_08") + Check(t, false, "permute_08") } func Test_Permute_09(t *testing.T) { - Check(t, "permute_09") + Check(t, false, "permute_09") } // =================================================================== @@ -499,35 +523,35 @@ func Test_Permute_09(t *testing.T) { // =================================================================== func Test_Lookup_01(t *testing.T) { - Check(t, "lookup_01") + Check(t, false, "lookup_01") } func Test_Lookup_02(t *testing.T) { - Check(t, "lookup_02") + Check(t, false, "lookup_02") } func Test_Lookup_03(t *testing.T) { - Check(t, "lookup_03") + Check(t, false, "lookup_03") } func Test_Lookup_04(t *testing.T) { - Check(t, "lookup_04") + Check(t, false, "lookup_04") } func Test_Lookup_05(t *testing.T) { - Check(t, "lookup_05") + Check(t, false, "lookup_05") } func Test_Lookup_06(t *testing.T) { - Check(t, "lookup_06") + Check(t, false, "lookup_06") } func Test_Lookup_07(t *testing.T) { - Check(t, "lookup_07") + Check(t, false, "lookup_07") } func Test_Lookup_08(t *testing.T) { - Check(t, "lookup_08") + Check(t, false, "lookup_08") } // =================================================================== @@ -535,19 +559,19 @@ func Test_Lookup_08(t *testing.T) { // =================================================================== func Test_Interleave_01(t *testing.T) { - Check(t, "interleave_01") + Check(t, false, "interleave_01") } func Test_Interleave_02(t *testing.T) { - Check(t, "interleave_02") + Check(t, false, "interleave_02") } func Test_Interleave_03(t *testing.T) { - Check(t, "interleave_03") + Check(t, false, "interleave_03") } func Test_Interleave_04(t *testing.T) { - Check(t, "interleave_04") + Check(t, false, "interleave_04") } // =================================================================== @@ -555,27 +579,27 @@ func Test_Interleave_04(t *testing.T) { // =================================================================== func Test_Fun_01(t *testing.T) { - Check(t, "fun_01") + Check(t, false, "fun_01") } func Test_Fun_02(t *testing.T) { - Check(t, "fun_02") + Check(t, false, "fun_02") } func Test_Fun_03(t *testing.T) { - Check(t, "fun_03") + Check(t, false, "fun_03") } func Test_Fun_04(t *testing.T) { - Check(t, "fun_04") + Check(t, false, "fun_04") } func Test_Fun_05(t *testing.T) { - Check(t, "fun_05") + Check(t, false, "fun_05") } func Test_Fun_06(t *testing.T) { - Check(t, "fun_06") + Check(t, false, "fun_06") } // =================================================================== @@ -583,21 +607,21 @@ func Test_Fun_06(t *testing.T) { // =================================================================== func Test_PureFun_01(t *testing.T) { - Check(t, "purefun_01") + Check(t, false, "purefun_01") } func Test_PureFun_02(t *testing.T) { - Check(t, "purefun_02") + Check(t, false, "purefun_02") } /* func Test_PureFun_03(t *testing.T) { - Check(t, "purefun_03") + Check(t, false, "purefun_03") } */ func Test_PureFun_04(t *testing.T) { - Check(t, "purefun_04") + Check(t, false, "purefun_04") } // =================================================================== @@ -605,49 +629,49 @@ func Test_PureFun_04(t *testing.T) { // =================================================================== func Test_Counter(t *testing.T) { - Check(t, "counter") + Check(t, true, "counter") } func Test_ByteDecomp(t *testing.T) { - Check(t, "byte_decomposition") + Check(t, true, "byte_decomposition") } func Test_BitDecomp(t *testing.T) { - Check(t, "bit_decomposition") + Check(t, true, "bit_decomposition") } func Test_ByteSorting(t *testing.T) { - Check(t, "byte_sorting") + Check(t, true, "byte_sorting") } func Test_WordSorting(t *testing.T) { - Check(t, "word_sorting") + Check(t, true, "word_sorting") } func Test_Memory(t *testing.T) { - Check(t, "memory") + Check(t, true, "memory") } func TestSlow_Add(t *testing.T) { - Check(t, "add") + Check(t, true, "add") } func TestSlow_BinStatic(t *testing.T) { - Check(t, "bin-static") + Check(t, true, "bin-static") } func TestSlow_BinDynamic(t *testing.T) { - Check(t, "bin-dynamic") + Check(t, true, "bin-dynamic") } func TestSlow_Wcp(t *testing.T) { - Check(t, "wcp") + Check(t, true, "wcp") } -func TestSlow_Mxp(t *testing.T) { - Check(t, "mxp") +/* func TestSlow_Mxp(t *testing.T) { + Check(t, true, "mxp") } - +*/ // =================================================================== // Test Helpers // =================================================================== @@ -659,7 +683,7 @@ const MAX_PADDING uint = 7 // For a given set of constraints, check that all traces which we // expect to be accepted are accepted, and all traces that we expect // to be rejected are rejected. -func Check(t *testing.T, test string) { +func Check(t *testing.T, stdlib bool, test string) { filename := fmt.Sprintf("%s.lisp", test) // Enable testing each trace in parallel t.Parallel() @@ -672,7 +696,7 @@ func Check(t *testing.T, test string) { // Package up as source file srcfile := sexp.NewSourceFile(filename, bytes) // Parse terms into an HIR schema - schema, errs := corset.CompileSourceFile(srcfile) + schema, errs := corset.CompileSourceFile(stdlib, srcfile) // Check terms parsed ok if len(errs) > 0 { t.Fatalf("Error parsing %s: %v\n", filename, errs) diff --git a/testdata/add.lisp b/testdata/add.lisp index 0f056cb..d676898 100644 --- a/testdata/add.lisp +++ b/testdata/add.lisp @@ -1,30 +1,97 @@ (module add) (defcolumns - (ACC_2 :i128) - (RES_LO :i128) + (STAMP :i32) + (CT_MAX :byte) + (CT :byte) + (INST :byte :display :opcode) + (ARG_1_HI :i128) (ARG_1_LO :i128) - (OVERFLOW :binary@prove) + (ARG_2_HI :i128) + (ARG_2_LO :i128) (RES_HI :i128) - (INST :i8) + (RES_LO :i128) (BYTE_1 :byte@prove) (BYTE_2 :byte@prove) (ACC_1 :i128) - (STAMP :i32) - (ARG_1_HI :i128) - (ARG_2_LO :i128) - (ARG_2_HI :i128) - (CT_MAX :i8) - (CT :i8)) + (ACC_2 :i128) + (OVERFLOW :binary@prove)) + +(defconst + EVM_INST_STOP 0x00 + EVM_INST_ADD 0x01 + EVM_INST_MUL 0x02 + EVM_INST_SUB 0x03 + LLARGEMO 15 + LLARGE 16 + THETA 340282366920938463463374607431768211456) ;; note that 340282366920938463463374607431768211456 = 256^16 -(defconstraint adder-constraints () (if STAMP 0 (if (- CT CT_MAX) (begin (- RES_HI ACC_1) (- RES_LO ACC_2) (if (- INST 3) 0 (begin (- (+ ARG_1_LO ARG_2_LO) (+ RES_LO (* 340282366920938463463374607431768211456 OVERFLOW))) (- (+ ARG_1_HI ARG_2_HI OVERFLOW) (+ RES_HI (* 340282366920938463463374607431768211456 (shift OVERFLOW -1)))))) (if (- INST 1) 0 (begin (- (+ RES_LO ARG_2_LO) (+ ARG_1_LO (* 340282366920938463463374607431768211456 OVERFLOW))) (- (+ RES_HI ARG_2_HI OVERFLOW) (+ ARG_1_HI (* 340282366920938463463374607431768211456 (shift OVERFLOW -1)))))))))) +(defconstraint stamp-constancies () + (begin (stamp-constancy STAMP ARG_1_HI) + (stamp-constancy STAMP ARG_1_LO) + (stamp-constancy STAMP ARG_2_HI) + (stamp-constancy STAMP ARG_2_LO) + (stamp-constancy STAMP RES_HI) + (stamp-constancy STAMP RES_LO) + (stamp-constancy STAMP INST) + (stamp-constancy STAMP CT_MAX))) -(defconstraint stamp-constancies () (begin (if (- (shift STAMP 1) STAMP) (- (shift ARG_1_HI 1) ARG_1_HI)) (if (- (shift STAMP 1) STAMP) (- (shift ARG_1_LO 1) ARG_1_LO)) (if (- (shift STAMP 1) STAMP) (- (shift ARG_2_HI 1) ARG_2_HI)) (if (- (shift STAMP 1) STAMP) (- (shift ARG_2_LO 1) ARG_2_LO)) (if (- (shift STAMP 1) STAMP) (- (shift RES_HI 1) RES_HI)) (if (- (shift STAMP 1) STAMP) (- (shift RES_LO 1) RES_LO)) (if (- (shift STAMP 1) STAMP) (- (shift INST 1) INST)) (if (- (shift STAMP 1) STAMP) (- (shift CT_MAX 1) CT_MAX)))) +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 1.3 heartbeat ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;; +(defconstraint first-row (:domain {0}) + (vanishes! STAMP)) -(defconstraint heartbeat () (begin (if STAMP (begin INST)) (* (- (shift STAMP 1) STAMP) (- (shift STAMP 1) (+ STAMP 1))) (if (- (shift STAMP 1) STAMP) 0 (shift CT 1)) (if STAMP 0 (begin (* (- INST 1) (- INST 3)) (if (- 1 (~ (- CT CT_MAX))) (- (shift CT 1) (+ CT 1)) (- (shift STAMP 1) (+ STAMP 1))) (- (~ (* (- CT 16) CT_MAX)) 1))))) +(defconstraint heartbeat () + (begin (if-zero STAMP + (begin (vanishes! INST) + ;; (debug (vanishes! CT)) + ;; (debug (vanishes! CT_MAX)) + )) + (vanishes! (* (will-remain-constant! STAMP) (will-inc! STAMP 1))) + (if-not-zero (will-remain-constant! STAMP) + (vanishes! (next CT))) + (if-not-zero STAMP + (begin (vanishes! (* (eq! INST EVM_INST_ADD) (eq! INST EVM_INST_SUB))) + (if (eq CT CT_MAX) + (will-inc! STAMP 1) + (will-inc! CT 1)) + (eq! (~ (* (- CT LLARGE) CT_MAX)) + 1))))) -(defconstraint binary-and-byte-decompositions () (begin (if CT (- ACC_1 BYTE_1) (- ACC_1 (+ (* 256 (shift ACC_1 -1)) BYTE_1))) (if CT (- ACC_2 BYTE_2) (- ACC_2 (+ (* 256 (shift ACC_2 -1)) BYTE_2))))) +(defconstraint last-row (:domain {-1}) + (eq! CT CT_MAX)) -(defconstraint last-row (:domain {-1}) (- CT CT_MAX)) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 1.4 binary, bytehood and byte decompositions ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defconstraint binary-and-byte-decompositions () + (begin (byte-decomposition CT ACC_1 BYTE_1) + (byte-decomposition CT ACC_2 BYTE_2))) -(defconstraint first-row (:domain {0}) STAMP) +;; TODO: bytehood constraints +;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 1.5 constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defconstraint adder-constraints (:guard STAMP) + (if-eq CT CT_MAX + (begin (eq! RES_HI ACC_1) + (eq! RES_LO ACC_2) + (if-not-zero (- INST EVM_INST_SUB) + (begin (eq! (+ ARG_1_LO ARG_2_LO) + (+ RES_LO (* THETA OVERFLOW))) + (eq! (+ ARG_1_HI ARG_2_HI OVERFLOW) + (+ RES_HI + (* THETA (prev OVERFLOW)))))) + (if-not-zero (- INST EVM_INST_ADD) + (begin (eq! (+ RES_LO ARG_2_LO) + (+ ARG_1_LO (* THETA OVERFLOW))) + (eq! (+ RES_HI ARG_2_HI OVERFLOW) + (+ ARG_1_HI + (* THETA (prev OVERFLOW))))))))) diff --git a/testdata/alias_01.lisp b/testdata/alias_01.lisp index e4902da..a947f38 100644 --- a/testdata/alias_01.lisp +++ b/testdata/alias_01.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns COUNTER) (defalias CT COUNTER) -(defconstraint heartbeat () CT) +(defconstraint heartbeat () (vanishes! CT)) diff --git a/testdata/alias_02.lisp b/testdata/alias_02.lisp index 7c03669..d87b6da 100644 --- a/testdata/alias_02.lisp +++ b/testdata/alias_02.lisp @@ -1,13 +1,16 @@ +(defpurefun ((vanishes! :@loob) x) x) + + (defcolumns X Y) (defalias X' X Y' Y) -(defconstraint c1 () (+ X' Y')) -(defconstraint c2 () (+ Y' X')) -(defconstraint c3 () (+ X Y')) -(defconstraint c4 () (+ Y X')) -(defconstraint c5 () (+ X' Y)) -(defconstraint c6 () (+ Y' X)) -(defconstraint c7 () (+ X Y)) -(defconstraint c8 () (+ Y X)) +(defconstraint c1 () (vanishes! (+ X' Y'))) +(defconstraint c2 () (vanishes! (+ Y' X'))) +(defconstraint c3 () (vanishes! (+ X Y'))) +(defconstraint c4 () (vanishes! (+ Y X'))) +(defconstraint c5 () (vanishes! (+ X' Y))) +(defconstraint c6 () (vanishes! (+ Y' X))) +(defconstraint c7 () (vanishes! (+ X Y))) +(defconstraint c8 () (vanishes! (+ Y X))) diff --git a/testdata/alias_03.lisp b/testdata/alias_03.lisp index 8bb6933..d89bc8c 100644 --- a/testdata/alias_03.lisp +++ b/testdata/alias_03.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defconst ONE 1 TWO 2 @@ -8,11 +10,11 @@ two TWO) (defcolumns X Y) -(defconstraint c1 () (+ X (* two Y))) -(defconstraint c2 () (+ (* two Y) X)) -(defconstraint c3 () (+ X Y Y)) -(defconstraint c4 () (+ Y X Y)) -(defconstraint c5 () (+ Y Y X)) -(defconstraint c6 () (+ (* one X) Y Y)) -(defconstraint c7 () (+ Y (* one X) Y)) -(defconstraint c8 () (+ Y Y (* one X))) +(defconstraint c1 () (vanishes! (+ X (* two Y)))) +(defconstraint c2 () (vanishes! (+ (* two Y) X))) +(defconstraint c3 () (vanishes! (+ X Y Y))) +(defconstraint c4 () (vanishes! (+ Y X Y))) +(defconstraint c5 () (vanishes! (+ Y Y X))) +(defconstraint c6 () (vanishes! (+ (* one X) Y Y))) +(defconstraint c7 () (vanishes! (+ Y (* one X) Y))) +(defconstraint c8 () (vanishes! (+ Y Y (* one X)))) diff --git a/testdata/alias_04.lisp b/testdata/alias_04.lisp index 6ff2673..d46d033 100644 --- a/testdata/alias_04.lisp +++ b/testdata/alias_04.lisp @@ -1,4 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns COUNTER) (defalias CT1 COUNTER) (defalias CT2 CT1) -(defconstraint heartbeat () CT2) +(defconstraint heartbeat () (vanishes! CT2)) diff --git a/testdata/alias_05.lisp b/testdata/alias_05.lisp index 42c5a33..3ddd070 100644 --- a/testdata/alias_05.lisp +++ b/testdata/alias_05.lisp @@ -1,4 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns COUNTER) (defalias CT2 CT1) (defalias CT1 COUNTER) -(defconstraint heartbeat () CT2) +(defconstraint heartbeat () (vanishes! CT2)) diff --git a/testdata/alias_06.lisp b/testdata/alias_06.lisp index 4c41cc4..83bbdcd 100644 --- a/testdata/alias_06.lisp +++ b/testdata/alias_06.lisp @@ -1,5 +1,7 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns COUNTER) (defalias CT3 CT2) (defalias CT2 CT1) (defalias CT1 COUNTER) -(defconstraint heartbeat () CT3) +(defconstraint heartbeat () (vanishes! CT3)) diff --git a/testdata/basic_01.lisp b/testdata/basic_01.lisp index c4779bb..1ada3af 100644 --- a/testdata/basic_01.lisp +++ b/testdata/basic_01.lisp @@ -1,2 +1,2 @@ -(defcolumns X) +(defcolumns (X :byte@loob)) (defconstraint heartbeat () X) diff --git a/testdata/basic_02.lisp b/testdata/basic_02.lisp index fabc9b3..d4bf043 100644 --- a/testdata/basic_02.lisp +++ b/testdata/basic_02.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y) -(defconstraint c1 () (+ X Y)) -(defconstraint c2 () (+ Y X)) +(defconstraint c1 () (vanishes! (+ X Y))) +(defconstraint c2 () (vanishes! (+ Y X))) diff --git a/testdata/basic_03.lisp b/testdata/basic_03.lisp index cef25a2..1666fd8 100644 --- a/testdata/basic_03.lisp +++ b/testdata/basic_03.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y) -(defconstraint c1 () (- X Y)) -(defconstraint c2 () (- Y X)) +(defconstraint c1 () (vanishes! (- X Y))) +(defconstraint c2 () (vanishes! (- Y X))) diff --git a/testdata/basic_04.lisp b/testdata/basic_04.lisp index eb1ce0d..3802dc5 100644 --- a/testdata/basic_04.lisp +++ b/testdata/basic_04.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y) -(defconstraint c1 () (* X Y)) -(defconstraint c2 () (* Y X)) +(defconstraint c1 () (vanishes! (* X Y))) +(defconstraint c2 () (vanishes! (* Y X))) diff --git a/testdata/basic_05.lisp b/testdata/basic_05.lisp index b3d8f02..cd908eb 100644 --- a/testdata/basic_05.lisp +++ b/testdata/basic_05.lisp @@ -1,9 +1,11 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y) -(defconstraint c1 () (+ X (* 2 Y))) -(defconstraint c2 () (+ (* 2 Y) X)) -(defconstraint c3 () (+ X Y Y)) -(defconstraint c4 () (+ Y X Y)) -(defconstraint c5 () (+ Y Y X)) -(defconstraint c6 () (+ (* 1 X) Y Y)) -(defconstraint c7 () (+ Y (* 1 X) Y)) -(defconstraint c8 () (+ Y Y (* 1 X))) +(defconstraint c1 () (vanishes! (+ X (* 2 Y)))) +(defconstraint c2 () (vanishes! (+ (* 2 Y) X))) +(defconstraint c3 () (vanishes! (+ X Y Y))) +(defconstraint c4 () (vanishes! (+ Y X Y))) +(defconstraint c5 () (vanishes! (+ Y Y X))) +(defconstraint c6 () (vanishes! (+ (* 1 X) Y Y))) +(defconstraint c7 () (vanishes! (+ Y (* 1 X) Y))) +(defconstraint c8 () (vanishes! (+ Y Y (* 1 X)))) diff --git a/testdata/basic_06.lisp b/testdata/basic_06.lisp index b36ff53..22a6de3 100644 --- a/testdata/basic_06.lisp +++ b/testdata/basic_06.lisp @@ -1,2 +1,4 @@ +(defpurefun ((vanishes! :@loob) x) x) +;; (defcolumns X) -(defconstraint c1 () (* X (- X 1))) +(defconstraint c1 () (vanishes! (* X (- X 1)))) diff --git a/testdata/basic_07.lisp b/testdata/basic_07.lisp index 43a4ab2..d09edd3 100644 --- a/testdata/basic_07.lisp +++ b/testdata/basic_07.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y) -(defconstraint c1 () (* Y (- Y 1) (- Y 2) (- Y 3))) -(defconstraint c2 () (* (- X Y) (- X Y 4))) +(defconstraint c1 () (vanishes! (* Y (- Y 1) (- Y 2) (- Y 3)))) +(defconstraint c2 () (vanishes! (* (- X Y) (- X Y 4)))) diff --git a/testdata/basic_08.lisp b/testdata/basic_08.lisp index 2055c1d..12e120e 100644 --- a/testdata/basic_08.lisp +++ b/testdata/basic_08.lisp @@ -1,4 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y Z) -(defconstraint c1 () (* Z (- Z 1))) -(defconstraint c2 () (* (- Y Z) (- Y Z 2))) -(defconstraint c3 () (* (- X Y) (- X Y 4))) +(defconstraint c1 () (vanishes! (* Z (- Z 1)))) +(defconstraint c2 () (vanishes! (* (- Y Z) (- Y Z 2)))) +(defconstraint c3 () (vanishes! (* (- X Y) (- X Y 4)))) diff --git a/testdata/basic_09.lisp b/testdata/basic_09.lisp index 63e3947..c353c4a 100644 --- a/testdata/basic_09.lisp +++ b/testdata/basic_09.lisp @@ -1,2 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns CT) -(defconstraint c1 () (* (- CT (shift CT 1)) (- (+ CT 1) (shift CT 1)))) +(defconstraint c1 () (vanishes! + (* (- CT (shift CT 1)) (- (+ CT 1) (shift CT 1))))) diff --git a/testdata/basic_10.lisp b/testdata/basic_10.lisp index 2be570a..a81f65d 100644 --- a/testdata/basic_10.lisp +++ b/testdata/basic_10.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y) ;; Y == X*X -(defconstraint c1 () (- Y (^ X 2))) +(defconstraint c1 () (vanishes! (- Y (^ X 2)))) diff --git a/testdata/bin-dynamic.lisp b/testdata/bin-dynamic.lisp index 0ebbf90..5e5a909 100644 --- a/testdata/bin-dynamic.lisp +++ b/testdata/bin-dynamic.lisp @@ -4,7 +4,7 @@ (STAMP :i32) (CT_MAX :byte) (COUNTER :byte) - (INST :byte) + (INST :byte :display :opcode) (ARGUMENT_1_HI :i128) (ARGUMENT_1_LO :i128) (ARGUMENT_2_HI :i128) @@ -40,42 +40,230 @@ (XXX_BYTE_HI :byte) (XXX_BYTE_LO :byte)) -(defconstraint byte_decompositions () (begin (if COUNTER (- ACC_1 BYTE_1) (- ACC_1 (+ (* 256 (shift ACC_1 -1)) BYTE_1))) (if COUNTER (- ACC_2 BYTE_2) (- ACC_2 (+ (* 256 (shift ACC_2 -1)) BYTE_2))) (if COUNTER (- ACC_3 BYTE_3) (- ACC_3 (+ (* 256 (shift ACC_3 -1)) BYTE_3))) (if COUNTER (- ACC_4 BYTE_4) (- ACC_4 (+ (* 256 (shift ACC_4 -1)) BYTE_4))) (if COUNTER (- ACC_5 BYTE_5) (- ACC_5 (+ (* 256 (shift ACC_5 -1)) BYTE_5))) (if COUNTER (- ACC_6 BYTE_6) (- ACC_6 (+ (* 256 (shift ACC_6 -1)) BYTE_6))))) +;; aliases +(defalias + CT COUNTER + ARG_1_HI ARGUMENT_1_HI + ARG_1_LO ARGUMENT_1_LO + ARG_2_HI ARGUMENT_2_HI + ARG_2_LO ARGUMENT_2_LO + RES_HI RESULT_HI + RES_LO RESULT_LO) -(defconstraint bits-and-related () (if (+ IS_BYTE IS_SIGNEXTEND) 0 (if (- COUNTER 15) (begin (- PIVOT (+ (* 128 (shift BITS -15)) (* 64 (shift BITS -14)) (* 32 (shift BITS -13)) (* 16 (shift BITS -12)) (* 8 (shift BITS -11)) (* 4 (shift BITS -10)) (* 2 (shift BITS -9)) (shift BITS -8))) (- BYTE_2 (+ (* 128 (shift BITS -7)) (* 64 (shift BITS -6)) (* 32 (shift BITS -5)) (* 16 (shift BITS -4)) (* 8 (shift BITS -3)) (* 4 (shift BITS -2)) (* 2 (shift BITS -1)) BITS)) (- LOW_4 (+ (* 8 (shift BITS -3)) (* 4 (shift BITS -2)) (* 2 (shift BITS -1)) BITS)) (- BIT_B_4 (shift BITS -4)) (- NEG (shift BITS -15)))))) +(defconst + ;; opcode values + SIGNEXTEND 11 + AND 22 + OR 23 + XOR 24 + NOT 25 + BYTE 26 + ;; constant values + LLARGE 16 + LLARGEMO 15) -(defconstraint pivot () (if CT_MAX 0 (begin (if (- IS_BYTE 1) (if LOW_4 (if COUNTER (if BIT_B_4 (- PIVOT BYTE_3) (- PIVOT BYTE_4))) (if (+ (shift BIT_1 -1) (- 1 BIT_1)) (if BIT_B_4 (- PIVOT BYTE_3) (- PIVOT BYTE_4))))) (if (- IS_SIGNEXTEND 1) (if (- LOW_4 15) (if COUNTER (if BIT_B_4 (- PIVOT BYTE_4) (- PIVOT BYTE_3))) (if (+ (shift BIT_1 -1) (- 1 BIT_1)) (if BIT_B_4 (- PIVOT BYTE_4) (- PIVOT BYTE_3)))))))) +(defpurefun (if-eq-else A B THEN ELSE) + (if-zero-else (- A B) + THEN + ELSE)) -(defconstraint counter-constancies () (begin (if COUNTER 0 (- ARGUMENT_1_HI (shift ARGUMENT_1_HI -1))) (if COUNTER 0 (- ARGUMENT_1_LO (shift ARGUMENT_1_LO -1))) (if COUNTER 0 (- ARGUMENT_2_HI (shift ARGUMENT_2_HI -1))) (if COUNTER 0 (- ARGUMENT_2_LO (shift ARGUMENT_2_LO -1))) (if COUNTER 0 (- RESULT_HI (shift RESULT_HI -1))) (if COUNTER 0 (- RESULT_LO (shift RESULT_LO -1))) (if COUNTER 0 (- INST (shift INST -1))) (if COUNTER 0 (- CT_MAX (shift CT_MAX -1))) (if COUNTER 0 (- PIVOT (shift PIVOT -1))) (if COUNTER 0 (- BIT_B_4 (shift BIT_B_4 -1))) (if COUNTER 0 (- LOW_4 (shift LOW_4 -1))) (if COUNTER 0 (- NEG (shift NEG -1))) (if COUNTER 0 (- SMALL (shift SMALL -1))))) +;; 2.2 Shorthands +(defun (flag-sum) + (+ IS_AND IS_OR IS_XOR IS_NOT IS_BYTE IS_SIGNEXTEND)) -(defconstraint bit_1 () (if CT_MAX 0 (begin (if (- IS_BYTE 1) (begin (if LOW_4 (- BIT_1 1) (if (- COUNTER 0) BIT_1 (if (- COUNTER LOW_4) (- BIT_1 (+ (shift BIT_1 -1) 1)) (- BIT_1 (shift BIT_1 -1))))))) (if (- IS_SIGNEXTEND 1) (begin (if (- 15 LOW_4) (- BIT_1 1) (if (- COUNTER 0) BIT_1 (if (- COUNTER (- 15 LOW_4)) (- BIT_1 (+ (shift BIT_1 -1) 1)) (- BIT_1 (shift BIT_1 -1)))))))))) +(defun (weight-sum) + (+ (* IS_AND AND) + (* IS_OR OR) + (* IS_XOR XOR) + (* IS_NOT NOT) + (* IS_BYTE BYTE) + (* IS_SIGNEXTEND SIGNEXTEND))) -(defconstraint is-signextend-result () (if IS_SIGNEXTEND 0 (if CT_MAX (begin (- RESULT_HI ARGUMENT_2_HI) (- RESULT_LO ARGUMENT_2_LO)) (if SMALL (begin (- RESULT_HI ARGUMENT_2_HI) (- RESULT_LO ARGUMENT_2_LO)) (begin (if BIT_B_4 (begin (- BYTE_5 (* NEG 255)) (if BIT_1 (- BYTE_6 (* NEG 255)) (- BYTE_6 BYTE_4))) (begin (if BIT_1 (- BYTE_5 (* NEG 255)) (- BYTE_5 BYTE_3)) (- RESULT_LO ARGUMENT_2_LO)))))))) +;; 2.3 Instruction decoding +(defconstraint no-bin-no-flag () + (if-zero-else STAMP + (vanishes! (flag-sum)) + (eq! (flag-sum) 1))) -(defconstraint small () (if (+ IS_BYTE IS_SIGNEXTEND) 0 (if (- COUNTER 15) (if ARGUMENT_1_HI (if (- ARGUMENT_1_LO (+ (* 16 (shift BITS -4)) (* 8 (shift BITS -3)) (* 4 (shift BITS -2)) (* 2 (shift BITS -1)) BITS)) (- SMALL 1) SMALL))))) +(defconstraint inst-to-flag () + (eq! INST (weight-sum))) -(defconstraint inst-to-flag () (- INST (+ (* IS_AND 22) (* IS_OR 23) (* IS_XOR 24) (* IS_NOT 25) (* IS_BYTE 26) (* IS_SIGNEXTEND 11)))) +;; 2.4 Heartbeat +(defconstraint first-row (:domain {0}) + (vanishes! STAMP)) -(defconstraint target-constraints () (if (- COUNTER CT_MAX) (begin (- ACC_1 ARGUMENT_1_HI) (- ACC_2 ARGUMENT_1_LO) (- ACC_3 ARGUMENT_2_HI) (- ACC_4 ARGUMENT_2_LO) (- ACC_5 RESULT_HI) (- ACC_6 RESULT_LO)))) +(defconstraint stamp-increments () + (vanishes! (* (will-inc! STAMP 0) (will-inc! STAMP 1)))) -(defconstraint countereset () (if STAMP 0 (if (- COUNTER CT_MAX) (- (shift STAMP 1) (+ STAMP 1)) (- (shift COUNTER 1) (+ COUNTER 1))))) +(defconstraint new-stamp-reset-ct () + (if-not-zero (- (next STAMP) STAMP) + (vanishes! (next CT)))) -(defconstraint stamp-increments () (* (- (shift STAMP 1) (+ STAMP 0)) (- (shift STAMP 1) (+ STAMP 1)))) +(defconstraint isnot-ctmax () + (if-eq IS_NOT 1 (eq! CT_MAX LLARGEMO))) -(defconstraint isbyte-ctmax () (if (- (+ IS_BYTE IS_SIGNEXTEND) 1) (if ARGUMENT_1_HI (- CT_MAX 15) CT_MAX))) +(defconstraint isbyte-ctmax () + (if-eq (+ IS_BYTE IS_SIGNEXTEND) 1 + (if-zero-else ARG_1_HI + (eq! CT_MAX LLARGEMO) + (vanishes! CT_MAX)))) -(defconstraint no-bin-no-flag () (if STAMP (+ IS_AND IS_OR IS_XOR IS_NOT IS_BYTE IS_SIGNEXTEND) (- (+ IS_AND IS_OR IS_XOR IS_NOT IS_BYTE IS_SIGNEXTEND) 1))) +(defconstraint ct-small () + (eq! 1 + (~ (- CT LLARGE)))) -(defconstraint is-byte-result () (if IS_BYTE 0 (if CT_MAX (begin RESULT_HI RESULT_LO) (begin RESULT_HI (- RESULT_LO (* SMALL PIVOT)))))) +(defconstraint countereset (:guard STAMP) + (if-eq-else CT CT_MAX (will-inc! STAMP 1) (will-inc! CT 1))) -(defconstraint result-via-deflookup () (if (+ IS_AND IS_OR IS_XOR IS_NOT) 0 (begin (- BYTE_5 XXX_BYTE_HI) (- BYTE_6 XXX_BYTE_LO)))) +(defconstraint last-row (:domain {-1}) + (eq! CT CT_MAX)) -(defconstraint isnot-ctmax () (if (- IS_NOT 1) (- CT_MAX 15))) +(defconstraint counter-constancies () + (begin (counter-constancy CT ARG_1_HI) + (counter-constancy CT ARG_1_LO) + (counter-constancy CT ARG_2_HI) + (counter-constancy CT ARG_2_LO) + (counter-constancy CT RES_HI) + (counter-constancy CT RES_LO) + (counter-constancy CT INST) + (counter-constancy CT CT_MAX) + (counter-constancy CT PIVOT) + (counter-constancy CT BIT_B_4) + (counter-constancy CT LOW_4) + (counter-constancy CT NEG) + (counter-constancy CT SMALL))) -(defconstraint ct-small () (- 1 (~ (- COUNTER 16)))) +;; 2.6 byte decompositions +(defconstraint byte_decompositions () + (begin (byte-decomposition CT ACC_1 BYTE_1) + (byte-decomposition CT ACC_2 BYTE_2) + (byte-decomposition CT ACC_3 BYTE_3) + (byte-decomposition CT ACC_4 BYTE_4) + (byte-decomposition CT ACC_5 BYTE_5) + (byte-decomposition CT ACC_6 BYTE_6))) -(defconstraint new-stamp-reset-ct () (if (- (shift STAMP 1) STAMP) 0 (shift COUNTER 1))) +;; 2.7 target constraints +(defconstraint target-constraints () + (if-eq CT CT_MAX + (begin (eq! ACC_1 ARG_1_HI) + (eq! ACC_2 ARG_1_LO) + (eq! ACC_3 ARG_2_HI) + (eq! ACC_4 ARG_2_LO) + (eq! ACC_5 RES_HI) + (eq! ACC_6 RES_LO)))) -(defconstraint last-row (:domain {-1}) (- COUNTER CT_MAX)) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.8 binary column constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; 2.8.2 BITS and related columns +(defconstraint bits-and-related (:guard (+ IS_BYTE IS_SIGNEXTEND)) + (if-eq CT LLARGEMO + (begin (eq! PIVOT + (+ (* 128 (shift BITS -15)) + (* 64 (shift BITS -14)) + (* 32 (shift BITS -13)) + (* 16 (shift BITS -12)) + (* 8 (shift BITS -11)) + (* 4 (shift BITS -10)) + (* 2 (shift BITS -9)) + (shift BITS -8))) + (eq! BYTE_2 + (+ (* 128 (shift BITS -7)) + (* 64 (shift BITS -6)) + (* 32 (shift BITS -5)) + (* 16 (shift BITS -4)) + (* 8 (shift BITS -3)) + (* 4 (shift BITS -2)) + (* 2 (shift BITS -1)) + BITS)) + (eq! LOW_4 + (+ (* 8 (shift BITS -3)) + (* 4 (shift BITS -2)) + (* 2 (shift BITS -1)) + BITS)) + (eq! BIT_B_4 (shift BITS -4)) + (eq! NEG (shift BITS -15))))) -(defconstraint first-row (:domain {0}) STAMP) +;; 2.8.3 [[1]] constraints +;; (defconstraint bit_1 (:guard CT_MAX) +;; (begin (if-eq IS_BYTE 1 (plateau-constraint CT BIT_1 LOW_4)) +;; (if-eq IS_SIGNEXTEND 1 +;; (plateau-constraint CT BIT_1 (- LLARGEMO LOW_4))))) + +;; 2.8.4 SMALL constraints +(defconstraint small (:guard (+ IS_BYTE IS_SIGNEXTEND)) + (if-eq CT LLARGEMO + (if-zero ARG_1_HI + (if-eq-else ARG_1_LO (+ (* 16 (shift BITS -4)) + (* 8 (shift BITS -3)) + (* 4 (shift BITS -2)) + (* 2 (shift BITS -1)) + BITS) + (eq! SMALL 1) + (vanishes! SMALL))))) + +;; 2.9 pivot constraints +(defconstraint pivot (:guard CT_MAX) + (begin (if-eq IS_BYTE 1 + (if-zero-else LOW_4 + (if-zero CT + (if-zero-else BIT_B_4 + (eq! PIVOT BYTE_3) + (eq! PIVOT BYTE_4))) + (if-zero (+ (prev BIT_1) (- 1 BIT_1)) + (if-zero-else BIT_B_4 + (eq! PIVOT BYTE_3) + (eq! PIVOT BYTE_4))))) + (if-eq IS_SIGNEXTEND 1 + (if-eq-else LOW_4 LLARGEMO + (if-zero CT + (if-zero-else BIT_B_4 + (eq! PIVOT BYTE_4) + (eq! PIVOT BYTE_3))) + (if-zero (+ (prev BIT_1) (- 1 BIT_1)) + (if-zero-else BIT_B_4 + (eq! PIVOT BYTE_4) + (eq! PIVOT BYTE_3))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.10 result constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defconstraint is-byte-result (:guard IS_BYTE) + (if-zero-else CT_MAX + (begin (vanishes! RES_HI) + (vanishes! RES_LO)) + (begin (vanishes! RES_HI) + (eq! RES_LO (* SMALL PIVOT))))) + +(defconstraint is-signextend-result (:guard IS_SIGNEXTEND) + (if-zero-else CT_MAX + (begin (eq! RES_HI ARG_2_HI) + (eq! RES_LO ARG_2_LO)) + (if-zero-else SMALL + ;; SMALL == 0 + (begin (eq! RES_HI ARG_2_HI) + (eq! RES_LO ARG_2_LO)) + ;; SMALL == 1 + (begin (if-zero-else BIT_B_4 + ;; b4 == 0 + (begin (eq! BYTE_5 (* NEG 255)) + (if-zero-else BIT_1 + ;; [[1]] == 0 + (eq! BYTE_6 (* NEG 255)) + ;; [[1]] == 1 + (eq! BYTE_6 BYTE_4))) + ;; b4 == 1 + (begin (if-zero-else BIT_1 + ;; [[1]] == 0 + (eq! BYTE_5 (* NEG 255)) + ;; [[1]] == 1 + (eq! BYTE_5 BYTE_3)) + (eq! RES_LO ARG_2_LO))))))) + +(defconstraint result-via-lookup (:guard (+ IS_AND IS_OR IS_XOR IS_NOT)) + (begin (eq! BYTE_5 XXX_BYTE_HI) + (eq! BYTE_6 XXX_BYTE_LO))) diff --git a/testdata/bin-static.lisp b/testdata/bin-static.lisp index ca69c33..24e60a5 100644 --- a/testdata/bin-static.lisp +++ b/testdata/bin-static.lisp @@ -41,45 +41,244 @@ (XXX_BYTE_HI :byte) (XXX_BYTE_LO :byte)) +;; aliases +(defalias + OLI ONE_LINE_INSTRUCTION + CT COUNTER + ARG_1_HI ARGUMENT_1_HI + ARG_1_LO ARGUMENT_1_LO + ARG_2_HI ARGUMENT_2_HI + ARG_2_LO ARGUMENT_2_LO + RES_HI RESULT_HI + RES_LO RESULT_LO) -(defconstraint byte_decompositions () (begin (if COUNTER (- ACC_1 BYTE_1) (- ACC_1 (+ (* 256 (shift ACC_1 -1)) BYTE_1))) (if COUNTER (- ACC_2 BYTE_2) (- ACC_2 (+ (* 256 (shift ACC_2 -1)) BYTE_2))) (if COUNTER (- ACC_3 BYTE_3) (- ACC_3 (+ (* 256 (shift ACC_3 -1)) BYTE_3))) (if COUNTER (- ACC_4 BYTE_4) (- ACC_4 (+ (* 256 (shift ACC_4 -1)) BYTE_4))) (if COUNTER (- ACC_5 BYTE_5) (- ACC_5 (+ (* 256 (shift ACC_5 -1)) BYTE_5))) (if COUNTER (- ACC_6 BYTE_6) (- ACC_6 (+ (* 256 (shift ACC_6 -1)) BYTE_6))))) +(defconst + ;; opcode values + SIGNEXTEND 11 + AND 22 + OR 23 + XOR 24 + NOT 25 + BYTE 26 + ;; constant values + LLARGE 16 + LLARGEMO 15) -(defconstraint bits-and-related () (if (- COUNTER 15) (begin (- PIVOT (+ (* 128 (shift BITS -15)) (* 64 (shift BITS -14)) (* 32 (shift BITS -13)) (* 16 (shift BITS -12)) (* 8 (shift BITS -11)) (* 4 (shift BITS -10)) (* 2 (shift BITS -9)) (shift BITS -8))) (- BYTE_2 (+ (* 128 (shift BITS -7)) (* 64 (shift BITS -6)) (* 32 (shift BITS -5)) (* 16 (shift BITS -4)) (* 8 (shift BITS -3)) (* 4 (shift BITS -2)) (* 2 (shift BITS -1)) BITS)) (- LOW_4 (+ (* 8 (shift BITS -3)) (* 4 (shift BITS -2)) (* 2 (shift BITS -1)) BITS)) (- BIT_B_4 (shift BITS -4)) (- NEG (shift BITS -15))))) +(defpurefun (if-eq-else A B THEN ELSE) + (if-zero-else (- A B) + THEN + ELSE)) -(defconstraint pivot () (if MLI 0 (begin (if IS_BYTE 0 (if LOW_4 (if COUNTER (if BIT_B_4 (- PIVOT BYTE_3) (- PIVOT BYTE_4))) (if (+ (shift BIT_1 -1) (- 1 BIT_1)) (if BIT_B_4 (- PIVOT BYTE_3) (- PIVOT BYTE_4))))) (if IS_SIGNEXTEND 0 (if (- LOW_4 15) (if COUNTER (if BIT_B_4 (- PIVOT BYTE_4) (- PIVOT BYTE_3))) (if (+ (shift BIT_1 -1) (- 1 BIT_1)) (if BIT_B_4 (- PIVOT BYTE_4) (- PIVOT BYTE_3)))))))) +;; 2.1 binary constraints +;; binary constraints +(defconstraint binary_constraints () + (begin (is-binary IS_AND) + (is-binary IS_OR) + (is-binary IS_XOR) + (is-binary IS_NOT) + (is-binary IS_BYTE) + (is-binary IS_SIGNEXTEND) + (is-binary SMALL) + (is-binary BITS) + (is-binary NEG) + (is-binary BIT_B_4) + (is-binary BIT_1))) -(defconstraint bit_1 () (begin (if (- IS_BYTE 1) (begin (if LOW_4 (- BIT_1 1) (if (- COUNTER 0) BIT_1 (if (- COUNTER LOW_4) (- BIT_1 (+ (shift BIT_1 -1) 1)) (- BIT_1 (shift BIT_1 -1))))))) (if (- IS_SIGNEXTEND 1) (begin (if (- 15 LOW_4) (- BIT_1 1) (if (- COUNTER 0) BIT_1 (if (- COUNTER (- 15 LOW_4)) (- BIT_1 (+ (shift BIT_1 -1) 1)) (- BIT_1 (shift BIT_1 -1))))))))) +;; 2.2 Shorthands +(defun (flag-sum) + (+ IS_AND IS_OR IS_XOR IS_NOT IS_BYTE IS_SIGNEXTEND)) -(defconstraint binary_constraints () (begin (* IS_AND (- 1 IS_AND)) (* IS_OR (- 1 IS_OR)) (* IS_XOR (- 1 IS_XOR)) (* IS_NOT (- 1 IS_NOT)) (* IS_BYTE (- 1 IS_BYTE)) (* IS_SIGNEXTEND (- 1 IS_SIGNEXTEND)) (* SMALL (- 1 SMALL)) (* BITS (- 1 BITS)) (* NEG (- 1 NEG)) (* BIT_B_4 (- 1 BIT_B_4)) (* BIT_1 (- 1 BIT_1)))) +(defun (weight-sum) + (+ (* IS_AND AND) + (* IS_OR OR) + (* IS_XOR XOR) + (* IS_NOT NOT) + (* IS_BYTE BYTE) + (* IS_SIGNEXTEND SIGNEXTEND))) -(defconstraint counter-constancies () (begin (if COUNTER 0 (- ARGUMENT_1_HI (shift ARGUMENT_1_HI -1))) (if COUNTER 0 (- ARGUMENT_1_LO (shift ARGUMENT_1_LO -1))) (if COUNTER 0 (- ARGUMENT_2_HI (shift ARGUMENT_2_HI -1))) (if COUNTER 0 (- ARGUMENT_2_LO (shift ARGUMENT_2_LO -1))) (if COUNTER 0 (- RESULT_HI (shift RESULT_HI -1))) (if COUNTER 0 (- RESULT_LO (shift RESULT_LO -1))) (if COUNTER 0 (- INST (shift INST -1))) (if COUNTER 0 (- PIVOT (shift PIVOT -1))) (if COUNTER 0 (- BIT_B_4 (shift BIT_B_4 -1))) (if COUNTER 0 (- LOW_4 (shift LOW_4 -1))) (if COUNTER 0 (- NEG (shift NEG -1))))) +;; 2.3 Instruction decoding +(defconstraint no-bin-no-flag () + (if-zero-else STAMP + (vanishes! (flag-sum)) + (eq! (flag-sum) 1))) -(defconstraint is-signextend-result () (if IS_SIGNEXTEND 0 (if (- ONE_LINE_INSTRUCTION 1) (begin (- RESULT_HI ARGUMENT_2_HI) (- RESULT_LO ARGUMENT_2_LO)) (if SMALL (begin (- RESULT_HI ARGUMENT_2_HI) (- RESULT_LO ARGUMENT_2_LO)) (begin (if BIT_B_4 (begin (- BYTE_5 (* NEG 255)) (if BIT_1 (- BYTE_6 (* NEG 255)) (- BYTE_6 BYTE_4))) (begin (if BIT_1 (- BYTE_5 (* NEG 255)) (- BYTE_5 BYTE_3)) (- RESULT_LO ARGUMENT_2_LO)))))))) +(defconstraint inst-to-flag () + (eq! INST (weight-sum))) -(defconstraint small () (if (- COUNTER 15) (if ARGUMENT_1_HI (if (- ARGUMENT_1_LO (+ (* 16 (shift BITS -4)) (* 8 (shift BITS -3)) (* 4 (shift BITS -2)) (* 2 (shift BITS -1)) BITS)) (- SMALL 1) SMALL)))) +;; 2.4 Heartbeat +(defconstraint first-row (:domain {0}) + (vanishes! STAMP)) -(defconstraint inst-to-flag () (- INST (+ (* IS_AND 22) (* IS_OR 23) (* IS_XOR 24) (* IS_NOT 25) (* IS_BYTE 26) (* IS_SIGNEXTEND 11)))) +(defconstraint stamp-increments () + (vanishes! (* (will-inc! STAMP 0) (will-inc! STAMP 1)))) -(defconstraint target-constraints () (if (- COUNTER 15) (begin (- ACC_1 ARGUMENT_1_HI) (- ACC_2 ARGUMENT_1_LO) (- ACC_3 ARGUMENT_2_HI) (- ACC_4 ARGUMENT_2_LO) (- ACC_5 RESULT_HI) (- ACC_6 RESULT_LO)))) +(defconstraint countereset () + (if-not-zero (will-remain-constant! STAMP) + (vanishes! (next CT)))) -(defconstraint mli-incrementation () (if MLI 0 (if (- COUNTER 15) (- (shift STAMP 1) (+ STAMP 1)) (- (shift COUNTER 1) (+ COUNTER 1))))) +(defconstraint oli-incrementation (:guard OLI) + (will-inc! STAMP 1)) -(defconstraint stamp-increments () (* (- (shift STAMP 1) (+ STAMP 0)) (- (shift STAMP 1) (+ STAMP 1)))) +(defconstraint mli-incrementation (:guard MLI) + (if-eq-else CT LLARGEMO (will-inc! STAMP 1) (will-inc! CT 1))) -(defconstraint is-byte-result () (if IS_BYTE 0 (if (- ONE_LINE_INSTRUCTION 1) (begin RESULT_HI RESULT_LO) (begin RESULT_HI (- RESULT_LO (* SMALL PIVOT)))))) +(defconstraint last-row (:domain {-1}) + (if-eq MLI 1 (eq! CT LLARGEMO))) -(defconstraint no-bin-no-flag () (if STAMP (+ IS_AND IS_OR IS_XOR IS_NOT IS_BYTE IS_SIGNEXTEND) (- (+ IS_AND IS_OR IS_XOR IS_NOT IS_BYTE IS_SIGNEXTEND) 1))) +(defconstraint counter-constancies () + (begin (counter-constancy CT ARG_1_HI) + (counter-constancy CT ARG_1_LO) + (counter-constancy CT ARG_2_HI) + (counter-constancy CT ARG_2_LO) + (counter-constancy CT RES_HI) + (counter-constancy CT RES_LO) + (counter-constancy CT INST) + (counter-constancy CT PIVOT) + (counter-constancy CT BIT_B_4) + (counter-constancy CT LOW_4) + (counter-constancy CT NEG))) -(defconstraint set-oli-mli () (if (+ IS_BYTE IS_SIGNEXTEND) ONE_LINE_INSTRUCTION (if ARGUMENT_1_HI ONE_LINE_INSTRUCTION (- ONE_LINE_INSTRUCTION 1)))) +;; 2.6 byte decompositions +(defconstraint byte_decompositions () + (begin (byte-decomposition CT ACC_1 BYTE_1) + (byte-decomposition CT ACC_2 BYTE_2) + (byte-decomposition CT ACC_3 BYTE_3) + (byte-decomposition CT ACC_4 BYTE_4) + (byte-decomposition CT ACC_5 BYTE_5) + (byte-decomposition CT ACC_6 BYTE_6))) -(defconstraint result-via-deflookup () (if (+ IS_AND IS_OR IS_XOR IS_NOT) 0 (begin (- BYTE_5 XXX_BYTE_HI) (- BYTE_6 XXX_BYTE_LO)))) +;; 2.7 target constraints +(defconstraint target-constraints () + (if-eq CT LLARGEMO + (begin (eq! ACC_1 ARG_1_HI) + (eq! ACC_2 ARG_1_LO) + (eq! ACC_3 ARG_2_HI) + (eq! ACC_4 ARG_2_LO) + (eq! ACC_5 RES_HI) + (eq! ACC_6 RES_LO)))) -(defconstraint oli-incrementation () (if ONE_LINE_INSTRUCTION 0 (- (shift STAMP 1) (+ STAMP 1)))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.8 binary column constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defconstraint set-oli-mli () + (if-zero-else (+ IS_BYTE IS_SIGNEXTEND) + (vanishes! OLI) + (if-zero-else ARG_1_HI + (vanishes! OLI) + (eq! OLI 1)))) -(defconstraint last-row (:domain {-1}) (if (- MLI 1) (- COUNTER 15))) +(defconstraint oli-mli-exclusivity () + (eq! (+ OLI MLI) (flag-sum))) -(defconstraint oli-mli-exclusivity () (- (+ ONE_LINE_INSTRUCTION MLI) (+ IS_AND IS_OR IS_XOR IS_NOT IS_BYTE IS_SIGNEXTEND))) +;; 2.8.2 BITS and related columns +(defconstraint bits-and-related () + (if-eq CT LLARGEMO + (begin (eq! PIVOT + (+ (* 128 (shift BITS -15)) + (* 64 (shift BITS -14)) + (* 32 (shift BITS -13)) + (* 16 (shift BITS -12)) + (* 8 (shift BITS -11)) + (* 4 (shift BITS -10)) + (* 2 (shift BITS -9)) + (shift BITS -8))) + (eq! BYTE_2 + (+ (* 128 (shift BITS -7)) + (* 64 (shift BITS -6)) + (* 32 (shift BITS -5)) + (* 16 (shift BITS -4)) + (* 8 (shift BITS -3)) + (* 4 (shift BITS -2)) + (* 2 (shift BITS -1)) + BITS)) + (eq! LOW_4 + (+ (* 8 (shift BITS -3)) + (* 4 (shift BITS -2)) + (* 2 (shift BITS -1)) + BITS)) + (eq! BIT_B_4 (shift BITS -4)) + (eq! NEG (shift BITS -15))))) -(defconstraint countereset () (if (- (shift STAMP 1) STAMP) 0 (shift COUNTER 1))) +;; 2.8.3 [[1]] constraints +;; (defconstraint bit_1 () +;; (begin (if-eq IS_BYTE 1 (plateau-constraint CT BIT_1 LOW_4)) +;; (if-eq IS_SIGNEXTEND 1 +;; (plateau-constraint CT BIT_1 (- LLARGEMO LOW_4))))) -(defconstraint first-row (:domain {0}) STAMP) +;; 2.8.4 SMALL constraints +(defconstraint small () + (if-eq CT LLARGEMO + (if-zero ARG_1_HI + (if-eq-else ARG_1_LO (+ (* 16 (shift BITS -4)) + (* 8 (shift BITS -3)) + (* 4 (shift BITS -2)) + (* 2 (shift BITS -1)) + BITS) + (eq! SMALL 1) + (vanishes! SMALL))))) + +;; 2.9 pivot constraints +(defconstraint pivot (:guard MLI) + (begin (if-not-zero IS_BYTE + (if-zero-else LOW_4 + (if-zero CT + (if-zero-else BIT_B_4 + (eq! PIVOT BYTE_3) + (eq! PIVOT BYTE_4))) + (if-zero (+ (prev BIT_1) (- 1 BIT_1)) + (if-zero-else BIT_B_4 + (eq! PIVOT BYTE_3) + (eq! PIVOT BYTE_4))))) + (if-not-zero IS_SIGNEXTEND + (if-eq-else LOW_4 LLARGEMO + (if-zero CT + (if-zero-else BIT_B_4 + (eq! PIVOT BYTE_4) + (eq! PIVOT BYTE_3))) + (if-zero (+ (prev BIT_1) (- 1 BIT_1)) + (if-zero-else BIT_B_4 + (eq! PIVOT BYTE_4) + (eq! PIVOT BYTE_3))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.10 result constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defconstraint is-byte-result (:guard IS_BYTE) + (if-eq-else OLI 1 + (begin (vanishes! RES_HI) + (vanishes! RES_LO)) + (begin (vanishes! RES_HI) + (eq! RES_LO (* SMALL PIVOT))))) + +(defconstraint is-signextend-result (:guard IS_SIGNEXTEND) + (if-eq-else OLI 1 + (begin (eq! RES_HI ARG_2_HI) + (eq! RES_LO ARG_2_LO)) + (if-zero-else SMALL + ;; SMALL == 0 + (begin (eq! RES_HI ARG_2_HI) + (eq! RES_LO ARG_2_LO)) + ;; SMALL == 1 + (begin (if-zero-else BIT_B_4 + ;; b4 == 0 + (begin (eq! BYTE_5 (* NEG 255)) + (if-zero-else BIT_1 + ;; [[1]] == 0 + (eq! BYTE_6 (* NEG 255)) + ;; [[1]] == 1 + (eq! BYTE_6 BYTE_4))) + ;; b4 == 1 + (begin (if-zero-else BIT_1 + ;; [[1]] == 0 + (eq! BYTE_5 (* NEG 255)) + ;; [[1]] == 1 + (eq! BYTE_5 BYTE_3)) + (eq! RES_LO ARG_2_LO))))))) + +(defconstraint result-via-lookup (:guard (+ IS_AND IS_OR IS_XOR IS_NOT)) + (begin (eq! BYTE_5 XXX_BYTE_HI) + (eq! BYTE_6 XXX_BYTE_LO))) diff --git a/testdata/bit_decomposition.lisp b/testdata/bit_decomposition.lisp index f5a33ce..4cfdb8b 100644 --- a/testdata/bit_decomposition.lisp +++ b/testdata/bit_decomposition.lisp @@ -6,4 +6,4 @@ (BIT_3 :i1@prove)) ;; NIBBLE = 8*BIT_3 + 4*BIT_2 + 2*BIT_1 + BIT_0 -(defconstraint decomp () (- NIBBLE (+ BIT_0 (* 2 BIT_1) (* 4 BIT_2) (* 8 BIT_3)))) +(defconstraint decomp () (eq! NIBBLE (+ BIT_0 (* 2 BIT_1) (* 4 BIT_2) (* 8 BIT_3)))) diff --git a/testdata/block_01.lisp b/testdata/block_01.lisp index 4ef2446..1027c35 100644 --- a/testdata/block_01.lisp +++ b/testdata/block_01.lisp @@ -1,2 +1,7 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y) -(defconstraint c1 () (begin X Y)) +(defconstraint c1 () + (begin + (vanishes! X) + (vanishes! Y))) diff --git a/testdata/block_02.lisp b/testdata/block_02.lisp index f3859b8..53de5c4 100644 --- a/testdata/block_02.lisp +++ b/testdata/block_02.lisp @@ -1,2 +1,8 @@ -(defcolumns X Y Z) -(defconstraint c1 () (if X (begin Y Z))) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns (X :@loob) Y Z) +(defconstraint c1 () + (if X + (begin + (vanishes! Y) + (vanishes! Z)))) diff --git a/testdata/block_03.lisp b/testdata/block_03.lisp index 9ffe6f7..187290e 100644 --- a/testdata/block_03.lisp +++ b/testdata/block_03.lisp @@ -1,8 +1,15 @@ -(defcolumns X Y Z) -(defconstraint c1 () (if X - ;; if X==0 then Y == Z - (begin Y Z) - ;; else X == Y && (Y == 0 || Z == 0) - (begin (- X Y) (* Y Z)))) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns (X :@loob) Y Z) +(defconstraint c1 () + (if X + ;; if X==0 then Y == Z + (begin + (vanishes! Y) + (vanishes! Z)) + ;; else X == Y && (Y == 0 || Z == 0) + (begin + (vanishes! (- X Y)) + (vanishes! (* Y Z))))) ;; Z is always 0! (defproperty a1 Z) diff --git a/testdata/byte_decomposition.lisp b/testdata/byte_decomposition.lisp index 1ec900e..8404283 100644 --- a/testdata/byte_decomposition.lisp +++ b/testdata/byte_decomposition.lisp @@ -6,44 +6,44 @@ ;; In the first row, ST is always zero. This allows for an ;; arbitrary amount of padding at the beginning which has no function. -(defconstraint first (:domain {0}) ST) +(defconstraint first (:domain {0}) (eq! ST 0)) ;; In the last row of a valid frame, the counter must have its max ;; value. This ensures that all non-padding frames are complete. -(defconstraint last (:domain {-1}) (* ST (- 3 CT))) +(defconstraint last (:domain {-1} :guard ST) + ;; CT[$] == 3 + (eq! CT 3)) ;; ST either remains constant, or increments by one. -(defconstraint increment () (* - ;; ST[k] == ST[k+1] - (- ST (shift ST 1)) - ;; Or, ST[k]+1 == ST[k+1] - (- (+ 1 ST) (shift ST 1)))) +(defconstraint increment () + (or! + ;; ST[k] == ST[k+1] + (eq! ST (shift ST 1)) + ;; Or, ST[k]+1 == ST[k+1] + (eq! (+ 1 ST) (next ST)))) ;; If ST changes, counter resets to zero. -(defconstraint reset () (* - ;; ST[k] == ST[k+1] - (- ST (shift ST 1)) - ;; Or, CT[k+1] == 0 - (shift CT 1))) +(defconstraint reset () + (or! + ;; ST[k] == ST[k+1] + (eq! ST (shift ST 1)) + ;; Or, CT[k+1] == 0 + (eq! (next CT) 0))) ;; Increment or reset counter -(defconstraint heartbeat () - ;; Only When ST != 0 - (* ST - ;; If CT[k] == 3 - (if (- 3 CT) - ;; Then, CT[k+1] == 0 - (shift CT 1) - ;; Else, CT[k]+1 == CT[k+1] - (- (+ 1 CT) (shift CT 1))))) +(defconstraint heartbeat (:guard ST) + ;; If CT[k] == 3 + (if-eq-else CT 3 + ;; Then, CT[k+1] == 0 + (eq! (next CT) 0) + ;; Else, CT[k]+1 == CT[k+1] + (eq! (+ 1 CT) (next CT)))) ;; Argument accumulates byte values. -(defconstraint accumulator () - ;; Only When ST != 0 - (* ST - ;; If CT[k] == 0 - (if CT - ;; Then, ARG == BYTE - (- ARG BYTE) - ;; Else, ARG = BYTE[k] + 256*BYTE[k-1] - (- ARG (+ BYTE (* 256 (shift ARG -1))))))) +(defconstraint accumulator (:guard ST) + ;; If CT[k] == 0 + (if-eq-else CT 0 + ;; Then, ARG == BYTE + (eq! ARG BYTE) + ;; Else, ARG = BYTE[k] + 256*BYTE[k-1] + (eq! ARG (+ BYTE (* 256 (prev ARG)))))) diff --git a/testdata/byte_sorting.lisp b/testdata/byte_sorting.lisp index 2e0624e..1a114f2 100644 --- a/testdata/byte_sorting.lisp +++ b/testdata/byte_sorting.lisp @@ -8,4 +8,4 @@ (defcolumns (Delta :i8@prove)) ;; Delta == X - X[i-1] -(defconstraint sort () (- Delta (- X (shift X -1)))) +(defconstraint sort () (eq! Delta (- X (shift X -1)))) diff --git a/testdata/constant_01.lisp b/testdata/constant_01.lisp index 959d4cc..92fe7b6 100644 --- a/testdata/constant_01.lisp +++ b/testdata/constant_01.lisp @@ -1,14 +1,16 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defconst ONE 1 TWO 2 ) (defcolumns X Y) -(defconstraint c1 () (+ X (* TWO Y))) -(defconstraint c2 () (+ (* TWO Y) X)) -(defconstraint c3 () (+ X Y Y)) -(defconstraint c4 () (+ Y X Y)) -(defconstraint c5 () (+ Y Y X)) -(defconstraint c6 () (+ (* ONE X) Y Y)) -(defconstraint c7 () (+ Y (* ONE X) Y)) -(defconstraint c8 () (+ Y Y (* ONE X))) +(defconstraint c1 () (vanishes! (+ X (* TWO Y)))) +(defconstraint c2 () (vanishes! (+ (* TWO Y) X))) +(defconstraint c3 () (vanishes! (+ X Y Y))) +(defconstraint c4 () (vanishes! (+ Y X Y))) +(defconstraint c5 () (vanishes! (+ Y Y X))) +(defconstraint c6 () (vanishes! (+ (* ONE X) Y Y))) +(defconstraint c7 () (vanishes! (+ Y (* ONE X) Y))) +(defconstraint c8 () (vanishes! (+ Y Y (* ONE X)))) diff --git a/testdata/constant_02.lisp b/testdata/constant_02.lisp index 584e0bb..479b767 100644 --- a/testdata/constant_02.lisp +++ b/testdata/constant_02.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defconst ONE 1) (defcolumns X) -(defconstraint c1 () (* X (- X ONE))) +(defconstraint c1 () (vanishes! (* X (- X ONE)))) diff --git a/testdata/constant_03.lisp b/testdata/constant_03.lisp index 80f49f3..4e3f007 100644 --- a/testdata/constant_03.lisp +++ b/testdata/constant_03.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defconst ONE 0x01 TWO 0x02 @@ -6,5 +8,5 @@ ) (defcolumns X Y) -(defconstraint c1 () (* Y (- Y ONE) (- Y TWO) (- Y THREE))) -(defconstraint c2 () (* (- X Y) (- X Y FOUR))) +(defconstraint c1 () (vanishes! (* Y (- Y ONE) (- Y TWO) (- Y THREE)))) +(defconstraint c2 () (vanishes! (* (- X Y) (- X Y FOUR)))) diff --git a/testdata/constant_04.lisp b/testdata/constant_04.lisp index aac7b81..8e404c0 100644 --- a/testdata/constant_04.lisp +++ b/testdata/constant_04.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defconst ONE_ 1 ONE ONE_ @@ -6,6 +8,6 @@ ) (defcolumns X Y Z) -(defconstraint c1 () (* Z (- Z ONE))) -(defconstraint c2 () (* (- Y Z) (- Y Z TWO))) -(defconstraint c3 () (* (- X Y) (- X Y FOUR))) +(defconstraint c1 () (vanishes! (* Z (- Z ONE)))) +(defconstraint c2 () (vanishes! (* (- Y Z) (- Y Z TWO)))) +(defconstraint c3 () (vanishes! (* (- X Y) (- X Y FOUR)))) diff --git a/testdata/constant_05.lisp b/testdata/constant_05.lisp index a7f6172..a6ce2b4 100644 --- a/testdata/constant_05.lisp +++ b/testdata/constant_05.lisp @@ -1,3 +1,7 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defconst ONE 1) (defcolumns CT) -(defconstraint c1 () (* (- CT (shift CT ONE)) (- (+ CT ONE) (shift CT ONE)))) +(defconstraint c1 () + (vanishes! + (* (- CT (shift CT ONE)) (- (+ CT ONE) (shift CT ONE))))) diff --git a/testdata/constant_06.lisp b/testdata/constant_06.lisp index f7cfc0a..f86e28e 100644 --- a/testdata/constant_06.lisp +++ b/testdata/constant_06.lisp @@ -1,4 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defconst TWO 2) (defcolumns X Y) ;; Y == X*X -(defconstraint c1 () (- Y (^ X TWO))) +(defconstraint c1 () (vanishes! (- Y (^ X TWO)))) diff --git a/testdata/constant_07.lisp b/testdata/constant_07.lisp index 44a7a54..f6f2c83 100644 --- a/testdata/constant_07.lisp +++ b/testdata/constant_07.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X ST) (defconst ONE (^ -2 0)) -(defconstraint c1 () (* ST (shift X ONE))) +(defconstraint c1 () (vanishes! (* ST (shift X ONE)))) diff --git a/testdata/constexpr_01.lisp b/testdata/constexpr_01.lisp index 78a62fb..57a385e 100644 --- a/testdata/constexpr_01.lisp +++ b/testdata/constexpr_01.lisp @@ -1,5 +1,10 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y) ;; X == Y + n - n -(defconstraint c1 () (- X Y (+ 1 1) (- 0 2))) -(defconstraint c2 () (- X Y (+ 1 1 1) (- 0 1 2))) -(defconstraint c3 () (- X Y (+ 2 1) (- 0 2 1))) +(defconstraint c1 () + (vanishes! (- X Y (+ 1 1) (- 0 2)))) +(defconstraint c2 () + (vanishes! (- X Y (+ 1 1 1) (- 0 1 2)))) +(defconstraint c3 () + (vanishes! (- X Y (+ 2 1) (- 0 2 1)))) diff --git a/testdata/constexpr_02.lisp b/testdata/constexpr_02.lisp index 22d0e50..76b80d8 100644 --- a/testdata/constexpr_02.lisp +++ b/testdata/constexpr_02.lisp @@ -1,23 +1,25 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y) ;; X*2 == Y*2 -(defconstraint c1 () (- (* X (* 2 1)) (* Y (* 1 2)))) +(defconstraint c1 () (vanishes! (- (* X (* 2 1)) (* Y (* 1 2))))) ;; X*1458 == Y*1458 -(defconstraint c1 () (- (* X (* 243 22)) (* Y (* 6 891)))) +(defconstraint c1 () (vanishes! (- (* X (* 243 22)) (* Y (* 6 891))))) ;; X*2916 == Y*2916 -(defconstraint c1 () (- (* X (* 2 243 22)) (* Y (* 6 891 2)))) +(defconstraint c1 () (vanishes! (- (* X (* 2 243 22)) (* Y (* 6 891 2))))) ;; X*2916 == Y*2916 -(defconstraint c1 () (- (* X (* 243 2 22)) (* Y (* 6 891 2)))) +(defconstraint c1 () (vanishes! (- (* X (* 243 2 22)) (* Y (* 6 891 2))))) ;; X*2916 == Y*2916 -(defconstraint c1 () (- (* X (* 22 243 2)) (* Y (* 6 891 2)))) +(defconstraint c1 () (vanishes! (- (* X (* 22 243 2)) (* Y (* 6 891 2))))) ;; X*2916 == Y*2916 -(defconstraint c1 () (- (* X (* 2 243 22)) (* Y (* 891 6 2)))) +(defconstraint c1 () (vanishes! (- (* X (* 2 243 22)) (* Y (* 891 6 2))))) ;; X*2916 == Y*2916 -(defconstraint c1 () (- (* X (* 2 243 22)) (* Y (* 2 891 6)))) +(defconstraint c1 () (vanishes! (- (* X (* 2 243 22)) (* Y (* 2 891 6))))) ;; X*2916 == Y*2916 -(defconstraint c1 () (- (* X (* 2 243 22)) (* Y (* 2 891 6 1)))) +(defconstraint c1 () (vanishes! (- (* X (* 2 243 22)) (* Y (* 2 891 6 1))))) ;; X*2916 == Y*2916 -(defconstraint c1 () (- (* X (* 2 243 22)) (* Y (* 2 891 6 1 1)))) +(defconstraint c1 () (vanishes! (- (* X (* 2 243 22)) (* Y (* 2 891 6 1 1))))) ;; X*2916 == Y*2916 -(defconstraint c1 () (- (* X (* 2 243 22 1)) (* Y (* 2 891 6)))) +(defconstraint c1 () (vanishes! (- (* X (* 2 243 22 1)) (* Y (* 2 891 6))))) ;; X*2916 == Y*2916 -(defconstraint c1 () (- (* X (* 2 243 22 1 1)) (* Y (* 2 891 6)))) +(defconstraint c1 () (vanishes! (- (* X (* 2 243 22 1 1)) (* Y (* 2 891 6))))) diff --git a/testdata/constexpr_03.lisp b/testdata/constexpr_03.lisp index 605c1b2..6d8f3fc 100644 --- a/testdata/constexpr_03.lisp +++ b/testdata/constexpr_03.lisp @@ -1,21 +1,23 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y) ;; X == Y - 0 -(defconstraint c1 () (- X Y (* 0 1))) +(defconstraint c1 () (vanishes! (- X Y (* 0 1)))) ;; X == Y - 0 -(defconstraint c1 () (- X Y (* 1 0))) +(defconstraint c1 () (vanishes! (- X Y (* 1 0)))) ;; X == Y - 0 -(defconstraint c1 () (- X Y (* 0 2))) +(defconstraint c1 () (vanishes! (- X Y (* 0 2)))) ;; X == Y - 0 -(defconstraint c1 () (- X Y (* 2 0))) +(defconstraint c1 () (vanishes! (- X Y (* 2 0)))) ;; X == Y - 0 -(defconstraint c1 () (- X Y (* 0 0 1))) +(defconstraint c1 () (vanishes! (- X Y (* 0 0 1)))) ;; X == Y - 0 -(defconstraint c1 () (- X Y (* 0 1 0))) +(defconstraint c1 () (vanishes! (- X Y (* 0 1 0)))) ;; X == Y - 0 -(defconstraint c1 () (- X Y (* 0 1 1))) +(defconstraint c1 () (vanishes! (- X Y (* 0 1 1)))) ;; X == Y - 0 -(defconstraint c1 () (- X Y (* 1 0 0))) +(defconstraint c1 () (vanishes! (- X Y (* 1 0 0)))) ;; X == Y - 0 -(defconstraint c1 () (- X Y (* 1 0 1))) +(defconstraint c1 () (vanishes! (- X Y (* 1 0 1)))) ;; X == Y - 0 -(defconstraint c1 () (- X Y (* 1 1 0))) +(defconstraint c1 () (vanishes! (- X Y (* 1 1 0)))) diff --git a/testdata/constexpr_04.lisp b/testdata/constexpr_04.lisp index ab208c7..8cc1a16 100644 --- a/testdata/constexpr_04.lisp +++ b/testdata/constexpr_04.lisp @@ -1,17 +1,19 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y) ;; X + 2 == Y + 2 -(defconstraint c1 () (- (+ X 2) (+ Y (^ 2 1)))) +(defconstraint c1 () (vanishes! (- (+ X 2) (+ Y (^ 2 1))))) ;; X + 4 == Y + 4 -(defconstraint c1 () (- (+ X 4) (+ Y (^ 2 2)))) +(defconstraint c1 () (vanishes! (- (+ X 4) (+ Y (^ 2 2))))) ;; X + 8 == Y + 8 -(defconstraint c1 () (- (+ X 8) (+ Y (^ 2 3)))) +(defconstraint c1 () (vanishes! (- (+ X 8) (+ Y (^ 2 3))))) ;; X + 16 == Y + 16 -(defconstraint c1 () (- (+ X 16) (+ Y (^ 2 4)))) +(defconstraint c1 () (vanishes! (- (+ X 16) (+ Y (^ 2 4))))) ;; X + 32 == Y + 32 -(defconstraint c1 () (- (+ X 32) (+ Y (^ 2 5)))) +(defconstraint c1 () (vanishes! (- (+ X 32) (+ Y (^ 2 5))))) ;; X + 64 == Y + 64 -(defconstraint c1 () (- (+ X 64) (+ Y (^ 2 6)))) +(defconstraint c1 () (vanishes! (- (+ X 64) (+ Y (^ 2 6))))) ;; X + 128 == Y + 128 -(defconstraint c1 () (- (+ X 128) (+ Y (^ 2 7)))) +(defconstraint c1 () (vanishes! (- (+ X 128) (+ Y (^ 2 7))))) ;; X + 256 == Y + 256 -(defconstraint c1 () (- (+ X 256) (+ Y (^ 2 8)))) +(defconstraint c1 () (vanishes! (- (+ X 256) (+ Y (^ 2 8))))) diff --git a/testdata/constexpr_05.lisp b/testdata/constexpr_05.lisp index 694675c..78af2a8 100644 --- a/testdata/constexpr_05.lisp +++ b/testdata/constexpr_05.lisp @@ -1,3 +1,8 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y) ;; Y == 0 -(defconstraint c1 () (if (* 1 2) X Y)) +(defconstraint c1 () (if + (vanishes! (* 1 2)) + (vanishes! X) + (vanishes! Y))) diff --git a/testdata/counter.lisp b/testdata/counter.lisp index 44c364f..b52b0e0 100644 --- a/testdata/counter.lisp +++ b/testdata/counter.lisp @@ -1,16 +1,3 @@ -(defpurefun (vanishes! e0) e0) -;; -(defpurefun (next X) (shift X 1)) -(defpurefun (prev X) (shift X -1)) -;; -(defpurefun (eq! x y) (- x y)) -;; -(defpurefun (will-eq! e0 e1) (eq! (next e0) e1)) -(defpurefun (will-inc! e0 offset) (will-eq! e0 (+ e0 offset))) -(defpurefun (will-remain-constant! e0) (will-eq! e0 e0)) -;; -(defpurefun (if-eq-else x val then else) (if (eq! x val) then else)) - ;; =================================================== ;; Constraints ;; =================================================== @@ -18,7 +5,7 @@ ;; In the first row, STAMP is always zero. This allows for an ;; arbitrary amount of padding at the beginning which has no function. -(defconstraint first (:domain {0}) STAMP) +(defconstraint first (:domain {0}) (eq! STAMP 0)) ;; In the last row of a valid frame, the counter must have its max ;; value. This ensures that all non-padding frames are complete. diff --git a/testdata/domain_01.lisp b/testdata/domain_01.lisp index 2a12acb..3be4a16 100644 --- a/testdata/domain_01.lisp +++ b/testdata/domain_01.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns STAMP) ;; STAMP[0] == 0 -(defconstraint c1 (:domain {0}) STAMP) +(defconstraint c1 (:domain {0}) (vanishes! STAMP)) diff --git a/testdata/domain_02.lisp b/testdata/domain_02.lisp index 7790966..843bd48 100644 --- a/testdata/domain_02.lisp +++ b/testdata/domain_02.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns STAMP) ;; STAMP[-1] == 0 -(defconstraint c1 (:domain {-1}) STAMP) +(defconstraint c1 (:domain {-1}) (vanishes! STAMP)) diff --git a/testdata/domain_03.lisp b/testdata/domain_03.lisp index ae59ff1..344da97 100644 --- a/testdata/domain_03.lisp +++ b/testdata/domain_03.lisp @@ -1,12 +1,16 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns STAMP) ;; STAMP[0] == 0 -(defconstraint start (:domain {0}) STAMP) +(defconstraint start (:domain {0}) (vanishes! STAMP)) ;; STAMP[-1] == 5 -(defconstraint end (:domain {-1}) (- STAMP 5)) +(defconstraint end (:domain {-1}) (vanishes! (- STAMP 5))) ;; STAMP either remains constant, or increments by one. -(defconstraint increment () (* - ;; STAMP[k] == STAMP[k+1] - (- STAMP (shift STAMP 1)) - ;; Or, STAMP[k]+1 == STAMP[k+1] - (- (+ 1 STAMP) (shift STAMP 1)))) +(defconstraint increment () + (vanishes! + (* + ;; STAMP[k] == STAMP[k+1] + (- STAMP (shift STAMP 1)) + ;; Or, STAMP[k]+1 == STAMP[k+1] + (- (+ 1 STAMP) (shift STAMP 1))))) diff --git a/testdata/fun_01.lisp b/testdata/fun_01.lisp index 852b5b6..b9bfb1b 100644 --- a/testdata/fun_01.lisp +++ b/testdata/fun_01.lisp @@ -1,5 +1,5 @@ (defcolumns X Y) (defun (Xmul x) (* X x)) -(defpurefun (eq x y) (- x y)) +(defpurefun ((eq :@loob) x y) (- x y)) ;; Y == 2 * X (defconstraint c1 () (eq Y (Xmul 2))) diff --git a/testdata/fun_02.lisp b/testdata/fun_02.lisp index 997a0b5..85c4fb5 100644 --- a/testdata/fun_02.lisp +++ b/testdata/fun_02.lisp @@ -1,5 +1,5 @@ (defcolumns X Y) (defun (Xm1) (- X 1)) -(defpurefun (eq x y) (- x y)) +(defpurefun ((eq :@loob) x y) (- x y)) ;; Y == X (defconstraint c1 () (eq (- Y 1) (Xm1))) diff --git a/testdata/fun_03.lisp b/testdata/fun_03.lisp index 524b064..f8d1745 100644 --- a/testdata/fun_03.lisp +++ b/testdata/fun_03.lisp @@ -1,3 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) +;; (defcolumns X ST) (defun (get) X) -(defconstraint c1 () (* ST (shift (get) 1))) +(defconstraint c1 () + (vanishes! (* ST (shift (get) 1)))) diff --git a/testdata/fun_04.lisp b/testdata/fun_04.lisp index 8610684..adc4d97 100644 --- a/testdata/fun_04.lisp +++ b/testdata/fun_04.lisp @@ -1,3 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) +;; (defcolumns X) (defun (get) X) -(defconstraint c1 () (shift (get) -1)) +(defconstraint c1 () + (vanishes! (shift (get) -1))) diff --git a/testdata/fun_05.lisp b/testdata/fun_05.lisp index bfdb479..fd47201 100644 --- a/testdata/fun_05.lisp +++ b/testdata/fun_05.lisp @@ -1,3 +1,3 @@ (defcolumns X) -(defun (prevX) (shift X -1)) +(defun ((prevX :@loob)) (shift X -1)) (defconstraint c1 () (prevX)) diff --git a/testdata/fun_06.lisp b/testdata/fun_06.lisp index 380f626..61cd2fd 100644 --- a/testdata/fun_06.lisp +++ b/testdata/fun_06.lisp @@ -1,9 +1,11 @@ +(defpurefun ((vanishes! :@loob) x) x) +;; (defcolumns X Y ST) (defun (getX) X) (defun (getY) Y) (defun (nextX) (shift X 1)) -(defconstraint c1 () (* ST (+ (shift (getX) 1) Y))) -(defconstraint c2 () (* ST (+ (shift X 1) (getY)))) -(defconstraint c3 () (* ST (+ (shift (getX) 1) (getY)))) -(defconstraint c4 () (* ST (+ (nextX) Y))) +(defconstraint c1 () (vanishes! (* ST (+ (shift (getX) 1) Y)))) +(defconstraint c2 () (vanishes! (* ST (+ (shift X 1) (getY))))) +(defconstraint c3 () (vanishes! (* ST (+ (shift (getX) 1) (getY))))) +(defconstraint c4 () (vanishes! (* ST (+ (nextX) Y)))) diff --git a/testdata/funalias_01.lisp b/testdata/funalias_01.lisp index c01144a..f6ef702 100644 --- a/testdata/funalias_01.lisp +++ b/testdata/funalias_01.lisp @@ -1,4 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns A) (defpurefun (id x) x) (defunalias ID id) -(defconstraint test () (ID A)) +(defconstraint test () (vanishes! (ID A))) diff --git a/testdata/funalias_02.lisp b/testdata/funalias_02.lisp index 7eec36d..fd50b43 100644 --- a/testdata/funalias_02.lisp +++ b/testdata/funalias_02.lisp @@ -1,4 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns A B) (defpurefun (eq x y) (- y x)) (defunalias eq! eq) -(defconstraint test () (eq! A B)) +(defconstraint test () (vanishes! (eq! A B))) diff --git a/testdata/funalias_03.lisp b/testdata/funalias_03.lisp index 2bdc67c..735e26c 100644 --- a/testdata/funalias_03.lisp +++ b/testdata/funalias_03.lisp @@ -1,6 +1,8 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y) (defun (double x) (+ x x)) (defpurefun (eq x y) (- x y)) (defunalias times2 double) ;; Y == 2 * X -(defconstraint c1 () (eq Y (times2 X))) +(defconstraint c1 () (vanishes! (eq Y (times2 X)))) diff --git a/testdata/guard_01.lisp b/testdata/guard_01.lisp index 12bd380..eeaac62 100644 --- a/testdata/guard_01.lisp +++ b/testdata/guard_01.lisp @@ -1,3 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns STAMP X) ;; STAMP == 0 || X == 1 || X == 2 -(defconstraint c1 (:guard STAMP) (* (- X 1) (- X 2))) +(defconstraint c1 (:guard STAMP) + (vanishes! (* (- X 1) (- X 2)))) diff --git a/testdata/guard_02.lisp b/testdata/guard_02.lisp index 65de893..64742c5 100644 --- a/testdata/guard_02.lisp +++ b/testdata/guard_02.lisp @@ -1,3 +1,7 @@ -(defcolumns ST A B) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns ST (A :@loob) B) ;; STAMP == 0 || X == 1 || X == 2 -(defconstraint c1 (:guard ST) (if A B)) +(defconstraint c1 (:guard ST) + (if A + (vanishes! B))) diff --git a/testdata/guard_03.lisp b/testdata/guard_03.lisp index 0915909..a7328d8 100644 --- a/testdata/guard_03.lisp +++ b/testdata/guard_03.lisp @@ -1,2 +1,7 @@ -(defcolumns ST A B) -(defconstraint c1 (:guard ST) (if A 0 B)) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns ST (A :@loob) B) +(defconstraint c1 (:guard ST) + (if A + (vanishes! 0) + (vanishes! B))) diff --git a/testdata/guard_04.lisp b/testdata/guard_04.lisp index 50b3af4..72a5ded 100644 --- a/testdata/guard_04.lisp +++ b/testdata/guard_04.lisp @@ -1,2 +1,7 @@ -(defcolumns ST A B C) -(defconstraint c1 (:guard ST) (if A B C)) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns ST (A :@loob) B C) +(defconstraint c1 (:guard ST) + (if A + (vanishes! B) + (vanishes! C))) diff --git a/testdata/guard_05.lisp b/testdata/guard_05.lisp index 3dfc02e..dc0e6cf 100644 --- a/testdata/guard_05.lisp +++ b/testdata/guard_05.lisp @@ -1,2 +1,6 @@ -(defcolumns ST X Y Z) -(defconstraint test (:guard ST) (if X (- Z (if Y 0 16)))) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns ST (X :@loob) (Y :@loob) (Z :@loob)) +(defconstraint test (:guard ST) + (if X + (vanishes! (- Z (if Y 0 16))))) diff --git a/testdata/if_01.lisp b/testdata/if_01.lisp index f8cd776..e79819b 100644 --- a/testdata/if_01.lisp +++ b/testdata/if_01.lisp @@ -1,2 +1,6 @@ -(defcolumns A B) -(defconstraint c1 () (if A B)) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns (A :@loob) B) +(defconstraint c1 () + (if A + (vanishes! B))) diff --git a/testdata/if_02.lisp b/testdata/if_02.lisp index 81478bc..f2b5c5d 100644 --- a/testdata/if_02.lisp +++ b/testdata/if_02.lisp @@ -1,2 +1,7 @@ -(defcolumns A B C) -(defconstraint c1 () (if A B C)) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns (A :@loob) B C) +(defconstraint c1 () + (if A + (vanishes! B) + (vanishes! C))) diff --git a/testdata/if_03.lisp b/testdata/if_03.lisp index fb12196..b75e79e 100644 --- a/testdata/if_03.lisp +++ b/testdata/if_03.lisp @@ -1,2 +1,7 @@ -(defcolumns A B) -(defconstraint c1 () (if A 0 B)) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns (A :@loob) B) +(defconstraint c1 () + (if A + (vanishes! 0) + (vanishes! B))) diff --git a/testdata/if_04.lisp b/testdata/if_04.lisp index 57abe72..b49911a 100644 --- a/testdata/if_04.lisp +++ b/testdata/if_04.lisp @@ -1,4 +1,9 @@ -(defcolumns X Y) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns X (Y :@loob)) (defconstraint test () - (- X (if Y 0 16))) + (- X + (if Y + (vanishes! 0) + (vanishes! 16)))) diff --git a/testdata/if_05.lisp b/testdata/if_05.lisp index 9f6620d..1b0bc73 100644 --- a/testdata/if_05.lisp +++ b/testdata/if_05.lisp @@ -1,2 +1,7 @@ -(defcolumns X Y Z) -(defconstraint test () (if X (- Z (if Y 0 16)))) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns (X :@loob) (Y :@loob) Z) +(defconstraint test () + (if X + (vanishes! + (- Z (if Y 0 16))))) diff --git a/testdata/if_06.lisp b/testdata/if_06.lisp index c0c249f..cde8216 100644 --- a/testdata/if_06.lisp +++ b/testdata/if_06.lisp @@ -1,7 +1,14 @@ -(defcolumns X Y) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns X (Y :@loob)) (defconstraint test1 () - (- X (if Y 0))) + (- X + (if Y + (vanishes! 0)))) (defconstraint test2 () - (- X (if Y 0 16))) + (- X + (if Y + (vanishes! 0) + (vanishes! 16)))) diff --git a/testdata/if_07.lisp b/testdata/if_07.lisp index 5013f7f..520ccf6 100644 --- a/testdata/if_07.lisp +++ b/testdata/if_07.lisp @@ -1,2 +1,7 @@ -(defcolumns X Y Z) -(defconstraint test () (if X 0 (- Z (if Y 3 16)))) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns (X :@loob) (Y :@loob) Z) +(defconstraint test () + (if X + (vanishes! 0) + (vanishes! (- Z (if Y 3 16))))) diff --git a/testdata/if_08.lisp b/testdata/if_08.lisp index 81c5754..6bc4d60 100644 --- a/testdata/if_08.lisp +++ b/testdata/if_08.lisp @@ -1,3 +1,8 @@ -(defcolumns X Y Z) -(defconstraint test () (if X (- Z (if Y 0)))) -(defconstraint test () (if X (- Z (if Y 0 16)))) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns (X :@loob) (Y :@loob) Z) +(defconstraint test () + (if X (vanishes! (- Z (if Y 0))))) + +(defconstraint test () + (if X (vanishes! (- Z (if Y 0 16))))) diff --git a/testdata/if_09.lisp b/testdata/if_09.lisp index adf6b79..315994d 100644 --- a/testdata/if_09.lisp +++ b/testdata/if_09.lisp @@ -1,2 +1,5 @@ -(defcolumns X Y Z) -(defconstraint test () (- Z (if X (if Y 0 16)))) +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns (X :@loob) (Y :@loob) Z) +(defconstraint test () + (vanishes! (- Z (if X (if Y 0 16))))) diff --git a/testdata/if_10.accepts b/testdata/if_10.accepts new file mode 100644 index 0000000..5545c9b --- /dev/null +++ b/testdata/if_10.accepts @@ -0,0 +1,36 @@ +{ "X": [], "Y": [], "A": [] } +;; +{ "X": [0], "Y": [0], "A": [0] } +{ "X": [0], "Y": [1], "A": [0] } +{ "X": [1], "Y": [0], "A": [0] } +{ "X": [1], "Y": [1], "A": [0] } +{ "X": [1], "Y": [0], "A": [1] } +;; +{ "X": [0,0], "Y": [0,0], "A": [0,0] } +{ "X": [0,0], "Y": [0,1], "A": [0,0] } +{ "X": [0,1], "Y": [0,0], "A": [0,0] } +{ "X": [0,1], "Y": [0,1], "A": [0,0] } +{ "X": [1,0], "Y": [0,0], "A": [0,0] } +{ "X": [1,0], "Y": [0,1], "A": [0,0] } +{ "X": [1,1], "Y": [0,0], "A": [0,0] } +{ "X": [1,1], "Y": [0,1], "A": [0,0] } +{ "X": [0,0], "Y": [1,0], "A": [0,0] } +{ "X": [0,0], "Y": [1,1], "A": [0,0] } +{ "X": [0,1], "Y": [1,0], "A": [0,0] } +{ "X": [0,1], "Y": [1,1], "A": [0,0] } +{ "X": [1,0], "Y": [1,0], "A": [0,0] } +{ "X": [1,0], "Y": [1,1], "A": [0,0] } +{ "X": [1,1], "Y": [1,0], "A": [0,0] } +{ "X": [1,1], "Y": [1,1], "A": [0,0] } +;; +{ "X": [0,1], "Y": [0,0], "A": [0,1] } +{ "X": [1,1], "Y": [0,0], "A": [0,1] } +{ "X": [0,1], "Y": [1,0], "A": [0,1] } +{ "X": [1,1], "Y": [1,0], "A": [0,1] } +;; +{ "X": [1,0], "Y": [0,0], "A": [1,0] } +{ "X": [1,0], "Y": [0,1], "A": [1,0] } +{ "X": [1,1], "Y": [0,0], "A": [1,0] } +{ "X": [1,1], "Y": [0,1], "A": [1,0] } +;; +{ "X": [1,1], "Y": [0,0], "A": [1,1] } diff --git a/testdata/if_10.lisp b/testdata/if_10.lisp new file mode 100644 index 0000000..f918db2 --- /dev/null +++ b/testdata/if_10.lisp @@ -0,0 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + +(defcolumns (X :binary@loob) (Y :binary@bool) A) +(defconstraint c1 () (if X (vanishes! A))) +(defconstraint c2 () (if Y (vanishes! A))) diff --git a/testdata/if_10.rejects b/testdata/if_10.rejects new file mode 100644 index 0000000..c522445 --- /dev/null +++ b/testdata/if_10.rejects @@ -0,0 +1,45 @@ +{ "X": [0], "Y": [0], "A": [1] } +{ "X": [0], "Y": [1], "A": [1] } +{ "X": [1], "Y": [1], "A": [1] } +;; +{ "X": [0,0], "Y": [0,0], "A": [0,1] } +{ "X": [0,0], "Y": [0,1], "A": [0,1] } +{ "X": [0,1], "Y": [0,1], "A": [0,1] } +{ "X": [1,0], "Y": [0,0], "A": [0,1] } +{ "X": [1,0], "Y": [0,1], "A": [0,1] } +{ "X": [1,1], "Y": [0,1], "A": [0,1] } +{ "X": [0,0], "Y": [1,0], "A": [0,1] } +{ "X": [0,0], "Y": [1,1], "A": [0,1] } +{ "X": [0,1], "Y": [1,1], "A": [0,1] } +{ "X": [1,0], "Y": [1,0], "A": [0,1] } +{ "X": [1,0], "Y": [1,1], "A": [0,1] } +{ "X": [1,1], "Y": [1,1], "A": [0,1] } +;; +{ "X": [0,0], "Y": [0,0], "A": [1,0] } +{ "X": [0,0], "Y": [0,1], "A": [1,0] } +{ "X": [0,1], "Y": [0,0], "A": [1,0] } +{ "X": [0,1], "Y": [0,1], "A": [1,0] } +{ "X": [0,0], "Y": [1,0], "A": [1,0] } +{ "X": [0,0], "Y": [1,1], "A": [1,0] } +{ "X": [0,1], "Y": [1,0], "A": [1,0] } +{ "X": [0,1], "Y": [1,1], "A": [1,0] } +{ "X": [1,0], "Y": [1,0], "A": [1,0] } +{ "X": [1,0], "Y": [1,1], "A": [1,0] } +{ "X": [1,1], "Y": [1,0], "A": [1,0] } +{ "X": [1,1], "Y": [1,1], "A": [1,0] } +;; +{ "X": [0,0], "Y": [0,0], "A": [1,1] } +{ "X": [0,0], "Y": [0,1], "A": [1,1] } +{ "X": [0,1], "Y": [0,0], "A": [1,1] } +{ "X": [0,1], "Y": [0,1], "A": [1,1] } +{ "X": [1,0], "Y": [0,0], "A": [1,1] } +{ "X": [1,0], "Y": [0,1], "A": [1,1] } +{ "X": [1,1], "Y": [0,1], "A": [1,1] } +{ "X": [0,0], "Y": [1,0], "A": [1,1] } +{ "X": [0,0], "Y": [1,1], "A": [1,1] } +{ "X": [0,1], "Y": [1,0], "A": [1,1] } +{ "X": [0,1], "Y": [1,1], "A": [1,1] } +{ "X": [1,0], "Y": [1,0], "A": [1,1] } +{ "X": [1,0], "Y": [1,1], "A": [1,1] } +{ "X": [1,1], "Y": [1,0], "A": [1,1] } +{ "X": [1,1], "Y": [1,1], "A": [1,1] } diff --git a/testdata/interleave_01.lisp b/testdata/interleave_01.lisp index f393e06..c68e1bb 100644 --- a/testdata/interleave_01.lisp +++ b/testdata/interleave_01.lisp @@ -1,3 +1,3 @@ -(defcolumns X Y) +(defcolumns (X :@loob) (Y :@loob)) (definterleaved Z (X Y)) (defconstraint c1 () Z) diff --git a/testdata/interleave_02.lisp b/testdata/interleave_02.lisp index fda1cb3..2afa1c4 100644 --- a/testdata/interleave_02.lisp +++ b/testdata/interleave_02.lisp @@ -1,4 +1,8 @@ +(defpurefun ((vanishes! :@loob) x) x) +;; (defcolumns X Y) (definterleaved Z (X Y)) ;; Z[k]+1 == Z[k+1] || Z[k] == Z[k+1] -(defconstraint c1 () (* (- (+ 1 Z) (shift Z 1)) (- Z (shift Z 1)))) +(defconstraint c1 () + (vanishes! + (* (- (+ 1 Z) (shift Z 1)) (- Z (shift Z 1))))) diff --git a/testdata/interleave_03.lisp b/testdata/interleave_03.lisp index 6005f4b..3e161c5 100644 --- a/testdata/interleave_03.lisp +++ b/testdata/interleave_03.lisp @@ -1,4 +1,4 @@ -(defcolumns X Y) +(defcolumns (X :@loob) (Y :@loob)) (definterleaved A (X Y)) (definterleaved B (X Y)) (definterleaved Z (A B)) diff --git a/testdata/memory.lisp b/testdata/memory.lisp index a40470d..184a966 100644 --- a/testdata/memory.lisp +++ b/testdata/memory.lisp @@ -11,26 +11,56 @@ ;; written. ;; Program Counter (always increases by one) -(defcolumns (PC :i16@prove)) +(defcolumns (PC :i16@loob@prove)) ;; Read/Write flag (0=READ, 1=WRITE) (defcolumns (RW :i1@prove)) ;; Address being Read/Written (defcolumns (ADDR :i32@prove)) ;; Value being Read/Written (defcolumns (VAL :i8@prove)) + ;; Permutation (defpermutation (ADDR' PC' RW' VAL') ((+ ADDR) (+ PC) (+ RW) (+ VAL))) + ;; PC[0]=0 -(defconstraint heartbeat_1 (:domain {0}) PC) +(defconstraint heartbeat_1 (:domain {0}) (eq! PC 0)) + ;; PC[k]=0 || PC[k]=PC[k-1]+1 -(defconstraint heartbeat_2 () (* PC (- PC (+ 1 (shift PC -1))))) +(defconstraint heartbeat_2 () + (or! + (eq! PC 0) + (eq! PC (+ 1 (prev PC))))) + ;; PC[k]=0 ==> PC[k-1]=0 -(defconstraint heartbeat_3 () (if PC (shift PC -1))) +(defconstraint heartbeat_3 () + (if PC + (eq! (prev PC) 0))) + ;; PC[k]=0 ==> (RW[k]=0 && ADDR[k]=0 && VAL[k]=0) -(defconstraint heartbeat_4 () (if PC (+ RW ADDR VAL))) +(defconstraint heartbeat_4 () + (if PC + (+ + (eq! RW 0) + (eq! ADDR 0) + (eq! VAL 0)))) + ;; ADDR'[k] != ADDR'[k-1] ==> (RW'[k]=1 || VAL'[k]=0) -(defconstraint first_read_1 () (if (- ADDR' (shift ADDR' -1)) 0 (* (- 1 RW') VAL'))) +(defconstraint first_read_1 () + (if-not-eq ADDR' (prev ADDR') + (or! + (eq! RW' 1) + (eq! VAL' 0)))) + ;; (RW'[0]=1 || VAL'[0]=0) -(defconstraint first_read_2 (:domain {0}) (* (- 1 RW') VAL')) +(defconstraint first_read_2 (:domain {0}) + (or! + (eq! RW' 1) + (eq! VAL' 0))) + ;; ADDR'[k] == ADDR'[k-1] ==> (RW=1 || VAL'[k]=VAL'[k-1]) -(defconstraint next_read () (if (- ADDR' (shift ADDR' -1)) (* (- 1 RW') (- VAL' (shift VAL' -1))))) +(defconstraint next_read () + (if + (eq! ADDR' (prev ADDR')) + (or! + (eq! RW' 1) + (eq! VAL' (prev VAL'))))) diff --git a/testdata/module_01.lisp b/testdata/module_01.lisp index 634b17e..4670535 100644 --- a/testdata/module_01.lisp +++ b/testdata/module_01.lisp @@ -1,3 +1,3 @@ (module test) -(defcolumns X) +(defcolumns (X :@loob)) (defconstraint heartbeat () X) diff --git a/testdata/module_02.lisp b/testdata/module_02.lisp index 7d50d41..91b785c 100644 --- a/testdata/module_02.lisp +++ b/testdata/module_02.lisp @@ -1,4 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) (defcolumns X) (module test) (defcolumns X) -(defconstraint heartbeat () X) +(defconstraint heartbeat () (vanishes! X)) diff --git a/testdata/module_03.lisp b/testdata/module_03.lisp index 0882b05..d569eb4 100644 --- a/testdata/module_03.lisp +++ b/testdata/module_03.lisp @@ -1,6 +1,8 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X) (module m1) ;; Module without any column declarations to test alignment. (module m2) (defcolumns X) -(defconstraint heartbeat () X) +(defconstraint heartbeat () (vanishes! X)) diff --git a/testdata/module_04.lisp b/testdata/module_04.lisp index 736e4fe..28eaddd 100644 --- a/testdata/module_04.lisp +++ b/testdata/module_04.lisp @@ -2,5 +2,5 @@ (defcolumns X) ;; Module without any column declarations to test alignment. (module m2) -(defcolumns X) +(defcolumns (X :@loob)) (defconstraint heartbeat () X) diff --git a/testdata/module_05.lisp b/testdata/module_05.lisp index 42391f9..20535ff 100644 --- a/testdata/module_05.lisp +++ b/testdata/module_05.lisp @@ -1,5 +1,5 @@ (module m1) (defcolumns X) (module m2) -(defcolumns X Y) +(defcolumns (X :@loob) (Y :@loob)) (defconstraint heartbeat () (* X Y)) diff --git a/testdata/module_06.lisp b/testdata/module_06.lisp index 5d478ad..391b60b 100644 --- a/testdata/module_06.lisp +++ b/testdata/module_06.lisp @@ -1,6 +1,8 @@ +(defpurefun ((vanishes! :@loob) x) x) (defcolumns X) (module m1) (defcolumns ST (X :i16@prove)) (defpermutation (Y) ((+ X))) ;; Ensure sorted column increments by 1 -(defconstraint increment () (* ST (- (shift Y 1) (+ 1 Y)))) +(defconstraint increment () + (vanishes! (* ST (- (shift Y 1) (+ 1 Y))))) diff --git a/testdata/module_07.lisp b/testdata/module_07.lisp index 5aa16c3..1475d65 100644 --- a/testdata/module_07.lisp +++ b/testdata/module_07.lisp @@ -1,6 +1,7 @@ +(defpurefun ((vanishes! :@loob) x) x) (defcolumns (X :byte@prove) (Y :byte@prove)) ;; (module m1) (defcolumns (X :byte@prove) (Y :byte@prove)) (defpermutation (A B) ((+ X) (+ Y))) -(defconstraint diag_ab () (- (shift A 1) B)) +(defconstraint diag_ab () (vanishes! (- (shift A 1) B))) diff --git a/testdata/module_09.lisp b/testdata/module_09.lisp index f18b118..30ddc20 100644 --- a/testdata/module_09.lisp +++ b/testdata/module_09.lisp @@ -1,5 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) (defcolumns A B) (module m1) (defcolumns A B) -(defconstraint eq () (- A B)) +(defconstraint eq () (vanishes! (- A B))) (defproperty lem (- A B)) diff --git a/testdata/module_10.accepts b/testdata/module_10.accepts new file mode 100644 index 0000000..9750a89 --- /dev/null +++ b/testdata/module_10.accepts @@ -0,0 +1,11 @@ +{"m1.X": [], "m1.Y": []} +{"m1.X": [-4], "m1.Y": [2]} +{"m1.X": [-2], "m1.Y": [1]} +{"m1.X": [0], "m1.Y": [0]} +{"m1.X": [2], "m1.Y": [-1]} +{"m1.X": [4], "m1.Y": [-2]} +{"m1.X": [0,-4], "m1.Y": [0,2]} +{"m1.X": [0,-2], "m1.Y": [0,1]} +{"m1.X": [0,0], "m1.Y": [0,0]} +{"m1.X": [0,2], "m1.Y": [0,-1]} +{"m1.X": [0,4], "m1.Y": [0,-2]} diff --git a/testdata/module_10.lisp b/testdata/module_10.lisp new file mode 100644 index 0000000..937dab4 --- /dev/null +++ b/testdata/module_10.lisp @@ -0,0 +1,15 @@ +(defpurefun ((vanishes! :@loob) x) x) +(defconst + ONE 1 + TWO 2) +;; +(module m1) +(defcolumns X Y) +(defconstraint c1 () (vanishes! (+ X (* TWO Y)))) +(defconstraint c2 () (vanishes! (+ (* TWO Y) X))) +(defconstraint c3 () (vanishes! (+ X Y Y))) +(defconstraint c4 () (vanishes! (+ Y X Y))) +(defconstraint c5 () (vanishes! (+ Y Y X))) +(defconstraint c6 () (vanishes! (+ (* ONE X) Y Y))) +(defconstraint c7 () (vanishes! (+ Y (* ONE X) Y))) +(defconstraint c8 () (vanishes! (+ Y Y (* ONE X)))) diff --git a/testdata/module_10.rejects b/testdata/module_10.rejects new file mode 100644 index 0000000..321d4fc --- /dev/null +++ b/testdata/module_10.rejects @@ -0,0 +1,7 @@ +{"m1.X": [-2], "m1.Y": [-2]} +{"m1.X": [-2], "m1.Y": [-1]} +{"m1.X": [-2], "m1.Y": [0]} +{"m1.X": [-2], "m1.Y": [2]} +{"m1.X": [-2], "m1.Y": [3]} +{"m1.X": [0,1], "m1.Y": [0,1]} +{"m1.X": [-2,1], "m1.Y": [1,1]} diff --git a/testdata/mxp.lisp b/testdata/mxp.lisp index b4c8b12..d6c370e 100644 --- a/testdata/mxp.lisp +++ b/testdata/mxp.lisp @@ -1,131 +1,460 @@ (module mxp) (defcolumns - (STAMP :i32) - (CN :i64) - (CT :i5) - (ROOB :binary@prove) - (NOOP :binary@prove) - (MXPX :binary@prove) - (INST :byte) - (MXP_TYPE_1 :binary@prove) - (MXP_TYPE_2 :binary@prove) - (MXP_TYPE_3 :binary@prove) - (MXP_TYPE_4 :binary@prove) - (MXP_TYPE_5 :binary@prove) - (GBYTE :i64) - (GWORD :i64) - (DEPLOYS :binary@prove) - (OFFSET_1_LO :i128) - (OFFSET_2_LO :i128) - (OFFSET_1_HI :i128) - (OFFSET_2_HI :i128) - (SIZE_1_LO :i128) - (SIZE_2_LO :i128) - (SIZE_1_HI :i128) - (SIZE_2_HI :i128) - (MAX_OFFSET_1 :i128) - (MAX_OFFSET_2 :i128) - (MAX_OFFSET :i128) - (COMP :binary@prove) - (BYTE_1 :byte@prove) - (BYTE_2 :byte@prove) - (BYTE_3 :byte@prove) - (BYTE_4 :byte@prove) - (BYTE_A :byte@prove) - (BYTE_W :byte@prove) - (BYTE_Q :byte@prove) - (ACC_1 :i136) - (ACC_2 :i136) - (ACC_3 :i136) - (ACC_4 :i136) - (ACC_A :i136) - (ACC_W :i136) - (ACC_Q :i136) - (BYTE_QQ :byte@prove) - (BYTE_R :byte@prove) - (WORDS :i64) - (WORDS_NEW :i64) - (C_MEM :i64) - (C_MEM_NEW :i64) - (QUAD_COST :i64) - (LIN_COST :i64) - (GAS_MXP :i64) - (EXPANDS :binary@prove) - (MTNTOP :binary@prove)) + (STAMP :i32) + (CN :i64) + (CT :i5) + (ROOB :binary@prove) + (NOOP :binary@prove) + (MXPX :binary@prove) + (INST :byte :display :opcode) + (MXP_TYPE :binary@prove :array [5]) + (GBYTE :i64) + (GWORD :i64) + (DEPLOYS :binary@prove) + (OFFSET_1_LO :i128) + (OFFSET_2_LO :i128) + (OFFSET_1_HI :i128) + (OFFSET_2_HI :i128) + (SIZE_1_LO :i128) + (SIZE_2_LO :i128) + (SIZE_1_HI :i128) + (SIZE_2_HI :i128) + (MAX_OFFSET_1 :i128) + (MAX_OFFSET_2 :i128) + (MAX_OFFSET :i128) + (COMP :binary@prove) + (BYTE :byte@prove :array [4]) + (BYTE_A :byte@prove) + (BYTE_W :byte@prove) + (BYTE_Q :byte@prove) + (ACC :i136 :array [4]) + (ACC_A :i136) + (ACC_W :i136) + (ACC_Q :i136) + (BYTE_QQ :byte@prove) + (BYTE_R :byte@prove) + (WORDS :i64) + (WORDS_NEW :i64) + (C_MEM :i64) + (C_MEM_NEW :i64) + (QUAD_COST :i64) + (LIN_COST :i64) + (GAS_MXP :i64) + (EXPANDS :binary@prove) + (MTNTOP :binary@prove) + (SIZE_1_NONZERO_NO_MXPX :binary) + (SIZE_2_NONZERO_NO_MXPX :binary)) + + (defalias + S1NZNOMXPX SIZE_1_NONZERO_NO_MXPX + S2NZNOMXPX SIZE_2_NONZERO_NO_MXPX) -(defpermutation (CN_perm STAMP_perm C_MEM_perm C_MEM_NEW_perm WORDS_perm WORDS_NEW_perm) ((+ CN) (+ STAMP) (+ C_MEM) (+ C_MEM_NEW) (+ WORDS) (+ WORDS_NEW))) -(defconstraint counter-constancy () (begin (if CT 0 (- INST (shift INST -1))) (if CT 0 (- OFFSET_1_LO (shift OFFSET_1_LO -1))) (if CT 0 (- OFFSET_1_HI (shift OFFSET_1_HI -1))) (if CT 0 (- OFFSET_2_LO (shift OFFSET_2_LO -1))) (if CT 0 (- OFFSET_2_HI (shift OFFSET_2_HI -1))) (if CT 0 (- SIZE_1_LO (shift SIZE_1_LO -1))) (if CT 0 (- SIZE_1_HI (shift SIZE_1_HI -1))) (if CT 0 (- SIZE_2_LO (shift SIZE_2_LO -1))) (if CT 0 (- SIZE_2_HI (shift SIZE_2_HI -1))) (if CT 0 (- WORDS (shift WORDS -1))) (if CT 0 (- WORDS_NEW (shift WORDS_NEW -1))) (if CT 0 (- C_MEM (shift C_MEM -1))) (if CT 0 (- C_MEM_NEW (shift C_MEM_NEW -1))) (if CT 0 (- COMP (shift COMP -1))) (if CT 0 (- MXPX (shift MXPX -1))) (if CT 0 (- EXPANDS (shift EXPANDS -1))) (if CT 0 (- QUAD_COST (shift QUAD_COST -1))) (if CT 0 (- LIN_COST (shift LIN_COST -1))) (if CT 0 (- GAS_MXP (shift GAS_MXP -1))))) -(defconstraint byte-decompositions () (begin (if CT (- ACC_1 BYTE_1) (- ACC_1 (+ (* 256 (shift ACC_1 -1)) BYTE_1))) (if CT (- ACC_2 BYTE_2) (- ACC_2 (+ (* 256 (shift ACC_2 -1)) BYTE_2))) (if CT (- ACC_3 BYTE_3) (- ACC_3 (+ (* 256 (shift ACC_3 -1)) BYTE_3))) (if CT (- ACC_4 BYTE_4) (- ACC_4 (+ (* 256 (shift ACC_4 -1)) BYTE_4))) (if CT (- ACC_A BYTE_A) (- ACC_A (+ (* 256 (shift ACC_A -1)) BYTE_A))) (if CT (- ACC_W BYTE_W) (- ACC_W (+ (* 256 (shift ACC_W -1)) BYTE_W))) (if CT (- ACC_Q BYTE_Q) (- ACC_Q (+ (* 256 (shift ACC_Q -1)) BYTE_Q))))) - -(defconstraint euclidean-division-of-square-of-accA () (if (* (* STAMP (- 1 NOOP ROOB)) (* (* (- 1 (~ (- CT 3))) (- 1 MXPX)) EXPANDS)) 0 (begin (- (* ACC_A ACC_A) (+ (* 512 (+ ACC_Q (+ (* 4294967296 (shift BYTE_QQ -2)) (* 1099511627776 (shift BYTE_QQ -3))))) (+ (* 256 (shift BYTE_QQ -1)) BYTE_QQ))) (* (shift BYTE_QQ -1) (- 1 (shift BYTE_QQ -1)))))) - -(defconstraint setting-c-mem-new () (if (* (* STAMP (- 1 NOOP ROOB)) (* (* (- 1 (~ (- CT 3))) (- 1 MXPX)) EXPANDS)) 0 (- C_MEM_NEW (+ (* 3 ACC_A) (+ ACC_Q (+ (* 4294967296 (shift BYTE_QQ -2)) (* 1099511627776 (shift BYTE_QQ -3)))))))) - -(defconstraint setting-roob-type-5 () (if MXP_TYPE_5 0 (begin (if SIZE_1_HI 0 (- ROOB 1)) (if SIZE_2_HI 0 (- ROOB 1)) (if (* OFFSET_1_HI SIZE_1_LO) 0 (- ROOB 1)) (if (* OFFSET_2_HI SIZE_2_LO) 0 (- ROOB 1)) (if SIZE_1_HI (if SIZE_2_HI (if (* OFFSET_1_HI SIZE_1_LO) (if (* OFFSET_2_HI SIZE_2_LO) ROOB))))))) - -(defconstraint setting-noop () (if ROOB (begin (if (+ MXP_TYPE_1 MXP_TYPE_2 MXP_TYPE_3) 0 (- NOOP MXP_TYPE_1)) (if (- MXP_TYPE_4 1) (- NOOP (- 1 (~ SIZE_1_LO)))) (if (- MXP_TYPE_5 1) (- NOOP (* (- 1 (~ SIZE_1_LO)) (- 1 (~ SIZE_2_LO)))))))) - -(defconstraint non-trivial-instruction-counter-cycle () (if STAMP 0 (if (- 1 (+ ROOB NOOP)) 0 (if MXPX (if (- CT 3) (- (shift STAMP 1) (+ STAMP 1)) (- (shift CT 1) (+ CT 1))) (if (- CT 16) (- (shift STAMP 1) (+ STAMP 1)) (- (shift CT 1) (+ CT 1))))))) - -(defconstraint size-in-evm-words () (if (* (* STAMP (- 1 NOOP ROOB)) (* (- 1 (~ (- CT 3))) (- 1 MXPX))) 0 (if (- MXP_TYPE_4 1) (begin (- SIZE_1_LO (- (* 32 ACC_W) BYTE_R)) (- (shift BYTE_R -1) (+ 224 BYTE_R)))))) - -(defconstraint comparing-max-offsets-1-and-2 () (if (* (* STAMP (- 1 NOOP ROOB)) (* (- 1 (~ (- CT 3))) (- 1 MXPX))) 0 (- (+ ACC_3 (- 1 COMP)) (* (- MAX_OFFSET_1 MAX_OFFSET_2) (- (* 2 COMP) 1))))) - -(defconstraint defining-accA () (if (* (* STAMP (- 1 NOOP ROOB)) (* (- 1 (~ (- CT 3))) (- 1 MXPX))) 0 (begin (- (+ MAX_OFFSET 1) (- (* 32 ACC_A) (shift BYTE_R -2))) (- (shift BYTE_R -3) (+ 224 (shift BYTE_R -2)))))) - -(defconstraint setting-gas-mxp () (if (* (* STAMP (- 1 NOOP ROOB)) (* (- 1 (~ (- CT 3))) (- 1 MXPX))) 0 (if (- INST 243) (- GAS_MXP (+ QUAD_COST (* DEPLOYS LIN_COST))) (- GAS_MXP (+ QUAD_COST LIN_COST))))) - -(defconstraint mem-expansion-took-place () (if (* (* STAMP (- 1 NOOP ROOB)) (* (- 1 (~ (- CT 3))) (- 1 MXPX))) 0 (- (+ ACC_4 EXPANDS) (* (- ACC_A WORDS) (- (* 2 EXPANDS) 1))))) - -(defconstraint setting-quad-cost-and-lin-cost () (if (* (* STAMP (- 1 NOOP ROOB)) (* (- 1 (~ (- CT 3))) (- 1 MXPX))) 0 (begin (- QUAD_COST (- C_MEM_NEW C_MEM)) (- LIN_COST (+ (* GBYTE SIZE_1_LO) (* GWORD ACC_W)))))) - -(defconstraint defining-max-offset () (if (* (* STAMP (- 1 NOOP ROOB)) (* (- 1 (~ (- CT 3))) (- 1 MXPX))) 0 (- MAX_OFFSET (+ (* COMP MAX_OFFSET_1) (* (- 1 COMP) MAX_OFFSET_2))))) - -(defconstraint max-offsets-1-and-2-type-5 () (if (* STAMP (- 1 NOOP ROOB)) 0 (if (- MXP_TYPE_5 1) (begin (if SIZE_1_LO MAX_OFFSET_1 (- MAX_OFFSET_1 (+ OFFSET_1_LO (- SIZE_1_LO 1)))) (if SIZE_2_LO MAX_OFFSET_2 (- MAX_OFFSET_2 (+ OFFSET_2_LO (- SIZE_2_LO 1)))))))) - -(defconstraint binary-constraints () (begin (* ROOB (- 1 ROOB)) (* NOOP (- 1 NOOP)) (* MXPX (- 1 MXPX)) (* DEPLOYS (- 1 DEPLOYS)) (* COMP (- 1 COMP)) (* EXPANDS (- 1 EXPANDS)))) - -(defconstraint offsets-out-of-bounds () (if (* STAMP (- 1 NOOP ROOB)) 0 (if (- MXPX 1) (if (- CT 16) (* (- (- MAX_OFFSET_1 4294967296) ACC_1) (- (- MAX_OFFSET_2 4294967296) ACC_2)))))) - -(defconstraint no-expansion () (if (* (* STAMP (- 1 NOOP ROOB)) (* (- 1 (~ (- CT 3))) (- 1 MXPX))) 0 (if EXPANDS (begin (- WORDS_NEW WORDS) (- C_MEM_NEW C_MEM))))) - -(defconstraint max-offsets-1-and-2-are-small () (if (* (* STAMP (- 1 NOOP ROOB)) (* (- 1 (~ (- CT 3))) (- 1 MXPX))) 0 (begin (- ACC_1 MAX_OFFSET_1) (- ACC_2 MAX_OFFSET_2)))) - -(defconstraint setting-words-new () (if (* (* STAMP (- 1 NOOP ROOB)) (* (* (- 1 (~ (- CT 3))) (- 1 MXPX)) EXPANDS)) 0 (- WORDS_NEW ACC_A))) - -(defconstraint setting-roob-type-4 () (if MXP_TYPE_4 0 (begin (if SIZE_1_HI 0 (- ROOB 1)) (if (* OFFSET_1_HI SIZE_1_LO) 0 (- ROOB 1)) (if SIZE_1_HI (if (* OFFSET_1_HI SIZE_1_LO) ROOB))))) - -(defconstraint max-offsets-1-and-2-type-4 () (if (* STAMP (- 1 NOOP ROOB)) 0 (if (- MXP_TYPE_4 1) (begin (- MAX_OFFSET_1 (+ OFFSET_1_LO (- SIZE_1_LO 1))) MAX_OFFSET_2)))) - -(defconstraint max-offsets-1-and-2-type-2 () (if (* STAMP (- 1 NOOP ROOB)) 0 (if (- MXP_TYPE_2 1) (begin (- MAX_OFFSET_1 (+ OFFSET_1_LO 31)) MAX_OFFSET_2)))) - -(defconstraint consistency () (if CN_perm 0 (if (- (shift CN_perm -1) CN_perm) (if (- (shift STAMP_perm -1) STAMP_perm) 0 (begin (- WORDS_perm (shift WORDS_NEW_perm -1)) (- C_MEM_perm (shift C_MEM_NEW_perm -1)))) (begin WORDS_perm C_MEM_perm)))) - -(defconstraint type-flag-sum () (if STAMP 0 (- 1 (+ MXP_TYPE_1 (+ MXP_TYPE_2 (+ MXP_TYPE_3 (+ MXP_TYPE_5 MXP_TYPE_4))))))) - -(defconstraint max-offsets-1-and-2-type-3 () (if (* STAMP (- 1 NOOP ROOB)) 0 (if (- MXP_TYPE_3 1) (begin (- MAX_OFFSET_1 OFFSET_1_LO) MAX_OFFSET_2)))) - -(defconstraint stamp-increment-when-roob-or-noop () (if (+ ROOB NOOP) 0 (begin (- (shift STAMP 1) (+ STAMP 1)) (- MXPX ROOB)))) - -(defconstraint final-row (:domain {-1}) (if STAMP 0 (if (+ ROOB NOOP) (- CT (if MXPX 3 16))))) - -(defconstraint setting-roob-type-2-3 () (if (+ MXP_TYPE_2 MXP_TYPE_3) 0 (if OFFSET_1_HI ROOB (- ROOB 1)))) - -(defconstraint setting-mtntop () (if MXP_TYPE_4 MTNTOP (begin (if MXPX (if SIZE_1_LO MTNTOP (- MTNTOP 1)) MTNTOP)))) - -(defconstraint stamp-increments () (* (- (shift STAMP 1) STAMP) (- (shift STAMP 1) (+ STAMP 1)))) - -(defconstraint noop-consequences () (if NOOP 0 (begin QUAD_COST LIN_COST (- WORDS_NEW WORDS) (- C_MEM_NEW C_MEM)))) - -(defconstraint automatic-vanishing-when-padding () (if STAMP (begin (+ ROOB NOOP MXPX) CT INST))) +(module mxp) -(defconstraint counter-reset () (if (- (shift STAMP 1) STAMP) 0 (shift CT 1))) +(defconst + CT_MAX_TRIVIAL 0 + CT_MAX_NON_TRIVIAL 3 + CT_MAX_NON_TRIVIAL_BUT_MXPX 16 + TWO_POW_32 4294967296) -(defconstraint setting-roob-type-1 () (if MXP_TYPE_1 0 ROOB)) -(defconstraint noop-automatic-vanishing () (if ROOB 0 NOOP)) +(module mxp) -(defconstraint first-row (:domain {0}) STAMP) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.1 binary constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; done with binary@prove in columns.lisp + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.2 counter constancy ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint counter-constancy () + (begin (counter-constancy CT CN) + (counter-constancy CT INST) + (counter-constancy CT DEPLOYS) + (counter-constancy CT OFFSET_1_LO) + (counter-constancy CT OFFSET_1_HI) + (counter-constancy CT OFFSET_2_LO) + (counter-constancy CT OFFSET_2_HI) + (counter-constancy CT SIZE_1_LO) + (counter-constancy CT SIZE_1_HI) + (counter-constancy CT SIZE_2_LO) + (counter-constancy CT SIZE_2_HI) + (counter-constancy CT WORDS) + (counter-constancy CT WORDS_NEW) + (counter-constancy CT C_MEM) + (counter-constancy CT C_MEM_NEW) + (counter-constancy CT COMP) + (counter-constancy CT MXPX) + (counter-constancy CT EXPANDS) + (counter-constancy CT QUAD_COST) + (counter-constancy CT LIN_COST) + (counter-constancy CT GAS_MXP))) + +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.3 ROOB flag ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint setting-roob-type-1 (:guard [MXP_TYPE 1]) + (vanishes! ROOB)) + +(defconstraint setting-roob-type-2-3 (:guard (+ [MXP_TYPE 2] [MXP_TYPE 3])) + (if-not-zero OFFSET_1_HI + (eq! ROOB 1) + (vanishes! ROOB))) + +(defconstraint setting-roob-type-4 (:guard [MXP_TYPE 4]) + (begin (if-not-zero SIZE_1_HI + (eq! ROOB 1)) + (if-not-zero (* OFFSET_1_HI SIZE_1_LO) + (eq! ROOB 1)) + (if-zero SIZE_1_HI + (if-zero (* OFFSET_1_HI SIZE_1_LO) + (vanishes! ROOB))))) + +(defconstraint setting-roob-type-5 (:guard [MXP_TYPE 5]) + (begin (if-not-zero SIZE_1_HI + (eq! ROOB 1)) + (if-not-zero SIZE_2_HI + (eq! ROOB 1)) + (if-not-zero (* OFFSET_1_HI SIZE_1_LO) + (eq! ROOB 1)) + (if-not-zero (* OFFSET_2_HI SIZE_2_LO) + (eq! ROOB 1)) + (if-zero SIZE_1_HI + (if-zero SIZE_2_HI + (if-zero (* OFFSET_1_HI SIZE_1_LO) + (if-zero (* OFFSET_2_HI SIZE_2_LO) + (vanishes! ROOB))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.4 NOOP flag ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint noop-automatic-vanishing () + (if-not-zero ROOB + (vanishes! NOOP))) + +(defconstraint setting-noop () + (if-zero ROOB + (begin (if-not-zero (+ [MXP_TYPE 1] [MXP_TYPE 2] [MXP_TYPE 3]) + (eq! NOOP [MXP_TYPE 1])) + (if-eq [MXP_TYPE 4] 1 + (eq! NOOP (is-zero SIZE_1_LO))) + (if-eq [MXP_TYPE 5] 1 + (eq! NOOP + (* (is-zero SIZE_1_LO) (is-zero SIZE_2_LO))))))) + +(defconstraint noop-consequences (:guard NOOP) + (begin (vanishes! QUAD_COST) + (vanishes! LIN_COST) + (= WORDS_NEW WORDS) + (= C_MEM_NEW C_MEM))) + +;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.5 MTNTOP ;; +;; ;; +;;;;;;;;;;;;;;;;;;;; + +(defconstraint setting-mtntop () + (begin + (debug (is-binary MTNTOP)) + (debug (if-zero [MXP_TYPE 4] + (vanishes! MTNTOP))) + (if-not-zero MXPX + (vanishes! MTNTOP)) + (if-not-zero [MXP_TYPE 4] + (if-zero MXPX + (if-zero SIZE_1_LO + (vanishes! MTNTOP) + (eq! MTNTOP 1)))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.6 The S1NZNOMXPX and S2NZNOMXPX flags ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint setting-s1nznomp-s2nznomp () + (begin + (debug (is-binary S1NZNOMXPX)) + (debug (is-binary S2NZNOMXPX)) + (debug (counter-constancy CT S1NZNOMXPX)) + (debug (counter-constancy CT S2NZNOMXPX)) + (if-not-zero MXPX + (begin (vanishes! S1NZNOMXPX) + (vanishes! S2NZNOMXPX)) + (begin (if-not-zero SIZE_1_LO + (eq! S1NZNOMXPX 1)) + (if-not-zero SIZE_1_HI + (eq! S1NZNOMXPX 1)) + (if-zero SIZE_1_LO + (if-zero SIZE_1_HI + (vanishes! S1NZNOMXPX))) + (if-not-zero SIZE_2_LO + (eq! S2NZNOMXPX 1)) + (if-not-zero SIZE_2_HI + (eq! S2NZNOMXPX 1)) + (if-zero SIZE_2_LO + (if-zero SIZE_2_HI + (vanishes! S2NZNOMXPX))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.7 heartbeat ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint first-row (:domain {0}) + (vanishes! STAMP)) + +(defconstraint stamp-increments () + (any! (will-remain-constant! STAMP) (will-inc! STAMP 1))) + +(defconstraint automatic-vanishing-when-padding () + (if-zero STAMP + (begin (vanishes! (+ ROOB NOOP MXPX)) + (vanishes! CT) + (vanishes! INST)))) + +;; (defconstraint type-flag-sum (:guard STAMP) +;; (eq! 1 +;; (reduce + (for i [5] [MXP_TYPE i])))) + +(defconstraint counter-reset () + (if-not-zero (will-remain-constant! STAMP) + (vanishes! (next CT)))) + +(defconstraint stamp-increment-when-roob-or-noop () + (if-not-zero (+ ROOB NOOP) + (begin (will-inc! STAMP 1) + (eq! MXPX ROOB)))) + +(defconstraint non-trivial-instruction-counter-cycle () + (if-not-zero STAMP + ;; ROOB + NOOP is binary + (if-not-zero (- 1 (+ ROOB NOOP)) + (if-zero MXPX + (if-eq-else CT CT_MAX_NON_TRIVIAL + (will-inc! STAMP 1) + (will-inc! CT 1)) + (if-eq-else CT CT_MAX_NON_TRIVIAL_BUT_MXPX + (will-inc! STAMP 1) + (will-inc! CT 1)))))) + +(defconstraint final-row (:domain {-1}) + (if-not-zero STAMP + (if-zero (force-bool (+ ROOB NOOP)) + (eq! CT (if-zero MXPX + CT_MAX_NON_TRIVIAL + CT_MAX_NON_TRIVIAL_BUT_MXPX))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.8 Byte decompositions ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint byte-decompositions () + (begin (for k [1:4] (byte-decomposition CT [ACC k] [BYTE k])) + (byte-decomposition CT ACC_A BYTE_A) + (byte-decomposition CT ACC_W BYTE_W) + (byte-decomposition CT ACC_Q BYTE_Q))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; Specialized constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (standing-hypothesis) + (* STAMP (- 1 NOOP ROOB))) ;; NOOP + ROOB is binary cf noop section + +;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 3.1 Max offsets ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint max-offsets-1-and-2-type-2 (:guard (standing-hypothesis)) + (if-eq [MXP_TYPE 2] 1 + (begin (eq! MAX_OFFSET_1 (+ OFFSET_1_LO 31)) + (vanishes! MAX_OFFSET_2)))) + +(defconstraint max-offsets-1-and-2-type-3 (:guard (standing-hypothesis)) + (if-eq [MXP_TYPE 3] 1 + (begin (eq! MAX_OFFSET_1 OFFSET_1_LO) + (vanishes! MAX_OFFSET_2)))) + +(defconstraint max-offsets-1-and-2-type-4 (:guard (standing-hypothesis)) + (if-eq [MXP_TYPE 4] 1 + (begin (eq! MAX_OFFSET_1 + (+ OFFSET_1_LO (- SIZE_1_LO 1))) + (vanishes! MAX_OFFSET_2)))) + +(defconstraint max-offsets-1-and-2-type-5 (:guard (standing-hypothesis)) + (if-eq [MXP_TYPE 5] 1 + (begin (if-zero SIZE_1_LO + (vanishes! MAX_OFFSET_1) + (eq! MAX_OFFSET_1 + (+ OFFSET_1_LO (- SIZE_1_LO 1)))) + (if-zero SIZE_2_LO + (vanishes! MAX_OFFSET_2) + (eq! MAX_OFFSET_2 + (+ OFFSET_2_LO (- SIZE_2_LO 1))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 3.2 Offsets are out of bounds ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint offsets-out-of-bounds (:guard (standing-hypothesis)) + (if-eq MXPX 1 + (if-eq CT CT_MAX_NON_TRIVIAL_BUT_MXPX + (vanishes! (* (- (- MAX_OFFSET_1 TWO_POW_32) [ACC 1]) + (- (- MAX_OFFSET_2 TWO_POW_32) [ACC 2])))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 3.3 Offsets are in bounds ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (offsets-are-in-bounds) + (* (is-zero (- CT CT_MAX_NON_TRIVIAL)) + (- 1 MXPX))) + +(defconstraint size-in-evm-words (:guard (* (standing-hypothesis) (offsets-are-in-bounds))) + (if-eq [MXP_TYPE 4] 1 + (begin (eq! SIZE_1_LO + (- (* 32 ACC_W) BYTE_R)) + (eq! (prev BYTE_R) + (+ (- 256 32) BYTE_R))))) + +(defconstraint max-offsets-1-and-2-are-small (:guard (* (standing-hypothesis) (offsets-are-in-bounds))) + (begin (eq! [ACC 1] MAX_OFFSET_1) + (eq! [ACC 2] MAX_OFFSET_2))) + +(defconstraint comparing-max-offsets-1-and-2 (:guard (* (standing-hypothesis) (offsets-are-in-bounds))) + (eq! (+ [ACC 3] (- 1 COMP)) + (* (- MAX_OFFSET_1 MAX_OFFSET_2) + (- (* 2 COMP) 1)))) + +(defconstraint defining-max-offset (:guard (* (standing-hypothesis) (offsets-are-in-bounds))) + (eq! MAX_OFFSET + (+ (* COMP MAX_OFFSET_1) + (* (- 1 COMP) MAX_OFFSET_2)))) + +(defconstraint defining-accA (:guard (* (standing-hypothesis) (offsets-are-in-bounds))) + (begin (eq! (+ MAX_OFFSET 1) + (- (* 32 ACC_A) (shift BYTE_R -2))) + (eq! (shift BYTE_R -3) + (+ (- 256 32) (shift BYTE_R -2))))) + +(defconstraint mem-expansion-took-place (:guard (* (standing-hypothesis) (offsets-are-in-bounds))) + (eq! (+ [ACC 4] EXPANDS) + (* (- ACC_A WORDS) + (- (* 2 EXPANDS) 1)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 3.4.2 No expansion event ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint no-expansion (:guard (* (standing-hypothesis) (offsets-are-in-bounds))) + (if-zero EXPANDS + (begin (eq! WORDS_NEW WORDS) + (eq! C_MEM_NEW C_MEM)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 3.4.3 Expansion event ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun (expansion-happened) + (* (offsets-are-in-bounds) EXPANDS)) + +(defconstraint setting-words-new (:guard (* (standing-hypothesis) (expansion-happened))) + (eq! WORDS_NEW ACC_A)) + +(defun (large-quotient) + (+ ACC_Q + (+ (* TWO_POW_32 (shift BYTE_QQ -2)) + (* (* 256 TWO_POW_32) (shift BYTE_QQ -3))))) + +(defconstraint euclidean-division-of-square-of-accA (:guard (* (standing-hypothesis) (expansion-happened))) + (begin (eq! (* ACC_A ACC_A) + (+ (* 512 (large-quotient)) + (+ (* 256 (prev BYTE_QQ)) + BYTE_QQ))) + (vanishes! (* (prev BYTE_QQ) + (- 1 (prev BYTE_QQ)))))) + +(defconstraint setting-c-mem-new (:guard (* (standing-hypothesis) (expansion-happened))) + (eq! C_MEM_NEW + (+ (* GAS_CONST_G_MEMORY ACC_A) (large-quotient)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 3.4.4 Expansion gas ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconstraint setting-quad-cost-and-lin-cost (:guard (* (standing-hypothesis) (offsets-are-in-bounds))) + (begin (eq! QUAD_COST (- C_MEM_NEW C_MEM)) + (eq! LIN_COST + (+ (* GBYTE SIZE_1_LO) (* GWORD ACC_W))))) + +(defconstraint setting-gas-mxp (:guard (* (standing-hypothesis) (offsets-are-in-bounds))) + (if (eq! INST EVM_INST_RETURN) + (eq! GAS_MXP + (+ QUAD_COST (* DEPLOYS LIN_COST))) + (eq! GAS_MXP (+ QUAD_COST LIN_COST)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.12 Consistency Constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defpermutation + (CN_perm + STAMP_perm + C_MEM_perm + C_MEM_NEW_perm + WORDS_perm + WORDS_NEW_perm) + + ((↓ CN) + (↓ STAMP) + C_MEM + C_MEM_NEW + WORDS + WORDS_NEW) + ) + +(defconstraint consistency () + (if-not-zero CN_perm + (if-eq-else (prev CN_perm) CN_perm + (if-not-zero (- (prev STAMP_perm) STAMP_perm) + (begin (eq! WORDS_perm (prev WORDS_NEW_perm)) + (eq! C_MEM_perm (prev C_MEM_NEW_perm)))) + (begin (vanishes! WORDS_perm) + (vanishes! C_MEM_perm))))) diff --git a/testdata/norm_01.lisp b/testdata/norm_01.lisp index 8296070..f1e886c 100644 --- a/testdata/norm_01.lisp +++ b/testdata/norm_01.lisp @@ -1,2 +1,4 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns ST A) -(defconstraint c1 () (* ST (- 1 (~ A)))) +(defconstraint c1 () (vanishes! (* ST (- 1 (~ A))))) diff --git a/testdata/norm_02.lisp b/testdata/norm_02.lisp index 444639d..a1478e4 100644 --- a/testdata/norm_02.lisp +++ b/testdata/norm_02.lisp @@ -1,2 +1,4 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns ST A B) -(defconstraint c1 () (* ST (- 1 (~ (+ A B))))) +(defconstraint c1 () (vanishes! (* ST (- 1 (~ (+ A B)))))) diff --git a/testdata/norm_03.lisp b/testdata/norm_03.lisp index 6546b8c..2c9608a 100644 --- a/testdata/norm_03.lisp +++ b/testdata/norm_03.lisp @@ -1,2 +1,4 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns ST A B) -(defconstraint c1 () (* ST (- 1 (+ (~ A) (~ B))))) +(defconstraint c1 () (vanishes! (* ST (- 1 (+ (~ A) (~ B)))))) diff --git a/testdata/norm_04.lisp b/testdata/norm_04.lisp index c546e8e..62079e8 100644 --- a/testdata/norm_04.lisp +++ b/testdata/norm_04.lisp @@ -1,2 +1,4 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns ST A B) -(defconstraint c1 () (* ST (- 1 (~ A)) (- 1 (~ B)))) +(defconstraint c1 () (vanishes! (* ST (- 1 (~ A)) (- 1 (~ B))))) diff --git a/testdata/norm_05.lisp b/testdata/norm_05.lisp index a00a51f..a7dfded 100644 --- a/testdata/norm_05.lisp +++ b/testdata/norm_05.lisp @@ -1,2 +1,4 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns A) -(defconstraint c1 () (~ A)) +(defconstraint c1 () (vanishes! (~ A))) diff --git a/testdata/norm_06.lisp b/testdata/norm_06.lisp index 0573efb..9bb21bc 100644 --- a/testdata/norm_06.lisp +++ b/testdata/norm_06.lisp @@ -1,2 +1,4 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns A B) -(defconstraint c1 () (~ (+ A B))) +(defconstraint c1 () (vanishes! (~ (+ A B)))) diff --git a/testdata/norm_07.lisp b/testdata/norm_07.lisp index 52dec7c..a1929d0 100644 --- a/testdata/norm_07.lisp +++ b/testdata/norm_07.lisp @@ -1,2 +1,4 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns A) -(defconstraint c1 () (- 2 (~ A))) +(defconstraint c1 () (vanishes! (- 2 (~ A)))) diff --git a/testdata/permute_01.lisp b/testdata/permute_01.lisp index 3ba6932..8346075 100644 --- a/testdata/permute_01.lisp +++ b/testdata/permute_01.lisp @@ -1,5 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) (defcolumns (X :i16@prove)) (defpermutation (Y) ((↓ X))) (defpermutation (Z) ((+ X))) ;; Y == Z -(defconstraint eq () (- Y Z)) +(defconstraint eq () (vanishes! (- Y Z))) diff --git a/testdata/permute_02.lisp b/testdata/permute_02.lisp index 5b3a4bd..5ef5f59 100644 --- a/testdata/permute_02.lisp +++ b/testdata/permute_02.lisp @@ -1,3 +1,3 @@ -(defcolumns (X :i16@prove)) +(defcolumns (X :i16@loob@prove)) (defpermutation (Y) ((+ X))) (defconstraint first-row (:domain {0}) Y) diff --git a/testdata/permute_03.lisp b/testdata/permute_03.lisp index c095f52..552fd91 100644 --- a/testdata/permute_03.lisp +++ b/testdata/permute_03.lisp @@ -1,4 +1,7 @@ +(defpurefun ((vanishes! :@loob) x) x) (defcolumns ST (X :i16@prove)) (defpermutation (Y) ((↓ X))) ;; Ensure sorted column increments by 1 -(defconstraint increment () (* ST (- (shift Y 1) (+ 1 Y)))) +(defconstraint increment () + (vanishes! + (* ST (- (shift Y 1) (+ 1 Y))))) diff --git a/testdata/permute_04.lisp b/testdata/permute_04.lisp index d794a28..44120a5 100644 --- a/testdata/permute_04.lisp +++ b/testdata/permute_04.lisp @@ -1,5 +1,5 @@ (defcolumns - (ST :i16@prove) - (X :i16@prove)) + (ST :i16@loob@prove) + (X :i16@loob@prove)) (defpermutation (ST' Y) ((↓ ST) (↑ X))) (defconstraint first-row (:domain {-1}) (- Y 5)) diff --git a/testdata/permute_05.lisp b/testdata/permute_05.lisp index 09b2eb6..b66af5d 100644 --- a/testdata/permute_05.lisp +++ b/testdata/permute_05.lisp @@ -1,5 +1,5 @@ (defcolumns - (X :byte@prove) - (Y :byte@prove)) + (X :byte@loob@prove) + (Y :byte@loob@prove)) (defpermutation (A B) ((+ X) (+ Y))) (defconstraint diag_ab () (- (shift A 1) B)) diff --git a/testdata/permute_06.lisp b/testdata/permute_06.lisp index 23423c1..31db3b7 100644 --- a/testdata/permute_06.lisp +++ b/testdata/permute_06.lisp @@ -1,5 +1,5 @@ (defcolumns - (X :i16@prove) - (Y :i16@prove)) + (X :i16@loob@prove) + (Y :i16@loob@prove)) (defpermutation (A B) ((+ X) (+ Y))) (defconstraint diag_ab () (- (shift A 1) B)) diff --git a/testdata/permute_07.lisp b/testdata/permute_07.lisp index ec59c61..9eb22f8 100644 --- a/testdata/permute_07.lisp +++ b/testdata/permute_07.lisp @@ -1,6 +1,9 @@ +(defpurefun ((vanishes! :@loob) x) x) +;; (defcolumns (ST :i16@prove) (X :i16@prove) (Y :i16@prove)) (defpermutation (ST' A B) ((+ ST) (- X) (+ Y))) -(defconstraint diag_ab () (* ST' (- (shift A 1) B))) +(defconstraint diag_ab () + (vanishes! (* ST' (- (shift A 1) B)))) diff --git a/testdata/permute_08.lisp b/testdata/permute_08.lisp index 974e57d..333f17c 100644 --- a/testdata/permute_08.lisp +++ b/testdata/permute_08.lisp @@ -1,5 +1,5 @@ (defcolumns - (X :i16@prove) - (Y :i16@prove)) + (X :i16@loob@prove) + (Y :i16@loob@prove)) (defpermutation (A B) ((+ X) (- Y))) (defconstraint diag_ab () (* A (- (shift A 1) B))) diff --git a/testdata/permute_09.lisp b/testdata/permute_09.lisp index b2545d4..16c9e05 100644 --- a/testdata/permute_09.lisp +++ b/testdata/permute_09.lisp @@ -1,6 +1,9 @@ +(defpurefun ((vanishes! :@loob) x) x) +;; (defcolumns (ST :i16@prove) (X :i16@prove) (Y :i16@prove)) (defpermutation (ST' A B) ((+ ST) (- X) (- Y))) -(defconstraint diag_ab () (* ST' (- (shift A 1) B))) +(defconstraint diag_ab () + (vanishes! (* ST' (- (shift A 1) B)))) diff --git a/testdata/property_01.lisp b/testdata/property_01.lisp index 8d7d1b1..a719237 100644 --- a/testdata/property_01.lisp +++ b/testdata/property_01.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns A B) -(defconstraint eq () (- A B)) +(defconstraint eq () (vanishes! (- A B))) (defproperty lem (- A B)) diff --git a/testdata/purefun_01.lisp b/testdata/purefun_01.lisp index 7aafa59..e8f0143 100644 --- a/testdata/purefun_01.lisp +++ b/testdata/purefun_01.lisp @@ -1,3 +1,5 @@ +(defpurefun ((vanishes! :@loob) x) x) +;; (defcolumns A) (defpurefun (id x) x) -(defconstraint test () (id A)) +(defconstraint test () (vanishes! (id A))) diff --git a/testdata/purefun_02.lisp b/testdata/purefun_02.lisp index 5b5f120..3fa7d2c 100644 --- a/testdata/purefun_02.lisp +++ b/testdata/purefun_02.lisp @@ -1,3 +1,3 @@ (defcolumns A B) -(defpurefun (eq x y) (- y x)) +(defpurefun ((eq :@loob) x y) (- y x)) (defconstraint test () (eq A B)) diff --git a/testdata/purefun_04.lisp b/testdata/purefun_04.lisp index 9778f88..990419e 100644 --- a/testdata/purefun_04.lisp +++ b/testdata/purefun_04.lisp @@ -1,6 +1,6 @@ (defcolumns X Y) (defun (double x) (+ x x)) -(defpurefun (eq x y) (- x y)) +(defpurefun ((eq :@loob) x y) (- x y)) ;; Y == 2 * X (defconstraint c1 () (eq Y (double X))) diff --git a/testdata/purefun_invalid_08.lisp b/testdata/purefun_invalid_08.lisp new file mode 100644 index 0000000..5ff9847 --- /dev/null +++ b/testdata/purefun_invalid_08.lisp @@ -0,0 +1,5 @@ +(defcolumns (X :@loob) Y) +(defpurefun (id x) x) + +(defconstraint c1 () (id X)) +(defconstraint c2 () (id Y)) diff --git a/testdata/shift_01.lisp b/testdata/shift_01.lisp index af1b579..e2c41e8 100644 --- a/testdata/shift_01.lisp +++ b/testdata/shift_01.lisp @@ -1,2 +1,4 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X ST) -(defconstraint c1 () (* ST (shift X 1))) +(defconstraint c1 () (vanishes! (* ST (shift X 1)))) diff --git a/testdata/shift_02.lisp b/testdata/shift_02.lisp index 82369bb..98971a5 100644 --- a/testdata/shift_02.lisp +++ b/testdata/shift_02.lisp @@ -1,2 +1,4 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X) -(defconstraint c1 () (shift X -1)) +(defconstraint c1 () (vanishes! (shift X -1))) diff --git a/testdata/shift_03.lisp b/testdata/shift_03.lisp index 110b948..4159480 100644 --- a/testdata/shift_03.lisp +++ b/testdata/shift_03.lisp @@ -1,2 +1,4 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y ST) -(defconstraint c1 () (* ST (+ (shift X 1) Y))) +(defconstraint c1 () (vanishes! (* ST (+ (shift X 1) Y)))) diff --git a/testdata/shift_04.lisp b/testdata/shift_04.lisp index c730e71..3f61e08 100644 --- a/testdata/shift_04.lisp +++ b/testdata/shift_04.lisp @@ -1,2 +1,4 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y ST) -(defconstraint c1 () (* ST (- (shift X 1) Y))) +(defconstraint c1 () (vanishes! (* ST (- (shift X 1) Y)))) diff --git a/testdata/shift_05.lisp b/testdata/shift_05.lisp index 3a49e8e..4890db7 100644 --- a/testdata/shift_05.lisp +++ b/testdata/shift_05.lisp @@ -1,2 +1,4 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X Y) -(defconstraint c1 () (* (shift X 1) Y)) +(defconstraint c1 () (vanishes! (* (shift X 1) Y))) diff --git a/testdata/shift_06.lisp b/testdata/shift_06.lisp index dc0144b..543823c 100644 --- a/testdata/shift_06.lisp +++ b/testdata/shift_06.lisp @@ -1,2 +1,4 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X ST) -(defconstraint c1 () (* ST (- (shift X 1) (+ X 1)))) +(defconstraint c1 () (vanishes! (* ST (- (shift X 1) (+ X 1))))) diff --git a/testdata/shift_07.lisp b/testdata/shift_07.lisp index 38c4505..7889ac0 100644 --- a/testdata/shift_07.lisp +++ b/testdata/shift_07.lisp @@ -1,4 +1,4 @@ -(defcolumns (BIT_1 :binary@prove) ARG) +(defcolumns (BIT_1 :binary@loob@prove) (ARG :@loob)) (defconstraint pivot () ;; If BIT_1[k-1]=0 and BIT_1[k]=1 diff --git a/testdata/shift_08.lisp b/testdata/shift_08.lisp index ecad054..0d68df8 100644 --- a/testdata/shift_08.lisp +++ b/testdata/shift_08.lisp @@ -1,4 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns X) ;; intention is that shifts cancel. -(defconstraint c1 () (- X (shift (shift X -1) 1 ))) -(defconstraint c2 () (- (shift X 1) (shift (shift X -1) 2 ))) +(defconstraint c1 () (vanishes! (- X (shift (shift X -1) 1 )))) +(defconstraint c2 () (vanishes! (- (shift X 1) (shift (shift X -1) 2 )))) diff --git a/testdata/spillage_01.lisp b/testdata/spillage_01.lisp index b63a4d3..a519b68 100644 --- a/testdata/spillage_01.lisp +++ b/testdata/spillage_01.lisp @@ -1,2 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns ST A) -(defconstraint spills () (* ST (* A (~ (shift A 1))))) +(defconstraint spills () + (vanishes! + (* ST (* A (~ (shift A 1)))))) diff --git a/testdata/spillage_02.lisp b/testdata/spillage_02.lisp index 4b838e7..d71cc64 100644 --- a/testdata/spillage_02.lisp +++ b/testdata/spillage_02.lisp @@ -1,2 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns ST A) -(defconstraint spills () (* ST (* A (~ (shift A 2))))) +(defconstraint spills () + (vanishes! + (* ST (* A (~ (shift A 2)))))) diff --git a/testdata/spillage_03.lisp b/testdata/spillage_03.lisp index c901a28..ed9ab6f 100644 --- a/testdata/spillage_03.lisp +++ b/testdata/spillage_03.lisp @@ -1,2 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns ST A) -(defconstraint spills () (* ST A (~ (shift A 3)))) +(defconstraint spills () + (vanishes! + (* ST A (~ (shift A 3))))) diff --git a/testdata/spillage_04.lisp b/testdata/spillage_04.lisp index fe4e301..dc9542a 100644 --- a/testdata/spillage_04.lisp +++ b/testdata/spillage_04.lisp @@ -1,2 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns ST A B) -(defconstraint spills () (* ST A (~ (* (shift A 3) (shift B 2))))) +(defconstraint spills () + (vanishes! + (* ST A (~ (* (shift A 3) (shift B 2)))))) diff --git a/testdata/spillage_05.lisp b/testdata/spillage_05.lisp index cdd10cf..0cdb24a 100644 --- a/testdata/spillage_05.lisp +++ b/testdata/spillage_05.lisp @@ -1,7 +1,11 @@ +(defpurefun ((vanishes! :@loob) x) x) + (module m1) (defcolumns S1 A) -(defconstraint spills () (* S1 (* A (~ (shift A 2))))) +(defconstraint spills () + (vanishes! (* S1 (* A (~ (shift A 2)))))) (module m2) (defcolumns S2 B) -(defconstraint spills () (* S2 (* B (~ (shift B 3))))) +(defconstraint spills () + (vanishes! (* S2 (* B (~ (shift B 3)))))) diff --git a/testdata/spillage_06.lisp b/testdata/spillage_06.lisp index 04cf648..6189962 100644 --- a/testdata/spillage_06.lisp +++ b/testdata/spillage_06.lisp @@ -1,2 +1,6 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns ST A) -(defconstraint spills () (* ST (* A (~ (shift A -2))))) +(defconstraint spills () + (vanishes! + (* ST (* A (~ (shift A -2)))))) diff --git a/testdata/spillage_07.lisp b/testdata/spillage_07.lisp index 171183d..bd2c2b8 100644 --- a/testdata/spillage_07.lisp +++ b/testdata/spillage_07.lisp @@ -1,7 +1,11 @@ +(defpurefun ((vanishes! :@loob) x) x) + (module m1) (defcolumns S1 A) -(defconstraint spills () (* S1 (* A (~ (shift A -2))))) +(defconstraint spills () + (vanishes! (* S1 (* A (~ (shift A -2)))))) (module m2) (defcolumns S2 B) -(defconstraint spills () (* S2 (* B (~ (shift B 3))))) +(defconstraint spills () + (vanishes! (* S2 (* B (~ (shift B 3)))))) diff --git a/testdata/spillage_08.lisp b/testdata/spillage_08.lisp index b9489a4..0a5b1a4 100644 --- a/testdata/spillage_08.lisp +++ b/testdata/spillage_08.lisp @@ -1,7 +1,11 @@ +(defpurefun ((vanishes! :@loob) x) x) + (module m1) (defcolumns S1 A) -(defconstraint spills () (* S1 (* A (~ (shift A 2))))) +(defconstraint spills () + (vanishes! (* S1 (* A (~ (shift A 2)))))) (module m2) (defcolumns S2 B) -(defconstraint spills () (* S2 (* B (~ (shift B -3))))) +(defconstraint spills () + (vanishes! (* S2 (* B (~ (shift B -3)))))) diff --git a/testdata/spillage_09.lisp b/testdata/spillage_09.lisp index f2bdea3..a35de9a 100644 --- a/testdata/spillage_09.lisp +++ b/testdata/spillage_09.lisp @@ -1,7 +1,11 @@ +(defpurefun ((vanishes! :@loob) x) x) + (module m1) (defcolumns S1 A) -(defconstraint spills () (* S1 (* A (~ (shift A -2))))) +(defconstraint spills () + (vanishes! (* S1 (* A (~ (shift A -2)))))) (module m2) (defcolumns S2 B) -(defconstraint spills () (* S2 (* B (~ (shift B -3))))) +(defconstraint spills () + (vanishes! (* S2 (* B (~ (shift B -3)))))) diff --git a/testdata/type_03.lisp b/testdata/type_03.lisp index 0e0b8bb..f47edbd 100644 --- a/testdata/type_03.lisp +++ b/testdata/type_03.lisp @@ -1,4 +1,7 @@ +(defpurefun ((vanishes! :@loob) x) x) + (defcolumns (X16 :i16@prove) (D8 :i8@prove)) -(defconstraint sorted () (- D8 (- X16 (shift X16 -1)))) +(defconstraint sorted () + (vanishes! (- D8 (- X16 (shift X16 -1))))) diff --git a/testdata/type_05.accepts b/testdata/type_05.accepts new file mode 100644 index 0000000..b879a98 --- /dev/null +++ b/testdata/type_05.accepts @@ -0,0 +1,42 @@ +{ "BIT": [], "X": [] } +;; +{ "BIT": [0], "X": [0] } +{ "BIT": [1], "X": [1] } +{ "BIT": [1], "X": [2] } +{ "BIT": [1], "X": [45] } +{ "BIT": [1], "X": [0] } +;; +{ "BIT": [1,1], "X": [0,0] } +{ "BIT": [1,1], "X": [0,1] } +{ "BIT": [1,1], "X": [0,2] } +{ "BIT": [1,1], "X": [1,0] } +{ "BIT": [1,1], "X": [1,1] } +{ "BIT": [1,1], "X": [1,2] } +{ "BIT": [1,1], "X": [2,0] } +{ "BIT": [1,1], "X": [2,1] } +{ "BIT": [1,1], "X": [2,2] } +{ "BIT": [2,2], "X": [0,0] } +{ "BIT": [2,2], "X": [0,1] } +{ "BIT": [2,2], "X": [0,2] } +{ "BIT": [2,2], "X": [1,0] } +{ "BIT": [2,2], "X": [1,1] } +{ "BIT": [2,2], "X": [1,2] } +{ "BIT": [2,2], "X": [2,0] } +{ "BIT": [2,2], "X": [2,1] } +{ "BIT": [2,2], "X": [2,2] } +;; +{ "BIT": [0,1], "X": [0,0] } +{ "BIT": [0,1], "X": [0,1] } +{ "BIT": [0,1], "X": [0,2] } +{ "BIT": [0,2], "X": [0,0] } +{ "BIT": [0,2], "X": [0,1] } +{ "BIT": [0,2], "X": [0,2] } +;; +{ "BIT": [1,0], "X": [0,0] } +{ "BIT": [1,0], "X": [1,0] } +{ "BIT": [1,0], "X": [2,0] } +{ "BIT": [2,0], "X": [0,0] } +{ "BIT": [2,0], "X": [1,0] } +{ "BIT": [2,0], "X": [2,0] } +;; +{ "BIT": [0,0], "X": [0,0] } diff --git a/testdata/type_05.lisp b/testdata/type_05.lisp new file mode 100644 index 0000000..674c494 --- /dev/null +++ b/testdata/type_05.lisp @@ -0,0 +1,5 @@ +(defcolumns + (BIT :binary@loob) + (X :i8)) + +(defconstraint c1 () (if BIT X)) diff --git a/testdata/type_05.rejects b/testdata/type_05.rejects new file mode 100644 index 0000000..a57f18e --- /dev/null +++ b/testdata/type_05.rejects @@ -0,0 +1,20 @@ +{ "BIT": [0], "X": [1] } +{ "BIT": [0], "X": [2] } +{ "BIT": [0], "X": [3] } +;; +{ "BIT": [0,1], "X": [1,0] } +{ "BIT": [0,1], "X": [1,1] } +{ "BIT": [0,1], "X": [1,2] } +{ "BIT": [0,1], "X": [2,0] } +{ "BIT": [0,1], "X": [2,1] } +{ "BIT": [0,1], "X": [2,2] } +;; +{ "BIT": [1,0], "X": [0,1] } +{ "BIT": [1,0], "X": [0,2] } +{ "BIT": [1,0], "X": [1,1] } +{ "BIT": [1,0], "X": [1,2] } +{ "BIT": [1,0], "X": [2,1] } +{ "BIT": [1,0], "X": [2,2] } +;; +{ "BIT": [0,0], "X": [1,0] } +{ "BIT": [0,0], "X": [2,0] } diff --git a/testdata/type_06.accepts b/testdata/type_06.accepts new file mode 100644 index 0000000..bd69b00 --- /dev/null +++ b/testdata/type_06.accepts @@ -0,0 +1,34 @@ +{ "BIT": [], "X": [] } +;; +{ "BIT": [1], "X": [0] } +{ "BIT": [0], "X": [1] } +{ "BIT": [0], "X": [2] } +{ "BIT": [0], "X": [45] } +{ "BIT": [0], "X": [0] } +;; +{ "BIT": [0,0], "X": [0,0] } +{ "BIT": [0,0], "X": [0,1] } +{ "BIT": [0,0], "X": [0,2] } +{ "BIT": [0,0], "X": [1,0] } +{ "BIT": [0,0], "X": [1,1] } +{ "BIT": [0,0], "X": [1,2] } +{ "BIT": [0,0], "X": [2,0] } +{ "BIT": [0,0], "X": [2,1] } +{ "BIT": [0,0], "X": [2,2] } +;; +{ "BIT": [1,0], "X": [0,0] } +{ "BIT": [1,0], "X": [0,1] } +{ "BIT": [1,0], "X": [0,2] } +{ "BIT": [2,0], "X": [0,0] } +{ "BIT": [2,0], "X": [0,1] } +{ "BIT": [2,0], "X": [0,2] } +;; +{ "BIT": [0,1], "X": [0,0] } +{ "BIT": [0,1], "X": [1,0] } +{ "BIT": [0,1], "X": [2,0] } +{ "BIT": [0,2], "X": [0,0] } +{ "BIT": [0,2], "X": [1,0] } +{ "BIT": [0,2], "X": [2,0] } +;; +{ "BIT": [1,1], "X": [0,0] } +{ "BIT": [2,2], "X": [0,0] } diff --git a/testdata/type_06.lisp b/testdata/type_06.lisp new file mode 100644 index 0000000..41dc8c7 --- /dev/null +++ b/testdata/type_06.lisp @@ -0,0 +1,5 @@ +(defcolumns + (BIT :binary@bool) + (X :i8@loob)) + +(defconstraint c1 () (if BIT X)) diff --git a/testdata/type_06.rejects b/testdata/type_06.rejects new file mode 100644 index 0000000..afaf690 --- /dev/null +++ b/testdata/type_06.rejects @@ -0,0 +1,20 @@ +{ "BIT": [1], "X": [1] } +{ "BIT": [1], "X": [2] } +{ "BIT": [1], "X": [3] } +;; +{ "BIT": [1,0], "X": [1,0] } +{ "BIT": [1,0], "X": [1,1] } +{ "BIT": [1,0], "X": [1,2] } +{ "BIT": [1,0], "X": [2,0] } +{ "BIT": [1,0], "X": [2,1] } +{ "BIT": [1,0], "X": [2,2] } +;; +{ "BIT": [0,1], "X": [0,1] } +{ "BIT": [0,1], "X": [0,2] } +{ "BIT": [0,1], "X": [1,1] } +{ "BIT": [0,1], "X": [1,2] } +{ "BIT": [0,1], "X": [2,1] } +{ "BIT": [0,1], "X": [2,2] } +;; +{ "BIT": [1,1], "X": [1,0] } +{ "BIT": [1,1], "X": [2,0] } diff --git a/testdata/type_07.accepts b/testdata/type_07.accepts new file mode 100644 index 0000000..a9e5f7b --- /dev/null +++ b/testdata/type_07.accepts @@ -0,0 +1,44 @@ +{ "BIT": [], "X": [] } +;; +{ "BIT": [1], "X": [0] } +{ "BIT": [1], "X": [1] } +{ "BIT": [1], "X": [2] } +{ "BIT": [1], "X": [3] } +{ "BIT": [0], "X": [1] } +{ "BIT": [0], "X": [2] } +{ "BIT": [0], "X": [45] } +{ "BIT": [0], "X": [0] } +;; +{ "BIT": [0,0], "X": [0,0] } +{ "BIT": [0,0], "X": [0,1] } +{ "BIT": [0,0], "X": [0,2] } +{ "BIT": [0,0], "X": [1,0] } +{ "BIT": [0,0], "X": [1,1] } +{ "BIT": [0,0], "X": [1,2] } +{ "BIT": [0,0], "X": [2,0] } +{ "BIT": [0,0], "X": [2,1] } +{ "BIT": [0,0], "X": [2,2] } +;; +{ "BIT": [1,0], "X": [0,0] } +{ "BIT": [1,0], "X": [0,1] } +{ "BIT": [1,0], "X": [0,2] } +{ "BIT": [1,0], "X": [1,0] } +{ "BIT": [1,0], "X": [1,1] } +{ "BIT": [1,0], "X": [1,2] } +{ "BIT": [1,0], "X": [2,0] } +{ "BIT": [1,0], "X": [2,1] } +{ "BIT": [1,0], "X": [2,2] } +;; +{ "BIT": [0,1], "X": [0,0] } +{ "BIT": [0,1], "X": [1,0] } +{ "BIT": [0,1], "X": [2,0] } +{ "BIT": [0,1], "X": [0,1] } +{ "BIT": [0,1], "X": [0,2] } +{ "BIT": [0,1], "X": [1,1] } +{ "BIT": [0,1], "X": [1,2] } +{ "BIT": [0,1], "X": [2,1] } +{ "BIT": [0,1], "X": [2,2] } +;; +{ "BIT": [1,1], "X": [1,1] } +{ "BIT": [1,1], "X": [1,0] } +{ "BIT": [1,1], "X": [2,0] } diff --git a/testdata/type_07.lisp b/testdata/type_07.lisp new file mode 100644 index 0000000..dbef0d4 --- /dev/null +++ b/testdata/type_07.lisp @@ -0,0 +1,5 @@ +(defcolumns + (BIT :binary@loob) + (X :i8@loob)) + +(defconstraint c1 () (if (+ 1 BIT) X)) diff --git a/testdata/type_08.accepts b/testdata/type_08.accepts new file mode 100644 index 0000000..51fab06 --- /dev/null +++ b/testdata/type_08.accepts @@ -0,0 +1,27 @@ +{ "BIT": [], "X": [] } +;; +{ "BIT": [1], "X": [0] } +{ "BIT": [0], "X": [1] } +{ "BIT": [0], "X": [2] } +{ "BIT": [0], "X": [45] } +{ "BIT": [0], "X": [0] } +;; +{ "BIT": [0,0], "X": [0,0] } +{ "BIT": [0,0], "X": [0,1] } +{ "BIT": [0,0], "X": [0,2] } +{ "BIT": [0,0], "X": [1,0] } +{ "BIT": [0,0], "X": [1,1] } +{ "BIT": [0,0], "X": [1,2] } +{ "BIT": [0,0], "X": [2,0] } +{ "BIT": [0,0], "X": [2,1] } +{ "BIT": [0,0], "X": [2,2] } +;; +{ "BIT": [1,0], "X": [0,0] } +{ "BIT": [1,0], "X": [0,1] } +{ "BIT": [1,0], "X": [0,2] } +;; +{ "BIT": [0,1], "X": [0,0] } +{ "BIT": [0,1], "X": [1,0] } +{ "BIT": [0,1], "X": [2,0] } +;; +{ "BIT": [1,1], "X": [0,0] } diff --git a/testdata/type_08.lisp b/testdata/type_08.lisp new file mode 100644 index 0000000..fbcef66 --- /dev/null +++ b/testdata/type_08.lisp @@ -0,0 +1,3 @@ +(defcolumns (BIT :i1) (X :i1@loob)) + +(defconstraint c1 (:guard BIT) X) diff --git a/testdata/type_08.rejects b/testdata/type_08.rejects new file mode 100644 index 0000000..afaf690 --- /dev/null +++ b/testdata/type_08.rejects @@ -0,0 +1,20 @@ +{ "BIT": [1], "X": [1] } +{ "BIT": [1], "X": [2] } +{ "BIT": [1], "X": [3] } +;; +{ "BIT": [1,0], "X": [1,0] } +{ "BIT": [1,0], "X": [1,1] } +{ "BIT": [1,0], "X": [1,2] } +{ "BIT": [1,0], "X": [2,0] } +{ "BIT": [1,0], "X": [2,1] } +{ "BIT": [1,0], "X": [2,2] } +;; +{ "BIT": [0,1], "X": [0,1] } +{ "BIT": [0,1], "X": [0,2] } +{ "BIT": [0,1], "X": [1,1] } +{ "BIT": [0,1], "X": [1,2] } +{ "BIT": [0,1], "X": [2,1] } +{ "BIT": [0,1], "X": [2,2] } +;; +{ "BIT": [1,1], "X": [1,0] } +{ "BIT": [1,1], "X": [2,0] } diff --git a/testdata/type_09.accepts b/testdata/type_09.accepts new file mode 100644 index 0000000..aa9e59f --- /dev/null +++ b/testdata/type_09.accepts @@ -0,0 +1,27 @@ +{ "BIT": [], "X": [] } +;; +{ "BIT": [1], "X": [0] } +{ "BIT": [0], "X": [1] } +{ "BIT": [0], "X": [2] } +{ "BIT": [0], "X": [45] } +{ "BIT": [0], "X": [0] } +;; +{ "BIT": [0,0], "X": [0,0] } +{ "BIT": [0,0], "X": [0,1] } +{ "BIT": [0,0], "X": [0,2] } +{ "BIT": [0,0], "X": [1,0] } +{ "BIT": [0,0], "X": [1,1] } +{ "BIT": [0,0], "X": [1,2] } +{ "BIT": [0,0], "X": [2,0] } +{ "BIT": [0,0], "X": [2,1] } +{ "BIT": [0,0], "X": [2,2] } +;; +{ "BIT": [1,0], "X": [0,0] } +{ "BIT": [1,0], "X": [0,1] } +{ "BIT": [1,0], "X": [0,2] } +;; +{ "BIT": [0,1], "X": [0,0] } +{ "BIT": [0,1], "X": [1,0] } +{ "BIT": [0,1], "X": [2,0] } +;; +{ "BIT": [1,1], "X": [1,1] } diff --git a/testdata/type_09.lisp b/testdata/type_09.lisp new file mode 100644 index 0000000..da202f4 --- /dev/null +++ b/testdata/type_09.lisp @@ -0,0 +1,2 @@ +(defcolumns (X :i1@bool@prove) (Y :i4@loob)) +(defconstraint c1 () (if X Y)) diff --git a/testdata/type_09.rejects b/testdata/type_09.rejects new file mode 100644 index 0000000..d2bb84e --- /dev/null +++ b/testdata/type_09.rejects @@ -0,0 +1,29 @@ +{ "BIT": [1], "X": [1] } +{ "BIT": [1], "X": [2] } +{ "BIT": [1], "X": [3] } +;; +{ "BIT": [1,0], "X": [1,0] } +{ "BIT": [1,0], "X": [1,1] } +{ "BIT": [1,0], "X": [1,2] } +{ "BIT": [1,0], "X": [2,0] } +{ "BIT": [1,0], "X": [2,1] } +{ "BIT": [1,0], "X": [2,2] } +{ "BIT": [2,0], "X": [0,0] } +{ "BIT": [2,0], "X": [0,1] } +{ "BIT": [2,0], "X": [0,2] } +;; +{ "BIT": [0,1], "X": [0,1] } +{ "BIT": [0,1], "X": [0,2] } +{ "BIT": [0,1], "X": [1,1] } +{ "BIT": [0,1], "X": [1,2] } +{ "BIT": [0,1], "X": [2,1] } +{ "BIT": [0,1], "X": [2,2] } +{ "BIT": [0,2], "X": [0,0] } +{ "BIT": [0,2], "X": [1,0] } +{ "BIT": [0,2], "X": [2,0] } +;; +{ "BIT": [1,1], "X": [1,0] } +{ "BIT": [1,1], "X": [2,0] } +{ "BIT": [2,1], "X": [0,0] } +{ "BIT": [1,2], "X": [0,0] } +{ "BIT": [2,2], "X": [0,0] } diff --git a/testdata/type_invalid_01.lisp b/testdata/type_invalid_01.lisp new file mode 100644 index 0000000..674c494 --- /dev/null +++ b/testdata/type_invalid_01.lisp @@ -0,0 +1,5 @@ +(defcolumns + (BIT :binary@loob) + (X :i8)) + +(defconstraint c1 () (if BIT X)) diff --git a/testdata/type_invalid_02.lisp b/testdata/type_invalid_02.lisp new file mode 100644 index 0000000..d4ff88a --- /dev/null +++ b/testdata/type_invalid_02.lisp @@ -0,0 +1,5 @@ +(defcolumns + (BIT :binary) + (X :i8@loob)) + +(defconstraint c1 () (if BIT X)) diff --git a/testdata/type_invalid_03.lisp b/testdata/type_invalid_03.lisp new file mode 100644 index 0000000..d062e76 --- /dev/null +++ b/testdata/type_invalid_03.lisp @@ -0,0 +1,5 @@ +(defcolumns + (BIT :i8) + (X :i8@loob)) + +(defconstraint c1 () (if BIT X)) diff --git a/testdata/type_invalid_04.lisp b/testdata/type_invalid_04.lisp new file mode 100644 index 0000000..2336e90 --- /dev/null +++ b/testdata/type_invalid_04.lisp @@ -0,0 +1,5 @@ +(defcolumns + (BIT :binary@loob) + (X :binary@bool)) + +(defconstraint c1 () (if BIT X)) diff --git a/testdata/type_invalid_05.lisp b/testdata/type_invalid_05.lisp new file mode 100644 index 0000000..6b8e0f3 --- /dev/null +++ b/testdata/type_invalid_05.lisp @@ -0,0 +1,5 @@ +(defcolumns + (BIT :binary) + (X :binary@loob)) + +(defconstraint c1 () (if (+ 2 BIT) X)) diff --git a/testdata/type_invalid_06.lisp b/testdata/type_invalid_06.lisp new file mode 100644 index 0000000..8adcd7b --- /dev/null +++ b/testdata/type_invalid_06.lisp @@ -0,0 +1,3 @@ +(defcolumns (BIT :i1@loob) (X :i1@loob)) + +(defconstraint c1 (:guard BIT) X) diff --git a/testdata/type_invalid_07.lisp b/testdata/type_invalid_07.lisp new file mode 100644 index 0000000..92f87b0 --- /dev/null +++ b/testdata/type_invalid_07.lisp @@ -0,0 +1,5 @@ +(defcolumns (X :i1) (Y :i1) (A :i4@loob) (B :i4@loob)) +(definterleaved Z (X Y)) +(definterleaved C (A B)) +;; +(defconstraint c1 () (if Z C)) diff --git a/testdata/type_invalid_08.lisp b/testdata/type_invalid_08.lisp new file mode 100644 index 0000000..a40f373 --- /dev/null +++ b/testdata/type_invalid_08.lisp @@ -0,0 +1,5 @@ +(defcolumns (X :i1@loob) (Y :i1@loob) (A :i4) (B :i4)) +(definterleaved Z (X Y)) +(definterleaved C (A B)) +;; +(defconstraint c1 () (if Z C)) diff --git a/testdata/type_invalid_09.lisp b/testdata/type_invalid_09.lisp new file mode 100644 index 0000000..92f87b0 --- /dev/null +++ b/testdata/type_invalid_09.lisp @@ -0,0 +1,5 @@ +(defcolumns (X :i1) (Y :i1) (A :i4@loob) (B :i4@loob)) +(definterleaved Z (X Y)) +(definterleaved C (A B)) +;; +(defconstraint c1 () (if Z C)) diff --git a/testdata/type_invalid_10.lisp b/testdata/type_invalid_10.lisp new file mode 100644 index 0000000..58d8ccc --- /dev/null +++ b/testdata/type_invalid_10.lisp @@ -0,0 +1,5 @@ +(defcolumns (X :i1@loob) (Y :i1) (A :i4@loob) (B :i4@loob)) +(definterleaved Z (X Y)) +(definterleaved C (A B)) +;; +(defconstraint c1 () (if Z C)) diff --git a/testdata/type_invalid_11.lisp b/testdata/type_invalid_11.lisp new file mode 100644 index 0000000..953303a --- /dev/null +++ b/testdata/type_invalid_11.lisp @@ -0,0 +1,5 @@ +(defcolumns (X :i1) (Y :i1@loob) (A :i4@loob) (B :i4@loob)) +(definterleaved Z (X Y)) +(definterleaved C (A B)) +;; +(defconstraint c1 () (if Z C)) diff --git a/testdata/type_invalid_12.lisp b/testdata/type_invalid_12.lisp new file mode 100644 index 0000000..55f1e71 --- /dev/null +++ b/testdata/type_invalid_12.lisp @@ -0,0 +1,5 @@ +(defcolumns (X :i1@bool) (Y :i1) (A :i4@loob) (B :i4@loob)) +(definterleaved Z (X Y)) +(definterleaved C (A B)) +;; +(defconstraint c1 () (if Z C)) diff --git a/testdata/type_invalid_13.lisp b/testdata/type_invalid_13.lisp new file mode 100644 index 0000000..c4c1228 --- /dev/null +++ b/testdata/type_invalid_13.lisp @@ -0,0 +1,5 @@ +(defcolumns (X :i1) (Y :i1@bool) (A :i4@loob) (B :i4@loob)) +(definterleaved Z (X Y)) +(definterleaved C (A B)) +;; +(defconstraint c1 () (if Z C)) diff --git a/testdata/wcp.lisp b/testdata/wcp.lisp index f6e16e9..e237bba 100644 --- a/testdata/wcp.lisp +++ b/testdata/wcp.lisp @@ -4,7 +4,7 @@ (WORD_COMPARISON_STAMP :i32) (COUNTER :byte) (CT_MAX :byte) - (INST :byte) + (INST :byte :display :opcode) (ARGUMENT_1_HI :i128) (ARGUMENT_1_LO :i128) (ARGUMENT_2_HI :i128) @@ -40,32 +40,208 @@ (BIT_3 :binary@prove) (BIT_4 :binary@prove)) -(defconstraint result () (begin (if (- ONE_LINE_INSTRUCTION 1) (- RESULT (* BIT_1 BIT_2))) (if (- IS_LT 1) (- RESULT (- 1 (* BIT_1 BIT_2) (+ BIT_3 (* BIT_1 BIT_4))))) (if (- IS_GT 1) (- RESULT (+ BIT_3 (* BIT_1 BIT_4)))) (if (- IS_LEQ 1) (- RESULT (+ (- 1 (* BIT_1 BIT_2) (+ BIT_3 (* BIT_1 BIT_4))) (* BIT_1 BIT_2)))) (if (- IS_GEQ 1) (- RESULT (+ (+ BIT_3 (* BIT_1 BIT_4)) (* BIT_1 BIT_2)))) (if (- IS_LT 1) (- RESULT (- 1 (* BIT_1 BIT_2) (+ BIT_3 (* BIT_1 BIT_4))))) (if (- IS_SLT 1) (if (- NEG_1 NEG_2) (- RESULT (- 1 (* BIT_1 BIT_2) (+ BIT_3 (* BIT_1 BIT_4)))) (- RESULT NEG_1))) (if (- IS_SGT 1) (if (- NEG_1 NEG_2) (- RESULT (+ BIT_3 (* BIT_1 BIT_4))) (- RESULT NEG_2))))) - -(defconstraint bits-and-negs () (if (+ IS_SLT IS_SGT) 0 (if (- COUNTER 15) (begin (- (shift BYTE_1 -15) (+ (* 1 (shift BITS -8)) (+ (* 2 (shift BITS -9)) (+ (* 4 (shift BITS -10)) (+ (* 8 (shift BITS -11)) (+ (* 16 (shift BITS -12)) (+ (* 32 (shift BITS -13)) (+ (* 128 (shift BITS -15)) (* 64 (shift BITS -14)))))))))) (- (shift BYTE_3 -15) (+ (* 1 BITS) (+ (* 2 (shift BITS -1)) (+ (* 4 (shift BITS -2)) (+ (* 8 (shift BITS -3)) (+ (* 16 (shift BITS -4)) (+ (* 32 (shift BITS -5)) (+ (* 128 (shift BITS -7)) (* 64 (shift BITS -6)))))))))) (- NEG_1 (shift BITS -15)) (- NEG_2 (shift BITS -7)))))) - -(defconstraint byte_decompositions () (begin (if COUNTER (- ACC_1 BYTE_1) (- ACC_1 (+ (* 256 (shift ACC_1 -1)) BYTE_1))) (if COUNTER (- ACC_2 BYTE_2) (- ACC_2 (+ (* 256 (shift ACC_2 -1)) BYTE_2))) (if COUNTER (- ACC_3 BYTE_3) (- ACC_3 (+ (* 256 (shift ACC_3 -1)) BYTE_3))) (if COUNTER (- ACC_4 BYTE_4) (- ACC_4 (+ (* 256 (shift ACC_4 -1)) BYTE_4))) (if COUNTER (- ACC_5 BYTE_5) (- ACC_5 (+ (* 256 (shift ACC_5 -1)) BYTE_5))) (if COUNTER (- ACC_6 BYTE_6) (- ACC_6 (+ (* 256 (shift ACC_6 -1)) BYTE_6))))) - -(defconstraint target-constraints () (begin (if WORD_COMPARISON_STAMP 0 (begin (if (- ARGUMENT_1_HI ARGUMENT_2_HI) (- BIT_1 1) BIT_1) (if (- ARGUMENT_1_LO ARGUMENT_2_LO) (- BIT_2 1) BIT_2))) (if (- VARIABLE_LENGTH_INSTRUCTION 1) (if (- COUNTER CT_MAX) (begin (- ACC_1 ARGUMENT_1_HI) (- ACC_2 ARGUMENT_1_LO) (- ACC_3 ARGUMENT_2_HI) (- ACC_4 ARGUMENT_2_LO) (- ACC_5 (- (* (- (* 2 BIT_3) 1) (- ARGUMENT_1_HI ARGUMENT_2_HI)) BIT_3)) (- ACC_6 (- (* (- (* 2 BIT_4) 1) (- ARGUMENT_1_LO ARGUMENT_2_LO)) BIT_4))))) (if (- IS_ISZERO 1) (begin ARGUMENT_2_HI ARGUMENT_2_LO)))) - -(defconstraint counter-constancies () (begin (if COUNTER 0 (- ARGUMENT_1_HI (shift ARGUMENT_1_HI -1))) (if COUNTER 0 (- ARGUMENT_1_LO (shift ARGUMENT_1_LO -1))) (if COUNTER 0 (- ARGUMENT_2_HI (shift ARGUMENT_2_HI -1))) (if COUNTER 0 (- ARGUMENT_2_LO (shift ARGUMENT_2_LO -1))) (if COUNTER 0 (- RESULT (shift RESULT -1))) (if COUNTER 0 (- INST (shift INST -1))) (if COUNTER 0 (- CT_MAX (shift CT_MAX -1))) (if COUNTER 0 (- BIT_3 (shift BIT_3 -1))) (if COUNTER 0 (- BIT_4 (shift BIT_4 -1))) (if COUNTER 0 (- NEG_1 (shift NEG_1 -1))) (if COUNTER 0 (- NEG_2 (shift NEG_2 -1))))) - -(defconstraint setting-flag () (begin (- INST (+ (* 16 IS_LT) (* 17 IS_GT) (* 18 IS_SLT) (* 19 IS_SGT) (* 20 IS_EQ) (* 21 IS_ISZERO) (* 15 IS_GEQ) (* 14 IS_LEQ))) (- ONE_LINE_INSTRUCTION (+ IS_EQ IS_ISZERO)) (- VARIABLE_LENGTH_INSTRUCTION (+ IS_LT IS_GT IS_LEQ IS_GEQ IS_SLT IS_SGT)))) - -(defconstraint inst-decoding () (if WORD_COMPARISON_STAMP (+ (+ IS_EQ IS_ISZERO) (+ IS_LT IS_GT IS_LEQ IS_GEQ IS_SLT IS_SGT)) (- (+ (+ IS_EQ IS_ISZERO) (+ IS_LT IS_GT IS_LEQ IS_GEQ IS_SLT IS_SGT)) 1))) - -(defconstraint heartbeat () (if WORD_COMPARISON_STAMP 0 (if (- COUNTER CT_MAX) (- (shift WORD_COMPARISON_STAMP 1) (+ WORD_COMPARISON_STAMP 1)) (- (shift COUNTER 1) (+ COUNTER 1))))) - -(defconstraint stamp-increments () (* (- (shift WORD_COMPARISON_STAMP 1) WORD_COMPARISON_STAMP) (- (shift WORD_COMPARISON_STAMP 1) (+ WORD_COMPARISON_STAMP 1)))) - -(defconstraint ct-upper-bond () (- (~ (- 16 COUNTER)) 1)) - -(defconstraint counter-reset () (if (- (shift WORD_COMPARISON_STAMP 1) WORD_COMPARISON_STAMP) 0 (shift COUNTER 1))) - -(defconstraint setting-ct-max () (if (- ONE_LINE_INSTRUCTION 1) CT_MAX)) - -(defconstraint no-neg-if-small () (if (- CT_MAX 15) 0 (begin NEG_1 NEG_2))) - -(defconstraint lastRow (:domain {-1}) (- COUNTER CT_MAX)) - -(defconstraint first-row (:domain {0}) WORD_COMPARISON_STAMP) +;; aliases +(defalias + STAMP WORD_COMPARISON_STAMP + OLI ONE_LINE_INSTRUCTION + VLI VARIABLE_LENGTH_INSTRUCTION + CT COUNTER + ARG_1_HI ARGUMENT_1_HI + ARG_1_LO ARGUMENT_1_LO + ARG_2_HI ARGUMENT_2_HI + ARG_2_LO ARGUMENT_2_LO + RES RESULT) + +(defpurefun (if-eq-else A B then else) + (if-zero-else (- A B) + then + else)) + +;; opcode values +(defconst + LEQ 0x0E + GEQ 0x0F + LT 16 + GT 17 + SLT 18 + SGT 19 + EQ_ 20 + ISZERO 21 + LLARGE 16 + LLARGEMO 15) + + +(defun (one-line-inst) + (+ IS_EQ IS_ISZERO)) + +(defun (variable-length-inst) + (+ IS_LT IS_GT IS_LEQ IS_GEQ IS_SLT IS_SGT)) + +(defun (flag-sum) + (+ (one-line-inst) (variable-length-inst))) + +(defun (weight-sum) + (+ (* LT IS_LT) + (* GT IS_GT) + (* SLT IS_SLT) + (* SGT IS_SGT) + (* EQ_ IS_EQ) + (* ISZERO IS_ISZERO) + (* GEQ IS_GEQ) + (* LEQ IS_LEQ))) + +(defconstraint inst-decoding () + (if-zero-else STAMP + (vanishes! (flag-sum)) + (eq! (flag-sum) 1))) + +(defconstraint setting-flag () + (begin (eq! INST (weight-sum)) + (eq! OLI (one-line-inst)) + (eq! VLI (variable-length-inst)))) + +(defconstraint counter-constancies () + (begin (counter-constancy CT ARG_1_HI) + (counter-constancy CT ARG_1_LO) + (counter-constancy CT ARG_2_HI) + (counter-constancy CT ARG_2_LO) + (counter-constancy CT RES) + (counter-constancy CT INST) + (counter-constancy CT CT_MAX) + (counter-constancy CT BIT_3) + (counter-constancy CT BIT_4) + (counter-constancy CT NEG_1) + (counter-constancy CT NEG_2))) + +(defconstraint first-row (:domain {0}) + (vanishes! STAMP)) + +(defconstraint stamp-increments () + (* (will-remain-constant! STAMP) (will-inc! STAMP 1))) + +(defconstraint counter-reset () + (if-not-zero (will-remain-constant! STAMP) + (vanishes! (next CT)))) + +(defconstraint setting-ct-max () + (if-eq OLI 1 (vanishes! CT_MAX))) + +(defconstraint heartbeat (:guard STAMP) + (if-eq-else CT CT_MAX (will-inc! STAMP 1) (will-inc! CT 1))) + +(defconstraint ct-upper-bond () + (eq! (~ (- LLARGE CT)) + 1)) + +(defconstraint lastRow (:domain {-1}) + (eq! CT CT_MAX)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.6 byte decompositions ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; byte decompositions +(defconstraint byte_decompositions () + (begin (byte-decomposition CT ACC_1 BYTE_1) + (byte-decomposition CT ACC_2 BYTE_2) + (byte-decomposition CT ACC_3 BYTE_3) + (byte-decomposition CT ACC_4 BYTE_4) + (byte-decomposition CT ACC_5 BYTE_5) + (byte-decomposition CT ACC_6 BYTE_6))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.7 BITS and sign bit constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; (defun (first-eight-bits-bit-dec) +;; (reduce + +;; (for i +;; [0 :7] +;; (* (^ 2 i) +;; (shift BITS +;; (- 0 (+ i 8))))))) + +;; (defun (last-eight-bits-bit-dec) +;; (reduce + +;; (for i +;; [0 :7] +;; (* (^ 2 i) +;; (shift BITS (- 0 i)))))) + +;; (defconstraint bits-and-negs (:guard (+ IS_SLT IS_SGT)) +;; (if-eq CT LLARGEMO +;; (begin (eq! (shift BYTE_1 (- 0 LLARGEMO)) +;; (first-eight-bits-bit-dec)) +;; (eq! (shift BYTE_3 (- 0 LLARGEMO)) +;; (last-eight-bits-bit-dec)) +;; (eq! NEG_1 +;; (shift BITS (- 0 LLARGEMO))) +;; (eq! NEG_2 +;; (shift BITS (- 0 7)))))) + +(defconstraint no-neg-if-small () + (if-not-zero (- CT_MAX LLARGEMO) + (begin (vanishes! NEG_1) + (vanishes! NEG_2)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.6 target constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defconstraint target-constraints () + (begin (if-not-zero STAMP + (begin (if-eq-else ARG_1_HI ARG_2_HI (eq! BIT_1 1) (vanishes! BIT_1)) + (if-eq-else ARG_1_LO ARG_2_LO (eq! BIT_2 1) (vanishes! BIT_2)))) + (if-eq VLI 1 + (if-eq CT CT_MAX + (begin (eq! ACC_1 ARG_1_HI) + (eq! ACC_2 ARG_1_LO) + (eq! ACC_3 ARG_2_HI) + (eq! ACC_4 ARG_2_LO) + (eq! ACC_5 + (- (* (- (* 2 BIT_3) 1) + (- ARG_1_HI ARG_2_HI)) + BIT_3)) + (eq! ACC_6 + (- (* (- (* 2 BIT_4) 1) + (- ARG_1_LO ARG_2_LO)) + BIT_4))))) + (if-eq IS_ISZERO 1 + (begin (vanishes! ARG_2_HI) + (vanishes! ARG_2_LO))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; 2.7 result constraints ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; eq_ = [[1]] . [[2]] +;; gt_ = [[3]] + [[1]] . [[4]] +;; lt_ = 1 - eq - gt +(defun (eq_) + (* BIT_1 BIT_2)) + +(defun (gt_) + (+ BIT_3 (* BIT_1 BIT_4))) + +(defun (lt_) + (- 1 (eq_) (gt_))) + +;; 2.7.2 +(defconstraint result () + (begin (if-eq OLI 1 (eq! RES (eq_))) + (if-eq IS_LT 1 (eq! RES (lt_))) + (if-eq IS_GT 1 (eq! RES (gt_))) + (if-eq IS_LEQ 1 + (eq! RES (+ (lt_) (eq_)))) + (if-eq IS_GEQ 1 + (eq! RES (+ (gt_) (eq_)))) + (if-eq IS_LT 1 (eq! RES (lt_))) + (if-eq IS_SLT 1 + (if-eq-else NEG_1 NEG_2 (eq! RES (lt_)) (eq! RES NEG_1))) + (if-eq IS_SGT 1 + (if-eq-else NEG_1 NEG_2 (eq! RES (gt_)) (eq! RES NEG_2))))) diff --git a/testdata/word_sorting.lisp b/testdata/word_sorting.lisp index 81ec278..920f138 100644 --- a/testdata/word_sorting.lisp +++ b/testdata/word_sorting.lisp @@ -9,7 +9,7 @@ (defcolumns (Byte_0 :i8@prove) (Byte_1 :i8@prove)) ;; Ensure Delta is a u16 -(defconstraint delta_type () (- Delta (+ (* 256 Byte_1) Byte_0))) +(defconstraint delta_type () (eq! Delta (+ (* 256 Byte_1) Byte_0))) ;; Delta == X - X[i-1] -(defconstraint sort () (- Delta (- X (shift X -1)))) +(defconstraint sort () (eq! Delta (- X (shift X -1))))