github/powdr
1
1
Fork 0
mirror of https://github.com/powdr-labs/powdr.git synced 2026-04-20 03:03:25 -04:00
Code Issues Packages Projects Releases Wiki Activity

Expressions in instr/link params

Browse Source 
allow for `link` and RHS of `instr` params to use full on expressions
This commit is contained in:
Leandro Pacheco
2024-03-13 14:42:57 -03:00
parent e6b0b877d4
commit ff8fda1563
16 changed files with 185 additions and 215 deletions
Download Patch File Download Diff File Expand all files Collapse all files

37
analysis/src/machine_check.rs
View File

@@ -13,13 +13,11 @@ use powdr_ast::{
parsed::{
self,
asm::{
self, ASMModule, ASMProgram, AbsoluteSymbolPath, AssignmentRegister, CallableRef,
FunctionStatement, InstructionBody, LinkDeclaration, MachineStatement, ModuleStatement,
RegisterFlag, SymbolDefinition,
self, ASMModule, ASMProgram, AbsoluteSymbolPath, AssignmentRegister, FunctionStatement,
InstructionBody, LinkDeclaration, MachineStatement, ModuleStatement, RegisterFlag,
SymbolDefinition,
},
Expression,
},
SourceRef,
};
/// Verifies certain properties of each machine and constructs the Machine objects.
@@ -78,10 +76,7 @@ impl TypeChecker {
}
}
MachineStatement::LinkDeclaration(source, LinkDeclaration { flag, to }) => {
match self.check_link_declaration(source, flag, to) {
Ok(link_definition) => links.push(link_definition),
Err(e) => errors.extend(e),
}
links.push(LinkDefinitionStatement { source, flag, to });
}
MachineStatement::Pil(_source, statement) => {
pil.push(statement);
@@ -369,30 +364,6 @@ impl TypeChecker {
body: instruction.body,
})
}
fn check_link_declaration(
&self,
source: SourceRef,
flag: Expression,
to: CallableRef,
) -> Result<LinkDefinitionStatement, Vec<String>> {
let mut err = vec![];
to.params.inputs_and_outputs().for_each(|p| {
if let Some(ty) = &p.ty {
err.push(format!(
"Invalid type '{}: {}' in link declaration",
p.name, ty
));
}
});
if err.is_empty() {
Ok(LinkDefinitionStatement { source, flag, to })
} else {
Err(err)
}
}
}
#[cfg(test)]

1
asm-to-pil/Cargo.toml
View File

@@ -18,3 +18,4 @@ pretty_assertions = "1.4.0"
[dev-dependencies]
powdr-analysis = { path = "../analysis" }
powdr-importer = { path = "../importer" }

172
asm-to-pil/src/vm_to_constrained.rs
View File

