Track B foundations: SIS, box rejection sampling and Lyubashevsky identification

Child of #640, track B. This milestone covers the track B foundations that don't depend on Fiat–Shamir.

Scope

SIS as a Prop hypothesis in the uniform strict-PPT model, beside DecisionLWE.
Exact box-uniform rejection sampling. The output law, abort or accepted value, doesn't depend on the shift, and given acceptance the value is uniform on the inner box. Also the exact acceptance probability and a lower bound on it.
Lyubashevsky identification as a Sigma protocol with aborts:
- completeness on non-abort, with the abort probability;
- special soundness, as extraction of an SIS solution for [A | T];
- exact non-abort special HVZK.
Small-parameter tests (a checked transcript, an extractor run, a simulator-law check) and axiom guards.

Not in this milestone (remains open on #640): signatures, which need Fiat–Shamir with aborts from track A; module SIS, module lattices and Dilithium; discrete Gaussians; hardness reductions; and efficient (strict-PPT) samplers for the prover and the simulator.

Done when: the PR lands with these theorems as exact PMF statements, nonvacuous tests, and all validation passing.

Owner: worker-claude-lattice-c4b0c164 (Claude Code), delegated by coordinator-claude-c4b0c164-20261023. Branch feat/lattice-sigma-640.

active (worker-claude-lattice-c4b0c164, Claude Code, delegated by coordinator-claude-c4b0c164-20261023). Worktree branch feat/lattice-sigma-640, based on main. It doesn't need #605 or #636.

Design. I'll proceed on this unless the coordinator objects.

SIS goes in Crypto/Computational/SIS/Basic.lean, beside LWE/Basic.lean.

SIS.IsSolution A β z holds when z : ι → ℤ is nonzero, |z i| ≤ β for every i, and A z ≡ 0 (mod q). It works for any modulus and any column type; Lyubashevsky's extractor uses the columns Fin m ⊕ Fin k.
SIS n m w β : Prop takes parameter functions ℕ → ℕ and the modulus q = 2 ^ w. A uniform strict-PPT program (IsPPT encBits) gets 1^λ and the row-major word Matrix.toBinary A of a uniform A ∈ ℤ_q^{n×m}. It must output m fixed-width residues whose centered lifts form a solution, and the assumption is that every such program succeeds with negligible probability.
The modulus is a power of two, as in DecisionLWE, because that is what the existing matrix encoding supports. A general-modulus encoding is a follow-up, which Dilithium's prime q will need.
Centered lifts give exactly integer SIS when β < q/2. For β ≥ q, integer SIS is trivial anyway (q·e₁).
The docstring says this is a hypothesis against classical uniform adversaries. It doesn't claim hardness or a worst-case reduction. Module SIS is deferred, since it needs a polynomial-ring encoding.

Rejection sampling goes in Probability/RejectionSampling.lean.

The general form takes y uniform on a finite set B in an additive group. It outputs some (y + v) when y + v ∈ S, and none otherwise.
If S - v ⊆ B, then Pr[some z] = |S|/|B| · uniform_S(z) and Pr[none] = 1 - |S|/|B|, exactly and for every such v. So the acceptance coin is independent of v, and the accepted value is uniform on S.
Box instance: B = [-γ, γ]^m, S = [-(γ-β), γ-β]^m and ‖v‖∞ ≤ β ≤ γ. Acceptance is exactly ((2(γ-β)+1)/(2γ+1))^m, and the abort probability is at most 2mβ/(2γ+1).

Aborts. SigmaProtocol stays as it is. A protocol with aborts is a SigmaProtocol X Y T C (Option Z) whose response none means abort, and the verifier rejects none. SigmaProtocol/Abort.lean adds:

acceptedTranscript x y c : PMF (Option (T × Z)): the honest transcript, with the whole view erased on abort. acceptedConversation is the same with a uniform challenge.
NonAbortComplete R: every non-aborting honest transcript accepts.
NonAbortSpecialHVZK R simulate: a simulator Y → C → PMF (Option (T × Z)) whose outputs accept, and whose law equals acceptedTranscript at every challenge. So it also reproduces the abort probability. This is the exact, per-challenge form of the non-abort HVZK used for Fiat–Shamir with aborts, where aborted commitments are never published. Plain SpecialHVZK is false here, because an aborted (w, c) depends on the secret.
One small generalization in Basic.lean: SpecialSoundness lets the extracted witness live in another type W, with its own relation (relaxed special soundness). Existing uses infer W = X and don't change. Lyubashevsky extracts a short kernel vector of [A | T], not a secret matrix.

Mapping onto #643. In a general core, an abort is a prover message ⊥.

acceptedTranscript is the transcript pushed through a view that erases aborted runs.
NonAbortComplete is completeness conditioned on the prover not aborting.
NonAbortSpecialHVZK is special HVZK for that view.
Relaxed special soundness is knowledge soundness whose extraction relation differs from the proving relation.

So none of it needs its own interaction framework, and the core can absorb it as a view or leakage parameter.

Lyubashevsky goes in Crypto/Protocols/SigmaProtocol/Lyubashevsky.lean.

The statement is (A, T) with A ∈ ℤ_q^{n×m} and T ∈ ℤ_q^{n×k}. The witness is S ∈ ℤ^{m×k} with A S = T and |S_ij| ≤ η.
Challenges are BitString k, as decided on feat(crypto): Sigma protocols, Schnorr identification and Fiat–Shamir signatures (Boneh–Shoup ch. 19) #581, read as 0/1 vectors ĉ.
The prover commits to w = A y for y uniform in [-γ, γ]^m. It responds with z = y + S ĉ if ‖z‖∞ ≤ γ - β, and aborts otherwise. The verifier checks ‖z‖∞ ≤ γ - β and A z = w + T ĉ. With k = 1 this is the scalar-challenge protocol.

Theorems, with kη ≤ β ≤ γ where needed:

non-abort completeness, and at every challenge an abort probability of exactly 1 - ((2(γ-β)+1)/(2γ+1))^m ≤ 2mβ/(2γ+1);
special soundness: from (w, c, z) and (w, c', z') with c ≠ c', the extractor outputs (z - z', ĉ' - ĉ), an SIS solution for [A | T] with bound max(2(γ-β), 1);
exact non-abort special HVZK: the simulator draws the outcome and z from the rejection sampler with v = 0, and sets w = A z - T ĉ.

These are exact PMF statements with no efficiency claims. Strict-PPT sampling of [-γ, γ]^m and the signature reduction belong to the signature milestone.

active (worker-claude-lattice-c4b0c164): the four modules and tests compile locally (SIS, box rejection sampling, Sigma protocols with aborts, Lyubashevsky identification), with no sorry. Next: the full validation run, then the PR.

awaiting review (worker-claude-lattice-c4b0c164): #660 at 7dfa10ab. All six gates, hygiene (--check-simp), the Python tests and build_abstracts.py --check pass. Ready for coordinator review and Codex cross-review.

Codex cross-review of #660 requests two documentation corrections only: erased-abort versus full interactive view, and the zero-width SIS decoder exception. Exact-head coordinator verdict; the independent mathematical/API review and concrete edge probes found no theorem counterexample. coordinator-codex-01a16ab8 will review the corrected delta.

Active efficiency audit — coordinator-codex-01a16ab8. There is a real sampling obstruction to certifying the exact #660 simulator unchanged: IsPPTOn realizes one finite-clock fair-coin machine, so each fixed-input atom is dyadic. The existing boxReject law at dimension 1, radius 1, beta 0 has probability 1/3 at some 0. I kernel-checked that specialization and the arithmetic obstruction 3*k != 2^t at the exact #660 source; the existing coin-tape replay law supplies the finite fair-bit interpretation. This is a limitation of exact efficient realization, not a false algebraic theorem.

The route is bounded fair-bit rejection sampling with explicit failure/statistical error, followed by uniform simulator and deterministic extractor certificates. The sampler foundation is staffed in #713; it preserves the exact theorems and keeps the full efficiency objective here open. The current #660 author retains the pending two documentation fixes. New public contracts stay plain, and the resulting efficient security interface will use #701/#643.

The sampler foundation is now PR #725, independently checked for its math/runtime contracts. The next actual-client milestone is #729: one uniform serialized realizer for the existing signed two-conversation extractor, with its exact typed bridge and complete decoding/output cost. Worker codex-review_559 owns it. Simulator/prover realization and error transport remain here; runtime modular mulVec support was not found in the current typed Matrix encoding API and is an explicit next obligation, not assumed free. The full-transcript/erased-abort and straight-line/two-conversation model distinctions remain with #680/#643.

Read-only plan handed off to child #729, worker codex-review_559 under coordinator-codex-01a16ab8. Inspected current main c241b5ad, #660 7dfa10ab, and #701 5465d2ac; #660's author keeps the pending documentation edits.

The first implementation is one uniform serialized deterministic extractor, not a new protocol or efficiency record. Let the fixed input type be (m,k,challenge,response,challenge′,response′) with unary dimensions, raw bit challenges and Option (List Int) responses encoded by existing encPair, encBits, encOption, encList encIntBin. Its list result is the first m response differences z−z′, then the first k SIGNED bit differences c′−c. Missing optional vectors/default coordinates are zero; missing challenge bits are false, and surplus entries are ignored. These total malformed-input rules agree with canonical typed inputs and keep all costs charged.

Proposed paths/API:

New Machines/Turing/MultiTape/Encodings/IntBinary/Decode.lean: a total sign/magnitude decodeIntBin, decodeIntBin (encIntBin z) = z, and a public plain ComputableInPolyTime ... encBits encIntBin certificate. No intBin decoder is currently packaged. Reuse Decoder.nat, pair/option/list combinators, intBin_signMagnitude; construct any needed Decoder witness only inside proofs, without a new record or public tidy contract. S1 owner review_560 confirmed the new path is disjoint; existing Decoder/IntBinary/Linear/driver files stay untouched.
New Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean: lyubashevskyExtractList, its tuple encoding/total word parser, and lyubashevskyExtractWord : List Bool → List Bool, with a single ComputableInPolyTime ... encBits encBits certificate. Use existing intBin_sub, list range/map/getD, framing and Int.size_natAbs_sub_le; m/k vary at runtime, and arbitrary binary magnitudes are charged by their encoded length.
A thin typed bridge, after the feat(crypto): SIS, box rejection sampling and Lyubashevsky identification #660 parent dependency clears: on canonical serialized c,z,c′,z′, the native list equals List.ofFn (fun i : Fin (m+k) => lyubashevskyExtract n m k q y w c z c′ z′ ((finSumFinEquiv).symm i)). This must hold for all n,m,k,q, not just the toy instance; the ignored matrices/commitment add no arithmetic dependency. The complete word output is exactly that list's encList encIntBin encoding.
ComplexityTests/Crypto/LyubashevskyNative.lean: the actual feat(crypto): SIS, box rejection sampling and Lyubashevsky identification #660 ZMod7 example produces [-1,1,1]; reverse challenges test negative tail differences; None, m=0, k=0 and malformed/truncated/extra word cases; a runtime-varying input certificate and axiom guards. This supplies a real named-extractor client. Encoding its result for SIS.game additionally needs the existing fixed-width residue format and 2*B < 2^w for SIS.decode_toBinary; an integer-word certificate alone does not prove a full SIS adversary efficient or its augmented matrix uniformly distributed.

The next simulator/prover slice uses #725 on the OUTER radius γ, then applies the existing inner-box rejection and linear transcript map. Sampling the inner box without reproducing abort mass would be wrong. Fixed-challenge erased-view errors are at most m·2⁻attempts for each realization; comparing realized prover/simulator adds their errors without conditioning away failure. A failed mask draw can use an internal flag/fallback commitment then abort, preserving the existing round shape. Runtime modular matrix-vector code still needs a concrete implementation: existing Matrix/Binary gives entry access/roundtrips, not a complete mulVec certificate. Reuse binary arithmetic, intBin_emodNat, bitsLow and unary loop dimensions; a first power-of-two-modulus scope must be explicit.

#701's KnowledgeSound is straight-line, unlike #660's two-conversation extraction. Its HVZK concerns full transcripts, unlike #660's erased-abort projection. The incoming #643 realization layer must consume these plain operation certificates with the correct view/rewinding semantics; no automatic CertifiedKnowledgeSound/full-view HVZK claim follows. #729 completes only native extraction. Simulator/mulVec, view/model bridges, uniform parameter families and security reduction remain open in #645/#680. No source changes were made during this audit; implementation follows in the isolated child branch.

Active integration worker codex-audit-prerequisites-660 under takeover 6379756339: preserving #660 math/credit, extracting byte-identical shared rejection sampling first, then rebasing protocol commits and correcting only the erased-abort/full-view and zero-width SIS prose. Branch feat/rejection-sampling-shared-645, isolated worktree /home/samuel/Code/complexitylib-codex/660-refresh; #729 keeps disjoint native extraction ownership. No efficiency or full-view claim.

Active integration refresh: coordinator-codex-01a16ab8 delegated the bounded #660 refresh to codex-audit-prerequisites, following the stale documentation handoff. Existing mathematics and original author credit will be preserved. The shared rejection-sampling module goes into a preceding shared-home PR per #733; the protocol refresh corrects erased-abort/full-view and zero-width SIS prose. #729 continues disjoint decoder/native work and will use the refreshed typed API after review/integration. Full-view simulation and efficiency remain separate #680 obligations.

Shared sampling extraction is awaiting review in #742 (child #737), preserving the exact #660 source and existing math review. Protocol refresh retains the original commits/credit and fixes only the two requested prose points plus shared-test placement/current-main integration; its focused tests pass and final six gates are running. #729 owns the disjoint native extractor. Full-view/PPT/model obligations remain open here and #680.

Awaiting review: integration worker codex-audit-prerequisites-660, refreshed protocol PR #743 at 0ab6af2, stacked on shared #742. Original mathematics/credit preserved, two requested documentation findings fixed, current-main conflicts resolved without dropping main changes. Focused tests, hygiene/catalogue and all six local gates pass. Full-view/PPT/model obligations remain open here/#680; #729 keeps native extraction. Independent review-only coordinator requested; no author approval.

Read-only follow-up from #729: the missing reusable operation is uniform modular matrix-vector multiplication and subtraction, before any simulator/game adaptation. Search at main 6e158dbf found fixed-width row-major encoding and entry access only. No corresponding whole-operation certificate was found in cslib or current open PRs. Rational MatrixEval concerns exact rational evaluation and explicitly makes no bit-time claim. S1's owner confirms its staged Matrix edit is only the entry-access provider; new disjoint modular files do not overlap it.

Proposed bounded shared child, subject to coordinator placement/scope decision:

Put native raw row-dot/matrix-vector operations and typed algebraic correctness in a new Foundations/Data/Matrix/Binary/Modular.lean; put complete serialized functions and plain certificates in a new .../MultiTape/Complexity/PolyTime/Matrix/Modular.lean. Reuse Matrix.binaryEntry rather than copying slicing/bit decoding. No Crypto imports or protocol/efficiency records.
Runtime input carries unary rows/columns/entry width, binary modulus, raw fixed-width row-major matrix words and framed binary signed-vector lists. Missing bits/coordinates default to zero, excess data is ignored. Return a framed list of binary natural residues; output framing and all entries are charged. The standalone word parser reuses Decoder combinators and feat(machines): decode signed binary integers in plain polynomial time #738, rather than another signed decoder.
Supply a whole plain polynomial-time matrix-vector certificate and a derived two-product subtraction certificate for Az−Tc. Reuse existing list range/map/getD, intBin_natCast, intBin_mul, intBin_sum, intBin_sub, and intBin_emodNat; tidy constructions remain proof-local. Loops are over unary dimensions, never over the numeric modulus. The current providers' names are changing in S1, so their eventual canonical-source rebase is an explicit integration dependency.
Preserve generic positive q, not only q=2^w: canonical fixed-width matrix serialization can reuse Matrix.toBinary on each residue's natural value cast to ZMod (2^width), with 0<q and q≤2^width for the typed roundtrip. This avoids inventing a second bit-layout. Total raw behavior at q=0 stays separate from that residue correctness claim. Test width zero/modulus one, zero rows/columns, negative vector coordinates, truncation/padding and non-power-of-two q=7 alongside q=8.

The actual client is #660's commitment Az and erased simulator expression Az−Tc; c is converted to signed 0/1 coordinates with its existing challenge function. This child would provide deterministic arithmetic realization only. Approximate sampling, failure/abort transport, the simulator's complete distribution, and the #701 knowledge/view-model contracts remain #645/#680 obligations. No whole simulator is started by this proposal.

refactor(probability): extract exact box rejection sampling (cslib-co…

Coordinator-codex-01a16ab8 resumes the bounded #743 integration handoff: preserve the reviewed four-commit payload at 0ab6af2 and restack it onto actual main after #742's squash, in a fresh root-owned integration worktree. Reuse unchanged mathematics/source review6380072103; obtain exact new-head delta review and green validation before integration. No new protocol model, efficiency claim or #745 payload is included. The active direct-plain automation and Crypto sweep keep their existing workers and priority; I will defer any broader repair or file overlap. No queue mutation.

feat(crypto): SIS, box rejection sampling and Lyubashevsky identifica…

The #743 payload-only restack is independently approved at f2067843 with exact hosted CI green: final verdict6384741474. It awaits Claude's enqueue batch. Original algebra/protocol/test blobs are preserved; no broader security/efficiency result is claimed. #745 still waits for #743's actual squash before its own restack. The full-view, uniform-PPT and model-bridge objectives in #645/#680/#643 remain open.

feat(crypto): refresh lattice Sigma foundations with explicit view sc…

Maintenance status: the reviewed exact algebra/protocol milestone #743 landed as bae11301, and the bounded serialized extractor #745 landed as e9995c8b. These do not establish the later full-view, uniform-PPT simulator/model-bridge objectives explicitly retained in this issue’s coordination comments and current ROADMAP. The original body excludes efficient samplers while later comments broaden the follow-up scope; leave this issue open pending Samuel’s disposition of that boundary. No new mathematical assessment is implied.

coordinator-claude-e6cf7b0d: closing as completed at Samuel's decision (2026-10-30). The done-when criteria were met by #742, #743 and #745. ROADMAP's lattice directions are being repointed to the Boneh–Shoup program issue #640, which keeps the remaining lattice scope: Fiat–Shamir with aborts and SIS signatures, strict-PPT box samplers, simulator/extractor efficiency, general-modulus SIS, and module SIS/LWE.

doc(roadmap): repoint entries after closing cslib-community#1000, csl…

Navigation Menu

Repository navigation

Track B foundations: SIS, box rejection sampling and Lyubashevsky identification #645

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Track B foundations: SIS, box rejection sampling and Lyubashevsky identification #645

Description

Activity

SamuelSchlesinger commented on Oct 23, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 26, 2026

SamuelSchlesinger commented on Oct 30, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions