Skip to content

Commit

Permalink
Merge pull request #362 from Consensys/347-improved-modelling-mechanism
Browse files Browse the repository at this point in the history 
feat: support functional models
  • Loading branch information
@DavePearce
DavePearce authored Oct 23, 2024
2 parents aa02631 + 7c88219 commit 056df5b
Show file tree
Hide file tree
Showing 6 changed files with 4,470 additions and 9 deletions.
91 changes: 89 additions & 2 deletions cmd/testgen/main.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,8 @@ func main() {
}

func init() {
rootCmd.Flags().Uint("min-elem", 0, "Minimum element")
rootCmd.Flags().Uint("max-elem", 2, "Maximum element")
rootCmd.Flags().Uint("min-lines", 1, "Minimum number of lines")
rootCmd.Flags().Uint("max-lines", 4, "Maximum number of lines")
rootCmd.Flags().BoolP("toggle", "t", false, "Help message for toggle")
Expand All @@ -41,6 +43,8 @@ var rootCmd = &cobra.Command{
var cfg TestGenConfig
// Lookup model
cfg.model = findModel(args[0])
cfg.min_elem = util.GetUint(cmd, "min-elem")
cfg.max_elem = util.GetUint(cmd, "max-elem")
cfg.min_lines = util.GetUint(cmd, "min-lines")
cfg.max_lines = util.GetUint(cmd, "max-lines")
// Read schema
Expand All @@ -59,23 +63,29 @@ var rootCmd = &cobra.Command{
// TestGenConfig encapsulates configuration related to test generation.
type TestGenConfig struct {
model Model
min_elem uint
max_elem uint
min_lines uint
max_lines uint
}

// OracleFn defines function which determines whether or not a given trace is accepted by the model (or not).
type OracleFn = func(sc.Schema, tr.Trace) bool

// Model represents a hard-coded oracle for a given test.
type Model struct {
// Name of the model in question
Name string
// Predicate for determining which trace to accept
Oracle func(sc.Schema, tr.Trace) bool
Oracle OracleFn
}

var models []Model = []Model{
{"bit_decomposition", bitDecompositionModel},
{"byte_decomposition", byteDecompositionModel},
{"memory", memoryModel},
{"word_sorting", wordSortingModel},
{"counter", functionalModel("STAMP", counterModel)},
}

func findModel(name string) Model {
Expand All @@ -93,7 +103,7 @@ func generateTestTraces(cfg TestGenConfig, schema sc.Schema) ([]tr.Trace, []tr.T
// NOTE: This is really a temporary solution for now. It doesn't handle
// length multipliers. It doesn't allow for modules with different heights.
// It uses a fixed pool.
pool := []fr.Element{fr.NewElement(0), fr.NewElement(1), fr.NewElement(2)}
pool := generatePool(cfg)
valid := make([]tr.Trace, 0)
invalid := make([]tr.Trace, 0)
//
Expand All @@ -114,6 +124,18 @@ func generateTestTraces(cfg TestGenConfig, schema sc.Schema) ([]tr.Trace, []tr.T
return valid, invalid
}

func generatePool(cfg TestGenConfig) []fr.Element {
n := cfg.max_elem - cfg.min_elem + 1
elems := make([]fr.Element, n)
// Iterate values
for i := uint(0); i != n; i++ {
val := uint64(cfg.min_elem + i)
elems[i] = fr.NewElement(val)
}
// Done
return elems
}

func writeTestTraces(model Model, ext string, schema sc.Schema, traces []tr.Trace) {
var sb strings.Builder
// Construct filename
Expand Down Expand Up @@ -185,6 +207,48 @@ func findColumn(mod uint, col string, schema sc.Schema, trace tr.Trace) tr.Colum
return trace.Column(cid)
}

func functionalModel(stamp string, model func(uint, uint, sc.Schema, tr.Trace) bool) OracleFn {
return func(schema sc.Schema, trace tr.Trace) bool {
// Lookup stamp column
STAMP := findColumn(0, stamp, schema, trace).Data()
// Check STAMP initially zero
if STAMP.Len() > 0 {
STAMP_0 := STAMP.Get(0)
if !STAMP_0.IsZero() {
return false
}
}
// Set initial frame
start := uint(0)
current := fr.NewElement(0)
i := uint(1)
// Split frames
for ; i < STAMP.Len(); i++ {
stamp_i := STAMP.Get(i)
// Look for frame boundary
if stamp_i.Cmp(&current) != 0 {
// Check stamp incremented
if !isIncremented(current, stamp_i) {
return false
}
// Check whether valid frame (or padding)
if !current.IsZero() && !model(start, i-1, schema, trace) {
return false
}
// Reset for next frame
start = i
current = stamp_i
}
}
// Handle final frame
if !current.IsZero() && !model(start, i-1, schema, trace) {
return false
}
//
return true
}
}

// ============================================================================
// Models
// ============================================================================
Expand Down Expand Up @@ -364,6 +428,29 @@ func wordSortingModel(schema sc.Schema, trace tr.Trace) bool {
return true
}

// ============================================================================
// Functional Models
// ============================================================================

func counterModel(first uint, last uint, schema sc.Schema, trace tr.Trace) bool {
CT := findColumn(0, "CT", schema, trace).Data()
// All frames in this model must have length 4
if last-first != 3 {
return false
}
//
for i := first; i <= last; i++ {
ct_i := CT.Get(i)
expected := fr.NewElement(uint64(i - first))
// Check counter matches expected valid
if ct_i.Cmp(&expected) != 0 {
return false
}
}
//
return true
}

// ============================================================================
// Helpers
// ============================================================================
Expand Down
11 changes: 4 additions & 7 deletions testdata/counter.accepts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,9 @@
{ "STAMP": [0,0], "CT": [0,1] }
{ "STAMP": [0,0,0], "CT": [0,1,2] }
{ "STAMP": [0,0,0,0], "CT": [0,1,2,3] }
{ "STAMP": [0,0,0,0,1], "CT": [0,1,2,3,0] }
{ "STAMP": [0,0,0,0,1,1,1,1], "CT": [0,1,2,3,0,1,2,3] }
{ "STAMP": [0,1], "CT": [0,0] }
{ "STAMP": [0,1,1], "CT": [0,0,1] }
{ "STAMP": [0,1,1,1], "CT": [0,0,1,2] }
{ "STAMP": [0,0,0,0,0,0], "CT": [0,4,5,6,7,8] }
{ "STAMP": [0,1,1,1,1], "CT": [0,0,1,2,3] }
{ "STAMP": [0,1,1,1,1,2], "CT": [0,0,1,2,3,0] }
{ "STAMP": [0,0,0,0,1,1,1,1], "CT": [0,1,2,3,0,1,2,3] }
{ "STAMP": [0,1,1,1,1,2,2,2,2], "CT": [0,0,1,2,3,0,1,2,3] }
{ "STAMP": [0,0,0,0,0,0], "CT": [0,4,5,6,7,8] }
{ "STAMP": [0,0,1,1,1,1,2,2,2,2], "CT": [0,1,0,1,2,3,0,1,2,3] }
{ "STAMP": [0,0,1,1,1,1,2,2,2,2,3,3,3,3], "CT": [0,1,0,1,2,3,0,1,2,3,0,1,2,3] }
84 changes: 84 additions & 0 deletions testdata/counter.auto.accepts
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
{"STAMP": [0, 0], "CT": [0, 0]}
{"STAMP": [0, 0], "CT": [0, 1]}
{"STAMP": [0, 0], "CT": [0, 2]}
{"STAMP": [0, 0], "CT": [0, 3]}
{"STAMP": [0, 0, 0], "CT": [0, 0, 0]}
{"STAMP": [0, 0, 0], "CT": [0, 1, 0]}
{"STAMP": [0, 0, 0], "CT": [0, 2, 0]}
{"STAMP": [0, 0, 0], "CT": [0, 3, 0]}
{"STAMP": [0, 0, 0], "CT": [0, 0, 1]}
{"STAMP": [0, 0, 0], "CT": [0, 1, 1]}
{"STAMP": [0, 0, 0], "CT": [0, 2, 1]}
{"STAMP": [0, 0, 0], "CT": [0, 3, 1]}
{"STAMP": [0, 0, 0], "CT": [0, 0, 2]}
{"STAMP": [0, 0, 0], "CT": [0, 1, 2]}
{"STAMP": [0, 0, 0], "CT": [0, 2, 2]}
{"STAMP": [0, 0, 0], "CT": [0, 3, 2]}
{"STAMP": [0, 0, 0], "CT": [0, 0, 3]}
{"STAMP": [0, 0, 0], "CT": [0, 1, 3]}
{"STAMP": [0, 0, 0], "CT": [0, 2, 3]}
{"STAMP": [0, 0, 0], "CT": [0, 3, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 0, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 0, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 0, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 0, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 1, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 1, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 1, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 1, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 2, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 2, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 2, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 2, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 3, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 3, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 3, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 3, 0]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 0, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 0, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 0, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 0, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 1, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 1, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 1, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 1, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 2, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 2, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 2, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 2, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 3, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 3, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 3, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 3, 1]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 0, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 0, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 0, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 0, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 1, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 1, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 1, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 1, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 2, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 2, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 2, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 2, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 3, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 3, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 3, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 3, 2]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 0, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 0, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 0, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 0, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 1, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 1, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 1, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 1, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 2, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 2, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 2, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 2, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 0, 3, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 1, 3, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 2, 3, 3]}
{"STAMP": [0, 0, 0, 0], "CT": [0, 3, 3, 3]}
Loading

0 comments on commit 056df5b

Please sign in to comment.