Enum SpecType 

pub enum SpecType {
    Int,
    Float,
    Bool,
    Str,
    Record {
        fields: Vec<(String, SpecType)>,
    },
    List {
        element: Box<SpecType>,
    },
    Named {
        name: String,
    },
}

Variants

Int

Float

Bool

Str

Record

Record type with named fields (#208). Quantifying over a record-shaped binding lets specs reference structured agent state without flattening into per-field scalar bindings. Fields are stored in declaration order; the gate evaluator resolves expr.field against Value::Record’s IndexMap, which preserves insertion order.

Fields

fields: Vec<(String, SpecType)>

List

List of an element type (#208). Quantifying over a list lets specs reason about agent collections — outstanding orders, active charging sessions, message queues — via length, head, tail, and indexed access (xs[i]).

Fields

element: Box<SpecType>

Named

Named user type (#208 slice 3). Refers to a user-defined ADT from the host program (e.g. Message, Order). The gate evaluator inspects the value’s variant tag at match time; no compile-time variant table is needed for the gate path. The random-input prover (check_spec) can’t sample arbitrary user types and fails out — those tests should provide concrete bindings instead.

Fields

name: String

Trait Implementations

impl Clone for SpecType

fn clone(&self) -> SpecType

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SpecType

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for SpecType

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for SpecType

fn eq(&self, other: &SpecType) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for SpecType

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

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for SpecType