shard ownership |
neo-fold-clean should have one obvious shard prover owner that scripts the flow without absorbing all protocol internals. |
Auditors need one place to trace shard proving end to end. |
Refactor neo-fold-clean around a small shard::prover plus owner modules below it. |
main_lane |
SuperNeo Pi_CCS -> Pi_RLC -> Pi_DEC remains the core fold owner for CE-family claims at one shared point. |
This is the paper-core folding path; it should stay explicit and not get hidden behind generic wrappers. |
Define the minimal main_lane API and proof artifact boundary. |
twist_shout owner |
Twist/Shout should start as an extension owner module, not as a promised fold lane. |
The papers justify projection from virtual claims to committed evaluation obligations, but not arbitrary merging into the main lane. |
Create a twist_shout owner that outputs explicit obligation families. |
| Fold admissibility |
Fold together only claims of the same relation at the same evaluation point. |
"Project everything into the main lane" is not paper-backed unless there is an explicit reduction proving it. |
Partition obligations by relation family and evaluation point before folding. |
| Twist/Shout integration |
Use Twist/Shout first as projection protocols, then fold only whatever becomes an admissible CE family. |
This is the most straightforward sound path from the papers. |
Specify which outputs become main-lane CE claims, separate fold families, or final obligations. |
| SumCheck security accounting |
SumCheck soundness is probabilistic and must be aggregated globally across all SumCheck-family uses; do not treat thousands of SumChecks as isolated. SuperNeo already uses union-bound style accumulation for bad events and composition-level negligible loss. |
Security accounting is wrong if each local SumCheck error is mentally ignored after the call returns. |
Define one protocol-level eps_sumcheck_total for neo-fold-clean, or a tighter grouped theorem if available. |
| Lean validation |
The right formal target is a bridge layer between SuperNeo and Twist/Shout, not a literal transcription of implementation stages. |
We need theorem-backed architecture, not just code structure. |
Add a new Lean bridge package proving projection, family partition, fold admissibility, and shard composition. |
build_superneo_ring_forms API footprint |
The helper is acceptable as a deterministic algebra routine, but it should not stay a wide root-level compatibility surface forever. |
It is not a transcript/soundness risk, but it is extra neo-ccs API surface and a large materialized form object. |
Keep it for now, then remove the root re-export once downstream imports are localized and add a direct equivalence test against y_ring = Z · M_j^T · χ(r) before any deeper refactor. |
Shape-scalar API split (StructureScalar / PayloadScalar) |
HN §6.2 Def 12.2 (partial functions) requires every scalar routed into CCS matrix coefficient material, circuit hash preimages, or transcript-lane constants to depend only on F', never on payload/claim/witness values. This contract is enforceable at the type level but today lives only in developer memory: shape-bound helpers (alloc_k_constant_k_linear_combination, digest_const_inputs, alloc_const_field_values, sample_goldilocks_rot_rhos, sumcheck_eval_gadget_constant_challenge, build_superneo_ring_forms, recursive_extend_*_as_fields) all accept raw &[K] / &[F] / K with no type-level distinction between structural and payload scalars. |
Six independent shape-leak bugs surfaced during Goal 2 bring-up, all sharing the exact same mechanism: a helper accepts a native scalar and bakes it into matrix/preimage/LC-constant material where the paper requires enc_str(F') determinism. Each instance was caught only by a fingerprint-drift probe hours-to-days after landing, each required a probe-and-localize cycle, and each was patched identically (switch to a variable-driven gadget with constant offset = 0). Without a typed invariant, there is no structural reason instance #7 will not appear after any feature addition touching matrix / preimage / LC-constant material. The test-based conformance check is not a substitute: it catches only bugs exercised by the chosen payload distribution. |
After Goal 2 closes, introduce newtype wrappers StructureScalar<K> and PayloadScalar<K> (both #[repr(transparent)], zero runtime cost). Split every shape-bound helper signature: the structural variant accepts only &[StructureScalar<K>]; payload-coefficient callsites migrate to a variable-driven counterpart taking &[KNumVar] with constant offset = 0. Restrict StructureScalar::structural to pub(crate) visibility or expose it only through named factories (::domain_tag, ::dimension, ::coeff_of_fixed_identity) so the trusted-construction surface is enumerable. Require a line comment at every construction site naming the structural source, and add a CI grep (or clippy lint) to keep the count auditable. Formalize "every scalar routed into CCS matrix coefficient material has type StructureScalar" as an invariant in the planned Lean bridge package, making the enumerable StructureScalar-construction list the sole remaining audit obligation for shape stability. Expected migration: ~10–15 helper signatures, ~50–100 callsites; land as a single PR so reviewers see the full structural-vs-payload decision distribution in one read. |