Skip to content

Commit

Permalink
Support degree ranges (#1667)
Browse files Browse the repository at this point in the history
We currently hardcode the range of degrees that variable degree machines
are preprocessed for. Expose that in machines instead.

This changes pil namespaces to accept a min and max degree:
```
namespace main(123..456);
namespace main(5); // allowed for backward compatibility, translates to `5..5`
```

It adds two new builtins:
```
std::prover::min_degree
std::prover::max_degree
```

And sets the behavior of the `std::prover::degree` builtin to only
succeed if `min_degree` and `max_degree` are equal.
  • Loading branch information
Schaeff authored Sep 3, 2024
1 parent ecf5535 commit 7f259b4
Show file tree
Hide file tree
Showing 43 changed files with 573 additions and 304 deletions.
28 changes: 26 additions & 2 deletions analysis/src/machine_check.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@ use powdr_ast::{
asm_analysis::{
AnalysisASMFile, AssignmentStatement, CallableSymbolDefinitions, DebugDirective,
FunctionBody, FunctionStatements, FunctionSymbol, InstructionDefinitionStatement,
InstructionStatement, Item, LabelStatement, LinkDefinition, Machine, OperationSymbol,
RegisterDeclarationStatement, RegisterTy, Return, SubmachineDeclaration,
InstructionStatement, Item, LabelStatement, LinkDefinition, Machine, MachineDegree,
OperationSymbol, RegisterDeclarationStatement, RegisterTy, Return, SubmachineDeclaration,
},
parsed::{
self,
Expand Down Expand Up @@ -172,11 +172,35 @@ impl TypeChecker {

let MachineProperties {
degree,
min_degree,
max_degree,
latch,
operation_id,
call_selectors,
} = machine.properties;

let degree = match (degree, min_degree, max_degree) {
(Some(d), None, None) => MachineDegree {
min: Some(d.clone()),
max: Some(d),
},
(Some(d), Some(_), _) => {
errors.push("Machine {ctx} should not have a min_degree if it has a degree".into());
MachineDegree {
min: Some(d.clone()),
max: Some(d),
}
}
(Some(d), _, Some(_)) => {
errors.push("Machine {ctx} should not have a max_degree if it has a degree".into());
MachineDegree {
min: Some(d.clone()),
max: Some(d),
}
}
(None, min, max) => MachineDegree { min, max },
};

if !registers.iter().any(|r| r.ty.is_pc()) {
let operation_count = callable.operation_definitions().count();
if operation_count > 0 && latch.is_none() {
Expand Down
17 changes: 9 additions & 8 deletions asm-to-pil/src/vm_to_constrained.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ use powdr_ast::{
asm_analysis::{
combine_flags, AssignmentStatement, Batch, CallableSymbol, CallableSymbolDefinitions,
DebugDirective, FunctionStatement, InstructionDefinitionStatement, InstructionStatement,
LabelStatement, LinkDefinition, Machine, OperationSymbol, RegisterDeclarationStatement,
RegisterTy, Rom,
LabelStatement, LinkDefinition, Machine, MachineDegree, OperationSymbol,
RegisterDeclarationStatement, RegisterTy, Rom,
},
parsed::{
self,
Expand Down Expand Up @@ -62,12 +62,12 @@ pub const ROM_SUBMACHINE_NAME: &str = "_rom";
const ROM_ENTRY_POINT: &str = "get_line";

fn rom_machine<'a>(
degree: Expression,
degree: MachineDegree,
mut pil: Vec<PilStatement>,
mut line_lookup: impl Iterator<Item = &'a str>,
) -> Machine {
Machine {
degree: Some(degree),
degree,
operation_id: Some(ROM_OPERATION_ID.into()),
latch: Some(ROM_LATCH.into()),
pil: {
Expand Down Expand Up @@ -283,10 +283,11 @@ impl<T: FieldElement> VMConverter<T> {
// This is hacky: in the absence of proof objects, we want to support both monolithic proofs and composite proofs.
// In the monolithic case, all degrees must be the same, so we align the degree of the rom to that of the vm.
// In the composite case, we set the minimum degree for the rom, which is the number of lines in the code.
let rom_degree = input
.degree
.clone()
.unwrap_or_else(|| Expression::from(self.code_lines.len().next_power_of_two() as u32));
// this can lead to false negatives as we apply expression equality here, so `4` and `2 + 2` would be considered different.
let rom_degree = match input.degree.is_static() {
true => input.degree.clone(),
false => Expression::from(self.code_lines.len().next_power_of_two() as u32).into(),
};

(
input,
Expand Down
11 changes: 10 additions & 1 deletion ast/src/analyzed/display.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,11 +20,20 @@ use self::parsed::{

use super::*;

impl Display for DegreeRange {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
match (self.min, self.max) {
(min, max) if min == max => write!(f, "{min}"),
(min, max) => write!(f, "{min}..{max}"),
}
}
}

impl<T: Display> Display for Analyzed<T> {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
let (mut current_namespace, mut current_degree) = (AbsoluteSymbolPath::default(), None);
let mut update_namespace =
|name: &str, degree: Option<DegreeType>, f: &mut Formatter<'_>| {
|name: &str, degree: Option<DegreeRange>, f: &mut Formatter<'_>| {
let mut namespace =
AbsoluteSymbolPath::default().join(SymbolPath::from_str(name).unwrap());
let name = namespace.pop().unwrap();
Expand Down
77 changes: 74 additions & 3 deletions ast/src/analyzed/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -59,13 +59,23 @@ impl<T> Analyzed<T> {
.unique()
.exactly_one()
.unwrap()
.try_into_unique()
.unwrap()
}

pub fn degree_ranges(&self) -> HashSet<DegreeRange> {
self.definitions
.values()
.filter_map(|(symbol, _)| symbol.degree)
.collect::<HashSet<_>>()
}

/// Returns the set of all explicit degrees in this [`Analyzed<T>`].
pub fn degrees(&self) -> HashSet<DegreeType> {
self.definitions
.values()
.filter_map(|(symbol, _)| symbol.degree)
.map(|d| d.try_into_unique().unwrap())
.collect::<HashSet<_>>()
}

Expand Down Expand Up @@ -495,15 +505,53 @@ pub fn type_from_definition(
}
}

#[derive(PartialEq, Eq, Hash, Debug, Clone, Serialize, Deserialize, JsonSchema, Copy)]
pub struct DegreeRange {
pub min: DegreeType,
pub max: DegreeType,
}

impl From<DegreeType> for DegreeRange {
fn from(value: DegreeType) -> Self {
Self {
min: value,
max: value,
}
}
}

impl DegreeRange {
pub fn try_into_unique(self) -> Option<DegreeType> {
(self.min == self.max).then_some(self.min)
}

/// Iterate through powers of two in this range
pub fn iter(&self) -> impl Iterator<Item = DegreeType> {
let min_ceil = self.min.next_power_of_two();
let max_ceil = self.max.next_power_of_two();
let min_log = usize::BITS - min_ceil.leading_zeros() - 1;
let max_log = usize::BITS - max_ceil.leading_zeros() - 1;
(min_log..=max_log).map(|exponent| 1 << exponent)
}

/// Fit a degree to this range:
/// - returns the smallest value in the range which is larger or equal to `new_degree`
/// - panics if no such value exists
pub fn fit(&self, new_degree: u64) -> u64 {
assert!(new_degree <= self.max);
self.min.max(new_degree)
}
}

#[derive(Debug, Clone, Serialize, Deserialize, JsonSchema)]
pub struct Symbol {
pub id: u64,
pub source: SourceRef,
pub absolute_name: String,
pub stage: Option<u32>,
pub kind: SymbolKind,
pub length: Option<DegreeType>,
pub degree: Option<DegreeType>,
pub length: Option<u64>,
pub degree: Option<DegreeRange>,
}

impl Symbol {
Expand Down Expand Up @@ -1306,9 +1354,10 @@ impl Display for PolynomialType {

#[cfg(test)]
mod tests {
use powdr_number::DegreeType;
use powdr_parser_util::SourceRef;

use crate::analyzed::{AlgebraicReference, PolyID, PolynomialType};
use crate::analyzed::{AlgebraicReference, DegreeRange, PolyID, PolynomialType};

use super::{AlgebraicExpression, Analyzed};

Expand Down Expand Up @@ -1380,4 +1429,26 @@ mod tests {
let expr = column.clone() * column.clone() * column.clone();
assert_eq!(expr.degree(), 3);
}

#[test]
fn degree_range() {
assert_eq!(
DegreeRange { min: 4, max: 4 }.iter().collect::<Vec<_>>(),
vec![4]
);
assert_eq!(
DegreeRange { min: 4, max: 16 }.iter().collect::<Vec<_>>(),
vec![4, 8, 16]
);
assert_eq!(
DegreeRange { min: 3, max: 15 }.iter().collect::<Vec<_>>(),
vec![4, 8, 16]
);
assert_eq!(
DegreeRange { min: 15, max: 3 }
.iter()
.collect::<Vec<DegreeType>>(),
Vec::<DegreeType>::new()
);
}
}
29 changes: 23 additions & 6 deletions ast/src/asm_analysis/display.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ use super::{
AnalysisASMFile, AssignmentStatement, CallableSymbol, CallableSymbolDefinitionRef,
DebugDirective, FunctionBody, FunctionStatement, FunctionStatements, Incompatible,
IncompatibleSet, InstructionDefinitionStatement, InstructionStatement, Item, LabelStatement,
LinkDefinition, Machine, RegisterDeclarationStatement, RegisterTy, Return, Rom,
LinkDefinition, Machine, MachineDegree, RegisterDeclarationStatement, RegisterTy, Return, Rom,
SubmachineDeclaration,
};

Expand Down Expand Up @@ -76,13 +76,30 @@ impl Display for AnalysisASMFile {
}
}

impl Display for MachineDegree {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
match (&self.min, &self.max) {
(Some(min), Some(max)) if min == max => write!(f, "degree: {min}"),
(min, max) => write!(
f,
"{}",
min.iter()
.map(|min_degree| format!("min_degree: {min_degree}"))
.chain(
max.iter()
.map(|max_degree| format!("max_degree: {max_degree}")),
)
.collect::<Vec<_>>()
.join(", ")
),
}
}
}

impl Display for Machine {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
let props = self
.degree
.as_ref()
.map(|s| format!("degree: {s}"))
.into_iter()
let props = std::iter::once(&self.degree)
.map(|d| format!("{d}"))
.chain(self.latch.as_ref().map(|s| format!("latch: {s}")))
.chain(
self.operation_id
Expand Down
28 changes: 25 additions & 3 deletions ast/src/asm_analysis/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -697,10 +697,32 @@ impl Item {
}
}

#[derive(Clone, Default, Debug)]
#[derive(Default, Debug, PartialEq, Eq, PartialOrd, Ord, Clone)]
pub struct MachineDegree {
pub min: Option<Expression>,
pub max: Option<Expression>,
}

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

impl From<Expression> for MachineDegree {
fn from(value: Expression) -> Self {
Self {
min: Some(value.clone()),
max: Some(value),
}
}
}

#[derive(Clone, Debug, Default)]
pub struct Machine {
/// The degree if any, i.e. the number of rows in instances of this machine type
pub degree: Option<Expression>,
/// The degree i.e. the number of rows in instances of this machine type
pub degree: MachineDegree,
/// The latch, i.e. the boolean column whose values must be 1 in order for this machine to be accessed. Must be defined in one of the constraint blocks of this machine.
pub latch: Option<String>,
/// The operation id, i.e. the column whose values determine which operation is being invoked in the current block. Must be defined in one of the constraint blocks of this machine.
Expand Down
4 changes: 1 addition & 3 deletions ast/src/object/display.rs
Original file line number Diff line number Diff line change
Expand Up @@ -43,9 +43,7 @@ impl Display for PILGraph {

impl Display for Object {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
if let Some(degree) = self.degree.as_ref() {
writeln!(f, "// Degree {degree}")?;
}
writeln!(f, "// Degree {}", self.degree)?;
for s in &self.pil {
writeln!(f, "{s}")?;
}
Expand Down
18 changes: 7 additions & 11 deletions ast/src/object/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,12 @@ use std::collections::BTreeMap;

use powdr_number::BigUint;

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

mod display;
Expand Down Expand Up @@ -52,7 +55,7 @@ pub enum TypeOrExpression {

#[derive(Default, Clone)]
pub struct Object {
pub degree: Option<Expression>,
pub degree: MachineDegree,
/// the pil identities for this machine
pub pil: Vec<PilStatement>,
/// the links from this machine to its children
Expand All @@ -65,13 +68,6 @@ pub struct Object {
pub has_pc: bool,
}

impl Object {
pub fn with_degree<D: Into<Expression>>(mut self, degree: Option<D>) -> Self {
self.degree = degree.map(Into::into);
self
}
}

#[derive(Clone, Debug)]
/// A link between two machines
pub struct Link {
Expand Down
12 changes: 12 additions & 0 deletions ast/src/parsed/asm.rs
Original file line number Diff line number Diff line change
Expand Up @@ -440,6 +440,8 @@ impl MachineParams {
#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Default, Clone)]
pub struct MachineProperties {
pub degree: Option<Expression>,
pub min_degree: Option<Expression>,
pub max_degree: Option<Expression>,
pub latch: Option<String>,
pub operation_id: Option<String>,
pub call_selectors: Option<String>,
Expand All @@ -463,6 +465,16 @@ impl MachineProperties {
already_defined = true;
}
}
"min_degree" => {
if props.min_degree.replace(value).is_some() {
already_defined = true;
}
}
"max_degree" => {
if props.max_degree.replace(value).is_some() {
already_defined = true;
}
}
"latch" => {
let id = value.try_to_identifier().ok_or_else(|| {
source_ref.with_error(format!(
Expand Down
Loading

0 comments on commit 7f259b4

Please sign in to comment.