@@ -9,7 +9,7 @@ use powdr_ast::{
LinkDefinitionStatement, Machine, RegisterDeclarationStatement, RegisterTy, Rom,
},
parsed::{
asm::{CallableRef, InstructionBody, Params},
asm::{CallableRef, InstructionBody, InstructionParams},
build::{self, absolute_reference, direct_reference, next_reference},
visitor::ExpressionVisitable,
ArrayExpression, BinaryOperator, Expression, FunctionCall, FunctionDefinition,
@@ -353,7 +353,6 @@ impl<T: FieldElement> ASMPILConverter<T> {
Some(ty) if ty == "unsigned" => {
Input::Literal(param.name, LiteralKind::UnsignedConstant)
}
Some(ty) if ty == "write" => Input::Register(param.name),
None => Input::Register(param.name),
Some(ty) => panic!("Invalid param type {}", ty),
})
@@ -371,7 +370,7 @@ impl<T: FieldElement> ASMPILConverter<T> {
source: SourceRef,
name: &String,
flag: String,
params: &Params,
params: &InstructionParams,
mut body: Vec<PilStatement>,
) {
// check inputs are literals or assignment registers
@@ -480,7 +479,7 @@ impl<T: FieldElement> ASMPILConverter<T> {
&mut self,
source: SourceRef,
flag: String,
params: &Params,
params: &InstructionParams,
mut callable: CallableRef,
) -> LinkDefinitionStatement {
let lhs = params;
@@ -490,7 +489,7 @@ impl<T: FieldElement> ASMPILConverter<T> {
lhs.inputs_and_outputs().for_each(|p| {
assert!(
p.index.is_none(),
"Cannot use array elements for instruction outputs."
"Cannot use array elements for lhs params"
);
let is_assignment_register = self
@@ -506,64 +505,70 @@ impl<T: FieldElement> ASMPILConverter<T> {
if rhs.is_empty() {
// we allow declarations with an empty RHS as syntactic sugar for when RHS = LHS.
*rhs = lhs.clone();
} else {
// if rhs is not empty, check it's valid
// rhs params must either be assignment registers declared in the lhs or write registers
rhs
rhs.inputs = lhs
.inputs
.iter_mut()
.chain(rhs.outputs.iter_mut())
.for_each(|p| {
let reg = self.registers.get(&p.name).expect("All rhs params must be registers");
assert!(p.ty.is_none());
match reg.ty {
RegisterTy::Assignment => {
assert!(lhs.inputs_and_outputs().any(|p_lhs| p_lhs.name == p.name),
"Assignment register '{}' on rhs must be also present on lhs params", p.name);
}
RegisterTy::Write => {
// the linker needs this information to build the
// plookup when a write register is used as output.
// TODO: less hackish way of passing this info? proper type for param.ty?
p.ty = Some("write".to_string());
},
_ => panic!("The rhs of an external instruction declaration must only use write or assignment registers"),
}
});
.iter()
.map(|p| direct_reference(p.name.clone()))
.collect();
rhs.outputs = lhs
.outputs
.iter()
.map(|p| direct_reference(p.name.clone()))
.collect();
} else {
let mut rhs_assignment_registers = BTreeSet::new();
let mut rhs_next_write_registers = BTreeSet::new();
// all lhs params must be used on rhs
// collect assignment registers and next references to write registers used on rhs
for expr in rhs.inputs_and_outputs() {
expr.pre_visit_expressions(&mut |e| match e {
Expression::Reference(poly) => {
poly.try_to_identifier()
.and_then(|name| self.registers.get(name).map(|reg| (name, reg)))
.filter(|(_, reg)| reg.ty == RegisterTy::Assignment)
.map(|(name, _)| rhs_assignment_registers.insert(name.clone()));
}
Expression::UnaryOperation(UnaryOperator::Next, e) => {
if let Expression::Reference(poly) = e.as_ref() {
poly.try_to_identifier()
.and_then(|name| self.registers.get(name).map(|reg| (name, reg)))
.filter(|(_, reg)| reg.ty == RegisterTy::Write)
.map(|(name, _)| rhs_next_write_registers.insert(name.clone()));
}
}
_ => {}
})
}
// any assignment register present on the rhs (input or output) must be present on the lhs
for name in &rhs_assignment_registers {
assert!(
lhs.inputs_and_outputs().any(|p_lhs| p_lhs.name == *name),
"Assignment register '{}' used on rhs must be present on lhs params",
name
);
}
// all lhs assignment registers must be used on rhs
lhs.inputs_and_outputs().for_each(|p| {
assert!(
rhs.inputs_and_outputs().any(|rhs_p| rhs_p.name == p.name),
rhs_assignment_registers.contains(&p.name),
"'{}' is declared on lhs but not used on the rhs",
p.name
)
});
// can't repeat registers on output of rhs
let uniq: BTreeSet<_> = rhs.outputs.iter().map(|p| &p.name).collect();
assert_eq!(
rhs.outputs.len(),
uniq.len(),
"rhs of external instruction can't have repeated output registers"
);
}
// if a write register is used as output in an external instruction mapping, we
// must induce a tautology in the update clause (Reg' = Reg') when the
// instruction is active, to allow the operation plookup to match.
for p in rhs.outputs.iter() {
let reg = self
.registers
.get_mut(&p.name)
.expect("All rhs params must be registers");
if reg.ty.is_write() {
let value = next_reference(&p.name);
// if a write register next reference (R') is used in the instruction mapping,
// we must induce a tautology in the update clause (R' = R') when the
// instruction is active, to allow the operation plookup to match.
for name in rhs_next_write_registers {
let reg = self.registers.get_mut(&name).unwrap();
let value = next_reference(name);
reg.conditioned_updates
.push((direct_reference(&flag), value));
}
}
LinkDefinitionStatement {
source,
flag: direct_reference(flag),
@@ -1210,13 +1215,13 @@ fn extract_update(expr: Expression) -> (Option<String>, Expression) {
#[cfg(test)]
mod test {
use powdr_ast::asm_analysis::AnalysisASMFile;
use powdr_importer::load_dependencies_and_resolve_str;
use powdr_number::{FieldElement, GoldilocksField};
use crate::compile;
fn parse_analyse_and_compile<T: FieldElement>(input: &str) -> AnalysisASMFile {
let parsed = powdr_parser::parse_asm(None, input).unwrap();
// let resolved = powdr_importer::load_dependencies_and_resolve(None, parsed).unwrap();
let parsed = load_dependencies_and_resolve_str(input);
let analyzed = powdr_analysis::analyze(parsed).unwrap();
compile::<T>(analyzed)
}
@@ -1240,46 +1245,6 @@ machine Main {
parse_analyse_and_compile::<GoldilocksField>(asm);
}
#[test]
#[should_panic(expected = "All rhs params must be registers")]
fn instr_external_rhs_not_register1() {
let asm = r"
machine Main {
degree 8;
reg pc[@pc];
reg X[<=];
reg A;
instr foo X = vm.foo B;
function main {
foo;
}
}
";
parse_analyse_and_compile::<GoldilocksField>(asm);
}
#[test]
#[should_panic(expected = "All rhs params must be registers")]
fn instr_external_rhs_not_register2() {
let asm = r"
machine Main {
degree 8;
reg pc[@pc];
reg X[<=];
reg A;
instr foo = vm.foo l: label;
function main {
foo;
}
}
";
parse_analyse_and_compile::<GoldilocksField>(asm);
}
#[test]
#[should_panic(expected = "'X' is declared on lhs but not used on the rhs")]
fn instr_external_lhs_register_not_used() {
@@ -1302,7 +1267,7 @@ machine Main {
}
#[test]
#[should_panic(expected = "Assignment register 'Y' on rhs must be also present on lhs params")]
#[should_panic(expected = "Assignment register 'Y' used on rhs must be present on lhs params")]
fn instr_external_rhs_register_not_on_lhs() {
let asm = r"
machine Main {
@@ -1318,27 +1283,6 @@ machine Main {
foo;
}
}
";
parse_analyse_and_compile::<GoldilocksField>(asm);
}
#[test]
#[should_panic(expected = "rhs of external instruction can't have repeated output registers")]
fn instr_external_rhs_repeated_output_register() {
let asm = r"
machine Main {
degree 8;
reg pc[@pc];
reg X[<=];
reg Y[<=];
reg A;
instr foo X = vm.foo X -> A, A;
function main {
foo;
}
}
";
parse_analyse_and_compile::<GoldilocksField>(asm);
}

9
ast/src/asm_analysis/mod.rs
View File

@@ -14,7 +14,8 @@ use powdr_number::BigUint;
use crate::parsed::{
asm::{
AbsoluteSymbolPath, AssignmentRegister, CallableRef, InstructionBody, OperationId, Params,
AbsoluteSymbolPath, AssignmentRegister, CallableRef, FunctionParams, InstructionBody,
InstructionParams, OperationId, OperationParams,
},
visitor::{ExpressionVisitable, VisitOrder},
NamespacedPolynomialReference, PilStatement, TypedExpression,
@@ -65,7 +66,7 @@ pub struct InstructionDefinitionStatement {
#[derive(Clone, Debug)]
pub struct Instruction {
pub params: Params,
pub params: InstructionParams,
pub body: InstructionBody,
}
@@ -510,7 +511,7 @@ impl<'a> TryFrom<&'a mut CallableSymbol> for &'a mut OperationSymbol {
pub struct FunctionSymbol {
pub source: SourceRef,
/// the parameters of this function, in the form of values
pub params: Params,
pub params: FunctionParams,
/// the body of the function
pub body: FunctionBody,
}
@@ -521,7 +522,7 @@ pub struct OperationSymbol {
/// the id of this operation. This machine's operation id must be set to this value in order for this operation to be active.
pub id: OperationId,
/// the parameters of this operation, in the form of columns defined in some constraints block of this machine
pub params: Params,
pub params: OperationParams,
}
#[derive(Clone, Debug)]

6
ast/src/object/mod.rs
View File

@@ -3,7 +3,7 @@ use std::collections::BTreeMap;
use powdr_number::BigUint;
use crate::parsed::{
asm::{AbsoluteSymbolPath, Params},
asm::{AbsoluteSymbolPath, CallableParams, OperationParams},
Expression, PilStatement, TypedExpression,
};
@@ -63,7 +63,7 @@ pub struct Link {
#[derive(Clone)]
pub struct LinkFrom {
pub flag: Expression,
pub params: Params,
pub params: CallableParams,
}
#[derive(Clone)]
@@ -91,5 +91,5 @@ pub struct Operation {
/// the value of the operation id of this machine which activates this operation
pub id: Option<BigUint>,
/// the parameters
pub params: Params,
pub params: OperationParams,
}

47
ast/src/parsed/asm.rs
View File

@@ -397,23 +397,22 @@ pub struct MachineArguments {
}
#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Default)]
pub struct Params {
pub inputs: Vec<Param>,
pub outputs: Vec<Param>,
pub struct Params<T> {
pub inputs: Vec<T>,
pub outputs: Vec<T>,
}
impl Params {
pub fn inputs_and_outputs(&self) -> impl Iterator<Item = &Param> {
self.inputs.iter().chain(self.outputs.iter())
}
pub type CallableParams = Params<Expression>;
// TODO: should we have separate Param types here?
// - Function: doesn't use `index` or `type`
// - Instruction: doesn't use `index`
// - Operation: doesn't use `type`
pub type FunctionParams = Params<Param>;
pub type InstructionParams = Params<Param>;
pub type OperationParams = Params<Param>;
pub fn inputs_and_outputs_mut(&mut self) -> impl Iterator<Item = &mut Param> {
self.inputs.iter_mut().chain(self.outputs.iter_mut())
}
}
impl Params {
pub fn new(inputs: Vec<Param>, outputs: Vec<Param>) -> Self {
impl<T> Params<T> {
pub fn new(inputs: Vec<T>, outputs: Vec<T>) -> Self {
Self { inputs, outputs }
}
@@ -421,6 +420,16 @@ impl Params {
self.inputs.is_empty() && self.outputs.is_empty()
}
pub fn inputs_and_outputs(&self) -> impl Iterator<Item = &T> {
self.inputs.iter().chain(self.outputs.iter())
}
pub fn inputs_and_outputs_mut(&mut self) -> impl Iterator<Item = &mut T> {
self.inputs.iter_mut().chain(self.outputs.iter_mut())
}
}
impl<T: Display> Params<T> {
pub fn prepend_space_if_non_empty(&self) -> String {
let mut params_str = self.to_string();
if !self.is_empty() {
@@ -438,7 +447,7 @@ pub struct OperationId {
#[derive(Debug, PartialEq, Eq, Clone, PartialOrd, Ord)]
pub struct Instruction {
pub params: Params,
pub params: Params<Param>,
pub body: InstructionBody,
}
@@ -450,8 +459,8 @@ pub enum MachineStatement {
RegisterDeclaration(SourceRef, String, Option<RegisterFlag>),
InstructionDeclaration(SourceRef, String, Instruction),
LinkDeclaration(SourceRef, LinkDeclaration),
FunctionDeclaration(SourceRef, String, Params, Vec<FunctionStatement>),
OperationDeclaration(SourceRef, String, OperationId, Params),
FunctionDeclaration(SourceRef, String, FunctionParams, Vec<FunctionStatement>),
OperationDeclaration(SourceRef, String, OperationId, OperationParams),
}
#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)]
@@ -464,7 +473,7 @@ pub struct LinkDeclaration {
pub struct CallableRef {
pub instance: String,
pub callable: String,
pub params: Params,
pub params: CallableParams,
}
#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)]
@@ -516,7 +525,7 @@ pub enum RegisterFlag {
IsReadOnly,
}
#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)]
#[derive(Debug, Default, PartialEq, Eq, PartialOrd, Ord, Clone)]
pub struct Param {
pub name: String,
pub index: Option<BigUint>,

4
ast/src/parsed/display.rs
View File

@@ -274,7 +274,7 @@ impl Display for RegisterFlag {
}
}
impl Display for Params {
impl<T: Display> Display for Params<T> {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
write!(
f,
@@ -683,7 +683,7 @@ mod tests {
ty: Some("ty".into()),
};
assert_eq!(p.to_string(), "abc: ty");
let empty = Params::default();
let empty = Params::<Param>::default();
assert_eq!(empty.to_string(), "");
assert_eq!(empty.prepend_space_if_non_empty(), "");
let in_out = Params {

6
book/src/asm/instructions.md
View File

@@ -30,10 +30,10 @@ An external instruction calling into this operation can be declared as follows:
```
{{#include ../../../test_data/asm/book/instructions.asm:trivial}}
```
The left-hand side of the definition declares the local instruction and which assignment registers are used for its inputs and outputs.
The right-hand side of the definition specifies the external operation being called and how it should be called.
The left-hand side of the definition declares the local instruction and which assignment registers are used in its inputs and outputs.
It describes how the instruction is used.
The right-hand side of the definition specifies the call to the external operation, with its inputs and outputs.
All assignment registers on the left-hand side must be used in the call to the external operation.
Additionally, regular registers can also be used in the call (can be seen as implicit inputs/outputs of the instruction).
In the previous example, parameters of the instruction match exactly with how the target operation should be called, and the right-hand parameters can thus be omitted.
The following example shows more complex usages of external instructions:

2
book/src/asm/links.md
View File

@@ -1,7 +1,7 @@
# Links
Links enable a constrained machine to call into another machine.
They are defined by a boolean flag and a mapping from local machine columns to the operation and its parameters (inputs and outputs):
They are defined by a boolean flag and a call to the operation, where inputs and outputs are expressions.
```
{{#include ../../../test_data/asm/book/operations_and_links.asm:links}}
```

24
importer/src/path_canonicalizer.rs
View File

@@ -8,8 +8,9 @@ use powdr_ast::{
parsed::Expression,
parsed::{
asm::{
ASMModule, ASMProgram, AbsoluteSymbolPath, Import, Machine, MachineStatement, Module,
ModuleRef, ModuleStatement, SymbolDefinition, SymbolValue, SymbolValueRef,
ASMModule, ASMProgram, AbsoluteSymbolPath, Import, Instruction, InstructionBody,
LinkDeclaration, Machine, MachineStatement, Module, ModuleRef, ModuleStatement,
SymbolDefinition, SymbolValue, SymbolValueRef,
},
folder::Folder,
visitor::ExpressionVisitable,
@@ -356,6 +357,25 @@ fn check_machine(
MachineStatement::Pil(_, statement) => statement
.expressions()
.try_for_each(|e| check_expression(&module_location, e, state, &local_variables))?,
// check rhs input exrpressions for `instr` and `link` declarations
MachineStatement::LinkDeclaration(
_,
LinkDeclaration {
to: callable_ref, ..
},
)
| MachineStatement::InstructionDeclaration(
_,
_,
Instruction {
body: InstructionBody::CallableRef(callable_ref),
..
},
) => {
callable_ref.params.inputs.iter().try_for_each(|e| {
check_expression(&module_location, e, state, &local_variables)
})?;
}
_ => {}
}
}

24
linker/src/lib.rs
View File

@@ -6,7 +6,7 @@ use powdr_ast::{
parsed::{
asm::AbsoluteSymbolPath,
asm::SymbolPath,
build::{direct_reference, index_access, namespaced_reference, next_reference},
build::{index_access, namespaced_reference},
Expression, PILFile, PilStatement, SelectedExpressions, TypedExpression,
},
SourceRef,
@@ -98,24 +98,12 @@ pub fn link(graph: PILGraph) -> Result<PILFile, Vec<String>> {
.iter()
.cloned()
.map(|n| Expression::Number(n, None));
let inputs = from
.params
.inputs
.into_iter()
.map(|i| {
assert!(i.ty.is_none() || i.ty == Some("write".to_string()));
(i.name, i.index)
})
.map(|(name, index)| index_access(direct_reference(name), index));
let outputs = from.params.outputs.into_iter().map(|p| match p.ty {
None => index_access(direct_reference(p.name), p.index),
// write register as output is mapped as a next ref in the plookup
Some(s) if s == "write" => index_access(next_reference(p.name), p.index),
_ => panic!(),
});
let lhs = SelectedExpressions {
selector: Some(from.flag),
expressions: op_id.chain(inputs).chain(outputs).collect(),
expressions: op_id
.chain(from.params.inputs)
.chain(from.params.outputs)
.collect(),
};
// the rhs is `latch { operation_id, inputs, outputs }`
@@ -567,7 +555,7 @@ machine Main {
SubVM vm;
instr add5_into_A X = vm.add5 X -> A;
instr add5_into_A X = vm.add5 X -> A';
function main {
add5_into_A 10; // A <== 15

10
parser/src/powdr.lalrpop
View File

@@ -281,7 +281,13 @@ pub InstructionBody: InstructionBody = {
}
pub CallableRef: CallableRef = {
<instance:Identifier> "." <callable:Identifier> <params:Params> => CallableRef { instance, callable, params },
<instance:Identifier> "." <callable:Identifier> <params:CallableParams> => CallableRef { instance, callable, params },
}
CallableParams: CallableParams = {
<inputs: ExpressionList> "->" <output: ExpressionList> => CallableParams::new(inputs, output),
// we can ommit the arrow if there are no outputs
<inputs: ExpressionList> => CallableParams::new(inputs, vec![])
}
InstructionBodyElements: Vec<PilStatement> = {
@@ -295,7 +301,7 @@ InstructionBodyElement: PilStatement = {
ExpressionStatementWithoutSemicolon,
}
Params: Params = {
Params: Params<Param> = {
<_input: ParamList> "->" <output: ParamList> => Params::new(_input, output),
// we can ommit the arrow if there are no outputs
<_input: ParamList> => Params::new(_input, vec![])

2
riscv/src/coprocessors.rs
View File

@@ -59,7 +59,7 @@ static POSEIDON_GL_COPROCESSOR: CoProcessor = CoProcessor {
import: "use std::hash::poseidon_gl::PoseidonGL;",
instructions: r#"
// ================== hashing instructions ==============
instr poseidon_gl = poseidon_gl.poseidon_permutation P0, P1, P2, P3, P4, P5, P6, P7, P8, P9, P10, P11 -> P0, P1, P2, P3;
instr poseidon_gl = poseidon_gl.poseidon_permutation P0, P1, P2, P3, P4, P5, P6, P7, P8, P9, P10, P11 -> P0', P1', P2', P3';
"#,
runtime_function_impl: Some(("poseidon_gl_coprocessor", poseidon_gl_call)),

24
test_data/asm/book/instructions.asm
View File

@@ -40,11 +40,17 @@ machine Main {
instr add X, Y -> Z = submachine.add; // - trivial usage, equivalent to:
// instr add X, Y -> Z = submachine.add X, Y -> Z;
// ANCHOR_END: trivial
instr add_to_A X, Y = submachine.add X, Y -> A; // - output to a regular register
instr add_to_A X, Y = submachine.add X, Y -> A';// - output to a regular register
instr addAB -> X = submachine.add A, B -> X; // - inputs from regular registers
instr addAB_to_C = submachine.add A, B -> C; // - all inputs and output are regular registers
instr addAB_to_A = submachine.add A, B -> A; // - reusing an input register as output
instr sub X, Y -> Z = submachine.add Y, Z -> X; // - find input for a given output (doesn't always work!)
instr addAB_to_C = submachine.add A, B -> C'; // - inputs and output from regular registers
instr addAB_to_A = submachine.add A, B -> A'; // - reusing an input register as output
instr sub X, Y -> Z = submachine.add Y, Z -> X; // - swapping input/output
// any expression can be used in the external call
instr add5 X -> Z = submachine.add X, 3+2 -> Z; // - literal expression as argument
col fixed STEP(i) { i };
instr add_current_time_step X -> Z = submachine.add X, STEP -> Z;// - columns can be referenced
let arr = [1,2,3,4,5]; // - functions can be used
instr add_arr_sum X -> Z = submachine.add X, std::array::sum(arr) -> Z;
instr assert_eq X, Y { X = Y }
@@ -70,6 +76,16 @@ machine Main {
addAB_to_A;
assert_eq A, 77;
A <== add5(2);
assert_eq A, 7;
A <== add_arr_sum(3);
assert_eq A, 18;
// Note that the result of this operation depends on when it executed
A <== add_current_time_step(42);
B <== add_current_time_step(42);
assert_eq B - A, 1;
return;
}
}

4
test_data/asm/book/operations_and_links.asm
View File

@@ -33,6 +33,8 @@ machine Add4(latch, operation_id) {
link 1 => adder.add x, y -> n;
// - constrain the values of `z`, `w`, and `m` so that `m = adder.add(z, w)`
link 1 => adder.add z, w -> m;
// - constrain the values of `m`, `n` and `r` so that `r = adder.add(m,n)`
link 1 => adder.add m, n -> r;
col fixed operation_id = [0]*;
col fixed latch = [1]*;
@@ -44,8 +46,6 @@ machine Add4(latch, operation_id) {
col witness r;
col witness m;
col witness n;
r = m + n;
}
// ANCHOR: one_operation

28
test_data/asm/vm_instr_param_mapping.asm
View File

@@ -43,20 +43,33 @@ machine Main {
reg C;
instr add X, Y -> Z = addvm.add;
instr add_to_A X, Y = addvm.add X, Y -> A;
instr sub_from_add X, Y -> Z = addvm.add Y, Z -> X;
instr add_to_A X, Y = addvm.add X, Y -> A';
instr addAB -> X = addvm.add A, B -> X;
instr addAB_to_C = addvm.add A, B -> C;
instr addAB_to_A = addvm.add A, B -> A;
instr addAB_to_C = addvm.add A, B -> C';
instr addAB_to_A = addvm.add A, B -> A';
instr sub_from_add X, Y -> Z = addvm.add Y, Z -> X;
instr sub_from_add_into_A X, Y = addvm.add Y, A' -> X;
instr add5 X -> Z = addvm.add X, 5 -> Z;
col fixed NUM(i) { 42 };
instr add42 X -> Z = addvm.add X, NUM -> Z;
let arr = [1,2,3,4,5];
instr add_arr_sum X -> Z = addvm.add X, std::array::sum(arr) -> Z;
instr sub X, Y -> Z = subvm.sub;
instr sub_to_C X, Y = subvm.sub X, Y -> C;
instr sub_to_C X, Y = subvm.sub X, Y -> C';
instr assert_eq X, Y { X = Y }
function main {
A <== add(2, 3);
assert_eq A, 5;
A <== add5(2);
assert_eq A, 7;
A <== add42(3);
assert_eq A, 45;
add_to_A 6, 7;
assert_eq A, 13;
@@ -71,12 +84,13 @@ machine Main {
addAB_to_C;
assert_eq C, 5;
A <== add_arr_sum(3);
assert_eq A, 18;
A <=X= 33;
B <=X= 44;
C <== sub(B, A);
assert_eq C, 11;
addAB_to_A;
assert_eq A, 77;