┌─────────────────────────────────────────────────────────────────────┐
│                    OFFLINE PHASE  (once per model)                   │
│                                                                      │
│   Model weights (400B MoE, 4-bit, ~232GB)                            │
│            │                                                         │
│            ▼                                                         │
│   ┌────────────────────────────┐                                     │
│   │  Hiding commitment         │  ← 39 min on 1× H100                │
│   │  (short fingerprint,       │    good for ~16M requests           │
│   │   weights stay hidden)     │    client downloads ~6.5MB total    │
│   └────────────┬───────────────┘                                     │
└────────────────┼─────────────────────────────────────────────────────┘
                 │  published commitment
                 ▼
┌─────────────────────────────────────────────────────────────────────┐
│                    ONLINE PHASE  (per request)                       │
│                                                                      │
│   prompt (1024-token window) + output tokens                         │
│            │                                                         │
│            ▼                                                         │
│   ┌────────────────────────────┐    ┌──────────────────────────┐     │
│   │  Prover (1× H100)          │    │  Proof file ~18.78 MB    │     │
│   │  · record computation      │───▶│  · hides weights         │     │
│   │    trace (matmul, round,   │    │  · hides intermediate    │     │
│   │    nonlinearity)           │    │    values                │     │
│   │  · prove trace used        │    │  · hides which experts   │     │
│   │    committed weights       │    │    actually ran          │     │
│   │  · batch up to 64 requests │    └────────────┬─────────────┘     │
│   └────────────────────────────┘                 │                   │
└──────────────────────────────────────────────────┼───────────────────┘
                                                   ▼
┌─────────────────────────────────────────────────────────────────────┐
│                    VERIFIER  (user side)                             │
│                                                                      │
│   inputs: commitment + prompt + reply + proof                        │
│            │                                                         │
│            ▼                                                         │
│   ┌────────────────────────────┐                                     │
│   │  cp_verify (C++, fast)     │  17 s on 24 threads                 │
│   │    → accept / reject       │  21 s on 1 thread                   │
│   │                            │  no GPU, no weights                 │
│   │  lean-verify (Lean, slow)  │  provably accepts only what the     │
│   │    → formally guaranteed   │  soundness theorem accepts          │
│   └────────────────────────────┘                                     │
└─────────────────────────────────────────────────────────────────────┘

import hashlib
import secrets


def offline_commit(weights_bytes: bytes, nonce: bytes | None = None) -> dict:
    """
    Offline phase, simplified: build a hiding commitment to the weights.

    Real FlashProve uses a zkSNARK-friendly polynomial commitment so that
    later proofs can *open* specific entries without revealing the rest.
    Here we only model the hiding + binding properties.
    """
    if nonce is None:
        nonce = secrets.token_bytes(32)

    # A hiding commitment = hash(nonce || weights).
    # Without the nonce you cannot brute-force weights from the digest,
    # and you cannot find two (nonce, weights) pairs with the same digest.
    digest = hashlib.blake2b(nonce + weights_bytes, digest_size=32).hexdigest()

    return {
        "commitment": digest,
        "nonce_kept_by_prover": True,   # verifier never sees this
        "weights_hidden": True,
        "size_bytes": 32,
    }


def online_prove(commitment: str, prompt: str, output_tokens: list[int],
                 computation_trace: dict) -> dict:
    """
    Online phase, simplified: assert that the committed model, run on this
    prompt, produces exactly these tokens.

    A real proof is ~18.78MB of zkSNARK data; here we only model what the
    proof *claims* and what it *hides*.
    """
    claims = {
        "statement": "committed_model(prompt) == output_tokens",
        "commitment": commitment,
        "checked_tokens": len(output_tokens),
    }
    hides = {
        "weights": True,
        "intermediate_values": True,
        "expert_selection_per_layer": True,
        "architecture": False,          # explicitly NOT hidden
    }
    return {
        "claims": claims,
        "hides": hides,
        "proof_size_mb": 18.78,
        "prover_gpu": "1x H100",
        "prover_seconds_per_batch_of_24": 223,
    }


def verify(commitment: str, prompt: str, output_tokens: list[int],
           proof: dict) -> dict:
    """
    Verifier side: cheap, no GPU, no weights.
    """
    ok = (
        proof["claims"]["commitment"] == commitment
        and proof["claims"]["statement"] == "committed_model(prompt) == output_tokens"
    )
    return {
        "accepted": ok,
        "verify_seconds_24_threads": 17,
        "verify_seconds_1_thread": 21,
        "gpu_required": False,
        "weights_required": False,
    }


