research: ZK-Prologos lattice-native proof system plan#36
Draft
kumavis wants to merge 2 commits into
Draft
Conversation
Stage 0/1 research design for running Prologos on a lattice-based zero- knowledge proof system instead of compiling to a generic ZK-VM (RISC0, SP1, Jolt). Exploits the structural identity between Prologos's self- characterization as a module over the endomorphism ring of its lattice transformations (MODULE_THEORY_LATTICES.md) and Module-SIS-based crypto that proves statements about exactly that algebraic shape. Six-layer architecture: L0 R_q substrate, L1 cell-encoding bridges as on-network Galois pairs, L2 per-round LaBRADOR, L3 Lova/LatticeFold+ folding stratum, L4 verifier-as-stratum, L5 self-verifying compiler. Surveys current lattice-ZK landscape (LaBRADOR, Greyhound, SLAP, LatticeFold/+, Lova, Hachi, LaZer) with eprint citations. Identifies a research gap: no existing system natively proves dataflow / monotone- fixpoint computation, which Prologos's network execution trace is already a candidate witness for. Falsification paths for: type-lattice norm bounds, non-monotone strata (S(-1), S1 NAF), the "joincheck" speculation, quiescence as O(1) proof, concrete proof sizes, Fiat-Shamir assumptions, implementation realism. Phased plan ships incremental value: Phase 1 single-domain bridge, Phase 2 per-fire arithmetization, Phase 3 BSP-round prover, Phase 4 folding for succinctness, Phase 5 non-monotone, Phase 6 verifier- stratum, Phase 7 self-verifying compiler. Decision points (backend selection, verifiable subset, encoding granularity, self-verification depth) explicitly deferred to project lead. No implementation. No tests: pure research design.
Revise the lattice-ZK research doc to reflect honest assessment after review. Earlier draft claimed a "structural identity" between Prologos's order-theoretic lattices and Module-SIS's geometric lattices; that claim does not survive scrutiny. Idempotent commutative semilattice is not a Z-module. The bridge is an encoding, not an isomorphism. Changes: - TL;DR: drop "structural identity is not nominal"; add revision note pointing readers to honest accounting in new sections. - §1.4: replace strong/weak dichotomy with weak/medium/strong; medium (concrete shortcuts) is the operating thesis, strong is walked back. - §2.3: make algebraic mismatch explicit with a comparison table (idempotent monoid vs abelian group). - §2.4-2.6: split cell domains into Group A (native algebraic encoding, Galois bridge applies) and Group B (opaque-Merkle commit, no algebraic correspondence, R1CS circuits for joins). Galois-connection framing demoted to Group A only. - §5: soften Hyperlattice optimality claim; note two caveats (conjecture is about order-theoretic not cryptographic lattices; polylog(T) claim depends on Hasse-shaped folding, itself a research item). - §6 (NEW): twelve concrete shortcuts the lattice substrate enables, each tagged Group A / universal / theoretical. Includes "what is not a shortcut" subsection and per-round cost decomposition. - §7 (NEW): RISC0 feature-parity gap. Three engineering gaps (G1-G3) and two research gaps (R1-R2); explicit on which apply to ZK-Prologos. - §10.4: "lattice-on-lattice" qualified; partial realization for Group A, absent for Group B. - Renumber downstream sections (§7→§9, §8→§10, §9→§11, §10→§12); update cross-references. The architecture itself (six layers, phased plan, Lova/LatticeFold+ backends, verifier-as-stratum) is unchanged. What's changed is the framing: the document now commits to the medium thesis (lattice ZK is a good fit for Prologos's execution shape, with twelve concrete shortcuts to point at) instead of the strong thesis (the two senses of lattice are the same algebraic substrate).
kumavis
pushed a commit
that referenced
this pull request
May 9, 2026
Three new entries in 2026-04-27_GOBLIN_PITFALLS.md: - #36: Multi-line constructor / function application — continuation args on a separate line are eaten as an inner application. Hit twice in this branch (Phase 41 `bs-add-pipeline-msg`, Phase 48 `bs-gc-listeners-by-notified`); the second occurrence triggered codification per the workflow rule "codify a 2-occurrence pattern within a track immediately." - #37: Single-arg multi-arity `defn` over `data` patterns sometimes infers a phantom 2nd parameter. Hit on `resolution-syrup-of-pst` (Phase 48); the fix was to switch to `defn name [arg] match arg` shape, which pinned the inferred type back to the spec. - #38: `let X := EXPR` value can't span multiple lines. Hit on `drive-break-with-two-ops` (Phase 49); same workaround family as #21 and #36 — collapse to one line. Recorded separately because the error message ("missing value after :=") points at a different line than the actual broken `let`. Plus a "Recurrences during Phase 47-49" section noting that pitfall #16 (forward references) was hit again on `member-nat?` — existing entry confirmed correct. Also updated `.claude/rules/prologos-syntax.md` § "Application style" with two new bullets cross-referencing #36/#37/#38, so future implementations catch these at write time rather than at load-time error. Per the workflow rule "if a workaround is needed twice in the same track, add it to the pitfalls log AND to the relevant rule file immediately." https://claude.ai/code/session_01YM6gc3cMNH2Ymor4jdZY8u
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stage 0/1 research design for running Prologos on a lattice-based zero-
knowledge proof system instead of compiling to a generic ZK-VM (RISC0,
SP1, Jolt). Exploits the structural identity between Prologos's self-
characterization as a module over the endomorphism ring of its lattice
transformations (MODULE_THEORY_LATTICES.md) and Module-SIS-based crypto
that proves statements about exactly that algebraic shape.
Six-layer architecture: L0 R_q substrate, L1 cell-encoding bridges as
on-network Galois pairs, L2 per-round LaBRADOR, L3 Lova/LatticeFold+
folding stratum, L4 verifier-as-stratum, L5 self-verifying compiler.
Surveys current lattice-ZK landscape (LaBRADOR, Greyhound, SLAP,
LatticeFold/+, Lova, Hachi, LaZer) with eprint citations. Identifies a
research gap: no existing system natively proves dataflow / monotone-
fixpoint computation, which Prologos's network execution trace is
already a candidate witness for.
Falsification paths for: type-lattice norm bounds, non-monotone strata
(S(-1), S1 NAF), the "joincheck" speculation, quiescence as O(1) proof,
concrete proof sizes, Fiat-Shamir assumptions, implementation realism.
Phased plan ships incremental value: Phase 1 single-domain bridge,
Phase 2 per-fire arithmetization, Phase 3 BSP-round prover, Phase 4
folding for succinctness, Phase 5 non-monotone, Phase 6 verifier-
stratum, Phase 7 self-verifying compiler. Decision points (backend
selection, verifiable subset, encoding granularity, self-verification
depth) explicitly deferred to project lead.
No implementation. No tests: pure research design.