Builtin: Capture stage #1334
Builtin: Capture stage #1334
Conversation
pil-analyzer/src/condenser.rs
Outdated
| self.extract_new_constraints() | ||
| .into_iter() | ||
| .map(|id| { | ||
| (match id.kind { |
There was a problem hiding this comment.
Should maybe move to a helper
chriseth
force-pushed
the
capture_stage
branch
3 times, most recently
from
948b310
to
b3b9546
Compare
| std::prover::capture_stage(f); | ||
| "#; | ||
| analyze_string::<GoldilocksField>(input); | ||
| } |
There was a problem hiding this comment.
Can you explain what these do? Not sure I fully get it
There was a problem hiding this comment.
The idea is that you call capture_stage to capture a full stage. This means that before the call to capture_stage, there cannot be any constraints or witness columns in the environment. Since capture_stage increments the stage, they would have a different stage index than those after the call to capture_stage.
I would also prefer to do this differently so that we don't need this and assign the correct stage automatically, but I don't know how to do this currently, and I also don't think that this would occur often.
| pub fn capture_stage_non_fresh_inter() { | ||
| let input = r#" | ||
| namespace std::prover; | ||
| let capture_stage: (-> int) -> Constr[] = 9; |
There was a problem hiding this comment.
Why =9? Do we need a constraint here?
There was a problem hiding this comment.
This defines a builtin. Since the builtin is "overridden" during execution and type checking, I always like to assign a value that will create an error both at type checking and during runtime when the value is used instead of being overridden.
Now that we have the prelude mechanism, we could use a fixed identifier like "std::prelude::builtin" (which is a builtin itself that always fails or something).
| // Just use the second constraint. | ||
| std::prover::capture_stage(f)[1]; | ||
| let w; | ||
| w = 10; |
There was a problem hiding this comment.
I'd expect this to fail since there are other columns and constraints besides the call to capture_stage. Why doesn't it fail?
There was a problem hiding this comment.
I agree that this is a bit weird. In the end, you want to process the constraints that are returned by the call to capture_stage. Processing the constraints involves adding new constraints and witness column (but at a higher stage).
My current way to deal with it is that it's not OK to have witness columns or constraints above the call to capture_stage, but it is OK to have them below. The reason is that we only know the stage of witness columns once we return from capture_stage. Another way would be to retroactively change the stage of all witness columns that are already present in the condenser when we call capture_stage. This might indeed be a bit more uniform.
There was a problem hiding this comment.
Hmm yea this "above" and "below" separation is kinda weird. Why not have a function that receives the results of capture_stage as argument and then adds constraints on top of that?
Implements part of #424