Skip to content

Commit

Permalink
fix: constants involving exponents
Browse files Browse the repository at this point in the history
This puts through a simple fix for constant values involving exponents.
Again, this was a simple aliasing bug.
  • Loading branch information
DavePearce committed Dec 21, 2024
1 parent 8880564 commit 70b10bb
Show file tree
Hide file tree
Showing 6 changed files with 56 additions and 8 deletions.
15 changes: 13 additions & 2 deletions pkg/corset/expression.go
Original file line number Diff line number Diff line change
Expand Up @@ -270,7 +270,11 @@ func (e *Exp) AsConstant() *big.Int {
pow := e.Pow.AsConstant()
// Check if can evaluate
if arg != nil && pow != nil {
return arg.Exp(arg, pow, nil)
var res big.Int
// Compute exponent
res.Exp(arg, pow, nil)
// Done
return &res
}
//
return nil
Expand Down Expand Up @@ -605,7 +609,14 @@ type Normalise struct{ Arg Expr }
// AsConstant attempts to evaluate this expression as a constant (signed) value.
// If this expression is not constant, then nil is returned.
func (e *Normalise) AsConstant() *big.Int {
// FIXME: we could do better here.
if arg := e.Arg.AsConstant(); arg != nil {
if arg.Cmp(big.NewInt(0)) != 0 {
return big.NewInt(1)
}
// zero
return arg
}
//
return nil
}

Expand Down
11 changes: 7 additions & 4 deletions pkg/corset/translator.go
Original file line number Diff line number Diff line change
Expand Up @@ -449,7 +449,7 @@ func (t *translator) translateExpressionInModule(expr Expr, module string, shift
case *Shift:
return t.translateShiftInModule(e, module, shift)
case *VariableAccess:
return t.translateVariableAccessInModule(e, module, shift)
return t.translateVariableAccessInModule(e, shift)
default:
return nil, t.srcmap.SyntaxErrors(expr, "unknown expression encountered during translation")
}
Expand Down Expand Up @@ -519,16 +519,19 @@ func (t *translator) translateShiftInModule(expr *Shift, module string, shift in
return t.translateExpressionInModule(expr.Arg, module, shift+int(constant.Int64()))
}

func (t *translator) translateVariableAccessInModule(expr *VariableAccess, module string,
shift int) (hir.Expr, []SyntaxError) {
func (t *translator) translateVariableAccessInModule(expr *VariableAccess, shift int) (hir.Expr, []SyntaxError) {
if binding, ok := expr.Binding().(*ColumnBinding); ok {
// Lookup column binding
cinfo := t.env.Column(binding.module, expr.Name())
// Done
return &hir.ColumnAccess{Column: cinfo.ColumnId(), Shift: shift}, nil
} else if binding, ok := expr.Binding().(*ConstantBinding); ok {
// Just fill in the constant.
return t.translateExpressionInModule(binding.value, module, shift)
var constant fr.Element
// Initialise field from bigint
constant.SetBigInt(binding.value.AsConstant())
//
return &hir.Constant{Val: constant}, nil
}
// error
return nil, t.srcmap.SyntaxErrors(expr, "unbound variable")
Expand Down
8 changes: 6 additions & 2 deletions pkg/test/valid_corset_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,10 @@ func Test_Constant_09(t *testing.T) {
Check(t, false, "constant_09")
}

func Test_Constant_10(t *testing.T) {
Check(t, false, "constant_10")
}

// ===================================================================
// Alias Tests
// ===================================================================
Expand Down Expand Up @@ -818,9 +822,9 @@ func TestSlow_Stp(t *testing.T) {
Check(t, true, "stp")
}

/* func TestSlow_Mmio(t *testing.T) {
func TestSlow_Mmio(t *testing.T) {
Check(t, true, "mmio")
} */
}

// ===================================================================
// Test Helpers
Expand Down
5 changes: 5 additions & 0 deletions testdata/constant_10.accepts
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
{ "X": [], "Y": [] }
{ "X": [0], "Y": [0] }
{ "X": [16], "Y": [1] }
{ "X": [32], "Y": [2] }
{ "X": [64], "Y": [4] }
7 changes: 7 additions & 0 deletions testdata/constant_10.lisp
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
(defcolumns (X :@loob) Y)
(defconst
N 4
TWO_N (^ 2 N))

;; X == Y * 2^n
(defconstraint c1 () (- X (* Y TWO_N)))
18 changes: 18 additions & 0 deletions testdata/constant_10.rejects
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
{ "X": [1], "Y": [0] }
{ "X": [1], "Y": [1] }
{ "X": [2], "Y": [1] }
{ "X": [3], "Y": [1] }
{ "X": [4], "Y": [1] }
{ "X": [5], "Y": [1] }
{ "X": [6], "Y": [1] }
{ "X": [7], "Y": [1] }
{ "X": [8], "Y": [1] }
{ "X": [9], "Y": [1] }
{ "X": [10], "Y": [1] }
{ "X": [11], "Y": [1] }
{ "X": [12], "Y": [1] }
{ "X": [13], "Y": [1] }
{ "X": [14], "Y": [1] }
{ "X": [15], "Y": [1] }
{ "X": [17], "Y": [1] }
{ "X": [18], "Y": [1] }

0 comments on commit 70b10bb

Please sign in to comment.