Enum Shape 

pub enum Shape<Expr, ExprExt> {
    Unit,
    Expr(Expr),
    ExprExt(ExprExt),
    Word([Expr; 4]),
    Array(Vec<Box<Shape<Expr, ExprExt>>>),
    Struct(String, Vec<(String, Box<Shape<Expr, ExprExt>>)>),
}

Shapes of input type to SP1Operation

More like poor man’s facet::Facet…

Variants

Unit

A unit type. This should only be used for representing Output shapes.

Expr(Expr)

An arithmetic expression.

ExprExt(ExprExt)

An arithmetic expression over the extension field.

Word([Expr; 4])

A word in the base field.

Array(Vec<Box<Shape<Expr, ExprExt>>>)

An array of shapes of arbitrary size.

Struct(String, Vec<(String, Box<Shape<Expr, ExprExt>>)>)

A flexible struct type that can represent nested structures. Contains the struct name and a vector of (field_name, field_shape) pairs.

Implementations

impl<F: Field, EF: ExtensionField<F>> Shape<ExprRef<F>, ExprExtRef<EF>>

pub fn to_lean_constructor(&self, mapping: &HashMap<usize, String>) -> String

Output the string that would construct a value of this Shape

pub fn to_lean_destructor(&self) -> String

Output the string that would destruct a value of this Shape

pub fn map_input( &self, prefix: String, input_mapping: &mut HashMap<usize, String>, )

Calculates the full variable name that corresponds to InputArg(x).

For example,

structure AddOperation where
  value : Word SP1Field

def AddOperation.constraints
  (b : SP1Field)
  (c : SP1Field)
  (cols : AddOperation)
  (is_real : SP1Field) := sorry

Expr(InputArg(3)) then maps to “cols.value[1]” because if you recursively flatten the input arguments to AddOperation.constraints in argument/field declaration order, then the element at index 3 corresponds to cols.value[1].

impl<Expr, ExprExt> Shape<Expr, ExprExt>

pub fn to_lean_type(&self) -> String

Converts the shape to its corresponding Lean type.

SAFETY: all elements of Shape::Array must have the same shape. We use the first item as the shape.

SAFETY: Shape::Array must be non-empty.

Trait Implementations

impl<Expr: Clone, ExprExt: Clone> Clone for Shape<Expr, ExprExt>

fn clone(&self) -> Shape<Expr, ExprExt>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<Expr: Debug, ExprExt: Debug> Debug for Shape<Expr, ExprExt>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de, Expr, ExprExt> Deserialize<'de> for Shape<Expr, ExprExt>

where Expr: Deserialize<'de>, ExprExt: Deserialize<'de>,

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl<F: Field, EF: ExtensionField<F>, T: Into<Shape<ExprRef<F>, ExprExtRef<EF>>>, const N: usize> From<[T; N]> for Shape<ExprRef<F>, ExprExtRef<EF>>

fn from(val: [T; N]) -> Self

Converts to this type from the input type.

impl<F: Field, EF: ExtensionField<F>> From<()> for Shape<ExprRef<F>, ExprExtRef<EF>>

fn from(_val: ()) -> Self

Converts to this type from the input type.

impl<F: Field, EF: ExtensionField<F>> From<ExprExtRef<EF>> for Shape<ExprRef<F>, ExprExtRef<EF>>

fn from(val: ExprExtRef<EF>) -> Self

Converts to this type from the input type.

impl<F: Field, EF: ExtensionField<F>> From<ExprRef<F>> for Shape<ExprRef<F>, ExprExtRef<EF>>

fn from(val: ExprRef<F>) -> Self

Converts to this type from the input type.

impl<F: Field, EF: ExtensionField<F>, T: Into<ExprRef<F>>> From<Word<T>> for Shape<ExprRef<F>, ExprExtRef<EF>>

fn from(val: Word<T>) -> Self

Converts to this type from the input type.

impl<Expr, ExprExt> Serialize for Shape<Expr, ExprExt>

where Expr: Serialize, ExprExt: Serialize,

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.