|
| 1 | +# Debug Report JSON Format |
| 2 | + |
| 3 | +This document describes the JSON shape of the `DebugReport` value returned by |
| 4 | +`ProofMan::get_debug_info(...)` (the `debug-info` CLI subcommand). The same data |
| 5 | +is teed into `debug.log` (or stdout, per the `output` section of `debug.json`), |
| 6 | +but the JSON form is intended for programmatic consumers — e.g. a frontend that |
| 7 | +renders mismatches in whatever layout it likes. |
| 8 | + |
| 9 | +## Overview |
| 10 | + |
| 11 | +The report covers bus / std-lookup verification only. It is populated by the std |
| 12 | +lib's bus checker as it consumes accumulated debug data, alongside the textual |
| 13 | +report written to `debug.log`. |
| 14 | + |
| 15 | +| Field | Type | Description | |
| 16 | +|----------------|-----------------------|--------------------------------------------------------------| |
| 17 | +| `all_ok` | bool | `true` if no mismatched bus values were found during the run | |
| 18 | +| `bus_sections` | array of `BusSection` | One entry per opid that produced any mismatch | |
| 19 | + |
| 20 | +When `all_ok` is `true`, `bus_sections` is empty. |
| 21 | + |
| 22 | +## Root structure |
| 23 | + |
| 24 | +```json |
| 25 | +{ |
| 26 | + "all_ok": false, |
| 27 | + "bus_sections": [ ... ] |
| 28 | +} |
| 29 | +``` |
| 30 | + |
| 31 | +--- |
| 32 | + |
| 33 | +## `BusSection` — one opid |
| 34 | + |
| 35 | +```json |
| 36 | +{ |
| 37 | + "opid": 7, |
| 38 | + "mismatched": true, |
| 39 | + "num_overassumed": 3, |
| 40 | + "num_overproven": 1, |
| 41 | + "buckets": [ ... ] |
| 42 | +} |
| 43 | +``` |
| 44 | + |
| 45 | +### Fields |
| 46 | + |
| 47 | +- **`opid`** — bus operation ID this section reports on. |
| 48 | +- **`mismatched`** — `true` when this opid has at least one mismatched value |
| 49 | + (always `true` in practice, since clean opids are omitted from `bus_sections`). |
| 50 | +- **`num_overassumed`** — total number of values across all buckets where |
| 51 | + `num_assumes > num_proves` (assumed but not proven). |
| 52 | +- **`num_overproven`** — total number of values across all buckets where |
| 53 | + `num_proves > num_assumes` (proven but not assumed). |
| 54 | +- **`buckets`** — one entry per bucket within the opid. Opids without a |
| 55 | + per-opid bucketing rule have a single implicit bucket with `bucket_key = 0`. |
| 56 | + |
| 57 | +--- |
| 58 | + |
| 59 | +## `BusBucket` — one bucket within an opid |
| 60 | + |
| 61 | +```json |
| 62 | +{ |
| 63 | + "bucket_key": 0, |
| 64 | + "bucket_label": "col[2] in [0x100, 0x200)", |
| 65 | + "overassumed": [ ... ], |
| 66 | + "overproven": [ ... ] |
| 67 | +} |
| 68 | +``` |
| 69 | + |
| 70 | +### Fields |
| 71 | + |
| 72 | +- **`bucket_key`** — bucket discriminator, as set by the per-opid bucketing rule |
| 73 | + in `debug.json`'s `bus.group_by` section. |
| 74 | +- **`bucket_label`** — human-readable bucket description rendered from that rule |
| 75 | + (e.g. `"col[2] in [0x100, 0x200)"`). `null` when the opid has no bucketing |
| 76 | + rule. |
| 77 | +- **`overassumed`** — values appearing more as `assume` than `prove`. |
| 78 | +- **`overproven`** — values appearing more as `prove` than `assume`. |
| 79 | + |
| 80 | +Both lists may be empty (one side can be balanced while the other is not). |
| 81 | + |
| 82 | +--- |
| 83 | + |
| 84 | +## `BusValueMismatch` — one mismatched bus value |
| 85 | + |
| 86 | +```json |
| 87 | +{ |
| 88 | + "vals": [42, 0, 0], |
| 89 | + "hash": 14087324812907813462, |
| 90 | + "num_assumes": 3, |
| 91 | + "num_proves": 2, |
| 92 | + "global_origin": { ... }, |
| 93 | + "local_origins": [ ... ] |
| 94 | +} |
| 95 | +``` |
| 96 | + |
| 97 | +### Fields |
| 98 | + |
| 99 | +- **`vals`** — bus value tuple as canonical `u64` field elements. Extended-field |
| 100 | + components are flattened in order alongside base-field components, so a tuple |
| 101 | + of one cubic extension renders as a 3-element array. Frontends that need a |
| 102 | + specific tuple schema (e.g. `(payload..., multiplicity)`) should derive it |
| 103 | + from the opid's known width. |
| 104 | +- **`hash`** — the value's debug-data hash key (stable per `vals`). |
| 105 | +- **`num_assumes`** — total times this value appeared as `assume` across all |
| 106 | + origins. |
| 107 | +- **`num_proves`** — total times this value appeared as `prove` across all |
| 108 | + origins. |
| 109 | +- **`global_origin`** — aggregated global-level origin info when present, else |
| 110 | + `null`. See [`BusValueGlobalOrigin`](#busvalueglobalorigin). |
| 111 | +- **`local_origins`** — per-AIR-instance occurrences. See |
| 112 | + [`BusValueLocalOrigin`](#busvaluelocalorigin). May be empty if |
| 113 | + `store_row_info` was not enabled for the contributing instances. |
| 114 | + |
| 115 | +--- |
| 116 | + |
| 117 | +## `BusValueGlobalOrigin` |
| 118 | + |
| 119 | +```json |
| 120 | +{ |
| 121 | + "airgroup_id": 0, |
| 122 | + "airgroup_name": "Main", |
| 123 | + "piop_name": "RangeCheck", |
| 124 | + "expression_names": ["value"], |
| 125 | + "is_prod": false |
| 126 | +} |
| 127 | +``` |
| 128 | + |
| 129 | +### Fields |
| 130 | + |
| 131 | +- **`airgroup_id`** / **`airgroup_name`** — airgroup where the global origin was |
| 132 | + registered. |
| 133 | +- **`piop_name`** — friendly name of the bus operation (PIOP). |
| 134 | +- **`expression_names`** — names of the bus expressions, in tuple order. |
| 135 | +- **`is_prod`** — `true` for product-style PIOPs (`gprod`), `false` for |
| 136 | + sum-style (`gsum`). |
| 137 | + |
| 138 | +--- |
| 139 | + |
| 140 | +## `BusValueLocalOrigin` |
| 141 | + |
| 142 | +```json |
| 143 | +{ |
| 144 | + "airgroup_id": 0, |
| 145 | + "airgroup_name": "Main", |
| 146 | + "air_id": 1, |
| 147 | + "air_name": "Range8", |
| 148 | + "instance_id": 0, |
| 149 | + "hint_id": 4, |
| 150 | + "piop_name": "RangeCheck", |
| 151 | + "expression_names": ["value"], |
| 152 | + "is_prod": false, |
| 153 | + "rows": [12, 47, 130, 412] |
| 154 | +} |
| 155 | +``` |
| 156 | + |
| 157 | +### Fields |
| 158 | + |
| 159 | +- **`airgroup_id`** / **`airgroup_name`** — airgroup of the AIR instance that |
| 160 | + contributed. |
| 161 | +- **`air_id`** / **`air_name`** — AIR within that airgroup. |
| 162 | +- **`instance_id`** — process-local AIR instance ID. |
| 163 | +- **`hint_id`** — index of the debug-data hint inside this AIR (matches the |
| 164 | + ordering used by the std lib). |
| 165 | +- **`piop_name`** / **`expression_names`** — same semantics as on |
| 166 | + `BusValueGlobalOrigin`, but resolved against the AIR's local hints. |
| 167 | +- **`is_prod`** — `true` for `gprod`, `false` for `gsum`. |
| 168 | +- **`rows`** — row indices (sorted ascending) where this value appeared at this |
| 169 | + origin. **Not truncated** — the report keeps every row so the consumer can |
| 170 | + decide how to summarize. The text output in `debug.log` truncates to |
| 171 | + `bus.max_print` for readability; the structured form does not. |
| 172 | + |
| 173 | +--- |
| 174 | + |
| 175 | +## Examples |
| 176 | + |
| 177 | +### All bus values match |
| 178 | + |
| 179 | +```json |
| 180 | +{ |
| 181 | + "all_ok": true, |
| 182 | + "bus_sections": [] |
| 183 | +} |
| 184 | +``` |
| 185 | + |
| 186 | +### A mismatched opid |
| 187 | + |
| 188 | +```json |
| 189 | +{ |
| 190 | + "all_ok": false, |
| 191 | + "bus_sections": [ |
| 192 | + { |
| 193 | + "opid": 7, |
| 194 | + "mismatched": true, |
| 195 | + "num_overassumed": 1, |
| 196 | + "num_overproven": 0, |
| 197 | + "buckets": [ |
| 198 | + { |
| 199 | + "bucket_key": 0, |
| 200 | + "bucket_label": null, |
| 201 | + "overassumed": [ |
| 202 | + { |
| 203 | + "vals": [42, 0, 0], |
| 204 | + "hash": 14087324812907813462, |
| 205 | + "num_assumes": 3, |
| 206 | + "num_proves": 2, |
| 207 | + "global_origin": null, |
| 208 | + "local_origins": [ |
| 209 | + { |
| 210 | + "airgroup_id": 0, |
| 211 | + "airgroup_name": "Main", |
| 212 | + "air_id": 1, |
| 213 | + "air_name": "Range8", |
| 214 | + "instance_id": 0, |
| 215 | + "hint_id": 4, |
| 216 | + "piop_name": "RangeCheck", |
| 217 | + "expression_names": ["value"], |
| 218 | + "is_prod": false, |
| 219 | + "rows": [12, 47, 130] |
| 220 | + } |
| 221 | + ] |
| 222 | + } |
| 223 | + ], |
| 224 | + "overproven": [] |
| 225 | + } |
| 226 | + ] |
| 227 | + } |
| 228 | + ] |
| 229 | +} |
| 230 | +``` |
| 231 | + |
| 232 | +--- |
| 233 | + |
| 234 | +## Field index (quick lookup) |
| 235 | + |
| 236 | +| Path | Type | Notes | |
| 237 | +|---|---|---| |
| 238 | +| `all_ok` | bool | `true` only when `bus_sections` is empty | |
| 239 | +| `bus_sections[]` | array | one entry per mismatched opid | |
| 240 | +| `bus_sections[].opid` | u64 | bus operation ID | |
| 241 | +| `bus_sections[].mismatched` | bool | always `true` for entries in `bus_sections` | |
| 242 | +| `bus_sections[].num_overassumed` | usize | sum across buckets | |
| 243 | +| `bus_sections[].num_overproven` | usize | sum across buckets | |
| 244 | +| `bus_sections[].buckets[]` | array | one entry per non-empty bucket | |
| 245 | +| `bus_sections[].buckets[].bucket_key` | u64 | discriminator from `bus.group_by` | |
| 246 | +| `bus_sections[].buckets[].bucket_label` | string \| null | rendered label, `null` if no rule | |
| 247 | +| `bus_sections[].buckets[].overassumed[]` / `overproven[]` | array | one entry per mismatched value | |
| 248 | +| `…[].vals` | [u64] | flattened field elements | |
| 249 | +| `…[].hash` | u64 | debug-data hash key | |
| 250 | +| `…[].num_assumes` / `num_proves` | u64 | totals across origins | |
| 251 | +| `…[].global_origin` | object \| null | one aggregated global record per value | |
| 252 | +| `…[].local_origins[]` | array | per-AIR-instance occurrences | |
| 253 | +| `…[].local_origins[].rows` | [usize] | sorted, not truncated | |
0 commit comments