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

Merge pull request #150 from chriseth/in-out-instruction-syntax

Browse Source 
Functional instruction declaration syntax
This commit is contained in:
Leo
2023-04-14 15:57:14 +02:00
committed by GitHub
parent c3b6c7d959 a197775300
commit efe35d76ca
10 changed files with 166 additions and 98 deletions
Download Patch File Download Diff File Expand all files Collapse all files

162
src/asm_compiler/mod.rs
View File

@@ -82,7 +82,7 @@ impl ASMPILConverter {
Expression::FunctionCall(function_name, args) => {
self.handle_functional_instruction(
write_regs,
assign_reg,
assign_reg.unwrap(),
function_name,
args,
);
@@ -206,22 +206,49 @@ impl ASMPILConverter {
start: usize,
body: Vec<InstructionBodyElement>,
name: String,
params: Vec<InstructionParam>,
params: InstructionParams,
) {
let instruction_flag = format!("instr_{name}");
self.create_witness_fixed_pair(start, &instruction_flag);
// it's part of the lookup!
//self.pil.push(constrain_zero_one(&col_name));
let mut substitutions = HashMap::new();
for p in &params {
if p.assignment_reg.0.is_none() && p.assignment_reg.1.is_none() {
// literal argument
let param_col_name = format!("instr_{name}_param_{}", p.name);
let inputs: Vec<_> = params
.inputs
.params
.into_iter()
.map(|param| match param.ty {
Some(ty) if ty == "label" => Input::Label(param.name),
None => Input::Register(param.name),
Some(ty) => panic!("param type must be nothing or label, found `{}`", ty),
})
.collect();
let outputs = params
.outputs
.map(|outputs| {
outputs
.params
.into_iter()
.map(|param| {
assert!(param.ty.is_none(), "output must be a register");
param.name
})
.collect()
})
.unwrap_or(vec![]);
let instr = Instruction { inputs, outputs };
let substitutions = instr
.labels()
.map(|label| {
// label
let param_col_name = format!("instr_{name}_param_{}", label);
self.create_witness_fixed_pair(start, &param_col_name);
substitutions.insert(p.name.clone(), param_col_name);
}
}
(label.clone(), param_col_name)
})
.collect();
for expr in body {
match expr {
@@ -255,7 +282,6 @@ impl ASMPILConverter {
}
}
}
let instr = Instruction { params };
self.instructions.insert(name, instr);
}
@@ -283,18 +309,21 @@ impl ASMPILConverter {
fn handle_functional_instruction(
&mut self,
write_regs: Vec<String>,
assign_reg: Option<String>,
assign_reg: String,
instr_name: String,
args: Vec<Expression>,
) {
assert!(write_regs.len() == 1);
assert!(assign_reg.is_some());
let instr = &self.instructions[&instr_name];
assert_eq!(instr.params.len(), args.len() + 1);
let last_param = instr.params.last().unwrap();
assert!(last_param.param_type.is_none());
assert!(last_param.assignment_reg.0.is_none());
assert!(last_param.assignment_reg.1 == Some(assign_reg));
assert_eq!(instr.outputs.len(), 1);
let output = instr.outputs[0].clone();
assert!(
output == assign_reg,
"{} vs {} in {}",
output,
assign_reg,
instr_name
);
let mut args = args;
args.push(direct_reference(write_regs.first().unwrap().clone()));
@@ -303,43 +332,50 @@ impl ASMPILConverter {
fn handle_instruction(&mut self, instr_name: String, args: Vec<Expression>) {
let instr = &self.instructions[&instr_name];
assert_eq!(instr.params.len(), args.len());
let mut value = BTreeMap::new();
let mut instruction_literal_args = vec![];
let mut write_regs = BTreeMap::new();
for (p, a) in instr.params.iter().zip(args) {
// TODO literal arguments can actually only be passed in.
if p.assignment_reg.0.is_some() {
// We read a value into the assignment register "reg".
let reg = p.assignment_reg.0.as_ref().unwrap().as_ref();
assert!(reg.is_some());
assert!(!value.contains_key(reg.unwrap()));
value.insert(reg.unwrap().clone(), self.process_assignment_value(a));
instruction_literal_args.push(None);
} else if p.assignment_reg.1.is_some() {
assert_eq!(instr.inputs.len() + instr.outputs.len(), args.len());
let mut args = args.into_iter();
let (value, instruction_literal_args): (BTreeMap<_, _>, Vec<_>) =
instr.inputs.iter().zip(&mut args).fold(
Default::default(),
|(mut value, mut instruction_literal_arg), (input, a)| {
match input {
Input::Register(reg) => {
// We read a value into the assignment register "reg".
assert!(!value.contains_key(reg));
value.insert(reg.clone(), self.process_assignment_value(a));
}
Input::Label(_) => {
if let Expression::PolynomialReference(r) = a {
instruction_literal_arg.push(r.name);
} else {
panic!();
}
}
};
(value, instruction_literal_arg)
},
);
let write_regs: BTreeMap<_, _> = instr
.outputs
.iter()
.zip(&mut args)
.map(|(reg, a)| {
// Output a value trough assignment register "reg"
let reg = p.assignment_reg.1.as_ref().unwrap().as_ref();
assert!(reg.is_some());
if let Expression::PolynomialReference(r) = a {
assert!(!r.next);
assert!(r.index.is_none());
assert!(!write_regs.contains_key(&r.name));
write_regs.insert(reg.unwrap().clone(), vec![r.name.clone()]);
(reg.clone(), vec![r.name])
} else {
panic!("Expected direct register to assign to in instruction call.");
}
instruction_literal_args.push(None);
} else if p.param_type == Some("label".to_string()) {
if let Expression::PolynomialReference(r) = a {
instruction_literal_args.push(Some(r.name.clone()))
} else {
panic!();
}
} else {
todo!("Param type not supported.");
}
}
assert_eq!(instruction_literal_args.len(), instr.params.len());
})
.collect();
assert_eq!(write_regs.len(), instr.outputs.len());
self.code_lines.push(CodeLine {
write_regs,
instruction: Some(instr_name.to_string()),
@@ -548,14 +584,11 @@ impl ASMPILConverter {
for (arg, param) in line
.instruction_literal_args
.iter()
.zip(&self.instructions[instr].params)
.zip(self.instructions[instr].labels())
{
if let Some(arg) = arg {
// TODO has to be label for now
program_constants
.get_mut(&format!("p_instr_{instr}_param_{}", param.name))
.unwrap()[i] = (label_positions[arg] as i64).into();
}
program_constants
.get_mut(&format!("p_instr_{instr}_param_{}", param.clone()))
.unwrap()[i] = (label_positions[arg] as i64).into();
}
} else {
assert!(line.instruction_literal_args.is_empty());
@@ -661,8 +694,23 @@ impl Register {
}
}
enum Input {
Register(String),
Label(String),
}
struct Instruction {
params: Vec<InstructionParam>,
inputs: Vec<Input>,
outputs: Vec<String>,
}
impl Instruction {
fn labels(&self) -> impl Iterator<Item = &String> {
self.inputs.iter().filter_map(|input| match input {
Input::Label(label) => Some(label),
_ => None,
})
}
}
// TODO turn this into an enum, split into
@@ -677,7 +725,7 @@ struct CodeLine {
label: Option<String>,
instruction: Option<String>,
// TODO we only support labels for now.
instruction_literal_args: Vec<Option<String>>,
instruction_literal_args: Vec<String>,
}
enum AffineExpressionComponent {

31
src/parser/asm_ast.rs
View File

@@ -5,6 +5,29 @@ use super::ast::{Expression, SelectedExpressions, Statement};
#[derive(Debug, PartialEq, Eq)]
pub struct ASMFile(pub Vec<ASMStatement>);
#[derive(Debug, PartialEq, Eq, Clone)]
pub struct InstructionParamList {
pub params: Vec<InstructionParam>,
}
impl InstructionParamList {
pub fn new(params: Vec<InstructionParam>) -> Self {
Self { params }
}
}
#[derive(Debug, PartialEq, Eq, Clone)]
pub struct InstructionParams {
pub inputs: InstructionParamList,
pub outputs: Option<InstructionParamList>,
}
impl InstructionParams {
pub fn new(inputs: InstructionParamList, outputs: Option<InstructionParamList>) -> Self {
Self { inputs, outputs }
}
}
#[derive(Debug, PartialEq, Eq, Clone)]
pub enum ASMStatement {
Degree(usize, AbstractNumberType),
@@ -12,7 +35,7 @@ pub enum ASMStatement {
InstructionDeclaration(
usize,
String,
Vec<InstructionParam>,
InstructionParams,
Vec<InstructionBodyElement>,
),
InlinePil(usize, Vec<Statement>),
@@ -30,11 +53,7 @@ pub enum RegisterFlag {
#[derive(Debug, PartialEq, Eq, Clone)]
pub struct InstructionParam {
pub name: String,
pub param_type: Option<String>,
/// Which register this parameter is passed in (first) and out (second).
/// It is a double option, because the arrow can be optional and the
/// assign register inside the arrow is optional as well.
pub assignment_reg: (Option<Option<String>>, Option<Option<String>>),
pub ty: Option<String>,
}
#[derive(Debug, PartialEq, Eq, Clone)]

19
src/parser/powdr.lalrpop
View File

@@ -173,7 +173,7 @@ RegisterFlag: RegisterFlag = {
}
InstructionDeclaration: ASMStatement = {
<@L> "instr" <Identifier> <InstructionParamList> "{" <InstructionBodyElements> "}" => ASMStatement::InstructionDeclaration(<>)
<@L> "instr" <Identifier> <InstructionParams> "{" <InstructionBodyElements> "}" => ASMStatement::InstructionDeclaration(<>)
}
InstructionBodyElements: Vec<InstructionBodyElement> = {
@@ -194,14 +194,21 @@ PlookupOperator: PlookupOperator = {
"is" => PlookupOperator::Is,
}
InstructionParamList: Vec<InstructionParam> = {
=> vec![],
<mut list:( <InstructionParam> "," )*> <end:InstructionParam> => { list.push(end); list }
InstructionParams: InstructionParams = {
<_input: InstructionParamList> "->" <output: InstructionParamList> => InstructionParams::new(_input, Some(output)),
// we can ommit the arrow if there are no outputs
<_input: InstructionParamList> => InstructionParams::new(_input, None)
}
InstructionParamList: InstructionParamList = {
=> InstructionParamList::new(vec![]),
<mut list:( <InstructionParam> "," )*> <end:InstructionParam> => { list.push(end); InstructionParamList::new(list) }
}
InstructionParam: InstructionParam = {
<assign_read:AssignOperator?> <name: Identifier> <param_type:(":" <Identifier>)?> <assign_write:AssignOperator?> =>
InstructionParam{name, param_type, assignment_reg: (assign_read, assign_write)}
<name: Identifier> <ty:(":" <Identifier>)?> =>
InstructionParam{name, ty}
}
InlinePil: ASMStatement = {

20
src/riscv/compiler.rs
View File

@@ -110,8 +110,8 @@ pil{
// ============== memory instructions ==============
instr mstore <=X= val { { addr, STEP, X } is m_is_write { m_addr, m_step, m_value } }
instr mload r <=X= { { addr, STEP, X } is m_is_read { m_addr, m_step, m_value } }
instr mstore X { { addr, STEP, X } is m_is_write { m_addr, m_step, m_value } }
instr mload -> X { { addr, STEP, X } is m_is_read { m_addr, m_step, m_value } }
// ============== control-flow instructions ==============
@@ -119,23 +119,23 @@ instr jump l: label { pc' = l }
instr call l: label { pc' = l, x1' = pc + 1, x6' = l }
instr ret { pc' = x1 }
instr branch_if_nonzero <=X= c, l: label { pc' = (1 - XIsZero) * l + XIsZero * (pc + 1) }
instr branch_if_zero <=X= c, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) }
instr branch_if_nonzero X, l: label { pc' = (1 - XIsZero) * l + XIsZero * (pc + 1) }
instr branch_if_zero X, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) }
// input X is required to be the difference of two 32-bit unsigend values.
// i.e. -2**32 < X < 2**32
instr branch_if_positive <=X= c, l: label {
instr branch_if_positive X, l: label {
X + 2**32 - 1 = X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000 + wrap_bit * 2**32,
pc' = wrap_bit * l + (1 - wrap_bit) * (pc + 1)
}
// ================= logical instructions =================
instr is_equal_zero <=X= v, t <=Y= { Y = XIsZero }
instr is_equal_zero X -> Y { Y = XIsZero }
// ================= arith/bitwise instructions =================
// instr xor <=X= a, <=Y= b, c <=Z= {
// instr xor X, Y, Z {
// {X, Y, Z} in 1 { binary.X, binary.Y, binary.RESULT, 1 }
// }
// we wanted better synatx: { binary(X, Y, Z) }
@@ -145,9 +145,7 @@ instr is_equal_zero <=X= v, t <=Y= { Y = XIsZero }
// Wraps a value in Y to 32 bits.
// Requires 0 <= Y < 2**33
// TODO we need better syntax for defining instructions that are functions.
// Maybe like instr wrap <=Y= v -> X { Y = X + wrap_bit * 2**32, X = Xhi * 2**16 + Xlo }
instr wrap <=Y= v, x <=X= { Y = X + wrap_bit * 2**32, X = X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000 }
instr wrap Y -> X { Y = X + wrap_bit * 2**32, X = X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000 }
pil{
col fixed bytes(i) { i & 0xff };
col witness X_b1;
@@ -168,7 +166,7 @@ instr fail { 1 = 0 }
// Removes up to 16 bits beyond 32
// TODO is this really safe?
instr wrap16 <=Y= v, t <=X= { Y = Y_b5 * 2**32 + Y_b6 * 2**40 + X, X = X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000 }
instr wrap16 Y -> X { Y = Y_b5 * 2**32 + Y_b6 * 2**40 + X, X = X_b1 + X_b2 * 0x100 + X_b3 * 0x10000 + X_b4 * 0x1000000 }
pil{
col witness Y_b5;
col witness Y_b6;

6
tests/asm_data/bit_access.asm
View File

@@ -14,9 +14,7 @@ pil{
// Wraps a value in Y to 32 bits.
// Requires 0 <= Y < 2**33
// TODO we need better syntax for defining instructions that are functions.
// Maybe like instr wrap <=Y= v -> X { Y = X + wrap_bit * 2**32, X = Xhi * 2**16 + Xlo }
instr wrap <=Y= v, x <=X= { Y = X + wrap_bit * 2**32, X = XB1 + 0x100 * XB2 + 0x10000 * XB3 + 0x1000000 * XB4 }
instr wrap Y -> X { Y = X + wrap_bit * 2**32, X = XB1 + 0x100 * XB2 + 0x10000 * XB3 + 0x1000000 * XB4 }
pil{
col fixed BYTE(i) { i & 0xff };
col witness XB1;
@@ -31,7 +29,7 @@ pil{
wrap_bit * (1 - wrap_bit) = 0;
}
instr assert_zero <=X= a { XIsZero = 1 }
instr assert_zero X { XIsZero = 1 }
B <=X= ${ ("input", 0) };
wrap B + 0xffffffec, A;

6
tests/asm_data/functional_instructions.asm
View File

@@ -15,9 +15,7 @@ pil{
// Wraps a value in Y to 32 bits.
// Requires 0 <= Y < 2**33
// TODO we need better syntax for defining instructions that are functions.
// Maybe like instr wrap <=Y= v -> X { Y = X + wrap_bit * 2**32, X = Xhi * 2**16 + Xlo }
instr wrap <=Y= v, x <=X= { Y = X + wrap_bit * 2**32, X = XB1 + 0x100 * XB2 + 0x10000 * XB3 + 0x1000000 * XB4 }
instr wrap Y -> X { Y = X + wrap_bit * 2**32, X = XB1 + 0x100 * XB2 + 0x10000 * XB3 + 0x1000000 * XB4 }
pil{
col fixed BYTES(i) { i & 0xff };
col commit XB1;
@@ -32,7 +30,7 @@ pil{
wrap_bit * (1 - wrap_bit) = 0;
}
instr assert_zero <=X= a { XIsZero = 1 }
instr assert_zero X { XIsZero = 1 }
B <=X= ${ ("input", 0) };
A <=X= wrap(B + 0xffffffec);

6
tests/asm_data/mem_read_write.asm
View File

@@ -60,9 +60,9 @@ pil{
}
instr assert_zero <=X= a { XIsZero = 1 }
instr mstore <=X= val { { ADDR, STEP, X } is m_is_write { m_addr, m_step, m_value } }
instr mload r <=X= { { ADDR, STEP, X } is m_is_read { m_addr, m_step, m_value } }
instr assert_zero X { XIsZero = 1 }
instr mstore X { { ADDR, STEP, X } is m_is_write { m_addr, m_step, m_value } }
instr mload -> X { { ADDR, STEP, X } is m_is_read { m_addr, m_step, m_value } }
ADDR <=X= 3;

2
tests/asm_data/multi_assign.asm
View File

@@ -11,7 +11,7 @@ pil{
XIsZero * (1 - XIsZero) = 0;
}
instr assert_zero <=X= a { XIsZero = 1 }
instr assert_zero X { XIsZero = 1 }
A <=X= ${ ("input", 0) };
A <=Y= A - 7;

8
tests/asm_data/palindrome.asm
View File

@@ -32,13 +32,13 @@ pil{
NOTLAST { m_addr' - m_addr } in POSITIVE;
}
instr jmpz <=X= c, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) }
instr jmpz X, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) }
instr jmp l: label { pc' = l }
instr assert_zero <=X= a { XIsZero = 1 }
instr mstore <=X= val { { ADDR, X } in { m_addr, m_value } }
instr assert_zero X { XIsZero = 1 }
instr mstore X { { ADDR, X } in { m_addr, m_value } }
// TODO instructions that return values are currently rather clumsy.
// We should replace them by some function notion instead.
instr mload r <=X= { { ADDR, X } in { m_addr, m_value } }
instr mload -> X { { ADDR, X } in { m_addr, m_value } }
CNT <=X= ${ ("input", 0) };
ADDR <=X= 0;

4
tests/asm_data/simple_sum.asm
View File

@@ -25,10 +25,10 @@ pil{
XIsZero * (1 - XIsZero) = 0;
}
instr jmpz <=X= c, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) }
instr jmpz X, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) }
instr jmp l: label { pc' = l }
instr dec_CNT { CNT' = CNT - 1 }
instr assert_zero <=X= a { XIsZero = 1 }
instr assert_zero X { XIsZero = 1 }
CNT <=X= ${ ("input", 1) };