Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: initial support for corset syntax #382

Merged
merged 29 commits into from
Nov 24, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
5346400
Splitting out Corset syntax from HIR
DavePearce Nov 6, 2024
c59ed15
Slowly trying to put things back together
DavePearce Nov 6, 2024
0809006
New compiler framework taking shape
DavePearce Nov 7, 2024
51d60d9
Getting very bogged down
DavePearce Nov 7, 2024
050c47a
Code compiling again
DavePearce Nov 7, 2024
a8fd3b8
Flesh out parser
DavePearce Nov 8, 2024
275ea9e
Add missing file
DavePearce Nov 8, 2024
92b8fc0
Improve report of syntax errors
DavePearce Nov 12, 2024
77a85ee
Beginning resolution
DavePearce Nov 12, 2024
53bbc92
Syntax errors beginning to work.
DavePearce Nov 14, 2024
ea193cf
Columns & Constraints being parsed
DavePearce Nov 14, 2024
3d7617e
Making progress on resolution.
DavePearce Nov 15, 2024
e3d9e1d
Resolution of variables almost working
DavePearce Nov 15, 2024
935c9d8
Resolution of column names operational
DavePearce Nov 15, 2024
407f191
Apply guards
DavePearce Nov 15, 2024
e38693f
Vanishing constraints now working
DavePearce Nov 17, 2024
bc5be6b
Support range constraints
DavePearce Nov 17, 2024
661cb6a
Working on lookup constraints.
DavePearce Nov 18, 2024
564c31c
Working on `ContextOfExpressions`
DavePearce Nov 18, 2024
860f3dd
Working on resolving columns
DavePearce Nov 19, 2024
6f821f4
Working on resolver.
DavePearce Nov 19, 2024
f06e1a9
Still working on assignment resolution.
DavePearce Nov 19, 2024
2a6e604
Interleaving constraints operational
DavePearce Nov 21, 2024
8df6cd2
Assignment resolution is operational
DavePearce Nov 21, 2024
b5b7d78
Support column types
DavePearce Nov 22, 2024
0b72956
Support sorted permutations
DavePearce Nov 22, 2024
1412412
Fix `add.lisp`
DavePearce Nov 24, 2024
71a18a3
Fix `mxp` test
DavePearce Nov 24, 2024
309e3e1
Minor
DavePearce Nov 24, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions .golangci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -54,8 +54,6 @@ linters-settings:
severity: warning
confidence: 0.8
rules:
- name: indent-error-flow
severity: warning
- name: errorf
severity: warning
- name: context-as-argument
Expand Down
6 changes: 5 additions & 1 deletion cmd/testgen/main.go
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,10 @@ import (

"github.com/consensys/gnark-crypto/ecc/bls12-377/fr"
cmdutil "github.com/consensys/go-corset/pkg/cmd"
"github.com/consensys/go-corset/pkg/corset"
"github.com/consensys/go-corset/pkg/hir"
sc "github.com/consensys/go-corset/pkg/schema"
"github.com/consensys/go-corset/pkg/sexp"
tr "github.com/consensys/go-corset/pkg/trace"
"github.com/consensys/go-corset/pkg/trace/json"
"github.com/consensys/go-corset/pkg/util"
Expand Down Expand Up @@ -185,8 +187,10 @@ func readSchemaFile(filename string) *hir.Schema {
fmt.Println(err)
os.Exit(1)
}
// Package up as source file
srcfile := sexp.NewSourceFile(filename, bytes)
// Attempt to parse schema
schema, err2 := hir.ParseSchemaString(string(bytes))
schema, err2 := corset.CompileSourceFile(srcfile)
// Check whether parsed successfully or not
if err2 == nil {
// Ok
Expand Down
2 changes: 2 additions & 0 deletions pkg/binfile/computation.go
Original file line number Diff line number Diff line change
Expand Up @@ -102,6 +102,8 @@ func addInterleavedComputation(c *jsonInterleavedComputation, index uint,
// Update the column type
dst_type = sc.Join(dst_type, src_col.Type())
}
// Update multiplier
ctx = ctx.Multiply(uint(len(sources)))
// Finally, add the sorted permutation assignment
schema.AddAssignment(assignment.NewInterleaving(ctx, dst_hnd.column, sources, dst_type))
// Update allocation information.
Expand Down
4 changes: 2 additions & 2 deletions pkg/cmd/check.go
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ var checkCmd = &cobra.Command{
//
stats := util.NewPerfStats()
// Parse constraints
hirSchema = readSchemaFile(args[1])
hirSchema = readSchema(args[1:])
//
stats.Log("Reading constraints file")
// Parse trace file
Expand Down Expand Up @@ -136,7 +136,7 @@ func checkTrace(ir string, cols []tr.RawColumn, schema sc.Schema, cfg checkConfi
for n := cfg.padding.Left; n <= cfg.padding.Right; n++ {
stats := util.NewPerfStats()
trace, errs := builder.Padding(n).Build(cols)

// Log cost of expansion
stats.Log("Expanding trace columns")
// Report any errors
reportErrors(cfg.strict, ir, errs)
Expand Down
3 changes: 1 addition & 2 deletions pkg/cmd/debug.go
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,7 @@ var debugCmd = &cobra.Command{
air := GetFlag(cmd, "air")
stats := GetFlag(cmd, "stats")
// Parse constraints
hirSchema := readSchemaFile(args[0])

hirSchema := readSchema(args)
// Print constraints
if stats {
printStats(hirSchema, hir, mir, air)
Expand Down
2 changes: 1 addition & 1 deletion pkg/cmd/test.go
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ var testCmd = &cobra.Command{
//
stats := util.NewPerfStats()
// Parse constraints
hirSchema = readSchemaFile(args[0])
hirSchema = readSchema(args)
//
stats.Log("Reading constraints file")
//
Expand Down
89 changes: 56 additions & 33 deletions pkg/cmd/util.go
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ import (
"strings"

"github.com/consensys/go-corset/pkg/binfile"
"github.com/consensys/go-corset/pkg/corset"
"github.com/consensys/go-corset/pkg/hir"
"github.com/consensys/go-corset/pkg/sexp"
"github.com/consensys/go-corset/pkg/trace"
Expand Down Expand Up @@ -133,54 +134,76 @@ func readTraceFile(filename string) []trace.RawColumn {
return nil
}

// Parse a constraints schema file using a parser based on the extension of the
// filename.
func readSchemaFile(filename string) *hir.Schema {
func readSchema(filenames []string) *hir.Schema {
if len(filenames) == 0 {
fmt.Println("source or binary constraint(s) file required.")
os.Exit(5)
} else if len(filenames) == 1 && path.Ext(filenames[0]) == "bin" {
// Single (binary) file supplied
return readBinaryFile(filenames[0])
}
// Must be source files
return readSourceFiles(filenames)
}

// Read a "bin" file.
func readBinaryFile(filename string) *hir.Schema {
var schema *hir.Schema
// Read schema file
bytes, err := os.ReadFile(filename)
// Handle errors
if err == nil {
// Check file extension
ext := path.Ext(filename)
//
switch ext {
case ".lisp":
// Parse bytes into an S-Expression
schema, err = hir.ParseSchemaString(string(bytes))
if err == nil {
return schema
}
case ".bin":
schema, err = binfile.HirSchemaFromJson(bytes)
if err == nil {
return schema
}
default:
err = fmt.Errorf("Unknown schema file format: %s\n", ext)
// Read the binary file
schema, err = binfile.HirSchemaFromJson(bytes)
if err == nil {
return schema
}
}
// Handle error
if e, ok := err.(*sexp.SyntaxError); ok {
printSyntaxError(filename, e, string(bytes))
} else {
fmt.Println(err)
}

// Handle error & exit
fmt.Println(err)
os.Exit(2)
// unreachable
return nil
}

// 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 {
srcfiles := make([]*sexp.SourceFile, len(filenames))
// Read each file
for i, n := range filenames {
// Read source file
bytes, err := os.ReadFile(n)
// Sanity check for errors
if err != nil {
fmt.Println(err)
os.Exit(3)
}
//
srcfiles[i] = sexp.NewSourceFile(n, bytes)
}
// Parse and compile source files
schema, errs := corset.CompileSourceFiles(srcfiles)
// Check for any errors
if len(errs) == 0 {
return schema
}
// Report errors
for _, err := range errs {
printSyntaxError(&err)
}
// Fail
os.Exit(4)
// unreachable
return nil
}

// Print a syntax error with appropriate highlighting.
func printSyntaxError(filename string, err *sexp.SyntaxError, text string) {
func printSyntaxError(err *sexp.SyntaxError) {
span := err.Span()
// Construct empty source map in order to determine enclosing line.
srcmap := sexp.NewSourceMap[sexp.SExp]([]rune(text))
//
line := srcmap.FindFirstEnclosingLine(span)
line := err.FirstEnclosingLine()
// Print error + line number
fmt.Printf("%s:%d: %s\n", filename, line.Number(), err.Message())
fmt.Printf("%s:%d: %s\n", err.SourceFile().Filename(), line.Number(), err.Message())
// Print separator line
fmt.Println()
// Print line
Expand Down
Loading