forked from starkware-libs/cairo
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add init_circuit_data. (starkware-libs#5481)
- Loading branch information
1 parent
5c95ac1
commit ce3e4a7
Showing
17 changed files
with
347 additions
and
21 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,3 +1,16 @@ | ||
| pub type u96 = core::internal::BoundedInt<0, 79228162514264337593543950335>; | ||
|
|
||
| pub extern type RangeCheck96; | ||
|
|
||
|
|
||
| // Defines an input for a circuit. | ||
| #[phantom] | ||
| pub extern type CircuitInput<const N: usize>; | ||
|
|
||
|
|
||
| // Initializes the input data for running an instance of the circuit. | ||
| extern fn init_circuit_data<C>() -> CircuitInputAccumulator<C> implicits(RangeCheck96) nopanic; | ||
|
|
||
| // Type for accumulating inputs into the circuit instance's data. | ||
| extern type CircuitInputAccumulator<C>; | ||
|
|
||
| impl CircuitInputAccumulatorDrop<C> of Drop<CircuitInputAccumulator<C>>; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
46 changes: 46 additions & 0 deletions
46
crates/cairo-lang-sierra-to-casm/src/invocations/circuit.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,46 @@ | ||
| use cairo_lang_casm::builder::CasmBuilder; | ||
| use cairo_lang_casm::casm_build_extend; | ||
| use cairo_lang_sierra::extensions::circuit::CircuitConcreteLibfunc; | ||
|
|
||
| use super::{CompiledInvocation, CompiledInvocationBuilder, InvocationError}; | ||
| use crate::invocations::add_input_variables; | ||
|
|
||
| /// Builds instructions for Sierra array operations. | ||
| pub fn build( | ||
| libfunc: &CircuitConcreteLibfunc, | ||
| builder: CompiledInvocationBuilder<'_>, | ||
| ) -> Result<CompiledInvocation, InvocationError> { | ||
| match libfunc { | ||
| CircuitConcreteLibfunc::InitCircuitData(_) => build_init_circuit_data(builder), | ||
| } | ||
| } | ||
|
|
||
| /// Handles a Sierra statement for initializing circuit data. | ||
| fn build_init_circuit_data( | ||
| builder: CompiledInvocationBuilder<'_>, | ||
| ) -> Result<CompiledInvocation, InvocationError> { | ||
| let [expr_rc96] = builder.try_get_refs()?; | ||
| let rc96 = expr_rc96.try_unpack_single()?; | ||
|
|
||
| // TODO(ilya): get n_inputs and n_vals from the libfunc. | ||
| let n_inputs = 1; | ||
| let n_vals = 2; | ||
|
|
||
| let mut casm_builder = CasmBuilder::default(); | ||
|
|
||
| add_input_variables! {casm_builder, | ||
| buffer(1) rc96; | ||
| }; | ||
| casm_build_extend! {casm_builder, | ||
| const n_inputs = n_inputs; | ||
| let inputs_end = rc96 + n_inputs; | ||
| const n_vals = n_vals; | ||
| let vals_end = rc96 + n_vals; | ||
| }; | ||
|
|
||
| Ok(builder.build_from_casm_builder( | ||
| casm_builder, | ||
| [("Fallthrough", &[&[vals_end], &[rc96, inputs_end]], None)], | ||
| Default::default(), | ||
| )) | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
206 changes: 206 additions & 0 deletions
206
crates/cairo-lang-sierra/src/extensions/modules/circuit.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,206 @@ | ||
| use num_bigint::BigInt; | ||
|
|
||
| use super::range_check::RangeCheck96Type; | ||
| use super::structure::StructType; | ||
| use crate::extensions::lib_func::{ | ||
| DeferredOutputKind, LibfuncSignature, OutputVarInfo, ParamSignature, SierraApChange, | ||
| SignatureOnlyGenericLibfunc, SignatureSpecializationContext, | ||
| }; | ||
| use crate::extensions::type_specialization_context::TypeSpecializationContext; | ||
| use crate::extensions::types::TypeInfo; | ||
| use crate::extensions::{ | ||
| args_as_single_type, args_as_single_value, extract_type_generic_args, ConcreteType, NamedType, | ||
| OutputVarReferenceInfo, SpecializationError, | ||
| }; | ||
| use crate::ids::{ConcreteTypeId, GenericTypeId, UserTypeId}; | ||
| use crate::program::{ConcreteTypeLongId, GenericArg}; | ||
| use crate::{define_libfunc_hierarchy, define_type_hierarchy}; | ||
|
|
||
| define_type_hierarchy! { | ||
| pub enum CircuitType { | ||
| CircuitInput(CircuitInput), | ||
| CircuitInputAccumulator(CircuitInputAccumulator), | ||
| }, CircuitTypeConcrete | ||
| } | ||
|
|
||
| define_libfunc_hierarchy! { | ||
| pub enum CircuitLibFunc { | ||
| InitCircuitData(InitCircuitData), | ||
| }, CircuitConcreteLibfunc | ||
| } | ||
|
|
||
| /// Returns true if `garg` is a type that is considered a circuit component. | ||
| fn is_circuit_component( | ||
| context: &dyn TypeSpecializationContext, | ||
| garg: &GenericArg, | ||
| ) -> Result<bool, SpecializationError> { | ||
| let GenericArg::Type(ty) = garg else { | ||
| return Err(SpecializationError::UnsupportedGenericArg); | ||
| }; | ||
|
|
||
| let long_id = context.get_type_info(ty.clone())?.long_id; | ||
| let generic_id = long_id.generic_id; | ||
| if generic_id == CircuitInput::ID { | ||
| return Ok(true); | ||
| } | ||
| Ok(false) | ||
| } | ||
|
|
||
| /// Circuit input type. | ||
| #[derive(Default)] | ||
| pub struct CircuitInput {} | ||
| impl NamedType for CircuitInput { | ||
| type Concrete = ConcreteCircuitInput; | ||
| const ID: GenericTypeId = GenericTypeId::new_inline("CircuitInput"); | ||
|
|
||
| fn specialize( | ||
| &self, | ||
| context: &dyn TypeSpecializationContext, | ||
| args: &[GenericArg], | ||
| ) -> Result<Self::Concrete, SpecializationError> { | ||
| Self::Concrete::new(context, args) | ||
| } | ||
| } | ||
|
|
||
| /// Defines an input for a circuit. | ||
| pub struct ConcreteCircuitInput { | ||
| /// The type info of the concrete type. | ||
| pub info: TypeInfo, | ||
| /// The index of the circuit input. | ||
| pub idx: BigInt, | ||
| } | ||
| impl ConcreteCircuitInput { | ||
| fn new( | ||
| _context: &dyn TypeSpecializationContext, | ||
| args: &[GenericArg], | ||
| ) -> Result<Self, SpecializationError> { | ||
| let idx = args_as_single_value(args)?; | ||
| Ok(Self { | ||
| info: TypeInfo { | ||
| long_id: ConcreteTypeLongId { | ||
| generic_id: "CircuitInput".into(), | ||
| generic_args: args.to_vec(), | ||
| }, | ||
| duplicatable: false, | ||
| droppable: false, | ||
| storable: false, | ||
| zero_sized: false, | ||
| }, | ||
| idx, | ||
| }) | ||
| } | ||
| } | ||
|
|
||
| impl ConcreteType for ConcreteCircuitInput { | ||
| fn info(&self) -> &TypeInfo { | ||
| &self.info | ||
| } | ||
| } | ||
|
|
||
| /// Type for accumulating inputs into the circuit instance's data. | ||
| #[derive(Default)] | ||
| pub struct CircuitInputAccumulator {} | ||
| impl NamedType for CircuitInputAccumulator { | ||
| type Concrete = ConcreteCircuitInputAccumulator; | ||
| const ID: GenericTypeId = GenericTypeId::new_inline("CircuitInputAccumulator"); | ||
|
|
||
| fn specialize( | ||
| &self, | ||
| context: &dyn TypeSpecializationContext, | ||
| args: &[GenericArg], | ||
| ) -> Result<Self::Concrete, SpecializationError> { | ||
| Self::Concrete::new(context, args) | ||
| } | ||
| } | ||
|
|
||
| pub struct ConcreteCircuitInputAccumulator { | ||
| pub info: TypeInfo, | ||
| } | ||
|
|
||
| impl ConcreteCircuitInputAccumulator { | ||
| fn new( | ||
| context: &dyn TypeSpecializationContext, | ||
| args: &[GenericArg], | ||
| ) -> Result<Self, SpecializationError> { | ||
| let circ_ty = args_as_single_type(args)?; | ||
| validate_is_circuit(context, circ_ty)?; | ||
| Ok(Self { | ||
| info: TypeInfo { | ||
| long_id: ConcreteTypeLongId { | ||
| generic_id: "CircuitInputAccumulator".into(), | ||
| generic_args: args.to_vec(), | ||
| }, | ||
| duplicatable: false, | ||
| droppable: true, | ||
| storable: true, | ||
| zero_sized: false, | ||
| }, | ||
| }) | ||
| } | ||
| } | ||
|
|
||
| impl ConcreteType for ConcreteCircuitInputAccumulator { | ||
| fn info(&self) -> &TypeInfo { | ||
| &self.info | ||
| } | ||
| } | ||
|
|
||
| /// Validate that `circ_ty` is a circuit type. | ||
| fn validate_is_circuit( | ||
| context: &dyn TypeSpecializationContext, | ||
| circ_ty: ConcreteTypeId, | ||
| ) -> Result<(), SpecializationError> { | ||
| let struct_generic_args = extract_type_generic_args::<StructType>(context, &circ_ty)?; | ||
|
|
||
| let mut gargs = struct_generic_args.iter(); | ||
| if !matches!( | ||
| gargs.next(), | ||
| Some(GenericArg::UserType(ut)) | ||
| if (*ut == UserTypeId::from_string("Tuple")) | ||
|
|
||
| ) { | ||
| return Err(SpecializationError::UnsupportedGenericArg); | ||
| } | ||
|
|
||
| for garg in gargs { | ||
| // Note that its enough to check the topmost types as they validate their children. | ||
| if !is_circuit_component(context, garg)? { | ||
| return Err(SpecializationError::UnsupportedGenericArg); | ||
| } | ||
| } | ||
|
|
||
| Ok(()) | ||
| } | ||
|
|
||
| /// Libfunc for initializing the input data for running an instance of the circuit. | ||
| #[derive(Default)] | ||
| pub struct InitCircuitData {} | ||
| impl SignatureOnlyGenericLibfunc for InitCircuitData { | ||
| const STR_ID: &'static str = "init_circuit_data"; | ||
|
|
||
| fn specialize_signature( | ||
| &self, | ||
| context: &dyn SignatureSpecializationContext, | ||
| generic_args: &[GenericArg], | ||
| ) -> Result<LibfuncSignature, SpecializationError> { | ||
| let range_check96_type = context.get_concrete_type(RangeCheck96Type::id(), &[])?; | ||
| let circuit_input_accumulator_ty = | ||
| context.get_concrete_type(CircuitInputAccumulator::id(), generic_args)?; | ||
| Ok(LibfuncSignature::new_non_branch_ex( | ||
| vec![ParamSignature::new(range_check96_type.clone()).with_allow_add_const()], | ||
| vec![ | ||
| OutputVarInfo { | ||
| ty: range_check96_type.clone(), | ||
| ref_info: OutputVarReferenceInfo::Deferred(DeferredOutputKind::AddConst { | ||
| param_idx: 0, | ||
| }), | ||
| }, | ||
| OutputVarInfo { | ||
| ty: circuit_input_accumulator_ty.clone(), | ||
| ref_info: OutputVarReferenceInfo::Deferred(DeferredOutputKind::Generic), | ||
| }, | ||
| ], | ||
| SierraApChange::Known { new_vars_only: true }, | ||
| )) | ||
| } | ||
| } |
Oops, something went wrong.