Witgen inference. #2219
Witgen inference. #2219
Conversation
chriseth
force-pushed
the
witgen_inference
branch
from
b029753 to
95fc6a2
Compare
chriseth
force-pushed
the
witgen_inference
branch
from
95fc6a2 to
e348031
Compare
| // We cannot solve it, but we can also not learn anything new from it. | ||
| let result = constr.solve().unwrap(); | ||
| assert!(result.complete && result.effects.is_empty()); |
There was a problem hiding this comment.
This seems confusing, if we cannot solve it, why is it complete?
I think the answer is that there are no unknown symbols, right? But in that case, it is already solved, right?
There was a problem hiding this comment.
I mean it says it in the comment "we cannot learn anything new from it"
| pub trait ReferenceEvaluator<T: FieldElement> { | ||
| fn evaluate_fixed(&self, _var: &AlgebraicReference, _row_offset: i32) -> Option<T> { | ||
| None | ||
| } | ||
| fn evaluate_challenge(&self, _challenge: &Challenge) -> Option<T> { | ||
| None | ||
| } | ||
| fn evaluate_public(&self, _public: &String) -> Option<T> { | ||
| None | ||
| } | ||
| } |
There was a problem hiding this comment.
Few comments:
- Should we call this
FixedEvaluator? Because it doesn't evaluate all reference, just those to "fixed data"? - If so, should we remove publics? In my mind, they are closer to witness cells, basically variables that we want to solve for. Public references are anyway only half-supported, so I think I'd remove it here and just put a
todo!()insideevaluate()for now. - If the idea is that this trait allows to access fixed data, it should return a
Result<T, ()>, because we'd expect the data to always be available, right?
There was a problem hiding this comment.
This is just meant as a first version, I didn't think so much about it. In the end, we need to change the variable type from Cell to some enum that contains Cell, Public, Challenge and maybe even a reference to T (we would maybe use that for runtime conditionals).
But yeah, maybe you are right: Challenges will always be "known but arbitrary", so there is no point in asking the caller for a concrete value. For publics we might want to know if they are known or not, but that needs a different interface.
Co-authored-by: Georg Wiese <[email protected]>
…into witgen_inference
| Xor::C[5] = (Xor::C[6] & 65535); | ||
| assert Xor::C[6] == (Xor::C[6] | 16777215); | ||
| lookup(0, [Known(Xor::A_byte[6]), Unknown(Xor::B_byte[6]), Known(Xor::C_byte[6])]); | ||
| Xor::A_byte[4] = (65280 // 256); |
There was a problem hiding this comment.
This all looks good until here, we it goes south.
This PR adds a component that can derive assignments and other code on identities and multiple rows. It keeps track of which cells in the trace are already known and which not. The way to access fixed rows is abstracted because it does not have a concept of an absolute row. While this might work for block machines with cyclic fixed columns, it does not work in the general case.
What it does not do: