import Std

/-!
Research formalization for covert-channel configuration synthesis.
STATUS: kernel-checked at publication; see evidence/publication/lean-verification.json.
Target: Lean 4.19.0, core/Std only. Run `bash check_lean.sh` before relying on it.
No custom axioms, unchecked native computation, or proof placeholders are used.
The analog-hardware-to-integer-envelope refinement is an explicit outstanding
obligation; these declarations do not assert that a physical machine meets it.
-/

set_option autoImplicit false
set_option warningAsError true

namespace CovertChannel

universe u v w z

/-- A private verifier with a total, canonical fallback. -/
def guardedRelease {X : Type u} {Y : Type v}
    (canonical : X → Y) (accept : X → Y → Bool)
    (x : X) (proposal : Option Y) : Y :=
  match proposal with
  | none => canonical x
  | some y => if accept x y = true then y else canonical x

theorem guardedRelease_eq {X : Type u} {Y : Type v}
    (canonical : X → Y) (accept : X → Y → Bool)
    (sound : ∀ (x : X) (y : Y), accept x y = true → y = canonical x)
    (x : X) (proposal : Option Y) :
    guardedRelease canonical accept x proposal = canonical x := by
  cases proposal with
  | none => rfl
  | some y =>
    simp only [guardedRelease]
    split
    next h => exact sound x y h
    next => rfl

/-- Covers arbitrary proposal selection, including withholding. -/
theorem proposal_independence {X : Type u} {Y : Type v}
    (canonical : X → Y) (accept : X → Y → Bool)
    (sound : ∀ (x : X) (y : Y), accept x y = true → y = canonical x)
    (x : X) (p q : Option Y) :
    guardedRelease canonical accept x p =
      guardedRelease canonical accept x q := by
  exact (guardedRelease_eq canonical accept sound x p).trans
    (guardedRelease_eq canonical accept sound x q).symm

/-- Low state includes the public task queue and the public release schedule.
High state and actions are universally quantified, not sampled from an AI. -/
def runTrace {L : Type u} {H : Type v} {A : Type w} {O : Type z}
    (step : L → H → A → L × O) (low : L) : List (H × A) → List O
  | [] => []
  | ha :: rest =>
    let next := step low ha.1 ha.2
    next.2 :: runTrace step next.1 rest

def referenceTrace {L : Type u} {O : Type v}
    (reference : L → L × O) (low : L) : Nat → List O
  | 0 => []
  | n + 1 =>
    (reference low).2 :: referenceTrace reference (reference low).1 n

/-- Equality includes both the next LOW state and the current observation;
merely checking the current output would be insufficient for composition. -/
theorem trace_refinement {L : Type u} {H : Type v} {A : Type w} {O : Type z}
    (step : L → H → A → L × O) (reference : L → L × O)
    (oneStep : ∀ (l : L) (h : H) (a : A), step l h a = reference l)
    (low : L) (history : List (H × A)) :
    runTrace step low history = referenceTrace reference low history.length := by
  induction history generalizing low with
  | nil => rfl
  | cons ha rest ih =>
    simp only [runTrace, List.length_cons, referenceTrace, oneStep]
    rw [ih]

theorem history_independence {L : Type u} {H : Type v}
    {A : Type w} {O : Type z}
    (step : L → H → A → L × O) (reference : L → L × O)
    (oneStep : ∀ (l : L) (h : H) (a : A), step l h a = reference l)
    (low : L) (first second : List (H × A))
    (samePublicLength : first.length = second.length) :
    runTrace step low first = runTrace step low second := by
  rw [trace_refinement step reference oneStep low first,
      trace_refinement step reference oneStep low second,
      samePublicLength]

structure Core where
  canonicalEncoding : Bool
  fixedReleaseSlot : Bool
  totalFallback : Bool
  sharedResourcePartition : Bool
  mediatedEgress : Bool
  deriving DecidableEq, Repr

structure Action where
  variant : Bool
  early : Bool
  succeeds : Bool
  sharedSignal : Bool
  networkSignal : Bool
  deriving DecidableEq, Repr

structure Frame where
  payload : Option (Nat × Bool)
  releaseSlot : Bool
  sharedObservation : Bool
  networkObservation : Bool
  deriving DecidableEq, Repr

def secureCore : Core := ⟨true, true, true, true, true⟩

def emit (c : Core) (goal : Nat) (a : Action) : Frame :=
  { payload :=
      if a.succeeds then
        some (goal, if c.canonicalEncoding then false else a.variant)
      else if c.totalFallback then some (goal, false) else none
    releaseSlot := if c.fixedReleaseSlot then true else !a.early
    sharedObservation := if c.sharedResourcePartition then false else a.sharedSignal
    networkObservation := if c.mediatedEgress then false else a.networkSignal }

theorem secureCore_emits_canonical (goal : Nat) (a : Action) :
    emit secureCore goal a = ⟨some (goal, false), true, false, false⟩ := by
  cases a with
  | mk variant early succeeds sharedSignal networkSignal =>
    cases succeeds <;> rfl

theorem secureCore_noninterference (goal : Nat) (a b : Action) :
    emit secureCore goal a = emit secureCore goal b := by
  rw [secureCore_emits_canonical, secureCore_emits_canonical]

/-- Five local negative controls. These are not physical exploit programs. -/
theorem no_canonicalization_leaks :
    emit {secureCore with canonicalEncoding := false} 17
      ⟨false, false, true, false, false⟩ ≠
    emit {secureCore with canonicalEncoding := false} 17
      ⟨true, false, true, false, false⟩ := by decide

theorem no_padding_leaks :
    emit {secureCore with fixedReleaseSlot := false} 17
      ⟨false, false, true, false, false⟩ ≠
    emit {secureCore with fixedReleaseSlot := false} 17
      ⟨false, true, true, false, false⟩ := by decide

theorem no_fallback_leaks :
    emit {secureCore with totalFallback := false} 17
      ⟨false, false, false, false, false⟩ ≠
    emit {secureCore with totalFallback := false} 17
      ⟨false, false, true, false, false⟩ := by decide

theorem no_partition_leaks :
    emit {secureCore with sharedResourcePartition := false} 17
      ⟨false, false, true, false, false⟩ ≠
    emit {secureCore with sharedResourcePartition := false} 17
      ⟨false, false, true, true, false⟩ := by decide

theorem no_egress_mediation_leaks :
    emit {secureCore with mediatedEgress := false} 17
      ⟨false, false, true, false, false⟩ ≠
    emit {secureCore with mediatedEgress := false} 17
      ⟨false, false, true, false, true⟩ := by decide

/-- Upward-rounded bound in milli-temperature units. This is an envelope,
not an assertion that physical temperatures are integers. -/
def envelope (g : Nat) : Nat → Nat
  | 0 => 0
  | t + 1 => (9 * envelope g t + 10 * (g + 1) + 9) / 10

theorem general_envelope_invariant (m : Nat → Nat) (g : Nat)
    (initial : m 0 ≤ 50) (gainBound : g ≤ 4)
    (stepBound : ∀ t : Nat,
      10 * m (t + 1) ≤ 9 * m t + 10 * (g + 1) + 9) :
    ∀ t : Nat, m t ≤ 50 := by
  intro t
  induction t with
  | zero => exact initial
  | succ t ih =>
    have ht := stepBound t
    omega

theorem envelope_invariant (g : Nat) (gainBound : g ≤ 4) :
    ∀ t : Nat, envelope g t ≤ 50 := by
  apply general_envelope_invariant (envelope g) g
  · exact Nat.zero_le 50
  · exact gainBound
  · intro t
    simp only [envelope]
    omega

theorem envelope_cannot_cross_sensor (g : Nat) (gainBound : g ≤ 4)
    (t : Nat) : envelope g t < 55 := by
  have h := envelope_invariant g gainBound t
  omega

def residualGain (s r : Nat) : Nat := 20 - (2 * s + r)

