Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.05335

StateSync-GKR: Machine-Checking the Trust Chain from Sparse-Merkle State Transitions to GKR Verification

Jinwook Kim
View original source ↗Read source document ↗Export metadata ↓

Abstract

GKR soundness bounds false output claims about arithmetic circuits, but an application also needs assurance that its circuit encodes the intended state transition. We machine-check this connection for sparse-Merkle membership, non-membership, and update in Isabelle/HOL. A compiler model relates circuit acceptance to transition validity in both directions. A reusable protocol model assembles layer reduction, wiring-predicate extensions, and imported sumcheck soundness into a bound on an explicit chain event. Their composition transfers semantic invalidity to that bound, with the witness fixed before the challenge experiment. Concrete interpretations and premise activations expose vacuous assumption sets that a clean build alone would miss. A further development constructs the exact degree-four KoalaBear extension, lifts the base-field circuit objects, and establishes the assembly bound with denominator $p^4$ under its stated challenge assumptions. An executable Rust prover accompanies the model. Creusot/Why3 contracts provide a partial implementation connection, and a conditional theorem relates successful verifier traces to the model event under an undischarged value-correspondence premise. Neither the transcript's online challenge distribution nor a multi-round Fiat--Shamir reduction is established. The contribution is the composition, within one proof assistant, of compiler correctness with a GKR assembly model, together with an explicit account of the remaining implementation and cryptographic obligations.

Explore related subjects

cs.CRcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Jinwook Kim. 2026-10-04. StateSync-GKR: Machine-Checking the Trust Chain from Sparse-Merkle State Transitions to GKR Verification. https://arxiv.org/abs/2610.05335

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

PPFedIT: Towards Privacy-Preserving Federated Instruction Tuning with Few-shot Local Examples

Instruction tuning aligns large language models (LLMs) with human intentions but requires diverse, high-quality data that are difficult to collect in privacy-sensitive domains. Federated instruction tuning (FedIT) enables collaborative training across data owners, yet existing methods typically assume sufficient local data. In realistic few-shot settings, limited samples can cause overfitting, degrade performance, and increase vulnerability to training data extraction attacks. We propose PPFedIT, a federated algorithm that improves both model performance and privacy protection in federated few-shot learning. It comprises three client-side steps: (1) synthetic data generation, which uses LLMs to diversify and enrich local data; (2) parameter isolation training, which updates the shared global LLM on synthetic data and local LLMs on private local data to mitigate synthetic-data noise; and (3) local aggregation then sharing, which mixes global and local model parameters before uploading them for server aggregation to mitigate data extraction attacks. Experiments on three open-source datasets show that PPFedIT improves model performance by an average of 8.4% and reduces the risk of data extraction attacks by approximately 20% in challenging federated few-shot settings.

cs.CR↗
arXiv2026

Logit-Gap Steering: A Forward-Pass Diagnostic for Alignment Robustness

RLHF-style alignment trains language models to refuse unsafe requests, but how much operational margin does this refusal rest on? We introduce the refusal-affirmation logit gap: the difference between the top refusal-token logit and the top affirmative-token logit at the first decoding step. This single scalar quantifies the per-prompt safety margin that alignment provides. Empirically, alignment widens the gap on 97.5-99.8% of toxic prompts across three model families, and median gap closure co-varies with True-ASR ranking across suffix strategies (an internal consistency check, since our method optimises gap closure). To validate the metric's practical significance, we present logit-gap steering, a gradient-free, forward-pass-only method that discovers short in-distribution suffixes ($<$10 tokens per component) whose cumulative effect closes the gap. The method requires ${\approx}26{,}000$ forward-pass equivalents per family (${\approx}2$~min on one A100), ${\approx}125\times$ less than a single GCG search. Suffixes discovered on 0.5B--2B models transfer without modification to 72B within family. An 8-suffix ensemble reaches 38-96\% True ASR across 13 models on AdvBench and HarmBench, with most suffixes having $10^{3}$-$10^{4}\times$ lower perplexity than GCG-meaning published perplexity-filter defenses that collapse GCG (64.7%$\to$1.0%) leave our suffixes nearly intact (76.9%$\to$76.0%). These results demonstrate that current alignment margins, while consistently present, can be thin and efficiently measurable, and that defense strategies must account for in-distribution suffixes.

cs.CR↗
arXiv2026

Spoofing Missed-Detection Bounds for PRF GNSS Ranging Authentication Under AWGN Models

Pseudorandom-function (PRF) ranging codes, such as those used in Galileo's encrypted E6-C under the Signal Authentication Service (SAS), enable a receiver to authenticate pseudoranges once the PRF secret is revealed. This work bounds how much authentication security the receiver obtains under Additive White Gaussian Noise (AWGN) assumptions. Against a spoofer that does not estimate the code before submitting its forgery, PRF security makes the forged correlation zero-mean up to the security of the underlying PRF, allowing integration time and C/N$_0$ to mostly determine probability of missed detection (PMD) and probability of false alarm (PFA). Against such a spoofer at a conservative 30 dB-Hz, 400 ms of E6-C aggregation certifies a PMD below $2^{-128}$ (plus any PRF advantage). For a spoofer that estimates chips before submitting a forgery, I derive the receiving-antenna gain at which authentication security breaks, which is about 12 dB for E6-C for the adversaries modeled. This work can be used to design a PRF GNSS ranging code protocol and a receiver capable of correctly asserting PRF ranging security assuming an AWGN model.

cs.CR↗