-
Notifications
You must be signed in to change notification settings - Fork 102
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
Update public examples #2572
base: main
Are you sure you want to change the base?
Update public examples #2572
Changes from all commits
11db74f
041a879
910da15
77c6e7e
6e26390
0f67e0a
5b4d910
f5b059b
e33b47e
04ecf57
f2d01a8
521f0e3
0e5712d
61609f2
1ce0a97
a66328a
e449004
e989f3b
ccfbceb
dcbfa1e
bc8175b
a466877
f28b39c
b5d2f7a
bbb9334
f6eb6e9
7798d19
5cc7e1d
b11d553
0b34bb4
57cec98
9a58980
c78890e
3fc9910
d92168e
50038b4
823d04d
86971c5
346c952
5d623f4
cf87630
189d4c8
e6a6f44
6d993c6
d81a962
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -375,12 +375,22 @@ mod tests { | |
pol fixed FIRST = [1] + [0]*; | ||
pol witness x; | ||
pol witness y; | ||
y * y = y; | ||
y = 1; | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why is this change necessary? It seems like before There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. There are some witgen errors after I added in the public reference constraints. Previously, However, happy to look deeper into this or defer to another PR for a fix if we wonder why There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. No, I think it's fine, just curious :) Thanks! |
||
x' = (1 - FIRST') * (x + 1); | ||
public out0 = x(6); | ||
public out1 = x(7); | ||
public out2 = y(3); | ||
public out3 = y(5); | ||
|
||
pol fixed IS_6 = [0, 0, 0, 0, 0, 0, 1, 0]; | ||
pol fixed IS_7 = [0, 0, 0, 0, 0, 0, 0, 1]; | ||
pol fixed IS_3 = [0, 0, 0, 1, 0, 0, 0, 0]; | ||
pol fixed IS_5 = [0, 0, 0, 0, 0, 1, 0, 0]; | ||
|
||
IS_6 * (x - out0) = 0; | ||
IS_7 * (x - out1) = 0; | ||
IS_3 * (y - out2) = 0; | ||
IS_5 * (y - out3) = 0; | ||
"; | ||
run_test(content); | ||
} | ||
|
@@ -412,6 +422,9 @@ mod tests { | |
x + y = z; | ||
|
||
public outz = z(7); | ||
|
||
col fixed IS_LAST = [0]* + [1]; | ||
IS_LAST * (z - outz) = 0; | ||
"#; | ||
let malicious_publics = Some(vec![0]); | ||
run_test_publics(content, &malicious_publics); | ||
|
@@ -486,6 +499,9 @@ mod tests { | |
x = y + beta * alpha; | ||
|
||
public out = y(N - 1); | ||
|
||
col fixed IS_LAST = [0]* + [1]; | ||
IS_LAST * (y - out) = 0; | ||
"#; | ||
run_test(content); | ||
} | ||
|
Original file line number | Diff line number | Diff line change | ||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
@@ -37,10 +37,11 @@ pub struct RowValues<'a, F> { | |||||||||||||||||
row: usize, | ||||||||||||||||||
} | ||||||||||||||||||
|
||||||||||||||||||
impl<F: std::fmt::Debug> OwnedTerminalValues<F> { | ||||||||||||||||||
impl<F: std::fmt::Debug + Clone> OwnedTerminalValues<F> { | ||||||||||||||||||
pub fn new( | ||||||||||||||||||
pil: &Analyzed<F>, | ||||||||||||||||||
witness_columns: Vec<(String, Vec<F>)>, | ||||||||||||||||||
publics: BTreeMap<String, Option<F>>, | ||||||||||||||||||
fixed_columns: Vec<(String, Vec<F>)>, | ||||||||||||||||||
) -> Self { | ||||||||||||||||||
let mut columns_by_name = witness_columns | ||||||||||||||||||
|
@@ -57,9 +58,13 @@ impl<F: std::fmt::Debug> OwnedTerminalValues<F> { | |||||||||||||||||
.map(|column| (poly_id, column)) | ||||||||||||||||||
}) | ||||||||||||||||||
.collect(); | ||||||||||||||||||
let publics = publics | ||||||||||||||||||
.iter() | ||||||||||||||||||
.map(|(name, value)| (name.clone(), value.clone().unwrap())) | ||||||||||||||||||
.collect(); | ||||||||||||||||||
Comment on lines
+61
to
+64
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
Then you don't need the There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Also, I'm a bit confused, why does it expect an |
||||||||||||||||||
Self { | ||||||||||||||||||
trace, | ||||||||||||||||||
public_values: Default::default(), | ||||||||||||||||||
public_values: publics, | ||||||||||||||||||
challenge_values: Default::default(), | ||||||||||||||||||
} | ||||||||||||||||||
} | ||||||||||||||||||
|
@@ -123,7 +128,7 @@ impl<F: FieldElement, T: From<F>> TerminalAccess<T> for RowValues<'_, F> { | |||||||||||||||||
|
||||||||||||||||||
/// Evaluates an algebraic expression to a value. | ||||||||||||||||||
pub struct ExpressionEvaluator<'a, T, Expr, TA> { | ||||||||||||||||||
terminal_access: TA, | ||||||||||||||||||
pub terminal_access: TA, | ||||||||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
Seems like that change is not needed? |
||||||||||||||||||
intermediate_definitions: &'a BTreeMap<AlgebraicReferenceThin, Expression<T>>, | ||||||||||||||||||
/// Maps intermediate reference to their evaluation. Updated throughout the lifetime of the | ||||||||||||||||||
/// ExpressionEvaluator. | ||||||||||||||||||
|
Original file line number | Diff line number | Diff line change | ||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
@@ -3,7 +3,8 @@ use std::collections::{BTreeMap, HashMap}; | |||||||||||||||||||||||||
use itertools::{Either, Itertools}; | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
use num_traits::One; | ||||||||||||||||||||||||||
use powdr_ast::analyzed::{PolyID, PolynomialType}; | ||||||||||||||||||||||||||
use powdr_ast::analyzed::{AlgebraicExpression, PolyID, PolynomialType}; | ||||||||||||||||||||||||||
use powdr_ast::parsed::visitor::{AllChildren, Children}; | ||||||||||||||||||||||||||
use powdr_number::{DegreeType, FieldElement}; | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
use crate::witgen::data_structures::identity::BusReceive; | ||||||||||||||||||||||||||
|
@@ -42,6 +43,7 @@ pub struct WriteOnceMemory<'a, T: FieldElement> { | |||||||||||||||||||||||||
/// The memory content | ||||||||||||||||||||||||||
data: BTreeMap<DegreeType, Vec<Option<T>>>, | ||||||||||||||||||||||||||
name: String, | ||||||||||||||||||||||||||
public_names: Vec<String>, | ||||||||||||||||||||||||||
} | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
impl<'a, T: FieldElement> WriteOnceMemory<'a, T> { | ||||||||||||||||||||||||||
|
@@ -50,7 +52,13 @@ impl<'a, T: FieldElement> WriteOnceMemory<'a, T> { | |||||||||||||||||||||||||
fixed_data: &'a FixedData<'a, T>, | ||||||||||||||||||||||||||
parts: &MachineParts<'a, T>, | ||||||||||||||||||||||||||
) -> Option<Self> { | ||||||||||||||||||||||||||
if !parts.identities.is_empty() { | ||||||||||||||||||||||||||
// All identities should have a public reference | ||||||||||||||||||||||||||
if !parts.identities.iter().all(|id| { | ||||||||||||||||||||||||||
(*id).children().any(|c| { | ||||||||||||||||||||||||||
c.all_children() | ||||||||||||||||||||||||||
.any(|c| matches!(c, AlgebraicExpression::PublicReference(_))) | ||||||||||||||||||||||||||
}) | ||||||||||||||||||||||||||
}) { | ||||||||||||||||||||||||||
Comment on lines
+55
to
+61
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||||||||||||||||||||||
return None; | ||||||||||||||||||||||||||
} | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
|
@@ -135,6 +143,12 @@ impl<'a, T: FieldElement> WriteOnceMemory<'a, T> { | |||||||||||||||||||||||||
value_polys, | ||||||||||||||||||||||||||
key_to_index, | ||||||||||||||||||||||||||
data: BTreeMap::new(), | ||||||||||||||||||||||||||
public_names: parts | ||||||||||||||||||||||||||
.fixed_data | ||||||||||||||||||||||||||
.analyzed | ||||||||||||||||||||||||||
.public_declarations_in_source_order() | ||||||||||||||||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think this is fragile, because this would include publics of other machines. I opened #2600 as a suggested fix, it also contains the other suggestions to this file. |
||||||||||||||||||||||||||
.map(|(name, _)| name.clone()) | ||||||||||||||||||||||||||
.collect(), | ||||||||||||||||||||||||||
}) | ||||||||||||||||||||||||||
} | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
|
@@ -263,7 +277,8 @@ impl<'a, T: FieldElement> Machine<'a, T> for WriteOnceMemory<'a, T> { | |||||||||||||||||||||||||
&mut self, | ||||||||||||||||||||||||||
_mutable_state: &'b MutableState<'a, T, Q>, | ||||||||||||||||||||||||||
) -> HashMap<String, Vec<T>> { | ||||||||||||||||||||||||||
self.value_polys | ||||||||||||||||||||||||||
let witness = self | ||||||||||||||||||||||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think this change is not necessary? |
||||||||||||||||||||||||||
.value_polys | ||||||||||||||||||||||||||
.iter() | ||||||||||||||||||||||||||
.enumerate() | ||||||||||||||||||||||||||
.map(|(value_index, poly)| { | ||||||||||||||||||||||||||
|
@@ -285,6 +300,42 @@ impl<'a, T: FieldElement> Machine<'a, T> for WriteOnceMemory<'a, T> { | |||||||||||||||||||||||||
(*poly, column) | ||||||||||||||||||||||||||
}) | ||||||||||||||||||||||||||
.map(|(poly_id, column)| (self.fixed_data.column_name(&poly_id).to_string(), column)) | ||||||||||||||||||||||||||
.collect() | ||||||||||||||||||||||||||
.collect(); | ||||||||||||||||||||||||||
witness | ||||||||||||||||||||||||||
} | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
fn take_public_values(&mut self) -> BTreeMap<String, T> { | ||||||||||||||||||||||||||
if self.public_names.is_empty() { | ||||||||||||||||||||||||||
BTreeMap::new() | ||||||||||||||||||||||||||
} else { | ||||||||||||||||||||||||||
let public_values: Vec<_> = self | ||||||||||||||||||||||||||
.value_polys | ||||||||||||||||||||||||||
.iter() | ||||||||||||||||||||||||||
.enumerate() | ||||||||||||||||||||||||||
.flat_map(|(value_index, poly)| { | ||||||||||||||||||||||||||
self.fixed_data.witness_cols[poly] | ||||||||||||||||||||||||||
.external_values | ||||||||||||||||||||||||||
.cloned() | ||||||||||||||||||||||||||
.map(|mut external_values| { | ||||||||||||||||||||||||||
// External witness values might only be provided partially. | ||||||||||||||||||||||||||
external_values.resize(self.degree as usize, T::zero()); | ||||||||||||||||||||||||||
external_values | ||||||||||||||||||||||||||
}) | ||||||||||||||||||||||||||
.unwrap_or_else(|| { | ||||||||||||||||||||||||||
let mut column = vec![T::zero(); 8]; // 8 public values | ||||||||||||||||||||||||||
for (row, values) in self.data.iter() { | ||||||||||||||||||||||||||
column[*row as usize] = values[value_index].unwrap_or_default(); | ||||||||||||||||||||||||||
} | ||||||||||||||||||||||||||
column | ||||||||||||||||||||||||||
}) | ||||||||||||||||||||||||||
}) | ||||||||||||||||||||||||||
.collect(); | ||||||||||||||||||||||||||
|
||||||||||||||||||||||||||
self.public_names | ||||||||||||||||||||||||||
.clone() | ||||||||||||||||||||||||||
.into_iter() | ||||||||||||||||||||||||||
.zip(public_values) | ||||||||||||||||||||||||||
.collect() | ||||||||||||||||||||||||||
} | ||||||||||||||||||||||||||
} | ||||||||||||||||||||||||||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -247,10 +247,11 @@ impl<'a, 'b, T: FieldElement> WitnessGenerator<'a, 'b, T> { | |
let machines = MachineExtractor::new(&fixed).split_out_machines(); | ||
|
||
// Run main machine and extract columns from all machines. | ||
let (columns, _publics) = | ||
let (columns, publics) = | ||
MutableState::new(machines.into_iter(), &self.query_callback).run(); | ||
|
||
let publics = extract_publics(&columns, self.analyzed); | ||
let publics = extract_publics(publics, self.analyzed); | ||
|
||
Comment on lines
-250
to
+254
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The key change is that publics are now assembled from public reference witgen and passed off to the backend. |
||
if !publics.is_empty() { | ||
log::debug!("Publics:"); | ||
} | ||
|
@@ -291,22 +292,16 @@ impl<'a, 'b, T: FieldElement> WitnessGenerator<'a, 'b, T> { | |
} | ||
} | ||
|
||
pub fn extract_publics<'a, T, I>(witness: I, pil: &Analyzed<T>) -> BTreeMap<String, Option<T>> | ||
pub fn extract_publics<T>( | ||
public_references: BTreeMap<String, T>, | ||
pil: &Analyzed<T>, | ||
) -> BTreeMap<String, Option<T>> | ||
Comment on lines
+295
to
+298
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. What does this do exactly? I think the inputs are publics already, but then this makes sure that there is an entry for each public declaration? What would happen if we removed the function and just return the publics as returned from There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Exactly, it makes sure that we have a value for each public declaration, which might not be the case if we have stage-1 publics during stage-0 witgen, in which case |
||
where | ||
T: FieldElement, | ||
I: IntoIterator<Item = (&'a String, &'a Vec<T>)>, | ||
{ | ||
let witness = witness | ||
.into_iter() | ||
.map(|(name, col)| (name.clone(), col)) | ||
.collect::<BTreeMap<_, _>>(); | ||
pil.public_declarations_in_source_order() | ||
.map(|(name, public_declaration)| { | ||
let poly_name = &public_declaration.referenced_poly_name(); | ||
let poly_row = public_declaration.row(); | ||
let value = witness | ||
.get(poly_name) | ||
.map(|column| column[poly_row as usize]); | ||
.map(|(name, _)| { | ||
let value = public_references.get(name).cloned(); | ||
((*name).clone(), value) | ||
}) | ||
.collect() | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -541,16 +541,19 @@ impl<T: FieldElement> Pipeline<T> { | |
} | ||
|
||
/// Sets the witness to the provided value. | ||
pub fn set_witness(mut self, witness: Vec<(String, Vec<T>)>) -> Self { | ||
pub fn set_witness_and_publics( | ||
mut self, | ||
witness: Vec<(String, Vec<T>)>, | ||
publics: BTreeMap<String, Option<T>>, | ||
) -> Self { | ||
if self.output_dir.is_some() { | ||
// Some future steps require the witness to be persisted. | ||
let fixed_cols = self.compute_fixed_cols().unwrap(); | ||
self.maybe_write_witness(&fixed_cols, &witness).unwrap(); | ||
} | ||
Pipeline { | ||
artifact: Artifacts { | ||
// need to set publics to Some, or `compute_witness` will run auto witgen | ||
witness_and_publics: Some(Arc::new((witness, BTreeMap::new()))), | ||
witness_and_publics: Some(Arc::new((witness, publics))), | ||
// we're changing the witness, clear the current proof | ||
proof: None, | ||
..self.artifact | ||
|
@@ -708,7 +711,12 @@ impl<T: FieldElement> Pipeline<T> { | |
// but give it different witnesses and generate different proofs. | ||
// The previous alternative to this was cloning the entire pipeline. | ||
pub fn rollback_from_witness(&mut self) { | ||
self.artifact.witness_and_publics = None; | ||
if let Some(old_arc) = &self.artifact.witness_and_publics { | ||
// Clone the public part | ||
let public = old_arc.1.clone(); | ||
// Replace with an empty witness and the preserved public | ||
self.artifact.witness_and_publics = Some(Arc::new((Vec::new(), public))); | ||
Comment on lines
+715
to
+718
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why do we keep the publics? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think this causes a few other changes in the file. In my mind, scalar publics could almost be considered part of the witness (you solve for them, you need them to evaluate constraints, ...), so I don't see why they are treated differently. |
||
} | ||
self.artifact.proof = None; | ||
self.arguments.external_witness_values.clear(); | ||
} | ||
|
@@ -1047,7 +1055,10 @@ impl<T: FieldElement> Pipeline<T> { | |
|
||
pub fn compute_witness(&mut self) -> WitgenResult<T> { | ||
if let Some(arc) = &self.artifact.witness_and_publics { | ||
return Ok(arc.clone()); | ||
// If exists, witness will always be non-empty, but not necessarily publics | ||
if !arc.0.is_empty() { | ||
return Ok(arc.clone()); | ||
} | ||
} | ||
|
||
self.host_context.clear(); | ||
|
@@ -1079,8 +1090,16 @@ impl<T: FieldElement> Pipeline<T> { | |
.all(|name| external_witness_values.iter().any(|(e, _)| e == name)) | ||
{ | ||
self.log("All witness columns externally provided, skipping witness generation."); | ||
self.artifact.witness_and_publics = | ||
Some(Arc::new((external_witness_values, BTreeMap::new()))); | ||
if let Some(old_arc) = &self.artifact.witness_and_publics { | ||
// Clone the public part | ||
let public = old_arc.1.clone(); | ||
// Replace with an empty witness and the preserved public | ||
self.artifact.witness_and_publics = | ||
Some(Arc::new((external_witness_values, public))); | ||
} else { | ||
self.artifact.witness_and_publics = | ||
Some(Arc::new((external_witness_values, BTreeMap::new()))); | ||
} | ||
} else { | ||
self.log("Deducing witness columns..."); | ||
let start = Instant::now(); | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmm, I'm always a bit confused by the sender and receiver here, but why do we need to send a map and then always send an empty map?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This no longer appears after rebase as it's added in a prior PR #2567.
However, to answer this question, this is actually inferred by the compiler:
response_receiver.recv().unwrap()
therefore has to be(witness, publics)
.response_sender
always send a(witness, publics)
.I left this out so that #2567 don't grow too large, but I think one potential effect of this is that composite backends won't work for stage 1 publics, but I was planning to work on other backends in future PRs regardless. (It currently isn't an issue because all backends except Mock still use the witness for exposing publics after this PR).
To make sure this isn't forgotten, however, I'm adding a
TODO
comment here.