if __name__ == "__main__":
    fake_weights = b"\x00" * 1024  # stand-in for ~232GB of quantized weights
    c = offline_commit(fake_weights)
    print(f"commitment: {c['commitment'][:16]}...  ({c['size_bytes']} bytes)")

    p = online_prove(c["commitment"], "explain zkSNARKs", [1, 2, 3], {})
    print(f"proof size: {p['proof_size_mb']} MB, hides weights: {p['hides']['weights']}")

    v = verify(c["commitment"], "explain zkSNARKs", [1, 2, 3], p)
    print(f"accepted: {v['accepted']}, GPU needed: {v['gpu_required']}")

# Why MoE sparsity is the single biggest lever on proving cost
def moe_proving_cost(total_params_b=400, active_per_token_b=17,
                     n_experts_per_layer=128, layers=48):
    """
    Prover work is proportional to the experts that actually ran,
    not to the full parameter count.
    """
    dense_relative = total_params_b / active_per_token_b
    # Per layer: 1 of 128 routed experts + 1 shared expert
    experts_active_per_layer = 2
    sparsity_ratio = experts_active_per_layer / (n_experts_per_layer + 1)

    return {
        "total params (B)": total_params_b,
        "active per token (B)": active_per_token_b,
        "dense-equivalent slowdown": f"{dense_relative:.1f}x",
        "experts active per layer": f"{experts_active_per_layer} of {n_experts_per_layer + 1}",
        "sparsity ratio": f"{sparsity_ratio:.1%}",
        "layers": layers,
        "consequence": "proving cost tracks 17B, not 400B",
        "extra burden": "must also prove router picked the right expert, "
                        "while hiding which expert was picked",
    }


for k, v in moe_proving_cost().items():
    print(f"  {k:28s} {v}")

# Batching: the single change that took throughput from 17.6 to 110 tok/s
def batching_throughput(window_tokens=1024):
    single = {
        "requests": 1,
        "total_seconds": 58,
        "tokens": window_tokens,
    }
    batched = {
        "requests": 24,
        "total_seconds": 223,
        "tokens": 24 * window_tokens,
    }

    single_tps = single["tokens"] / single["total_seconds"]
    batched_tps = batched["tokens"] / batched["total_seconds"]

    return {
        "single request (s)": single["total_seconds"],
        "single throughput (tok/s)": f"{single_tps:.1f}",
        "batch of 24 (s)": batched["total_seconds"],
        "batched throughput (tok/s)": f"{batched_tps:.1f}",
        "speedup": f"{batched_tps / single_tps:.1f}x",
        "per-request amortized (s)": f"{batched['total_seconds'] / 24:.1f}",
    }


for k, v in batching_throughput().items():
    print(f"  {k:28s} {v}")

# The zkML throughput curve, in tokens per second
def zkml_history():
    rows = [
        ("2017  SafetyNets",        "MNIST 2-conv CNN",       None,  "verified, not throughput"),
        ("2021  zkCNN",             "VGG-16 (15M)",           None,  "88.3 s per proof"),
        ("2024  ZKML GPT-2",        "117M",                   0.006, "159 s per token"),
        ("2024  Modulus GPT-2 XL",  "1.5B",                   0.0,   "over 90 hours"),
        ("2023  EZKL",              "1M GPT-style",           0.001, "966 s per token"),
        ("2024  zkLLM",             "LLaMA-2-13B",            2.5,   "batch, 2048-token input"),
        ("2025  zkGPT",             "GPT-2",                  0.05,  "21.8 s per token"),
        ("2025  zkPyTorch",         "Llama-3 8B",             0.007, "150 s per token, 1 CPU core"),
        ("2025  ZKTorch",           "GPT-J 6B",               0.001, "~20 min"),
        ("2026  VerInf",            "Llama 4 Maverick 400B",  0.02,  "14.3 h for 1k tokens, 93.6GB proof"),
        ("2026  DeepProve",         "Gemma 3",                1.4,   "2.9 tok/s on GPT-2, 31 distributed"),
        ("2026  SASH prover",       "Llama 3.1 8B",           1.25,  "single H100"),
        ("2026  FlashProve",        "Llama 4 Maverick 400B",  110.0, "1x H100, 19MB proof, 17s verify"),
    ]

    print(f"{'System':<26}{'Model':<28}{'tok/s':<10}{'Note'}")
    print("-" * 104)
    for name, model, tps, note in rows:
        tps_s = f"{tps}" if tps is not None else "n/a"
        print(f"{name:<26}{model:<28}{tps_s:<10}{note}")


zkml_history()

print("\nFlashProve vs VerInf on the SAME model (Llama 4 Maverick):")
print(f"  throughput: 110 / 0.02 = {110 / 0.02:.0f}x")
print(f"  proof size: 93.6 GB / 0.019 GB = {93.6 / 0.019:.0f}x smaller")
print(f"  verify time: ~1 day -> 17 s")

