|
| 1 | +(** Interface definitions for the Kimchi backend constraint system. |
| 2 | +
|
| 3 | + This module defines the interfaces for working with the Kimchi constraint system |
| 4 | + over the Pasta curves (Pallas and Vesta). It provides functionality for |
| 5 | + building, managing, and finalizing constraint systems. *) |
| 6 | + |
1 | 7 | open Core_kernel |
2 | 8 |
|
| 9 | +(** Basic accessors for constraint system properties. |
| 10 | +
|
| 11 | + This module type defines the fundamental operations for creating and |
| 12 | + accessing properties of a constraint system, including input sizes, |
| 13 | + row counts, and challenge parameters. *) |
3 | 14 | module type With_accessors = sig |
| 15 | + (** The constraint system type. *) |
4 | 16 | type t |
5 | 17 |
|
| 18 | + (** Create a new empty constraint system. *) |
6 | 19 | val create : unit -> t |
7 | 20 |
|
| 21 | + (** Get the public input size (can only be set once). *) |
8 | 22 | val get_public_input_size : t -> int Set_once.t |
9 | 23 |
|
| 24 | + (** Get the number of primary (public) inputs. *) |
10 | 25 | val get_primary_input_size : t -> int |
11 | 26 |
|
| 27 | + (** Set the number of primary (public) inputs. *) |
12 | 28 | val set_primary_input_size : t -> int -> unit |
13 | 29 |
|
| 30 | + (** Get the number of auxiliary (private witness) inputs. *) |
14 | 31 | val get_auxiliary_input_size : t -> int |
15 | 32 |
|
| 33 | + (** Set the number of auxiliary (private witness) inputs. *) |
16 | 34 | val set_auxiliary_input_size : t -> int -> unit |
17 | 35 |
|
| 36 | + (** Get the number of previous challenges used in recursive proofs. |
| 37 | + Returns [None] if not set. *) |
18 | 38 | val get_prev_challenges : t -> int option |
19 | 39 |
|
| 40 | + (** Set the number of previous challenges for recursive proofs. *) |
20 | 41 | val set_prev_challenges : t -> int -> unit |
21 | 42 |
|
| 43 | + (** Get the total number of rows in the constraint system. *) |
22 | 44 | val get_rows_len : t -> int |
23 | 45 |
|
| 46 | + (** Get the total number of constraints added to the system. *) |
24 | 47 | val num_constraints : t -> int |
25 | 48 |
|
| 49 | + (** Get the index of the next available row for adding constraints. *) |
26 | 50 | val next_row : t -> int |
27 | 51 | end |
28 | 52 |
|
| 53 | +(** Complete constraint system interface with all operations. |
| 54 | +
|
| 55 | + This module type extends [With_accessors] with constraint management, |
| 56 | + witness computation, lookup tables, and finalization operations. *) |
29 | 57 | module type Full = sig |
| 58 | + (** Field element type (either Pallas or Vesta scalar field). *) |
30 | 59 | type fp |
31 | 60 |
|
| 61 | + (** Variable type representing field elements in constraints. *) |
32 | 62 | type field_var |
33 | 63 |
|
| 64 | + (** Gate collection type for the compiled constraint system. *) |
34 | 65 | type gates |
35 | 66 |
|
| 67 | + (** Constraint types and operations. |
| 68 | +
|
| 69 | + This module provides different types of constraints that can be added |
| 70 | + to the constraint system, along with evaluation and debugging functions. *) |
36 | 71 | module Constraint : sig |
| 72 | + (** A basic Plonk constraint over field variables and field elements. *) |
37 | 73 | type t = |
38 | 74 | ( field_var |
39 | 75 | , fp ) |
40 | 76 | Kimchi_pasta_snarky_backend.Plonk_constraint_system.Plonk_constraint.basic |
41 | 77 | [@@deriving sexp] |
42 | 78 |
|
| 79 | + (** Create a boolean constraint: x * (x - 1) = 0. |
| 80 | + Ensures the variable is either 0 or 1. *) |
43 | 81 | val boolean : field_var -> t |
44 | 82 |
|
| 83 | + (** Create an equality constraint: x = y. *) |
45 | 84 | val equal : field_var -> field_var -> t |
46 | 85 |
|
| 86 | + (** Create an R1CS constraint: a * b = c. |
| 87 | + This is the fundamental constraint type in R1CS systems. *) |
47 | 88 | val r1cs : field_var -> field_var -> field_var -> t |
48 | 89 |
|
| 90 | + (** Create a square constraint: x * x = y. *) |
49 | 91 | val square : field_var -> field_var -> t |
50 | 92 |
|
| 93 | + (** Evaluate a constraint given a variable assignment. |
| 94 | + Returns [true] if the constraint is satisfied. *) |
51 | 95 | val eval : t -> (field_var -> fp) -> bool |
52 | 96 |
|
| 97 | + (** Generate a human-readable string representation of the constraint |
| 98 | + with the given variable assignment for debugging. *) |
53 | 99 | val log_constraint : t -> (field_var -> fp) -> string |
54 | 100 | end |
55 | 101 |
|
| 102 | + (** Alias for constraint type. *) |
56 | 103 | type constraint_ = Constraint.t |
57 | 104 |
|
58 | 105 | include |
59 | 106 | With_accessors |
60 | 107 | with type t = (fp, gates) Kimchi_backend_common.Plonk_constraint_system.t |
61 | 108 |
|
| 109 | + (** Add a constraint to the constraint system. *) |
62 | 110 | val add_constraint : t -> Constraint.t -> unit |
63 | 111 |
|
| 112 | + (** Compute the witness for the constraint system. |
| 113 | +
|
| 114 | + In this context, "witness" refers to the entire execution trace, |
| 115 | + including both public inputs and private values. |
| 116 | +
|
| 117 | + @param t The constraint system |
| 118 | + @param int -> fp Function mapping variable indices to field values |
| 119 | + @return A pair of: |
| 120 | + - The witness (full trace) columns as a 2D array |
| 121 | + - Runtime lookup tables *) |
64 | 122 | val compute_witness : |
65 | 123 | t -> (int -> fp) -> fp array array * fp Kimchi_types.runtime_table array |
66 | 124 |
|
| 125 | + (** Finalize the constraint system, preparing it for proof generation. |
| 126 | + This must be called before generating proofs. *) |
67 | 127 | val finalize : t -> unit |
68 | 128 |
|
| 129 | + (** Finalize the constraint system and extract the gates and lookup tables. |
| 130 | +
|
| 131 | + @return A triple of: |
| 132 | + - Compiled gates |
| 133 | + - Fixed lookup tables |
| 134 | + - Runtime lookup table configurations *) |
69 | 135 | val finalize_and_get_gates : |
70 | 136 | t |
71 | 137 | -> gates |
72 | 138 | * fp Kimchi_types.lookup_table array |
73 | 139 | * fp Kimchi_types.runtime_table_cfg array |
74 | 140 |
|
75 | 141 | (** Return the size of all the fixed lookup tables concatenated, without the |
76 | | - built-in XOR and RangeCheck tables *) |
| 142 | + built-in XOR and RangeCheck tables. *) |
77 | 143 | val get_concatenated_fixed_lookup_table_size : t -> int |
78 | 144 |
|
79 | | - (** Return the size of all the runtime lookup tables concatenated *) |
| 145 | + (** Return the size of all the runtime lookup tables concatenated. *) |
80 | 146 | val get_concatenated_runtime_lookup_table_size : t -> int |
81 | 147 |
|
82 | | - (** Finalize the fixed lookup tables. The function can not be called twice *) |
| 148 | + (** Finalize the fixed lookup tables. The function can not be called twice. *) |
83 | 149 | val finalize_fixed_lookup_tables : t -> unit |
84 | 150 |
|
85 | | - (** Finalize the runtime lookup table configurations. The function can not be called twice. *) |
| 151 | + (** Finalize the runtime lookup table configurations. The function can not be |
| 152 | + called twice. *) |
86 | 153 | val finalize_runtime_lookup_tables : t -> unit |
87 | 154 |
|
| 155 | + (** Compute an MD5 digest of the constraint system. |
| 156 | + Useful for caching and verification of constraint system integrity. *) |
88 | 157 | val digest : t -> Md5.t |
89 | 158 |
|
| 159 | + (** Serialize the constraint system to JSON format. |
| 160 | + Useful for debugging and external analysis. *) |
90 | 161 | val to_json : t -> string |
| 162 | + |
| 163 | + (** Dump extra circuit data to a file for use by external systems. |
| 164 | +
|
| 165 | + This function exports additional circuit metadata and configuration |
| 166 | + that is needed by the Mina Rust node for circuit verification and |
| 167 | + proof processing. |
| 168 | +
|
| 169 | + @param t The constraint system |
| 170 | + @param string The file path where the circuit data should be written *) |
| 171 | + val dump_extra_circuit_data : t -> string -> unit |
91 | 172 | end |
0 commit comments