Skip to content

Commit

Permalink
Add model for byte decomposition
Browse files Browse the repository at this point in the history 
This model is covers byte decompositions.  However, its not super
satisfiying because the model itself is confusing and difficult to
follow.  It feels like a better way of modelling the function being
computed would be helpful.
  • Loading branch information
@DavePearce
DavePearce committed Oct 22, 2024
1 parent 9d3085e commit dd86203
Show file tree
Hide file tree
Showing 4 changed files with 6,753 additions and 42 deletions.
142 changes: 100 additions & 42 deletions cmd/testgen/main.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,7 @@ type Model struct {

var models []Model = []Model{
{"bit_decomposition", bitDecompositionModel},
{"byte_decomposition", byteDecompositionModel},
{"memory", memoryModel},
{"word_sorting", wordSortingModel},
}
Expand Down Expand Up @@ -187,6 +188,96 @@ func findColumn(mod uint, col string, schema sc.Schema, trace tr.Trace) tr.Colum
// ============================================================================
// Models
// ============================================================================
func bitDecompositionModel(schema sc.Schema, trace tr.Trace) bool {
TWO_1 := fr.NewElement(2)
TWO_2 := fr.NewElement(4)
TWO_3 := fr.NewElement(8)
TWO_4 := fr.NewElement(16)
//
NIBBLE := findColumn(0, "NIBBLE", schema, trace).Data()
BIT_0 := findColumn(0, "BIT_0", schema, trace).Data()
BIT_1 := findColumn(0, "BIT_1", schema, trace).Data()
BIT_2 := findColumn(0, "BIT_2", schema, trace).Data()
BIT_3 := findColumn(0, "BIT_3", schema, trace).Data()
//
for i := uint(0); i < NIBBLE.Len(); i++ {
NIBBLE_i := NIBBLE.Get(i)
BIT_0_i := BIT_0.Get(i)
BIT_1_i := BIT_1.Get(i)
BIT_2_i := BIT_2.Get(i)
BIT_3_i := BIT_3.Get(i)
// Check types
t_NIBBLE := NIBBLE_i.Cmp(&TWO_4) < 0
t_BIT_0 := BIT_0_i.Cmp(&TWO_1) < 0
t_BIT_1 := BIT_1_i.Cmp(&TWO_1) < 0
t_BIT_2 := BIT_2_i.Cmp(&TWO_1) < 0
t_BIT_3 := BIT_3_i.Cmp(&TWO_1) < 0
// Check type constraints
if !(t_NIBBLE && t_BIT_0 && t_BIT_1 && t_BIT_2 && t_BIT_3) {
return false
}
//
b1 := mul(BIT_1_i, TWO_1)
b2 := mul(BIT_2_i, TWO_2)
b3 := mul(BIT_3_i, TWO_3)
sum := add(add(add(b3, b2), b1), BIT_0_i)
// Check decomposition matches
if NIBBLE_i.Cmp(&sum) != 0 {
return false
}
}
// Success
return true
}

func byteDecompositionModel(schema sc.Schema, trace tr.Trace) bool {
TWO_8 := fr.NewElement(256)
//
ST := findColumn(0, "ST", schema, trace).Data()
CT := findColumn(0, "CT", schema, trace).Data()
BYTE := findColumn(0, "BYTE", schema, trace).Data()
ARG := findColumn(0, "ARG", schema, trace).Data()
//
padding := true
//
for i := uint(0); i < ST.Len(); i++ {
st_i := ST.Get(i)
ct_i := CT.Get(i)
byte_i := BYTE.Get(i)
arg_i := ARG.Get(i)
// Type constraints
t_byte := byte_i.Cmp(&TWO_8) < 0
// Check type constraints
if !t_byte {
return false
}
//
if padding && st_i.IsZero() {

} else if padding && !st_i.IsZero() {
padding = false
} else if st_i.IsZero() {
return false
}
//
if i+1 < ST.Len() {
st_ip1 := ST.Get(i + 1)
if !(eq(st_i, st_ip1) || eq(add_const(st_i, 1), st_ip1)) {
return false
}
}
// Check other constraints
if ct_i.IsZero() && !eq(arg_i, byte_i) {
return false
} else if !ct_i.IsZero() && !eq(arg_i, add(byte_i, mul(TWO_8, BYTE.Get(i-1)))) {
return false
} else if !padding && i+1 < ST.Len() && !eq(add_const(ct_i, 1), CT.Get(i+1)) {
return false
}
}
// Success
return true
}

func memoryModel(schema sc.Schema, trace tr.Trace) bool {
TWO_1 := fr.NewElement(2)
Expand Down Expand Up @@ -273,48 +364,6 @@ func wordSortingModel(schema sc.Schema, trace tr.Trace) bool {
return true
}

func bitDecompositionModel(schema sc.Schema, trace tr.Trace) bool {
TWO_1 := fr.NewElement(2)
TWO_2 := fr.NewElement(4)
TWO_3 := fr.NewElement(8)
TWO_4 := fr.NewElement(16)
//
NIBBLE := findColumn(0, "NIBBLE", schema, trace).Data()
BIT_0 := findColumn(0, "BIT_0", schema, trace).Data()
BIT_1 := findColumn(0, "BIT_1", schema, trace).Data()
BIT_2 := findColumn(0, "BIT_2", schema, trace).Data()
BIT_3 := findColumn(0, "BIT_3", schema, trace).Data()
//
for i := uint(0); i < NIBBLE.Len(); i++ {
NIBBLE_i := NIBBLE.Get(i)
BIT_0_i := BIT_0.Get(i)
BIT_1_i := BIT_1.Get(i)
BIT_2_i := BIT_2.Get(i)
BIT_3_i := BIT_3.Get(i)
// Check types
t_NIBBLE := NIBBLE_i.Cmp(&TWO_4) < 0
t_BIT_0 := BIT_0_i.Cmp(&TWO_1) < 0
t_BIT_1 := BIT_1_i.Cmp(&TWO_1) < 0
t_BIT_2 := BIT_2_i.Cmp(&TWO_1) < 0
t_BIT_3 := BIT_3_i.Cmp(&TWO_1) < 0
// Check type constraints
if !(t_NIBBLE && t_BIT_0 && t_BIT_1 && t_BIT_2 && t_BIT_3) {
return false
}
//
b1 := mul(BIT_1_i, TWO_1)
b2 := mul(BIT_2_i, TWO_2)
b3 := mul(BIT_3_i, TWO_3)
sum := add(add(add(b3, b2), b1), BIT_0_i)
// Check decomposition matches
if NIBBLE_i.Cmp(&sum) != 0 {
return false
}
}
// Success
return true
}

// ============================================================================
// Helpers
// ============================================================================
Expand All @@ -331,6 +380,10 @@ func add(lhs fr.Element, rhs fr.Element) fr.Element {
return lhs
}

func add_const(lhs fr.Element, rhs uint64) fr.Element {
return add(lhs, fr.NewElement(rhs))
}

func sub(lhs fr.Element, rhs fr.Element) fr.Element {
lhs.Sub(&lhs, &rhs)
return lhs
Expand All @@ -340,3 +393,8 @@ func mul(lhs fr.Element, rhs fr.Element) fr.Element {
lhs.Mul(&lhs, &rhs)
return lhs
}

func eq(lhs fr.Element, rhs fr.Element) bool {
d := sub(lhs, rhs)
return d.IsZero()
}
120 changes: 120 additions & 0 deletions testdata/byte_decomposition.auto.accepts
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,120 @@
{"ST": [0, 0], "CT": [0, 0], "BYTE": [0, 0], "ARG": [0, 0]}
{"ST": [0, 1], "CT": [0, 0], "BYTE": [0, 0], "ARG": [0, 0]}
{"ST": [0, 0], "CT": [0, 1], "BYTE": [0, 0], "ARG": [0, 0]}
{"ST": [0, 1], "CT": [0, 1], "BYTE": [0, 0], "ARG": [0, 0]}
{"ST": [0, 0], "CT": [0, 2], "BYTE": [0, 0], "ARG": [0, 0]}
{"ST": [0, 1], "CT": [0, 2], "BYTE": [0, 0], "ARG": [0, 0]}
{"ST": [0, 0], "CT": [0, 0], "BYTE": [0, 1], "ARG": [0, 1]}
{"ST": [0, 1], "CT": [0, 0], "BYTE": [0, 1], "ARG": [0, 1]}
{"ST": [0, 0], "CT": [0, 1], "BYTE": [0, 1], "ARG": [0, 1]}
{"ST": [0, 1], "CT": [0, 1], "BYTE": [0, 1], "ARG": [0, 1]}
{"ST": [0, 0], "CT": [0, 2], "BYTE": [0, 1], "ARG": [0, 1]}
{"ST": [0, 1], "CT": [0, 2], "BYTE": [0, 1], "ARG": [0, 1]}
{"ST": [0, 0], "CT": [0, 0], "BYTE": [0, 2], "ARG": [0, 2]}
{"ST": [0, 1], "CT": [0, 0], "BYTE": [0, 2], "ARG": [0, 2]}
{"ST": [0, 0], "CT": [0, 1], "BYTE": [0, 2], "ARG": [0, 2]}
{"ST": [0, 1], "CT": [0, 1], "BYTE": [0, 2], "ARG": [0, 2]}
{"ST": [0, 0], "CT": [0, 2], "BYTE": [0, 2], "ARG": [0, 2]}
{"ST": [0, 1], "CT": [0, 2], "BYTE": [0, 2], "ARG": [0, 2]}
{"ST": [0, 0, 0], "CT": [0, 0, 0], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 1], "CT": [0, 0, 0], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 0], "CT": [0, 1, 0], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 1], "CT": [0, 1, 0], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 0], "CT": [0, 2, 0], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 1], "CT": [0, 2, 0], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 0], "CT": [0, 0, 1], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 1], "CT": [0, 0, 1], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 1, 1], "CT": [0, 0, 1], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 1, 2], "CT": [0, 0, 1], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 0], "CT": [0, 1, 1], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 1], "CT": [0, 1, 1], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 0], "CT": [0, 2, 1], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 1], "CT": [0, 2, 1], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 0], "CT": [0, 0, 2], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 1], "CT": [0, 0, 2], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 0], "CT": [0, 1, 2], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 1], "CT": [0, 1, 2], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 1, 1], "CT": [0, 1, 2], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 1, 2], "CT": [0, 1, 2], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 0], "CT": [0, 2, 2], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 1], "CT": [0, 2, 2], "BYTE": [0, 0, 0], "ARG": [0, 0, 0]}
{"ST": [0, 0, 0], "CT": [0, 0, 0], "BYTE": [0, 1, 0], "ARG": [0, 1, 0]}
{"ST": [0, 0, 1], "CT": [0, 0, 0], "BYTE": [0, 1, 0], "ARG": [0, 1, 0]}
{"ST": [0, 0, 0], "CT": [0, 1, 0], "BYTE": [0, 1, 0], "ARG": [0, 1, 0]}
{"ST": [0, 0, 1], "CT": [0, 1, 0], "BYTE": [0, 1, 0], "ARG": [0, 1, 0]}
{"ST": [0, 0, 0], "CT": [0, 2, 0], "BYTE": [0, 1, 0], "ARG": [0, 1, 0]}
{"ST": [0, 0, 1], "CT": [0, 2, 0], "BYTE": [0, 1, 0], "ARG": [0, 1, 0]}
{"ST": [0, 0, 0], "CT": [0, 0, 0], "BYTE": [0, 2, 0], "ARG": [0, 2, 0]}
{"ST": [0, 0, 1], "CT": [0, 0, 0], "BYTE": [0, 2, 0], "ARG": [0, 2, 0]}
{"ST": [0, 0, 0], "CT": [0, 1, 0], "BYTE": [0, 2, 0], "ARG": [0, 2, 0]}
{"ST": [0, 0, 1], "CT": [0, 1, 0], "BYTE": [0, 2, 0], "ARG": [0, 2, 0]}
{"ST": [0, 0, 0], "CT": [0, 2, 0], "BYTE": [0, 2, 0], "ARG": [0, 2, 0]}
{"ST": [0, 0, 1], "CT": [0, 2, 0], "BYTE": [0, 2, 0], "ARG": [0, 2, 0]}
{"ST": [0, 0, 0], "CT": [0, 0, 0], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 1], "CT": [0, 0, 0], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 0], "CT": [0, 1, 0], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 1], "CT": [0, 1, 0], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 0], "CT": [0, 2, 0], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 1], "CT": [0, 2, 0], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 0], "CT": [0, 0, 1], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 1], "CT": [0, 0, 1], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 1, 1], "CT": [0, 0, 1], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 1, 2], "CT": [0, 0, 1], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 0], "CT": [0, 1, 1], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 1], "CT": [0, 1, 1], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 0], "CT": [0, 2, 1], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 1], "CT": [0, 2, 1], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 0], "CT": [0, 0, 2], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 1], "CT": [0, 0, 2], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 0], "CT": [0, 1, 2], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 1], "CT": [0, 1, 2], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 1, 1], "CT": [0, 1, 2], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 1, 2], "CT": [0, 1, 2], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 0], "CT": [0, 2, 2], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 1], "CT": [0, 2, 2], "BYTE": [0, 0, 1], "ARG": [0, 0, 1]}
{"ST": [0, 0, 0], "CT": [0, 0, 0], "BYTE": [0, 1, 1], "ARG": [0, 1, 1]}
{"ST": [0, 0, 1], "CT": [0, 0, 0], "BYTE": [0, 1, 1], "ARG": [0, 1, 1]}
{"ST": [0, 0, 0], "CT": [0, 1, 0], "BYTE": [0, 1, 1], "ARG": [0, 1, 1]}
{"ST": [0, 0, 1], "CT": [0, 1, 0], "BYTE": [0, 1, 1], "ARG": [0, 1, 1]}
{"ST": [0, 0, 0], "CT": [0, 2, 0], "BYTE": [0, 1, 1], "ARG": [0, 1, 1]}
{"ST": [0, 0, 1], "CT": [0, 2, 0], "BYTE": [0, 1, 1], "ARG": [0, 1, 1]}
{"ST": [0, 0, 0], "CT": [0, 0, 0], "BYTE": [0, 2, 1], "ARG": [0, 2, 1]}
{"ST": [0, 0, 1], "CT": [0, 0, 0], "BYTE": [0, 2, 1], "ARG": [0, 2, 1]}
{"ST": [0, 0, 0], "CT": [0, 1, 0], "BYTE": [0, 2, 1], "ARG": [0, 2, 1]}
{"ST": [0, 0, 1], "CT": [0, 1, 0], "BYTE": [0, 2, 1], "ARG": [0, 2, 1]}
{"ST": [0, 0, 0], "CT": [0, 2, 0], "BYTE": [0, 2, 1], "ARG": [0, 2, 1]}
{"ST": [0, 0, 1], "CT": [0, 2, 0], "BYTE": [0, 2, 1], "ARG": [0, 2, 1]}
{"ST": [0, 0, 0], "CT": [0, 0, 0], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 1], "CT": [0, 0, 0], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 0], "CT": [0, 1, 0], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 1], "CT": [0, 1, 0], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 0], "CT": [0, 2, 0], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 1], "CT": [0, 2, 0], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 0], "CT": [0, 0, 1], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 1], "CT": [0, 0, 1], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 1, 1], "CT": [0, 0, 1], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 1, 2], "CT": [0, 0, 1], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 0], "CT": [0, 1, 1], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 1], "CT": [0, 1, 1], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 0], "CT": [0, 2, 1], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 1], "CT": [0, 2, 1], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 0], "CT": [0, 0, 2], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 1], "CT": [0, 0, 2], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 0], "CT": [0, 1, 2], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 1], "CT": [0, 1, 2], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 1, 1], "CT": [0, 1, 2], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 1, 2], "CT": [0, 1, 2], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 0], "CT": [0, 2, 2], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 1], "CT": [0, 2, 2], "BYTE": [0, 0, 2], "ARG": [0, 0, 2]}
{"ST": [0, 0, 0], "CT": [0, 0, 0], "BYTE": [0, 1, 2], "ARG": [0, 1, 2]}
{"ST": [0, 0, 1], "CT": [0, 0, 0], "BYTE": [0, 1, 2], "ARG": [0, 1, 2]}
{"ST": [0, 0, 0], "CT": [0, 1, 0], "BYTE": [0, 1, 2], "ARG": [0, 1, 2]}
{"ST": [0, 0, 1], "CT": [0, 1, 0], "BYTE": [0, 1, 2], "ARG": [0, 1, 2]}
{"ST": [0, 0, 0], "CT": [0, 2, 0], "BYTE": [0, 1, 2], "ARG": [0, 1, 2]}
{"ST": [0, 0, 1], "CT": [0, 2, 0], "BYTE": [0, 1, 2], "ARG": [0, 1, 2]}
{"ST": [0, 0, 0], "CT": [0, 0, 0], "BYTE": [0, 2, 2], "ARG": [0, 2, 2]}
{"ST": [0, 0, 1], "CT": [0, 0, 0], "BYTE": [0, 2, 2], "ARG": [0, 2, 2]}
{"ST": [0, 0, 0], "CT": [0, 1, 0], "BYTE": [0, 2, 2], "ARG": [0, 2, 2]}
{"ST": [0, 0, 1], "CT": [0, 1, 0], "BYTE": [0, 2, 2], "ARG": [0, 2, 2]}
{"ST": [0, 0, 0], "CT": [0, 2, 0], "BYTE": [0, 2, 2], "ARG": [0, 2, 2]}
{"ST": [0, 0, 1], "CT": [0, 2, 0], "BYTE": [0, 2, 2], "ARG": [0, 2, 2]}
Loading

0 comments on commit dd86203

Please sign in to comment.