zkMemory: Zinc+ backend does not enforce original-trace consistency or the sorted-original permutation link

[bao-ninh-orochi]

Problem

PR #98 integrated Zinc+ as an optional proof-system backend for zkMemory's memory-consistency argument, but the Zinc+ UAIR currently proves only the sorted-trace consistency sub-statement: that a trace sorted by (address, time_log) is internally consistent.

Compared with the composed Halo2 circuit (MemoryConsistencyCircuit), two sub-statements are missing:

1. Original-trace consistency (OriginalMemoryCircuit): time_log[0] = 0 and time_log[i] < time_log[i+1] on the time-ordered execution trace.
2. Permutation link (PermutationCircuit / PLONK shuffle): the sorted trace is a permutation of the original time-ordered trace.

Without these, the Zinc+ backend is not a drop-in replacement for the Halo2 circuits.

Why this is hard in Zinc+

Zinc+ has no permutation/lookup argument (upstream's lookup layer is scaffolded but unimplemented), no verifier-randomness (RAP-style) columns, and all committed cells must be small integers fixed before the random prime modulus is sampled — so the standard randomized grand-product/LogUp permutation arguments are not expressible.

Proposed fix

Enforce the permutation link deterministically with a Beneš switching network inside the UAIR (the established challenge-free technique for RAM checking, cf. Pantry/Buffet/xJsnark):

• commit the original trace O (input wires) and sorted trace S (output side) plus 2v-2 intermediate routing states, where v = log2(padded rows);
• each layer applies boolean-selected conditional swaps between rows i and i + 2^k, expressed with Zinc+'s static row shifts and public bit-indicator mask columns;
• switch equations force each state to be an exact cell-wise permutation of the previous one, so multiset(O) = multiset(S) holds exactly (not probabilistically);
• add the original-trace time constraints (time[0] = 0, strictly increasing u64 time via limb-lexicographic slack) on the output side.

Routing bits are free witnesses: soundness never depends on how the prover routes, only completeness does.

This makes the Zinc+ statement match the Halo2 composed statement exactly (both have zero public inputs). Costs: trace width grows by the network states (~21 columns per state), and verification pays O(shift) per large-stride shifted column, so MAX_NUM_VARS should be reduced to a practical bound.