Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[WIP] Mandatory degree #2097

Closed
wants to merge 2 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 29 additions & 4 deletions airgen/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,11 @@
use std::collections::BTreeMap;

use powdr_ast::{
asm_analysis::{self, combine_flags, AnalysisASMFile, LinkDefinition, MachineDegree},
asm_analysis::{self, combine_flags, AnalysisASMFile, LinkDefinition},
object::{Link, LinkFrom, LinkTo, Location, Machine, MachineInstanceGraph, Object, Operation},
parsed::{
asm::{parse_absolute_path, AbsoluteSymbolPath, CallableRef, MachineParams},
Expression, PilStatement,
Expression, NamespaceDegree, PilStatement,
},
};

Expand All @@ -18,6 +18,8 @@ use itertools::Itertools;

use powdr_analysis::utils::parse_pil_statement;

use powdr_number::BigUint;

const MAIN_MACHINE: &str = "::Main";
const MAIN_FUNCTION: &str = "main";

Expand All @@ -41,10 +43,24 @@ pub fn compile(input: AnalysisASMFile) -> MachineInstanceGraph {
operation_id: None,
call_selectors: None,
};
let zero_expr = Expression::from(BigUint::from(0u8));
let degree = NamespaceDegree {
min: zero_expr.clone(),
max: zero_expr,
};

