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))))