# What 70-95x GPU time means in practice
def proving_overhead(overhead_low=70, overhead_high=95,
                     h100_hourly_usd=2.0, tokens=1_000_000):
    """
    Translate the GPU-time multiplier into money per million tokens.
    """
    # Assume vLLM serves ~2000 tok/s per H100 for a 17B-active MoE at high load
    vllm_tps = 2000
    base_gpu_hours = tokens / vllm_tps / 3600

    rows = []
    for label, mult in [("proving, low end", overhead_low),
                        ("proving, high end", overhead_high)]:
        gpu_hours = base_gpu_hours * mult
        cost = gpu_hours * h100_hourly_usd
        rows.append((label, f"{gpu_hours:.1f}", f"${cost:.2f}"))

    print(f"{'Case':<22}{'GPU-hours / 1M tok':<22}{'Cost @ $2/h'}")
    print("-" * 62)
    for label, gh, cost in rows:
        print(f"{label:<22}{gh:<22}{cost}")

    print(f"\nBaseline (vLLM only): {base_gpu_hours:.2f} GPU-hours, "
          f"${base_gpu_hours * h100_hourly_usd:.2f}")
    print("\nInterpretation: proving is not free, but it is a *bounded* multiple —")
    print("two orders of magnitude, not six. That is what makes it deployable at all.")


proving_overhead()

# Cost model for sampling: full proof coverage is not the intended use
def sampling_policy(total_requests_per_day=10_000_000,
                    full_proof_cost_multiple=70,
                    audit_fraction=0.001):
    """
    Prove a sample of traffic, not all of it.
    """
    audited = int(total_requests_per_day * audit_fraction)
    # Cost is only paid on audited requests
    effective_multiple = 1 + (full_proof_cost_multiple - 1) * audit_fraction

    return {
        "daily requests": f"{total_requests_per_day:,}",
        "audited requests": f"{audited:,}",
        "audit fraction": f"{audit_fraction:.2%}",
        "effective cost multiple": f"{effective_multiple:.3f}x",
        "detection logic": "random audit makes substitution a losing bet: "
                           "one caught sample voids the provider's whole claim",
    }


for k, v in sampling_policy().items():
    print(f"  {k:26s} {v}")

# The three top-level properties, stated as assertions a checker could test
def check_properties():
    """
    Informal restatement of what Lean proves. Not a formal proof — just
    the shape of the three claims.
    """
    properties = {
        "completeness": {
            "claim": "honest prover's proof is accepted",
            "failure mode if violated": "honest providers get wrongly rejected",
            "who depends on it": "the provider",
            "lean statement": "forall stmt, is_true stmt -> verify (prove stmt) = accept",
        },
        "soundness": {
            "claim": "no valid proof exists for a false statement",
            "failure mode if violated": "a cheater can substitute a model and pass",
            "who depends on it": "the verifier",
            "lean statement": "forall stmt proof, verify proof = accept -> is_true stmt",
        },
        "zero_knowledge": {
            "claim": "proof leaks nothing about weights beyond the reply",
            "failure mode if violated": "provider's IP leaks through proofs",
            "who depends on it": "the provider",
            "lean statement": "exists simulator s.t. proof ~ simulator(commitment, stmt)",
        },
    }

    for name, d in properties.items():
        print(f"\n[{name}]")
        for k, v in d.items():
            print(f"  {k:26s}: {v}")

    print("\nKey asymmetry:")
    print("  soundness  depends ONLY on the verifier  -> provide a Lean verifier")
    print("  zero-knowledge depends ONLY on the prover -> no Lean prover is practical")
    print("  completeness depends on BOTH              -> test prover against Lean verifier")


check_properties()

# What a proof does and does not establish
def proof_scope():
    establishes = [
        "the reply came from the committed weights",
        "the committed weights were run on this exact prompt",
        "the checked token is that model's greedy choice",
        "no token in the stream was tampered with after generation",
    ]
    does_not_establish = [
        "the reply is factually correct",
        "the reply is safe",
        "the model is the one the provider advertised by name "
        "(only that it matches the published commitment)",
        "the architecture is hidden (it is NOT hidden)",
        "the hardware is not simultaneously training something else",
        "side channels (e.g. proving time) leak nothing",
    ]

    print("PROVES:")
    for i, s in enumerate(establishes, 1):
        print(f"  {i}. {s}")
    print("\nDOES NOT PROVE:")
    for i, s in enumerate(does_not_establish, 1):
        print(f"  {i}. {s}")


proof_scope()