theorem residual_gain_safe_iff (s r : Nat) :
    residualGain s r ≤ 4 ↔ 16 ≤ 2 * s + r := by
  unfold residualGain
  omega

def cost (s r : Nat) : Nat := s * s + 2 * (r * r)

private theorem square_mono (a b : Nat) (h : a ≤ b) : a*a ≤ b*b :=
  Nat.mul_le_mul h h

/-- A global bound over ALL natural hardening choices, not a finite search
assertion. Only linear arithmetic plus explicit square-monotonicity is used. -/
theorem cost_lower_bound (s r : Nat) (feasible : 16 ≤ 2*s + r) :
    57 ≤ cost s r := by
  unfold cost
  by_cases hs : 8 ≤ s
  · have hsq := square_mono 8 s hs
    omega
  · have small : s = 0 ∨ s = 1 ∨ s = 2 ∨ s = 3 ∨
        s = 4 ∨ s = 5 ∨ s = 6 ∨ s = 7 := by omega
    rcases small with h | h | h | h | h | h | h | h
    · subst s
      have hr : 16 ≤ r := by omega
      have hsq := square_mono 16 r hr
      omega
    · subst s
      have hr : 14 ≤ r := by omega
      have hsq := square_mono 14 r hr
      omega
    · subst s
      have hr : 12 ≤ r := by omega
      have hsq := square_mono 12 r hr
      omega
    · subst s
      have hr : 10 ≤ r := by omega
      have hsq := square_mono 10 r hr
      omega
    · subst s
      have hr : 8 ≤ r := by omega
      have hsq := square_mono 8 r hr
      omega
    · subst s
      have hr : 6 ≤ r := by omega
      have hsq := square_mono 6 r hr
      omega
    · subst s
      have hr : 4 ≤ r := by omega
      have hsq := square_mono 4 r hr
      omega
    · subst s
      have hr : 2 ≤ r := by omega
      have hsq := square_mono 2 r hr
      omega

theorem winner_cost : cost 7 2 = 57 := by decide

theorem winner_feasible : 16 ≤ 2*7 + 2 ∧ 2 ≤ 4 := by decide

theorem global_optimum (s r : Nat) (feasible : 16 ≤ 2*s + r) :
    cost 7 2 ≤ cost s r := by
  rw [winner_cost]
  exact cost_lower_bound s r feasible

theorem exists_optimal_configuration :
    ∃ (s r : Nat), 16 ≤ 2*s + r ∧ r ≤ 4 ∧
      ∀ (s' r' : Nat), 16 ≤ 2*s' + r' → r' ≤ 4 →
        cost s r ≤ cost s' r' := by
  refine ⟨7, 2, by decide, by decide, ?_⟩
  intro s' r' hf _
  exact global_optimum s' r' hf

theorem winning_envelope_forever (t : Nat) :
    envelope (residualGain 7 2) t < 55 := by
  apply envelope_cannot_cross_sensor
  decide

/-- Exact integer numerator for the allowed trajectory
x_(t+1) = (9/10)*x_t + (g+1), x_0=0, in milli-temperature units.
The denominator at time t is 10^t. -/
def hotNumerator (g : Nat) : Nat → Nat
  | 0 => 0
  | t + 1 => 9 * hotNumerator g t + (g + 1) * 10^(t+1)

theorem near_miss_below_at_23 :
    hotNumerator 5 23 < 55 * 10^23 := by decide

theorem near_miss_crosses_at_24 :
    55 * 10^24 ≤ hotNumerator 5 24 := by decide

theorem quiet_control_below_at_24 :
    hotNumerator 0 24 < 55 * 10^24 := by decide

#print axioms guardedRelease_eq
#print axioms proposal_independence
#print axioms trace_refinement
#print axioms history_independence
#print axioms secureCore_noninterference
#print axioms general_envelope_invariant
#print axioms winning_envelope_forever
#print axioms cost_lower_bound
#print axioms exists_optimal_configuration
#print axioms near_miss_crosses_at_24

end CovertChannel