dalek-ed25519-verified/verification/Proofs/Audit.lean

/- ──────────────────────────────────────────────────────────────────────────
   Proofs/Audit.lean — statement + specification binding (P1-a).

   WHAT THIS ADDS over check.sh Phases 2b/3/3b. Those establish that each
   certificate is a theorem and rests on exactly the declared axioms. None
   of them establishes WHAT THE THEOREM SAYS. A certificate gutted to a
   tautology keeps its name, its kind, and its axiom cone, and passes every
   one of them. Worse, the reference definitions the statements are stated
   AGAINST can be redefined to be the extracted code itself, at which point
   the certificate says `loop = loop` and every cone is unchanged.

   So this file emits a canonical AUDIT-MANIFEST block covering:
     · the POLICY constants (both cone tiers, and the module prefix that
       defines what counts as a specification);
     · every certificate's fully-elaborated STATEMENT (`pp.all`);
     · every specification constant transitively reachable from those
       statements, with its fully-elaborated DEFINITION BODY. A Prop-valued
       constant contributes its statement rather than its proof term, by
       proof irrelevance — the proof term is not what fidelity lives in.

   check.sh binds the SHA-256 of that block, and the block itself is
   committed, so a mismatch can be DIFFED against a reference rather than
   merely reported.

   TWO TIERS, NOT ONE. This repository has an arithmetic tier that must
   stay oracle-free and an apex tier that legitimately carries this fork's
   hash and wire-format axioms. The boundary differs BETWEEN FORKS. A
   single global allowed-axiom list would silently widen the arithmetic
   tier to accept hash oracles, which is the most valuable property these
   repositories have. Hence a per-certificate expected cone below.

   NO HAND-KEPT STATEMENT FINGERPRINTS. The companion SLH-DSA auditor pins
   a 32-bit `Expr.hash` per certificate as a diagnostic. That table is one
   more thing that can fall out of sync, and the canonical block already
   covers every statement at full fidelity — a diff of the block says more
   than a changed integer does. Membership is derived, not listed.

   STANDING LIMIT: an audit executed by a harness cannot defend against an
   author who edits that harness. The consumer defence is, and remains, the
   pinned commit reviewed at the pin.
────────────────────────────────────────────────────────────────────────── -/
import Proofs.FieldMain
import Proofs.EdMain
import Proofs.DsmTableSpec
import Proofs.DsmStepSpec
import Proofs.DsmLoopSpec
import Proofs.DsmNafLoadSpec
import Proofs.DsmNafMath
import Proofs.DsmNafSpec
import Proofs.DsmMulSpec
import Proofs.ToBytesSpec
import Proofs.CompressSpec
import Proofs.ScalarPackSpec
import Proofs.SigApexSpec
import Proofs.PointLiftSpec
import Proofs.PointEqSpec
import Proofs.DecompressSpec
import Proofs.FromBytesSpec
import Proofs.DecompressMain
import Lean
open Lean Elab Command

namespace Ed25519Audit

