/-
  Two-tier interface for the whole aok system, not just zkpop.

  Tier 0 (Publishable) is universal -- every project (zkpop, monster, lean4,
  dotagents, dasl) already satisfies it via aok-publish.py / manifest.json.
  Nothing new to build; this just names the existing shape.

  Tier 1 (Argument) is for projects that make a checkable CLAIM about
  something -- a subset of projects, not all of them. ZkPoPArgument (see
  ZkPoPCore.lean) is one refinement of Argument, for claims whose evidence
  must stay hidden. Plain arguments (evidence public) are the other.

  dotagents does NOT get a Tier-1 instance below, on purpose: it has not
  published a claim, only tooling. Giving it a fake Statement/verify pair
  would be the same error as forcing mog's content modulus onto a generic
  crypto rung -- inventing structure the project doesn't actually have.
-/

/-- Tier 0: universal. Mirrors manifest.json's existing entry shape exactly,
    so this is a description of what already exists, not a migration. -/
structure Publishable where
  uuid      : String
  project   : String
  title     : String
  tags      : List String
  sha256    : String
  files     : List String
  author    : String
  published : String   -- ISO timestamp, as already stored

/-- Tier 1: for projects making a checkable claim. Deliberately minimal --
    `Evidence` is a type parameter so a project chooses whether its evidence
    is public (plain argument) or must stay hidden (zk argument, see
    ZkPoPArgument, which additionally requires `[ZkPoPGroup G]` and routes
    Evidence through a commitment). -/
