Skip to content
This repository has been archived by the owner on Nov 4, 2024. It is now read-only.

Padding for chiquito 2024 #265

Merged
merged 11 commits into from
Jul 15, 2024
Merged
Show file tree
Hide file tree
Changes from 4 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
194 changes: 173 additions & 21 deletions src/compiler/compiler.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,13 @@ use crate::{
},
interpreter::InterpreterTraceGenerator,
parser::{
ast::{debug_sym_factory::DebugSymRefFactory, tl::TLDecl, Identifiable, Identifier},
ast::{
debug_sym_factory::DebugSymRefFactory,
expression::Expression,
statement::{Statement, TypedIdDecl},
tl::TLDecl,
DebugSymRef, Identifiable, Identifier,
},
lang::TLDeclsParser,
},
plonkish,
Expand All @@ -21,7 +27,7 @@ use crate::{

use super::{
semantic::{SymTable, SymbolCategory},
setup_inter::{interpret, Setup},
setup_inter::{interpret, MachineSetup, Setup},
Config, Message, Messages,
};

Expand Down Expand Up @@ -63,7 +69,10 @@ pub(super) struct Compiler<F> {

impl<F: Field + Hash> Compiler<F> {
/// Creates a configured compiler.
pub fn new(config: Config) -> Self {
pub fn new(mut config: Config) -> Self {
if config.max_steps == 0 {
config.max_steps = 1000; // TODO: organise this better
leolara marked this conversation as resolved.
Show resolved Hide resolved
}
Compiler {
config,
..Compiler::default()
Expand All @@ -79,6 +88,8 @@ impl<F: Field + Hash> Compiler<F> {
let ast = self
.parse(source, debug_sym_ref_factory)
.map_err(|_| self.messages.clone())?;
let ast = self.add_virtual(ast);
println!("{:?}", ast);
leolara marked this conversation as resolved.
Show resolved Hide resolved
let symbols = self.semantic(&ast).map_err(|_| self.messages.clone())?;
let setup = Self::interpret(&ast, &symbols);
let setup = Self::map_consts(setup);
Expand All @@ -90,8 +101,12 @@ impl<F: Field + Hash> Compiler<F> {
circuit
};

let circuit =
circuit.with_trace(InterpreterTraceGenerator::new(ast, symbols, self.mapping));
let circuit = circuit.with_trace(InterpreterTraceGenerator::new(
ast,
symbols,
self.mapping,
self.config.max_steps,
));

Ok(CompilerResult {
messages: self.messages,
Expand All @@ -117,6 +132,113 @@ impl<F: Field + Hash> Compiler<F> {
}
}

fn add_virtual(
&mut self,
mut ast: Vec<TLDecl<BigInt, Identifier>>,
) -> Vec<TLDecl<BigInt, Identifier>> {
for tldc in ast.iter_mut() {
match tldc {
TLDecl::MachineDecl {
dsym,
id: _,
input_params: _,
output_params,
block,
} => self.add_virtual_to_machine(dsym, output_params, block),
}
}

ast
}

fn add_virtual_to_machine(
&mut self,
dsym: &DebugSymRef,
output_params: &Vec<Statement<BigInt, Identifier>>,
block: &mut Statement<BigInt, Identifier>,
) {
let dsym = DebugSymRef::virt(dsym);
let output_params = Self::get_decls(output_params);

if let Statement::Block(_, stmts) = block {
let mut has_final = false;

for stmt in stmts.iter() {
if let Statement::StateDecl(_, id, _) = stmt
&& id.name() == "final"
{
has_final = true
}
}
if !has_final {
stmts.push(Statement::StateDecl(
dsym.clone(),
Identifier::new("final", dsym.clone()),
Box::new(Statement::Block(dsym.clone(), vec![])),
));
}

let final_state = Self::find_state_mut("final", stmts).unwrap();

let mut padding_transitions = output_params
.iter()
.map(|output_signal| {
Statement::SignalAssignmentAssert(
dsym.clone(),
vec![output_signal.id.next()],
vec![Expression::Query::<BigInt, Identifier>(
dsym.clone(),
output_signal.id.clone(),
)],
)
})
.collect::<Vec<_>>();

padding_transitions.push(Statement::Transition(
dsym.clone(),
Identifier::new("__padding", dsym.clone()),
Box::new(Statement::Block(dsym.clone(), vec![])),
));

Self::add_virtual_to_state(final_state, padding_transitions.clone());

stmts.push(Statement::StateDecl(
dsym.clone(),
Identifier::new("__padding", dsym.clone()),
Box::new(Statement::Block(dsym.clone(), padding_transitions)),
));
} // Semantic analyser must show an error in the else case
}

fn find_state_mut<S: Into<String>>(
state_id: S,
stmts: &mut [Statement<BigInt, Identifier>],
) -> Option<&mut Statement<BigInt, Identifier>> {
let state_id = state_id.into();
let mut final_state: Option<&mut Statement<BigInt, Identifier>> = None;

for stmt in stmts.iter_mut() {
if let Statement::StateDecl(_, id, _) = stmt
&& id.name() == state_id
{
final_state = Some(stmt)
}
}

final_state
}

fn add_virtual_to_state(
state: &mut Statement<BigInt, Identifier>,
add_statements: Vec<Statement<BigInt, Identifier>>,
) {
if let Statement::StateDecl(_, _, final_state_stmts) = state {
if let Statement::Block(_, stmts) = final_state_stmts.as_mut() {
stmts.extend(add_statements)
}
}
}

fn semantic(&mut self, ast: &[TLDecl<BigInt, Identifier>]) -> Result<SymTable, ()> {
let result = super::semantic::analyser::analyse(ast);
let has_errors = result.messages.has_errors();
Expand All @@ -130,26 +252,28 @@ impl<F: Field + Hash> Compiler<F> {
}
}

fn interpret(
ast: &[TLDecl<BigInt, Identifier>],
symbols: &SymTable,
) -> Setup<BigInt, Identifier> {
fn interpret(ast: &[TLDecl<BigInt, Identifier>], symbols: &SymTable) -> Setup<BigInt> {
interpret(ast, symbols)
}

fn map_consts(setup: Setup<BigInt, Identifier>) -> Setup<F, Identifier> {
fn map_consts(setup: Setup<BigInt>) -> Setup<F> {
setup
.iter()
.map(|(machine_id, machine)| {
let new_machine: HashMap<String, Vec<Expr<F, Identifier, ()>>> = machine
.iter()
// let new_machine: MachineSetup<F, Identifier> =
leolara marked this conversation as resolved.
Show resolved Hide resolved

let poly_constraints: HashMap<String, Vec<Expr<F, Identifier, ()>>> = machine
.iter_states_poly_constraints()
.map(|(step_id, step)| {
let new_step = step.iter().map(|pi| Self::map_pi_consts(pi)).collect();
let new_step: Vec<Expr<F, Identifier, ()>> =
step.iter().map(|pi| Self::map_pi_consts(pi)).collect();

(step_id.clone(), new_step)
})
.collect();

let new_machine: MachineSetup<F> =
machine.replace_poly_constraints(poly_constraints);
(machine_id.clone(), new_machine)
})
.collect()
Expand All @@ -169,17 +293,17 @@ impl<F: Field + Hash> Compiler<F> {
}
}

fn build(
&mut self,
setup: &Setup<F, Identifier>,
symbols: &SymTable,
) -> SBPIR<F, NullTraceGenerator> {
fn build(&mut self, setup: &Setup<F>, symbols: &SymTable) -> SBPIR<F, NullTraceGenerator> {
circuit::<F, (), _>("circuit", |ctx| {
for (machine_id, machine) in setup {
self.add_forwards(ctx, symbols, machine_id);
self.add_step_type_handlers(ctx, symbols, machine_id);

for state_id in machine.keys() {
ctx.pragma_num_steps(self.config.max_steps);
ctx.pragma_first_step(self.mapping.get_step_type_handler(machine_id, "initial"));
ctx.pragma_last_step(self.mapping.get_step_type_handler(machine_id, "__padding"));

for state_id in machine.states() {
ctx.step_type_def(
self.mapping.get_step_type_handler(machine_id, state_id),
|ctx| {
Expand Down Expand Up @@ -242,11 +366,15 @@ impl<F: Field + Hash> Compiler<F> {
fn translate_queries(
&mut self,
symbols: &SymTable,
setup: &Setup<F, Identifier>,
setup: &Setup<F>,
machine_id: &str,
state_id: &str,
) -> Vec<Expr<F, Queriable<F>, ()>> {
let exprs = setup.get(machine_id).unwrap().get(state_id).unwrap();
let exprs = setup
.get(machine_id)
.unwrap()
.get_poly_constraints(state_id)
.unwrap();

exprs
.iter()
Expand Down Expand Up @@ -433,6 +561,18 @@ impl<F: Field + Hash> Compiler<F> {
.symbol_uuid
.insert((scope_name, state_id), handler.uuid());
}

// Padding step

let scope_name = format!("//{}", machine_id);
leolara marked this conversation as resolved.
Show resolved Hide resolved
let name = format!("{}:{}", scope_name, "__padding");
let handler = ctx.step_type(&name);
self.mapping
.step_type_handler
.insert(handler.uuid(), handler);
self.mapping
.symbol_uuid
.insert((scope_name, "__padding".to_string()), handler.uuid());
}

fn add_forwards<TG: TraceGenerator<F>>(
Expand Down Expand Up @@ -468,6 +608,18 @@ impl<F: Field + Hash> Compiler<F> {
}
}
}

fn get_decls(stmts: &Vec<Statement<BigInt, Identifier>>) -> Vec<TypedIdDecl<Identifier>> {
let mut result: Vec<TypedIdDecl<Identifier>> = vec![];

for stmt in stmts {
if let Statement::SignalDecl(_, ids) = stmt {
result.extend(ids.clone())
}
}

result
}
}

// Basic signal factory.
Expand Down
7 changes: 7 additions & 0 deletions src/compiler/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ mod setup_inter;
#[derive(Default)]
pub struct Config {
pub(self) max_degree: Option<usize>,
pub(self) max_steps: usize,
}

impl Config {
Expand All @@ -27,6 +28,12 @@ impl Config {

self
}

pub fn max_steps(mut self, steps: usize) -> Self {
self.max_steps = steps;

self
}
}

/// Compiler message.
Expand Down
23 changes: 2 additions & 21 deletions src/compiler/semantic/analyser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -181,25 +181,6 @@ impl Analyser {
} else {
unreachable!("the parser should produce machine declaration with a block");
}

if self
.symbols
.get_symbol(&self.cur_scope, "final".to_string())
.is_none()
{
let id = Identifier("final".to_string(), 0, block.get_dsym());
let stmt = Statement::StateDecl(
block.get_dsym(),
id.clone(),
Box::new(Statement::Block(block.get_dsym(), vec![])),
);

let sym = SymTableEntry::new(id.name(), block.get_dsym(), SymbolCategory::State, None);

RULES.apply_new_symbol_statement(self, &stmt, &id, &sym);

self.symbols.add_symbol(&self.cur_scope, id.name(), sym);
}
}

fn analyse_state(&mut self, id: Identifier, block: Statement<BigInt, Identifier>) {
Expand Down Expand Up @@ -406,7 +387,7 @@ mod test {

assert_eq!(
format!("{:?}", result),
r#"AnalysisResult { symbols: "/": ScopeTable { symbols: "\"fibo\": SymTableEntry { id: \"fibo\", definition_ref: DebugSymRef { line: 2, cols: \"17-21\" }, usages: [], category: Machine, ty: None }", scope: Global },"//fibo": ScopeTable { symbols: "\"a\": SymTableEntry { id: \"a\", definition_ref: DebugSymRef { line: 5, cols: \"20-21\" }, usages: [DebugSymRef { line: 13, cols: \"17-18\" }, DebugSymRef { line: 16, cols: \"15-17\" }, DebugSymRef { line: 23, cols: \"20-21\" }, DebugSymRef { line: 31, cols: \"20-22\" }], category: Signal, ty: Some(\"field\") },\"b\": SymTableEntry { id: \"b\", definition_ref: DebugSymRef { line: 2, cols: \"40-41\" }, usages: [DebugSymRef { line: 13, cols: \"20-21\" }, DebugSymRef { line: 16, cols: \"30-31\" }, DebugSymRef { line: 16, cols: \"19-21\" }, DebugSymRef { line: 23, cols: \"24-25\" }, DebugSymRef { line: 27, cols: \"20-22\" }, DebugSymRef { line: 31, cols: \"42-43\" }, DebugSymRef { line: 31, cols: \"24-26\" }], category: OutputSignal, ty: Some(\"field\") },\"final\": SymTableEntry { id: \"final\", definition_ref: DebugSymRef { start: \"2:50\", end: \"40:13\" }, usages: [DebugSymRef { line: 26, cols: \"18-23\" }], category: State, ty: None },\"i\": SymTableEntry { id: \"i\", definition_ref: DebugSymRef { line: 5, cols: \"30-31\" }, usages: [DebugSymRef { line: 13, cols: \"14-15\" }, DebugSymRef { line: 25, cols: \"17-18\" }, DebugSymRef { line: 27, cols: \"31-32\" }, DebugSymRef { line: 27, cols: \"16-18\" }, DebugSymRef { line: 31, cols: \"35-36\" }, DebugSymRef { line: 31, cols: \"16-18\" }], category: Signal, ty: None },\"initial\": SymTableEntry { id: \"initial\", definition_ref: DebugSymRef { line: 10, cols: \"19-26\" }, usages: [], category: State, ty: None },\"middle\": SymTableEntry { id: \"middle\", definition_ref: DebugSymRef { line: 20, cols: \"19-25\" }, usages: [DebugSymRef { line: 15, cols: \"17-23\" }, DebugSymRef { line: 30, cols: \"18-24\" }], category: State, ty: None },\"n\": SymTableEntry { id: \"n\", definition_ref: DebugSymRef { line: 2, cols: \"29-30\" }, usages: [DebugSymRef { line: 16, cols: \"36-37\" }, DebugSymRef { line: 16, cols: \"23-25\" }, DebugSymRef { line: 25, cols: \"26-27\" }, DebugSymRef { line: 27, cols: \"41-42\" }, DebugSymRef { line: 27, cols: \"24-26\" }, DebugSymRef { line: 31, cols: \"48-49\" }, DebugSymRef { line: 31, cols: \"28-30\" }], category: InputSignal, ty: None }", scope: Machine },"//fibo/final": ScopeTable { symbols: "", scope: State },"//fibo/initial": ScopeTable { symbols: "\"c\": SymTableEntry { id: \"c\", definition_ref: DebugSymRef { line: 11, cols: \"21-22\" }, usages: [DebugSymRef { line: 13, cols: \"23-24\" }, DebugSymRef { line: 16, cols: \"33-34\" }], category: Signal, ty: None }", scope: State },"//fibo/middle": ScopeTable { symbols: "\"c\": SymTableEntry { id: \"c\", definition_ref: DebugSymRef { line: 21, cols: \"21-22\" }, usages: [DebugSymRef { line: 23, cols: \"14-15\" }, DebugSymRef { line: 27, cols: \"38-39\" }, DebugSymRef { line: 31, cols: \"45-46\" }], category: Signal, ty: None }", scope: State }, messages: [] }"#
)
r#"AnalysisResult { symbols: /: ScopeTable { symbols: "fibo: SymTableEntry { id: \"fibo\", definition_ref: nofile:2:17, usages: [], category: Machine, ty: None }", scope: Global },//fibo: ScopeTable { symbols: "a: SymTableEntry { id: \"a\", definition_ref: nofile:5:20, usages: [nofile:13:17, nofile:16:15, nofile:23:20, nofile:31:20], category: Signal, ty: Some(\"field\") },b: SymTableEntry { id: \"b\", definition_ref: nofile:2:40, usages: [nofile:13:20, nofile:16:30, nofile:16:19, nofile:23:24, nofile:27:20, nofile:31:42, nofile:31:24], category: OutputSignal, ty: Some(\"field\") },i: SymTableEntry { id: \"i\", definition_ref: nofile:5:30, usages: [nofile:13:14, nofile:25:17, nofile:27:31, nofile:27:16, nofile:31:35, nofile:31:16], category: Signal, ty: None },initial: SymTableEntry { id: \"initial\", definition_ref: nofile:10:19, usages: [], category: State, ty: None },middle: SymTableEntry { id: \"middle\", definition_ref: nofile:20:19, usages: [nofile:15:17, nofile:30:18], category: State, ty: None },n: SymTableEntry { id: \"n\", definition_ref: nofile:2:29, usages: [nofile:16:36, nofile:16:23, nofile:25:26, nofile:27:41, nofile:27:24, nofile:31:48, nofile:31:28], category: InputSignal, ty: None }", scope: Machine },//fibo/initial: ScopeTable { symbols: "c: SymTableEntry { id: \"c\", definition_ref: nofile:11:21, usages: [nofile:13:23, nofile:16:33], category: Signal, ty: None }", scope: State },//fibo/middle: ScopeTable { symbols: "c: SymTableEntry { id: \"c\", definition_ref: nofile:21:21, usages: [nofile:23:14, nofile:27:38, nofile:31:45], category: Signal, ty: None }", scope: State }, messages: [] }"#
);
}
}
7 changes: 3 additions & 4 deletions src/compiler/semantic/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -156,7 +156,7 @@ impl Debug for ScopeTable {
.symbols
.keys()
.sorted()
.map(|id| format!("\"{}\": {:?}", id, self.symbols[id]))
.map(|id| format!("{}: {:?}", id, self.symbols[id]))
.collect::<Vec<_>>()
.join(",");

Expand Down Expand Up @@ -232,7 +232,7 @@ impl Debug for SymTable {
.scopes
.keys()
.sorted()
.map(|scope| format!("\"{}\": {:?}", scope, self.scopes[scope]))
.map(|scope| format!("{}: {:?}", scope, self.scopes[scope]))
.collect::<Vec<_>>()
.join(",");

Expand Down Expand Up @@ -531,8 +531,6 @@ mod test {
let test_cases = [
(396, "a"),
(397, "a"),
(395, "final"),
(398, "final"),
(460, "a"),
(584, "a"),
(772, "a"),
Expand Down Expand Up @@ -566,6 +564,7 @@ mod test {
];

for (offset, expected_id) in test_cases {
println!("{} {}", offset, expected_id);
let SymTableEntry { id, .. } = result
.symbols
.find_symbol_by_offset("some".to_string(), offset)
Expand Down
Loading
Loading