/-- Lean's three kernel axioms. -/
def kernel3 : List Name := [`propext, `Classical.choice, `Quot.sound]

/-- This fork's apex boundary: the hash oracle and wire-format symbols the
    signature-level certificates are permitted to rest on, and nothing else.
    POLICY CONSTANT — folded into the digest, so widening it moves the hash
    and fails the build. -/
def apexExtra : List Name :=
  [`ed25519.Signature, `sha2.Sha512, `verifying.sha512_finalize_bytes, `verifying.sha512_new, `verifying.sha512_update, `ed25519.Signature.to_bytes, `signature.error.Error, `signature.error.Error.new]

def apexBoundary : List Name := kernel3 ++ apexExtra

/-- A constant counts as SPECIFICATION if it was declared in a `Proofs.`
    module — i.e. hand-written by us, as opposed to the extracted model in
    `gen/` (pinned separately by Phase 0). Derived from the environment, not
    from a list, so a new specification module cannot appear unnoticed. -/
def specPrefix : String := "Proofs."

/-- Per-certificate expected cone. Arithmetic tier first, apex tier last. -/
def manifest : List (Name × List Name) :=
  [ (`CurveFieldProofs.fieldImplementation,            kernel3)
  , (`CurveFieldProofs.edwardsImplementation,          kernel3)
  , (`CurveFieldProofs.naf_table_spec,                 kernel3)
  , (`CurveFieldProofs.naf_select_spec,                kernel3)
  , (`CurveFieldProofs.proj_double_law,                kernel3)
  , (`CurveFieldProofs.compl_as_projective_law,        kernel3)
  , (`CurveFieldProofs.dsm_step_p_law,                 kernel3)
  , (`CurveFieldProofs.dsm_step_b_law,                 kernel3)
  , (`CurveFieldProofs.dsm_loop_spec,                  kernel3)
  , (`CurveFieldProofs.naf_load_spec,                  kernel3)
  , (`CurveFieldProofs.naf_exit,                       kernel3)
  , (`CurveFieldProofs.naf_digit_loop_spec,            kernel3)
  , (`CurveFieldProofs.non_adjacent_form_spec,         kernel3)
  , (`CurveFieldProofs.run_basepoint,                  kernel3)
  , (`CurveFieldProofs.vartime_double_base_mul_spec,   kernel3)
  , (`CurveFieldProofs.verify_loop_full,               kernel3)
  , (`CurveFieldProofs.to_bytes_spec,                  kernel3)
  , (`CurveFieldProofs.ed_compress_spec,               kernel3)
  , (`ScalarProofs.from_bytes_mod_order_wide_spec,     kernel3)
  , (`CurveFieldProofs.vartime_dsm_basepoint_spec,     kernel3)
  , (`CurveFieldProofs.enc_point_inj,                  kernel3)
  , (`CurveFieldProofs.pow_p58_spec,                   kernel3)
  , (`CurveFieldProofs.fe_ct_eq_spec,                  kernel3)
  , (`CurveFieldProofs.sqrt_core,                      kernel3)
  , (`CurveFieldProofs.sqrt_ratio_i_sq_spec,           kernel3)
  , (`CurveFieldProofs.from_bytes_spec,                kernel3)
  , (`CurveFieldProofs.decompress_of_canonical,        kernel3)
  , (`CurveFieldProofs.verify_accepts_iff,             apexBoundary)
  , (`CurveFieldProofs.verify_accepts_iff_point,       apexBoundary)
  , (`CurveFieldProofs.verify_accepts_iff_point_eq,    apexBoundary)
  , (`CurveFieldProofs.verify_accepts_iff_decompress,  apexBoundary)
  ]

/-- Deterministic name ordering for the canonical serialization. -/
def sortNames (l : List Name) : List Name :=
  ((l.map toString).toArray.qsort (· < ·)).toList.map (·.toName)

/-- Whitespace-canonical: every whitespace run collapses to one space, so the
    pretty-printer's line wrapping cannot perturb the digest. -/
def normWs (s : String) : String :=
  (s.foldl (fun (acc : String × Bool) c =>
      let c := if c.isWhitespace then ' ' else c
      if c == ' ' then (if acc.2 then acc else (acc.1.push ' ', true))
      else (acc.1.push c, false))
    ("", true)).1

/-- Was `n` hand-written by us, in a `Proofs.` module? -/
def isSpecConst (env : Environment) (n : Name) : Bool :=
  match env.getModuleIdxFor? n with
  | some idx => (toString env.header.moduleNames[idx.toNat]!).startsWith specPrefix
  | none => false

/-- Transitive closure over specification constants, starting from a
    certificate's STATEMENT and following DEFINITION bodies (a theorem
    contributes its statement only). This discovers the reference definitions —
    and any future one — automatically, so a new specification cannot be
    introduced, or an existing one redefined, without moving the digest. -/
partial def closureOf (env : Environment) (seen : NameSet) (work : List Name) : NameSet :=
  match work with
  | [] => seen
  | n :: rest =>
    if seen.contains n || !isSpecConst env n then closureOf env seen rest
    else
      let seen := seen.insert n
      let more := match env.find? n with
        | some (.defnInfo v) => v.value.getUsedConstants.toList ++ v.type.getUsedConstants.toList
        | some ci            => ci.type.getUsedConstants.toList
        | none               => []
      closureOf env seen (more ++ rest)

/-- Fully-explicit (`pp.all`) rendering, whitespace-canonicalized. Implicit
    arguments, instances and universe levels are all made visible, so two
    statements that merely LOOK alike cannot share a rendering. -/