class Argument (Statement Evidence : Type) where
  verify      : Statement → Evidence → Bool
  contentOnly : Bool   -- true if this claim's parameters ARE its content
                        -- (e.g. mog's sporadic modulus) and must not be
                        -- swapped for a "better" generic choice

/-- Per-project fit. GENERATED, not hand-maintained -- see
    bootstrap_transport.py. This block is the checked-in snapshot of that
    script's last solve; regenerate it whenever a project's declared
    features change or a new project is added. Do not hand-edit this list
    the way an earlier draft of this file did. -/
inductive ProjectKind
  | zkArgument      -- evidence hidden
  | contentArgument -- evidence public but IS the claim
  | plainArgument   -- evidence public, ordinary check
  | publishOnly     -- Tier 0 only, no Tier-1 claim yet

-- GENERATED by bootstrap_transport.py, total cost 5.0 -- do not hand-edit.
def projectFit : List (String × ProjectKind × Nat) := [
  ("agda-zkpop-v1",       .zkArgument,      1),
  ("mojo-zkpop-v1",       .zkArgument,      1),
  ("nodejs-zkpop",        .zkArgument,      2),
  ("zk-pop-solana-lean4", .zkArgument,      1),
  ("mog-zk-pop-v1",       .contentArgument, 0),
  ("monster",             .contentArgument, 0),
  ("dasl",                .plainArgument,   0),
  ("dotagents",           .publishOnly,     0),
  ("lean4",               .publishOnly,     0)
]

/-
  ZkPoPCore: a standard API that every zkPoP argument (agda, mojo, nodejs,
  solana-lean4, and future instances) implements, instead of each paper
  restating its own commitment/protocol from scratch.

  This does NOT reprove completeness/soundness/HVZK per instance. Those are
  proved once, generically, against the `ZkPoPGroup` interface. An instance
  only has to prove it satisfies the interface -- exactly the move the
  transport plan identified as low-cost (cost 1-2 per source) for four of
  the five source papers.
-/

/-- The group interface every concrete instantiation (Ristretto255, or in
    principle any other group) must satisfy. This is the ONE thing that
    changes when you swap crypto cores; nothing downstream re-proves. -/
class ZkPoPGroup (G : Type) where
  op        : G → G → G
  inv       : G → G
  id        : G
  q         : Nat                       -- group order (must be prime)
  q_prime   : q.Prime
  g h       : G                         -- two generators; h via fixed hash-to-group, NOT ad hoc
  h_indep   : True                      -- placeholder: "discrete log of h w.r.t. g is unknown"
  hard_dl   : True                      -- placeholder: discrete-log hardness assumption

/-- A statement being argued: a Merkle root over the withheld corpus, plus
    the environment/checker identifiers every paper already publishes. -/
structure ZkPoPStatement where
  merkleRoot   : ByteArray
  envHash      : ByteArray
  checkerId    : ByteArray

/-- A witness: the digest/scalar the prover actually knows, never disclosed. -/
structure ZkPoPWitness (G : Type) [ZkPoPGroup G] where
  m : Nat   -- the committed scalar (e.g. Merkle root mod q)
  r : Nat   -- Pedersen blinding factor

/-- The transcript, built by ONE shared strong-Fiat-Shamir routine, not a
    per-paper hash string. Binds protocol name + all public params + all
    prover messages BEFORE the challenge is derived. -/
structure ZkPoPTranscript (G : Type) where
  protocolTag : String := "aok-zkpop/2"
  statement   : ZkPoPStatement
  commitment  : G
  announcement: G
  challenge   : Nat
  responses   : Nat × Nat

/-- L5 Session: the actual protocol exchange (commitment, challenge,
    response). Swappable independently of the L4 guarantee below -- e.g.
    Schnorr vs. a different Sigma-protocol shape, same guarantee. -/
class ZkPoPSession (G : Type) [ZkPoPGroup G] where
  commit   : ZkPoPWitness G → G
  prove    : ZkPoPWitness G → ZkPoPStatement → ZkPoPTranscript G
  verify   : ZkPoPStatement → ZkPoPTranscript G → Bool

/-- L4 Transport: the delivery GUARANTEE a session must satisfy, proved
    once, generically, against any [ZkPoPSession]. Swapping the session
    (L5) does not require reproving this; swapping the guarantee's strength
    (e.g. adding post-quantum soundness later) does not require touching L5. -/
class ZkPoPTransportGuarantee (G : Type) [ZkPoPGroup G] (S : ZkPoPSession G) where
  completeness      : ∀ w s, S.verify s (S.prove w s) = true
  special_soundness : ZkPoPTranscript G → ZkPoPTranscript G → ZkPoPWitness G
  perfect_hvzk      : True  -- placeholder: simulator distribution = real distribution

-- ZkPoPArgument (previous version) = ZkPoPSession + ZkPoPTransportGuarantee
-- bundled together. Kept as a convenience alias, not the primary interface:
class ZkPoPArgument (G : Type) [ZkPoPGroup G] extends ZkPoPSession G where
  extract : ZkPoPTranscript G → ZkPoPTranscript G → ZkPoPWitness G

/-- Registry entry: what each paper actually instantiates. This is the
    diagonalized manifest row, expressed as data instead of prose. -/
structure ZkPoPInstance where
  name          : String
  groupChoice   : String   -- "Ristretto255" | "2^521-1 Mersenne (content)" | "sporadic-order (content)"
  transportCost : Nat      -- from the LP solve
  contentBearing: Bool     -- true only when the modulus IS the theorem (e.g. mog)

def registry : List ZkPoPInstance := [
  ⟨"agda-zkpop-v1",        "Ristretto255", 1, false⟩,
  ⟨"mojo-zkpop-v1",        "Ristretto255", 1, false⟩,
  ⟨"nodejs-zkpop",         "Ristretto255", 2, false⟩,
  ⟨"zk-pop-solana-lean4",  "Ristretto255", 1, false⟩,
  ⟨"mog-zk-pop-v1",        "sporadic-order (content)", 1, true⟩
]

/-
  Folded reconstruction across untrusted peers.

  This is NOT a refinement of the existing N-of-M PNG carrier scheme --
  that scheme tolerates erasure (missing shares), not corruption (wrong
  shares from an adversarial peer). This interface is strictly stronger and
  should be treated as a new primitive, not a drop-in upgrade.

  Two separable concerns, each its own typeclass on purpose (same reasoning
  as splitting ZkPoPSession from ZkPoPTransportGuarantee): reconstruction
  and folding are independently swappable and should not be bundled.
-/

/-- A single slice of execution contributed by one (possibly adversarial)
    peer/thread, bound to a commitment so a wrong slice is detectable, not
    just missing. -/
structure ExecSlice where
  threadId    : Nat
  commitment  : ByteArray   -- binds this slice's content
  merklePath  : List ByteArray  -- authenticates commitment against the global root
  payload     : ByteArray   -- the slice itself (opened only on reconstruction)

/-- L4-analogue for reconstruction: the guarantee is "t-of-n authenticated
    slices reconstruct the execution, and any slice failing its own
    Merkle path is REJECTED, not silently included." This is what turns
    erasure-coding into Byzantine fault tolerance -- the authentication,
    not the erasure code itself. -/
class ByzantineReconstruction (n t : Nat) where
  globalRoot   : ByteArray
  authenticate : ExecSlice → Bool          -- checks merklePath against globalRoot
  reconstruct  : List ExecSlice → Option ByteArray
                                            -- succeeds iff ≥ t authenticated slices present
  -- guarantee to prove: ∀ slices, (authenticated slices).length ≥ t →
  --   reconstruct slices = some (true execution), independent of what the
  --   remaining n-t peers (up to fully adversarial) contributed.

/-- Folding: combine per-slice execution proofs into one proof whose size
    does not grow with the number of threads. Concretely: Nova-style
    relaxed-R1CS folding, `U' = fold U1 U2` via a Fiat-Shamir challenge `r`
    and cross-term correction. This is ASSOCIATIVE under tree-shaped
    reduction (any balanced binary tree of pairwise folds over the
    authenticated slice set gives a sound final instance) -- it is NOT
    commutative as a raw binary op, since each fold step has a "running"
    and an "incoming" role with an asymmetric cross-term. Tree-shaped
    associativity, not commutativity, is what lets untrusted peers'
    slices fold correctly regardless of arrival order. -/
class FoldedExecution (RelaxedInstance : Type) where
  fold       : RelaxedInstance → RelaxedInstance → RelaxedInstance  -- Nova fold step
  proveSlice : ExecSlice → RelaxedInstance
  -- guarantee to prove:
  --   1. tree-associativity: for any two balanced binary trees T1, T2 over
  --      the same authenticated slice multiset, foldTree T1 = foldTree T2
  --      up to relaxed-instance equivalence (NOT claiming `fold` itself is
  --      commutative -- only that the final folded result is tree-shape-
  --      independent, which is the actual property Nova needs and gives).
  --   2. soundness transports through fold: if U1, U2 are each sound
  --      (satisfy their relaxed R1CS relation), fold U1 U2 is sound.
  --      Same "soundness transports, is not created" statement the
  --      self-hosted paper already makes about ordinary recursion.
  --   3. a single unauthenticated/corrupted slice's `proveSlice` output
  --      must make every subsequent fold containing it unsound -- folding
  --      must not average a bad slice's error away.

/-- The decider: wraps the single final relaxed R1CS instance (after all
    folding is done) into one short, pairing-based SNARK -- Groth16 -- so
    the verifier never touches relaxed-R1CS objects directly. This is the
    only place a per-circuit trusted setup is needed; the fold steps
    themselves need none. -/
class Decider (RelaxedInstance Groth16Proof : Type) where
  decide : RelaxedInstance → Groth16Proof
  verify : Groth16Proof → Bool
  -- guarantee to prove: verify (decide U) = true iff U satisfies its
  -- relaxed R1CS relation -- i.e. the decider is complete and sound with
  -- respect to whatever the fold tree actually accumulated.

/-- The composed guarantee this whole thing is actually for: reconstruction
    succeeds AND the folded proof verifies, using only threads that pass
    authentication -- explicitly not "most threads agree," which is a much
    weaker and different property (that would be closer to a BFT consensus
    guarantee, not a proof-of-execution guarantee). -/
structure FaultTolerantExecutionClaim (n t : Nat) (RelaxedInstance Groth16Proof : Type)
    [ByzantineReconstruction n t] [FoldedExecution RelaxedInstance]
    [Decider RelaxedInstance Groth16Proof] where
  claim : String := "execution is reconstructible and its tree-folded Nova instance, \
                      once decided into a Groth16 proof, verifies from any t-of-n peers, \
                      with corrupted/unauthenticated contributions rejected rather than \
                      averaged in"