Skip to content

Commit 2ef6d3c

Browse files
srinathsettysrinathsetty
authored
Add the proof object specification chapter (#142)
Specify the byte-exact layout of the MC zk-SNARK proof: the eight top-level fields and the full recursive type tree down to primitives, deferring the primitive encodings to the serialization chapter. Document the single-field struct transparency, the shared-witness commitment hoisting that leaves each instance's shared commitment as a None tag, the fixed three-scalar outer-claims tuple, the bare compressed points in the evaluation argument, and the compressed round-polynomial layout.
1 parent f700f82 commit 2ef6d3c

1 file changed

Lines changed: 211 additions & 1 deletion

File tree

‎book/src/spec/proof-object.md‎

Lines changed: 211 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,213 @@
11
# The proof object
22

3-
> **Not yet written.** This chapter is a placeholder in a work-in-progress book. Its content will be added in a later revision.
3+
This chapter specifies the byte-exact layout of `VegaMcZkSNARK`, the value that \\(\mathrm{Vega}\_{\mathrm{MC}}\\)'s `verify` procedure consumes. The proof is the [bincode serialization](serialization.md) of this struct, applied recursively until every field resolves to a primitive. All primitive encodings — scalars, group elements, sequences, options, and tuples — live in [Serialization](serialization.md); this chapter specifies structure: which fields exist, in which order, and of which type.
4+
5+
The proof path contains no user-defined enums — so the enum variant-index encoding never appears — and no cached or skipped fields. The only sum types are the `Option<Commitment>` values: `comm_W_shared` at the top level and the two `Option<Commitment>` fields inside each `SplitR1CSInstance`, all of which use the one-byte [Option tag encoding](serialization.md#rust-shaped-values). Every other field contributes bytes unconditionally.
6+
7+
## Single-field struct transparency
8+
9+
Several types in the proof tree are single-field structs. The struct rule in [Serialization](serialization.md) states that a single-field struct serializes exactly as its field, with no extra tag, length prefix, or padding. Treating these as opaque containers and inserting framing bytes produces incorrect output. The affected types are:
10+
11+
| Type | Wire bytes identical to |
12+
| --- | --- |
13+
| `HyraxCommitment` | its `Vec` of group elements |
14+
| `HyraxEvaluationArgument` | its `InnerProductArgumentLinear` |
15+
| `SumcheckProof` | its `Vec<CompressedUniPoly>` |
16+
| `CompressedUniPoly` | its `Vec` of scalars |
17+
| `NovaNIFS` | its `Commitment` |
18+
19+
A `Commitment` is a type alias for `HyraxCommitment`, so every commitment in the proof is transparently a length-prefixed vector of 33-byte compressed group elements. The [commitment example](serialization.md#commitment-example) in the serialization chapter works through the encoding in full.
20+
21+
## Top-level object: `VegaMcZkSNARK`
22+
23+
The proof has eight fields in this declaration order:
24+
25+
| Field | Type | Role |
26+
| --- | --- | --- |
27+
| `comm_W_shared` | `Option<Commitment>` | Shared witness commitment, stored once at the top level; `None` when no witness is shared. |
28+
| `step_instances` | `Vec<SplitR1CSInstance>` | One R1CS instance per step circuit execution. |
29+
| `core_instance` | `SplitR1CSInstance` | R1CS instance for the aggregated core circuit. |
30+
| `eval_arg` | `HyraxEvaluationArgument` | Hyrax batch evaluation argument. |
31+
| `U_verifier` | `SplitMultiRoundR1CSInstance` | R1CS instance for the in-circuit verifier. |
32+
| `nifs` | `NovaNIFS` | Non-interactive folding proof (a single commitment). |
33+
| `random_U` | `RelaxedR1CSInstance` | Relaxed R1CS instance after folding. |
34+
| `relaxed_snark` | `RelaxedR1CSSpartanProof` | Relaxed Spartan proof over the folded instance. |
35+
36+
```text
37+
VegaMcZkSNARK =
38+
comm_W_shared
39+
|| step_instances
40+
|| core_instance
41+
|| eval_arg
42+
|| U_verifier
43+
|| nifs
44+
|| random_U
45+
|| relaxed_snark
46+
```
47+
48+
**Shared-witness optimization.** When several step circuits share a common witness prefix, its commitment is identical across every step instance and the core instance. The prover sets the top-level `comm_W_shared` to a clone of the *first* step instance's `comm_W_shared`, then sets the per-instance `comm_W_shared` to `None` in every element of `step_instances` and in `core_instance`. In the serialized proof, each instance's `comm_W_shared` is therefore always the single tag byte `00`; the shared commitment, when present, appears only at the top level. When the circuit family declares no shared witness prefix — as in the canonical configuration — the first step instance's `comm_W_shared` is itself `None`, so the top-level field is also `None` (a lone `00` tag byte) and no shared-commitment bytes appear anywhere in the proof. A byte-equivalent prover must reproduce this exactly: copy the first step instance's original `comm_W_shared` to the top level, then emit `None` within every instance. The verifier copies the top-level value back into each instance before checking.
49+
50+
## R1CS instance types
51+
52+
### `SplitR1CSInstance`
53+
54+
Each element of `step_instances` and the `core_instance` field are of this type. Five fields in declaration order:
55+
56+
| Field | Type | Role |
57+
| --- | --- | --- |
58+
| `comm_W_shared` | `Option<Commitment>` | Always `None` in the proof; the shared commitment is hoisted to the top level (see above). |
59+
| `comm_W_precommitted` | `Option<Commitment>` | Pre-committed column commitment; `None` if not present. |
60+
| `comm_W_rest` | `Commitment` | Commitment to the remaining witness columns. |
61+
| `public_values` | `Vec<Scalar>` | Public input scalars. |
62+
| `challenges` | `Vec<Scalar>` | Verifier challenges for this instance. |
63+
64+
```text
65+
SplitR1CSInstance =
66+
comm_W_shared (Option<Commitment>)
67+
|| comm_W_precommitted (Option<Commitment>)
68+
|| comm_W_rest (Commitment)
69+
|| public_values (Vec of Scalar)
70+
|| challenges (Vec of Scalar)
71+
```
72+
73+
Each `Option<Commitment>` follows the [Option encoding](serialization.md#rust-shaped-values): one tag byte (`00` = `None`, `01` = `Some`), then the commitment bytes if the tag is `01`.
74+
75+
### `SplitMultiRoundR1CSInstance`
76+
77+
The `U_verifier` field is of this type. Three fields:
78+
79+
| Field | Type | Role |
80+
| --- | --- | --- |
81+
| `comm_w_per_round` | `Vec<Commitment>` | Witness commitments, one per round. |
82+
| `public_values` | `Vec<Scalar>` | Public input scalars. |
83+
| `challenges_per_round` | `Vec<Vec<Scalar>>` | Verifier challenges grouped by round. |
84+
85+
```text
86+
SplitMultiRoundR1CSInstance =
87+
comm_w_per_round (Vec of Commitment)
88+
|| public_values (Vec of Scalar)
89+
|| challenges_per_round (Vec of Vec of Scalar)
90+
```
91+
92+
`challenges_per_round` is a `Vec` of `Vec`s. The outer `Vec` carries an 8-byte `u64` count; each inner `Vec` carries its own 8-byte count followed by its scalars. There is no extra framing between the inner vectors beyond what the `Vec` rule provides.
93+
94+
### `RelaxedR1CSInstance`
95+
96+
The `random_U` field is of this type. Four fields:
97+
98+
| Field | Type | Role |
99+
| --- | --- | --- |
100+
| `comm_W` | `Commitment` | Witness commitment. |
101+
| `comm_E` | `Commitment` | Error-vector commitment. |
102+
| `X` | `Vec<Scalar>` | Public input vector. |
103+
| `u` | `Scalar` | Relaxation scalar. |
104+
105+
```text
106+
RelaxedR1CSInstance =
107+
comm_W (Commitment)
108+
|| comm_E (Commitment)
109+
|| X (Vec of Scalar)
110+
|| u (Scalar, 32 bytes)
111+
```
112+
113+
## Evaluation argument
114+
115+
### `HyraxEvaluationArgument`
116+
117+
`HyraxEvaluationArgument` is a single-field struct whose sole field is `ipa : InnerProductArgumentLinear`. Its wire bytes are those of the `InnerProductArgumentLinear` directly, with no wrapper framing.
118+
119+
### `InnerProductArgumentLinear`
120+
121+
Five fields:
122+
123+
| Field | Type | Role |
124+
| --- | --- | --- |
125+
| `delta` | group element | First blinding commitment; a bare 33-byte compressed point. |
126+
| `beta` | group element | Second blinding commitment; a bare 33-byte compressed point. |
127+
| `z_vec` | `Vec<Scalar>` | Response vector. |
128+
| `z_delta` | `Scalar` | Scalar response for `delta`. |
129+
| `z_beta` | `Scalar` | Scalar response for `beta`. |
130+
131+
```text
132+
InnerProductArgumentLinear =
133+
delta (33-byte compressed point, no length prefix)
134+
|| beta (33-byte compressed point, no length prefix)
135+
|| z_vec (Vec of Scalar)
136+
|| z_delta (Scalar, 32 bytes)
137+
|| z_beta (Scalar, 32 bytes)
138+
```
139+
140+
`delta` and `beta` are bare group elements, not `Commitment` structs: each is a single 33-byte compressed point with no preceding `u64` count. The point encoding is `flag || x(BE)` as specified in [Serialization](serialization.md#group-elements).
141+
142+
## Folding proof
143+
144+
### `NovaNIFS`
145+
146+
`NovaNIFS` is a single-field struct whose sole field is `comm_T : Commitment`. Its wire bytes are those of that commitment: an 8-byte `u64` count followed by compressed points.
147+
148+
```text
149+
NovaNIFS = comm_T (Commitment)
150+
```
151+
152+
## Relaxed Spartan proof
153+
154+
### `RelaxedR1CSSpartanProof`
155+
156+
Seven fields in declaration order:
157+
158+
| Field | Type | Role |
159+
| --- | --- | --- |
160+
| `sc_proof_outer` | `SumcheckProof` | Sum-check proof for the outer reduction. |
161+
| `claims_outer` | `(Scalar, Scalar, Scalar)` | Three claimed evaluations; a fixed tuple, exactly 96 bytes. |
162+
| `sc_proof_inner` | `SumcheckProof` | Sum-check proof for the inner reduction. |
163+
| `v_W` | `Vec<Scalar>` | Evaluation claims for the witness polynomial. |
164+
| `blind_W` | `Scalar` | Blinding scalar for the witness opening. |
165+
| `v_E` | `Vec<Scalar>` | Evaluation claims for the error polynomial. |
166+
| `blind_E` | `Scalar` | Blinding scalar for the error opening. |
167+
168+
```text
169+
RelaxedR1CSSpartanProof =
170+
sc_proof_outer (SumcheckProof)
171+
|| claims_outer.0 (Scalar, 32 bytes)
172+
|| claims_outer.1 (Scalar, 32 bytes)
173+
|| claims_outer.2 (Scalar, 32 bytes)
174+
|| sc_proof_inner (SumcheckProof)
175+
|| v_W (Vec of Scalar)
176+
|| blind_W (Scalar, 32 bytes)
177+
|| v_E (Vec of Scalar)
178+
|| blind_E (Scalar, 32 bytes)
179+
```
180+
181+
`claims_outer` is a 3-tuple of scalars. Tuples carry no tag, length prefix, or padding (see [Serialization](serialization.md#rust-shaped-values)), so these three scalars occupy exactly 96 consecutive bytes with no intervening count.
182+
183+
### `SumcheckProof`
184+
185+
`SumcheckProof` is a single-field struct whose sole field is `compressed_polys : Vec<CompressedUniPoly>`. Its wire bytes are those of the `Vec` directly. For a sum-check with \\(r\\) rounds:
186+
187+
```text
188+
SumcheckProof =
189+
u64_le(r) (8-byte round count)
190+
|| CompressedUniPoly_0
191+
|| CompressedUniPoly_1
192+
|| ...
193+
|| CompressedUniPoly_{r-1}
194+
```
195+
196+
### `CompressedUniPoly`
197+
198+
`CompressedUniPoly` is a single-field struct whose sole field is `coeffs_except_linear_term : Vec<Scalar>`. Its wire bytes are those of the `Vec` directly. A degree-\\(d\\) round polynomial has \\(d + 1\\) coefficients; the single linear (degree-1) coefficient is omitted, so exactly \\(d\\) coefficients are stored — the constant term followed by the degree-2 through degree-\\(d\\) coefficients:
199+
200+
```text
201+
CompressedUniPoly =
202+
u64_le(d) (number of stored coefficients = degree of the round polynomial)
203+
|| Scalar_0 (constant term, degree 0)
204+
|| Scalar_1 (degree 2)
205+
|| ...
206+
|| Scalar_{d-1} (degree d)
207+
```
208+
209+
The linear term (the coefficient of the degree-1 monomial) is absent from the proof. The verifier recovers it from the sum-check invariant for the round; no extra bytes are needed. Every stored coefficient is written as a 32-byte little-endian scalar per the [scalar encoding](serialization.md#scalar-field-elements).
210+
211+
---
212+
213+
The complete type tree established here, together with the primitive rules in [Serialization](serialization.md), fully determines the byte string for any `VegaMcZkSNARK` value. The companion chapter [A simple reference prover](reference-prover.md) shows how these fields are populated, and [Conformance and test vectors](test-vectors.md) provides byte-exact examples that an implementation can check against.

0 commit comments

Comments
 (0)