Using TypedADT constructs in Inox

Question

The inox documentation states the following

Inox provides the utility types TypedADTSort and TypedADTConstructor (see file inox/ast/Definitions.scala) that correspond to ADT definitions whose type parameters have been instantiated with concrete types. One can use these to access parameters/fields and enclosed expressions with instantiated types.

The following object contains the sorts and constructors necessary for modelling a mathematical field.

import inox._
import inox.trees.{forall => _, _}
import inox.trees.dsl._

import welder._

object Field { 
  /*
    A non trivial field has elements different from zero.
    We can further assume the existence of a nonzero element called one.
    Any other element is of type notOne.

    field -> zero
          -> nonZero -> one
                     -> notOne
  */

  val element = FreshIdentifier("element")
  val zero = FreshIdentifier("zero")
  val nonZero = FreshIdentifier("nonZero")
  val one = FreshIdentifier("one")
  val notOne = FreshIdentifier("notOne")

  val elementADT = mkSort(element)()(Seq(zero, one, nonZero, notOne))
  val nonZeroADT = mkConstructor(nonZero)()(Some(element)) {_ => Seq()}
  val zeroADT = mkConstructor(zero)()(Some(element)) {_ => Seq()}
  val oneADT = mkConstructor(one)()(Some(nonZero)) {_ => Seq()}
  val notOneADT = mkConstructor(notOne)()(Some(nonZero)) {_ => Seq()}


  val symbols = NoSymbols
    .withADTs(Seq(elementADT, nonZeroADT, zeroADT, oneADT, notOneADT))
    .withFunctions(Seq(/*Register functions*/))

  val program = InoxProgram(Context.empty, symbols)

  val theory = theoryOf(program)
  import theory._
}

Now I introduce the sorts and constructs for modelling affine points of an elliptic curve.

import inox._
import inox.trees.{forall => _, _}
import inox.trees.dsl._

import welder._

object Curve {

  val F: ADTType = T(Field.element)()
  val affinePoint = FreshIdentifier("affinePoint")
  val infinitePoint = FreshIdentifier("infinitePoint")
  val finitePoint = FreshIdentifier("finitePoint")
  val x = FreshIdentifier("x")
  val y = FreshIdentifier("y")

  val affinePointADT = mkSort(affinePoint)("F")(Seq(infinitePoint,finitePoint))
  val infiniteADT = mkConstructor(infinitePoint)("F")(Some(affinePoint))(_ => Seq())
  val finiteADT = mkConstructor(finitePoint)("F")(Some(affinePoint)){ case Seq(fT) =>
    Seq(ValDef(x, fT), ValDef(y, fT))
  }

  val affine = TypedADTSort(affinePointADT,Seq(F))
  val infinite = TypedADTConstructor(infiniteADT,Seq(F))
  val finite = TypedADTConstructor(finiteADT,Seq(F))

  val symbols = NoSymbols
    .withADTs(Seq(affinePointADT, infiniteADT, finiteADT))
    .withFunctions(Seq(/*Register functions here*/))
}

You can observe that at the end I'm using TypedADTSort and TypedADTConstructor to use the field elements as parameter instead of a generic parameter. I need this to talk about operations on field elements in the context of affine points.

Compile error

Compiling this gives an error of the type

could not find implicit value for parameter symbols: inox.trees.Symbols
[error]   val affine = TypedADTSort(affinePointADT,Seq(F))
[error]                            ^
could not find implicit value for parameter symbols: inox.trees.Symbols
[error]   val infinite = TypedADTConstructor(infiniteADT,Seq(F))

Why does this happen? What solutions are there?

user1868607 · Accepted Answer · 2017-04-15T12:13:51.970

There is no need to use the TypedADT construct in this case. It suffices to model the following hierarchy with sorts and constructors.

abstract class Element
abstract class AffinePoint[T]

The hard part is perhaps realizing that AffinePoint[Element] can be modeled as T(affinePoint)(T(element)()) using the Inox DSL in here.

In any case, the compile error that I get arises from the fact that I need to pass an implicit argument to the corresponding call.

Using TypedADT constructs in Inox

1 Answers1