Add more instructions on AIR constraints, rename rules

Author: gnull

.cursor/rules/air-pv.mdc

@@ -0,0 +1,43 @@
+---
+description: 
+globs: 
+alwaysApply: false
+---
+Following the structure of [pcs-shots.mdc](mdc:.cursor/rules/pcs-shots.mdc),
+  the Prover and Verifier for AIR constraints consist of the following steps.
+We present each step marked with P or V depending on whether Prover or Verifier performs the step.
+In terms of interaction with the challenger,
+  steps with the same numbers correpond to the dual steps between Prover and Verifier
+  (e.g. if a step 3P correponds to `pcs.open`, then 3V will correspond to `pcs.verify`),
+  steps without a P or V correpond to both Prover and Verifier doing the same thing.
+
+1: Compute `trace_domain` and `quotient_domain`.
+
+2P: Commit to given `trace`.
+
+3: Include the trace commitment, public values and logarithm of trace degree in transcript.
+
+4P. Evaluate the trace on quotient domain.
+
+5. Sample challenge `alpha` from transcript.
+
+6P. Compute the values of quotient on all of quotient domain (using parallel SIMD-enabled loop), using AIR constraints as `Q(X) = C(X) / Z_{quotient_domain}(X)` (where `C(X)` is the folded constraints).
+
+7P. Split the quotient polynomial into chunks, commit to the chunks.
+
+8. Include the commitment to quotient chunks in the transcript.
+
+9. Sample challenge `zeta` and compute `zeta_next`.
+
+10P. Open the trace at points `zeta` and `zeta_next`, and quotient chunks at `zeta`.
+
+10V. Verify the openings from step 10P.
+
+11V. Reconstruct the value of quotient at `zeta` from the opening values.
+
+12V. Compute the value of folded constraints polynomial at `zeta` using the opened values.
+
+13V. Ensure that quotient value computed from folded constraints matches the one reconstructed from chunks.
+
+
+

.cursor/rules/shots.mdc renamed to .cursor/rules/pv-steps.mdc

@@ -1,8 +1,8 @@
 ---
 description: 
 globs: 
+alwaysApply: false
 ---
-
 ## Synchronizing Prover and Verifier
 
 The `Challenger` interface we use here is the same is the same for both Prover and Verifier
@@ -21,12 +21,27 @@ The values Prover adds to Challenger transcript (with "observe" methods) must be
   it's the job of proof produced by the Prover to make sure of that;
   one straightforward way to ensure that is to directly include
     such observed values in the proof.
-When Prover is calling a functon that modifies the Challenger transcript, Verifier must call its dual of that function. For example, `verify` is Verifier's dual of Prover's `open` (when called with corresponding values); any "observe" or "sample" function is dual to itself.
+When Prover is calling a functon that modifies the Challenger transcript, Verifier must call its dual of that function.
+For example, `pcs.verify` is Verifier's dual of Prover's `pcs.open`
+  (assuming the verifier is passing to `pcs.verify` the opening proof and values 
+    that Prover got from the `pcs.open` call);
+  any "observe" or "sample" function is dual to itself.
+
+As a rule, all values Prover opens through `pcs.open` must be included
+  in the proof (together with the opening proofs) to ensure that
+  Verifier can make the corresponding `pcs.verify` call.
 
-A Prover and Verifier that are in sync and handle Challenger transcript correctly may be used by another Prover' and Verifier' if Prover' calls prover at a stage that corresponds to Verifier' calling Verifier. This way, Prover-Verifier pairs may be re-used as subroutines by other Provers and Verifiers if the calls are in sync.
+A Prover and Verifier that are in sync and handle Challenger transcript correctly 
+  may be used by another Prover' and Verifier' if Prover' calls Prover at a stage that corresponds to Verifier' calling Verifier.
+This way, Prover-Verifier pairs may be re-used
+  as subroutines by other Provers and Verifiers if the calls are in sync.
 This way, Verifier is dual of its Prover,
   and another Prover' calling Prover requires Verifier' calling Verifier.
-(The functions like `commit` or `get_evaluations_on_domain`, for example, on the other hand, don't require Verifier to do anything special because the functions touch the Challenger.)
+(The functions like `pcs.commit` or `pcs.get_evaluations_on_domain`, for example,
+  on the other hand,
+  don't require Verifier to do anything special
+    because the functions touch the Challenger.
+)
 
 Following the rules above,
   the code of Prover and Verifier must be written side by side,