let obj: Object = Object {
degree,
pil: Default::default(),
links: Default::default(),
latch: Default::default(),
call_selectors: Default::default(),
has_pc: Default::default(),
};
return MachineInstanceGraph {
main,
entry_points: Default::default(),
objects: [(main_location, Default::default())].into(),
objects: [(main_location, obj)].into(),
statements: module_level_pil_statements(input),
};
}
Expand Down Expand Up @@ -301,7 +317,16 @@ impl<'a> ASMPILConverter<'a> {
// the passed degrees have priority over the ones defined in the machine type
let min = instance.min_degree.clone().or(input.degree.min);
let max = instance.max_degree.clone().or(input.degree.max);
let degree = MachineDegree { min, max };
let degree = NamespaceDegree {
min: min.expect(&format!(
"No min_degree set for machine instance {}",
self.location
)),
max: max.expect(&format!(
"No max_degree set for machine instance {}",
self.location
)),
};

self.submachines = input
.submachines
Expand Down
13 changes: 5 additions & 8 deletions ast/src/object/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,9 @@ use std::collections::BTreeMap;

use powdr_number::BigUint;

use crate::{
asm_analysis::MachineDegree,
parsed::{
asm::{AbsoluteSymbolPath, CallableParams, OperationParams},
Expression, PilStatement,
},
use crate::parsed::{
asm::{AbsoluteSymbolPath, CallableParams, OperationParams},
Expression, NamespaceDegree, PilStatement,
};

mod display;
Expand Down Expand Up @@ -49,9 +46,9 @@ pub struct MachineInstanceGraph {
pub statements: BTreeMap<AbsoluteSymbolPath, Vec<PilStatement>>,
}

#[derive(Default, Clone)]
#[derive(Clone)]
pub struct Object {
pub degree: MachineDegree,
pub degree: NamespaceDegree,
/// the pil identities for this machine
pub pil: Vec<PilStatement>,
/// the links from this machine to its children
Expand Down
7 changes: 7 additions & 0 deletions ast/src/parsed/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,13 @@ pub struct NamespaceDegree {
pub max: Expression,
}

impl NamespaceDegree {
pub fn is_static(&self) -> bool {
// we use expression equality here, so `2 + 2 != 4`
self.min == self.max
}
}

impl Children<Expression> for NamespaceDegree {
fn children(&self) -> Box<dyn Iterator<Item = &Expression> + '_> {
Box::new(once(&self.min).chain(once(&self.max)))
Expand Down
48 changes: 5 additions & 43 deletions linker/src/lib.rs
Original file line number Diff line number Diff line change
@@ -1,51 +1,19 @@
#![deny(clippy::print_stdout)]

use lazy_static::lazy_static;
use powdr_analysis::utils::parse_pil_statement;
use powdr_ast::{
asm_analysis::{combine_flags, MachineDegree},
asm_analysis::combine_flags,
object::{Link, Location, MachineInstanceGraph},
parsed::{
asm::{AbsoluteSymbolPath, SymbolPath},
build::{index_access, lookup, namespaced_reference, permutation, selected},
ArrayLiteral, Expression, NamespaceDegree, PILFile, PilStatement,
ArrayLiteral, PILFile, PilStatement,
},
};
use powdr_parser_util::SourceRef;
use std::{collections::BTreeMap, iter::once};

const MAIN_OPERATION_NAME: &str = "main";
/// The log of the default minimum degree
pub const MIN_DEGREE_LOG: usize = 5;
lazy_static! {
// The maximum degree can add a significant cost during setup, because
// the fixed columns need to be committed to in all sizes up to the max degree.
// This gives the user the possibility to overwrite the default value.
/// The log of the default maximum degree
pub static ref MAX_DEGREE_LOG: usize = {
let default_max_degree_log = 22;

let max_degree_log = match std::env::var("MAX_DEGREE_LOG") {
Ok(val) => val.parse::<usize>().unwrap(),
Err(_) => default_max_degree_log,
};
log::info!("For variably-sized machine, the maximum degree is 2^{max_degree_log}. \
You can set the environment variable MAX_DEGREE_LOG to change this value.");
max_degree_log
};
}

/// Convert a [MachineDegree] into a [NamespaceDegree], setting any unset bounds to the relevant default values
fn to_namespace_degree(d: MachineDegree) -> NamespaceDegree {
NamespaceDegree {
min: d
.min
.unwrap_or_else(|| Expression::from(1 << MIN_DEGREE_LOG)),
max: d
.max
.unwrap_or_else(|| Expression::from(1 << *MAX_DEGREE_LOG)),
}
}

/// The optional degree of the namespace is set to that of the object if it's set, to that of the main object otherwise.
pub fn link(graph: MachineInstanceGraph) -> Result<PILFile, Vec<String>> {
Expand All @@ -69,7 +37,7 @@ pub fn link(graph: MachineInstanceGraph) -> Result<PILFile, Vec<String>> {
pil.push(PilStatement::Namespace(
SourceRef::unknown(),
SymbolPath::from_identifier(location.to_string()),
Some(to_namespace_degree(degree)),
Some(degree),
));

pil.extend(object.pil);
Expand Down Expand Up @@ -240,7 +208,7 @@ mod test {

use pretty_assertions::assert_eq;

use crate::{link, MAX_DEGREE_LOG, MIN_DEGREE_LOG};
use crate::link;

fn parse_analyze_and_compile_file<T: FieldElement>(file: &str) -> MachineInstanceGraph {
let contents = fs::read_to_string(file).unwrap();
Expand Down Expand Up @@ -304,13 +272,7 @@ namespace main__rom(4 + 4);

#[test]
fn compile_really_empty_vm() {
let expectation = format!(
r#"namespace main({}..{});
"#,
1 << MIN_DEGREE_LOG,
1 << *MAX_DEGREE_LOG
);

let expectation = "namespace main(0);\n";
let graph = parse_analyze_and_compile::<GoldilocksField>("");
let pil = link(graph).unwrap();
assert_eq!(extract_main(&format!("{pil}")), expectation);
Expand Down
2 changes: 1 addition & 1 deletion pipeline/tests/asm.rs
Original file line number Diff line number Diff line change
Expand Up @@ -767,7 +767,7 @@ fn types_in_expressions() {
O::A(x) => x,
} = 0
};
machine Main {
machine Main with degree: 64 {
col witness w;
f();
}
Expand Down
2 changes: 1 addition & 1 deletion pipeline/tests/powdr_std.rs
Original file line number Diff line number Diff line change
Expand Up @@ -413,7 +413,7 @@ fn sort() {
vec![8, 0, 9, 20, 23, 88, 14, -9],
];
let code =
"let test_sort: int[] -> int[] = |x| std::array::sort(x, |a, b| a < b); machine Main { }"
"let test_sort: int[] -> int[] = |x| std::array::sort(x, |a, b| a < b); machine Main with degree: 1024 { }"
.to_string();
let mut pipeline = Pipeline::<GoldilocksField>::default().from_asm_string(code, None);
let analyzed = pipeline.compute_analyzed_pil().unwrap().clone();
Expand Down
1 change: 0 additions & 1 deletion riscv/src/continuations.rs
Original file line number Diff line number Diff line change
Expand Up @@ -272,7 +272,6 @@ pub fn rust_continuations_dry_run<F: FieldElement>(

let length: usize = match max_degree_expr {
Some(Expression::Number(_, n)) => n.value.clone().try_into().unwrap(),
// if the max degree is not defined, it defaults to `1 << MAX_DEGREE_LOG` which is too large
None => unimplemented!("Continuations rely on `Main` defining a max degree"),
Some(e) => {
unimplemented!("Continuations rely on `Main` not using a complex expression as its max degree, found {e}")
Expand Down
2 changes: 1 addition & 1 deletion test_data/asm/book/instructions.asm
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ machine Main with degree: 32 {
reg C;

// ANCHOR: trivial
SubMachine submachine;
SubMachine submachine(32, 32);

instr add X, Y -> Z link => Z = submachine.add(X, Y); // - trivial usage: only instruction inputs/outputs used in the call
// ANCHOR_END: trivial
Expand Down
2 changes: 1 addition & 1 deletion test_data/asm/book/instructions2.asm
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ machine Main with degree: 16 {
col witness B;
col witness C;

SubMachine submachine;
SubMachine submachine(16, 16);

// multiple links can be activated by a single instruction,
// witness columns can be used for temporary values,
Expand Down
8 changes: 4 additions & 4 deletions test_data/asm/book/modules.asm
Original file line number Diff line number Diff line change
Expand Up @@ -22,16 +22,16 @@ mod utils {

machine Main with degree: 8 {
// use a machine from another module by relative path
my_module::Other a;
my_module::Other a(8, 8);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This started as a one-day-before-the-realease-hack and now it's mandatory?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In my understanding, the hacky part is the syntax around how degrees are passed to sub-machines. I don't think that we want to pass degree ranges is controversial?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For me it is, shouldn't it somehow at least have a default? What do I care about the degree of a sub-machine, unless I already know that I will call it every single row like the memory machine?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it's hard to pick a good default heuristically. It depends on the block size and how often we expect to call the machine, and both the user would know better than us.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Basically,

  • The status quo (pre Remove env var MAX_DEGREE_LOG #2092) is that the default is min_degree: 2**5, max_degree: 2**MAX_DEGREE_LOG, where MAX_DEGREE_LOG is an environment variable. But using env variables is weird.
  • With Remove env var MAX_DEGREE_LOG #2092, we fail if the degree range is unknown after the linker. This is already kind of making it mandatory to set the range, except that we have a strange rule in the linker: If the degree of the main machine is static, use that degree for all sub-machines (even if it's already been set differently). That rule is also weird and should be removed IMO. It also doesn't have any effect if the main machine is dynamically sized, which should be the case in most real-world applications.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The problem I see with having default ones is that only very large defaults are safe enough, but with that you make the life of any user that doesn't need it worse because fixed columns gen and setup time will be massive

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not generate the fixed columns only once they are needed? Because of the verification key?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, exactly, we only know what's needed at runtime, but at that time, we already need to have committed to the fixed columns in all possible sizes.


// use a machine from another module using a local binding
LocalOther b;
LocalOther b(8, 8);

// use a machine from another module defined in a different file
SubmoduleOther c;
SubmoduleOther c(8, 8);

// use a machine from another module defined in a different directory
FolderSubmoduleOther d;
FolderSubmoduleOther d(8, 8);

reg pc[@pc];

Expand Down
4 changes: 2 additions & 2 deletions test_data/asm/book/operations_and_links.asm
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
machine Main with degree: 16 {
Add4 adder;
Add4 adder(16, 16);

reg pc[@pc];
reg X[<=];
Expand All @@ -26,7 +26,7 @@ machine Add4 with
latch: latch,
operation_id: operation_id
{
Add adder;
Add adder(16, 16);

operation add4<0> x, y, z, w -> r;

Expand Down
2 changes: 1 addition & 1 deletion test_data/asm/different_signatures.asm
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
machine Main with degree: 16 {
DifferentSignatures sub;
DifferentSignatures sub(16, 16);

reg pc[@pc];
reg X[<=];
Expand Down
8 changes: 5 additions & 3 deletions test_data/asm/dynamic_vadcop.asm
Original file line number Diff line number Diff line change
Expand Up @@ -13,12 +13,14 @@ machine Byte2 with
col fixed operation_id = [0]*;
}

machine Main {
Arith arith;
let MIN: int = 2**8;
let MAX: int = 2**9;
machine Main with min_degree: MIN, max_degree: MAX {
Arith arith(MIN, MAX);

col fixed STEP(i) { i };
Byte2 byte2;
Memory memory(byte2);
Memory memory(byte2, MIN, MAX);

reg pc[@pc];
reg X[<=];
Expand Down
2 changes: 2 additions & 0 deletions test_data/asm/keccakf.asm
Original file line number Diff line number Diff line change
Expand Up @@ -164,7 +164,9 @@ let main: int, int[], int -> int[] = |W, input, delim| {

// main machine
machine KeccakF with
degree: 8,
latch: LATCH,
degree: 8
{
let x;
let y;
Expand Down
3 changes: 2 additions & 1 deletion test_data/asm/permutations/binary4.asm
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
/// Binary machine that works on chunks of 4 bits,
/// to be used with permutation lookups.
machine Binary4 with
degree: 2**16,
latch: latch,
operation_id: operation_id,
// Allow this machine to be connected via a permutation
Expand Down Expand Up @@ -34,4 +35,4 @@ machine Binary4 with
C' = C * (1 - latch) + C_byte * FACTOR;

[A_byte, B_byte, C_byte] in [P_A, P_B, P_C];
}
}
6 changes: 3 additions & 3 deletions test_data/asm/permutations/block_to_block.asm
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ machine Binary4x with
operation_id: operation_id,
call_selectors: sel,
{
Binary4 bin;
Binary4 bin(256, 256);

operation or4<0> A, B, C, D -> E;

Expand Down Expand Up @@ -40,8 +40,8 @@ machine Main with degree: 256 {
reg A;
reg B;

Binary4 bin;
Binary4x bin4;
Binary4 bin(256, 256);
Binary4x bin4(256, 256);

// two permutations to machine bin
instr or X, Y -> Z link ~> Z = bin.or(X, Y);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ machine Main with degree: 128 {
reg Z[<=];
reg A;

Binary4 bin;
Binary4 bin(128, 128);

// lookup to machine bin
instr or X, Y -> Z link => Z = bin.or(X, Y);
Expand Down
2 changes: 1 addition & 1 deletion test_data/asm/permutations/incoming_needs_selector.asm
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ machine Main with degree: 32 {
reg Z[<=];
reg A;

Binary bin;
Binary bin(32, 32);

// permutation into Binary
instr add X, Y -> Z link ~> Z = bin.add(X, Y);
Expand Down
2 changes: 1 addition & 1 deletion test_data/asm/permutations/link_merging.asm
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ machine Main with degree: 32 {
reg C;
col witness tmp;

SubMachine submachine;
SubMachine submachine(32, 32);

// these are merged into 1 link
instr add X, Y -> Z link => Z = submachine.add(X, Y);
Expand Down
2 changes: 1 addition & 1 deletion test_data/asm/permutations/simple.asm
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ machine Main with degree: 128 {
reg Z[<=];
reg A;

Binary4 bin;
Binary4 bin(128, 128);

// permutation to machine bin
instr or X, Y -> Z link ~> Z = bin.or(X, Y);
Expand Down
2 changes: 1 addition & 1 deletion test_data/asm/permutations/vm_to_block.asm
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ machine Main with degree: 128 {
reg A;
reg B;

Binary4 bin;
Binary4 bin(128, 128);

// two permutations to machine bin
instr or X, Y -> Z link ~> Z = bin.or(X, Y);
Expand Down
Loading
Loading