def ppAll (e : Expr) : CommandElabM String := do
  let s ← Command.liftCoreM <| Meta.MetaM.run' <|
    withOptions (fun o => o.setBool `pp.all true) do
      return (← Meta.ppExpr e).pretty
  return normWs s

elab "auditStatements" : command => do
  let env ← getEnv
  let mut errs : Array String := #[]

  -- (0) The manifest may not permit an axiom outside the two declared tiers.
  --     Without this, widening a cone in the manifest would be invisible.
  for (cert, cone) in manifest do
    for a in cone do
      unless apexBoundary.contains a do
        errs := errs.push s!"manifest permits {a} for {cert}, which is outside every declared tier"

  -- (1) Each certificate must EXIST, be a THEOREM, and have EXACTLY its cone.
  --     Exact, not subset: a certificate that stopped depending on the hash
  --     oracle is as wrong as one that acquired a new axiom.
  for (cert, expected) in manifest do
    match env.find? cert with
    | none                 => errs := errs.push s!"{cert}: NOT FOUND (renamed or deleted?)"
    | some (.thmInfo _)    =>
        let got := (← collectAxioms cert).toList
        let extras  := got.filter      (fun a => !expected.contains a)
        let missing := expected.filter (fun a => !got.contains a)
        unless extras.isEmpty && missing.isEmpty do
          errs := errs.push s!"{cert}: cone extra={extras} missing={missing}"
    | some (.axiomInfo _)  => errs := errs.push s!"{cert}: is an AXIOM, not a proven theorem"
    | some (.opaqueInfo _) => errs := errs.push s!"{cert}: is OPAQUE, not a proven theorem"
    | some _               => errs := errs.push s!"{cert}: is not a theorem"

  unless errs.isEmpty do
    throwError "AUDIT FAILED (fail-closed):\n{String.intercalate "\n" errs.toList}"

  -- (2) CANONICAL BLOCK: policy, then statements, then specification bodies.
  let mut lines : Array String := #[]
  lines := lines.push
    s!"policy|kernel3={String.intercalate "," ((sortNames kernel3).map toString)}|apexExtra={String.intercalate "," ((sortNames apexExtra).map toString)}|specPrefix={specPrefix}"
  let mut specs : NameSet := {}
  for (cert, cone) in manifest do
    let ci := (env.find? cert).get!
    specs := (closureOf env {} ci.type.getUsedConstants.toList).toList.foldl (·.insert ·) specs
    lines := lines.push
      s!"cert|{cert}|cone={String.intercalate "," ((sortNames cone).map toString)}|type={← ppAll ci.type}"
  for nm in sortNames specs.toList do
    match env.find? nm with
    | none => errs := errs.push s!"specification constant vanished mid-audit: {nm}"
    | some ci =>
      let isProp ← Command.liftCoreM <| Meta.MetaM.run' <| Meta.isProp ci.type
      -- Proof irrelevance: a Prop-valued constant contributes its STATEMENT; a
      -- data definition contributes its BODY, which is where fidelity lives.
      if isProp then
        lines := lines.push s!"spec|{nm}|prop|type={← ppAll ci.type}"
      else
        match ci with
        | .defnInfo v => lines := lines.push s!"spec|{nm}|def|value={← ppAll v.value}"
        | _           => lines := lines.push s!"spec|{nm}|other|type={← ppAll ci.type}"

  unless errs.isEmpty do
    throwError "AUDIT FAILED (fail-closed):\n{String.intercalate "\n" errs.toList}"

  -- FAIL CLOSED ON ABSENCE: a manifest that somehow produced no specification
  -- constants would emit a block that binds statements only. That is a weaker
  -- claim than this file advertises, so it is an error, not a quiet pass.
  if specs.toList.isEmpty then
    throwError "AUDIT FAILED: statements reached ZERO specification constants — the closure is not doing its job"

  logInfo ("AUDIT-MANIFEST-BEGIN\n" ++ String.intercalate "\n" lines.toList ++ "\nAUDIT-MANIFEST-END")
  -- check.sh cross-checks its own CERTS array against THIS line, so the two
  -- cannot drift apart without the build noticing.
  logInfo s!"AUDITED-CERTIFICATES: {String.intercalate " " ((manifest.map (·.1)).map toString)}"
  logInfo s!"statement audit PASSED: {manifest.length} certificates (exact cones + elaborated statements), {specs.toList.length} specification constants pinned"

end Ed25519Audit

open Ed25519Audit in
auditStatements