
import Runtime.Adequacy.EnvelopeCore.ReconfigurationBridge

/-! # VM Envelope Adherence

Determinism profiles, certified envelope capabilities, and admission
checking infrastructure for VM-to-envelope correspondence. -/

/-
The Problem. The VM must adhere to declared envelope bounds. We need
to classify determinism guarantees (full, trace-modulo, commutativity-
modulo) and check that user-requested capabilities (`D_user`) are
contained within certified program capabilities (`D_prog`).

Solution Structure. Define `DeterminismProfileClass` enum. Define
`CertifiedEnvelopeCapability` and `DUser` structures. Provide
`dUserContained` decision procedure for admission checking.
-/

/- ## Structured Block 1 -/
set_option autoImplicit false

namespace Runtime
namespace Adequacy

universe u v

-- Determinism Profiles

inductive DeterminismProfileClass where
  | full
  | traceModulo
  | commutativityModulo
  deriving Repr, DecidableEq, Inhabited

-- Capability Objects and Admission Predicate

/-- Certified envelope capability summary used for admission checks. -/
structure CertifiedEnvelopeCapability where
  maxDiff : Nat
  supportsEqSafeOnly : Bool := true
  supportedProfiles : List DeterminismProfileClass := []
  deriving Repr, DecidableEq, Inhabited

/-- User-requested diff policy language (`D_user`). -/
structure DUser where
  maxRequestedDiff : Nat
  eqSafeOnly : Bool := true
  requiredProfiles : List DeterminismProfileClass := []
  deriving Repr, DecidableEq, Inhabited

def profilesContained
    (required available : List DeterminismProfileClass) : Bool :=
  required.all (fun p => p ∈ available)

/-- Decidable containment of `D_user` inside a certified envelope capability. -/
def dUserContained (d : DUser) (cap : CertifiedEnvelopeCapability) : Bool :=
  (d.maxRequestedDiff <= cap.maxDiff) &&
  (!d.eqSafeOnly || cap.supportsEqSafeOnly) &&
  profilesContained d.requiredProfiles cap.supportedProfiles

/-- E3: scheduler determinism modulo certified exchange in sharded mode. -/
def ShardedExchangeNormalization {State : Type u} {Obs : Type v}
    (E : ShardedEnvelope State Obs)
    (exchange : AdmissibleExchange State) : Prop :=
  ∀ ref₁ ref₂ impl₁ impl₂,
    exchange ref₁ ref₂ →
    exchange impl₁ impl₂ →
      EqEnvShard E ref₁ impl₁ → EqEnvShard E ref₂ impl₂

-- VM Local/Sharded Hypothesis Bundles

/-- E3: VM-side local determinism/envelope hypothesis bundle. -/
structure VMLocalEnvelopeHypotheses (State : Type u) (Obs : Type v) where
  localEnvelope : LocalEnvelope State Obs
  refRun : Run State → Prop
  vmRun : Run State → Prop
  certifiedExchange : AdmissibleExchange State
  adherenceWitness :
    LocalEnvelopeSoundness localEnvelope refRun vmRun
  schedulerDeterminismWitness :
    ExchangeNormalization localEnvelope certifiedExchange

/-- E3: VM-side sharded determinism/envelope hypothesis bundle. -/
structure VMShardedEnvelopeHypotheses (State : Type u) (Obs : Type v) where
  shardedEnvelope : ShardedEnvelope State Obs
  refRun : Run State → Prop
  vmRun : Run State → Prop
  certifiedExchange : AdmissibleExchange State
  adherenceWitness :
    ShardedEnvelopeSoundness shardedEnvelope refRun vmRun
  schedulerDeterminismWitness :
/- ## Structured Block 2 -/
    ShardedExchangeNormalization shardedEnvelope certifiedExchange

/-- E3: extract VM local adherence from local hypothesis bundle assumptions. -/
theorem vm_local_adherence_of_hypotheses
    {State : Type u} {Obs : Type v}
    (h : VMLocalEnvelopeHypotheses State Obs) :
    LocalEnvelopeSoundness h.localEnvelope h.refRun h.vmRun :=
  h.adherenceWitness

/-- E3: extract VM sharded adherence from sharded hypothesis bundle assumptions. -/
theorem vm_sharded_adherence_of_hypotheses
    {State : Type u} {Obs : Type v}
    (h : VMShardedEnvelopeHypotheses State Obs) :
    ShardedEnvelopeSoundness h.shardedEnvelope h.refRun h.vmRun :=
  h.adherenceWitness

/-- E3: extract scheduler determinism modulo certified exchange (local). -/
theorem scheduler_determinism_local_of_hypotheses
    {State : Type u} {Obs : Type v}
    (h : VMLocalEnvelopeHypotheses State Obs) :
    ExchangeNormalization h.localEnvelope h.certifiedExchange :=
  h.schedulerDeterminismWitness

/-- E3: extract scheduler determinism modulo certified exchange (sharded). -/
theorem scheduler_determinism_sharded_of_hypotheses
    {State : Type u} {Obs : Type v}
    (h : VMShardedEnvelopeHypotheses State Obs) :
    ShardedExchangeNormalization h.shardedEnvelope h.certifiedExchange :=
  h.schedulerDeterminismWitness

-- Adequacy and Capability Relations

/-- E3: adequacy statement form between reference and VM semantics modulo envelope. -/
def VMObservationalAdequacyModuloEnvelope {State : Type u}
    (R : Run State → Run State → Prop)
    (refRun vmRun : Run State → Prop) : Prop :=
  ∀ ref vm, refRun ref → vmRun vm → R ref vm

/-- E3: full-abstraction/adequacy statement over safety-visible observations. -/
def EnvelopeFullAbstraction {State : Type u} {Obs : Type v}
    (observe : State → Obs)
    (R : Run State → Run State → Prop) : Prop :=
  (∀ ref vm, R ref vm → eraseObs observe ref = eraseObs observe vm) ∧
  (∀ ref vm, eraseObs observe ref = eraseObs observe vm → R ref vm)

/-- E3: capability-strength relation ("stronger" provides at least weak guarantees). -/
def CapabilityStrengthens
    (strong weak : CertifiedEnvelopeCapability) : Prop :=
  weak.maxDiff ≤ strong.maxDiff ∧
  (weak.supportsEqSafeOnly → strong.supportsEqSafeOnly) ∧
  (∀ p, p ∈ weak.supportedProfiles → p ∈ strong.supportedProfiles)

/-- E3: monotonicity statement for capability-indexed envelope guarantees. -/
def CapabilityMonotonicity
    (guarantee : CertifiedEnvelopeCapability → Prop) : Prop :=
  ∀ weak strong,
    CapabilityStrengthens strong weak →
    guarantee weak →
    guarantee strong

-- VM Adherence Premises

/-- E3: VM adherence + adequacy premise bundle for theorem extraction. -/
structure VMEnvelopeAdherencePremises
    (State : Type u) (Obs : Type v) (Placement : Type (max u v)) where
  localHypotheses : VMLocalEnvelopeHypotheses State Obs
  shardedHypotheses : VMShardedEnvelopeHypotheses State Obs
  subtype : SpatialSubtype Placement
  obligation : Placement → Run State → Run State → Prop
  monotonicityWitness :
    SpatialSubtypingMonotonicity subtype obligation
  localAdequacyWitness :
/- ## Structured Block 3 -/
    VMObservationalAdequacyModuloEnvelope
      (EqEnvLocal localHypotheses.localEnvelope)
      localHypotheses.refRun localHypotheses.vmRun
  shardedAdequacyWitness :
    VMObservationalAdequacyModuloEnvelope
      (EqEnvShard shardedHypotheses.shardedEnvelope)
      shardedHypotheses.refRun shardedHypotheses.vmRun
  localFullAbstractionWitness :
    EnvelopeFullAbstraction
      localHypotheses.localEnvelope.toEnvelope.observe
      (EqEnvLocal localHypotheses.localEnvelope)
  shardedFullAbstractionWitness :
    EnvelopeFullAbstraction
      shardedHypotheses.shardedEnvelope.toEnvelope.observe
      (EqEnvShard shardedHypotheses.shardedEnvelope)
  guarantee : CertifiedEnvelopeCapability → Prop
  weakCapability : CertifiedEnvelopeCapability
  strongCapability : CertifiedEnvelopeCapability
  capabilityMonotonicityWitness : CapabilityMonotonicity guarantee
  strongStrengthensWeak :
    CapabilityStrengthens strongCapability weakCapability

-- Premise Projections

/-- E3: extract local observational adequacy modulo envelope from VM premises. -/
theorem vm_local_adequacy_of_premises
    {State : Type u} {Obs : Type v} {Placement : Type (max u v)}
    (p : VMEnvelopeAdherencePremises State Obs Placement) :
    VMObservationalAdequacyModuloEnvelope
      (EqEnvLocal p.localHypotheses.localEnvelope)
      p.localHypotheses.refRun p.localHypotheses.vmRun :=
  p.localAdequacyWitness

/-- E3: extract sharded observational adequacy modulo envelope from VM premises. -/
theorem vm_sharded_adequacy_of_premises
    {State : Type u} {Obs : Type v} {Placement : Type (max u v)}
    (p : VMEnvelopeAdherencePremises State Obs Placement) :
    VMObservationalAdequacyModuloEnvelope
      (EqEnvShard p.shardedHypotheses.shardedEnvelope)
      p.shardedHypotheses.refRun p.shardedHypotheses.vmRun :=
  p.shardedAdequacyWitness

/-- E3: extract local full-abstraction/adequacy witness from VM premises. -/
theorem vm_local_full_abstraction_of_premises
    {State : Type u} {Obs : Type v} {Placement : Type (max u v)}
    (p : VMEnvelopeAdherencePremises State Obs Placement) :
    EnvelopeFullAbstraction
      p.localHypotheses.localEnvelope.toEnvelope.observe
      (EqEnvLocal p.localHypotheses.localEnvelope) :=
  p.localFullAbstractionWitness

/-- E3: extract sharded full-abstraction/adequacy witness from VM premises. -/
theorem vm_sharded_full_abstraction_of_premises
    {State : Type u} {Obs : Type v} {Placement : Type (max u v)}
    (p : VMEnvelopeAdherencePremises State Obs Placement) :
    EnvelopeFullAbstraction
      p.shardedHypotheses.shardedEnvelope.toEnvelope.observe
      (EqEnvShard p.shardedHypotheses.shardedEnvelope) :=
  p.shardedFullAbstractionWitness

/-- E3: extract VM adherence monotonicity under spatial refinement. -/
theorem vm_adherence_monotonicity_of_premises
/- ## Structured Block 4 -/
    {State : Type u} {Obs : Type v} {Placement : Type (max u v)}
    (p : VMEnvelopeAdherencePremises State Obs Placement) :
    SpatialSubtypingMonotonicity p.subtype p.obligation :=
  p.monotonicityWitness

-- Capability-Monotonicity Projection

/-- E3: extract capability monotonicity theorem from VM premises. -/
theorem vm_capability_monotonicity_of_premises
    {State : Type u} {Obs : Type v} {Placement : Type (max u v)}
    (p : VMEnvelopeAdherencePremises State Obs Placement) :
    p.guarantee p.weakCapability → p.guarantee p.strongCapability := by
  intro hWeak
  exact p.capabilityMonotonicityWitness
    p.weakCapability p.strongCapability p.strongStrengthensWeak hWeak

-- Packaged VM Adherence Protocol

/-- E3: packaged VM adherence/adequacy protocol-level theorem family. -/
structure VMEnvelopeAdherenceProtocol where
  State : Type u
  Obs : Type v
  Placement : Type (max u v)
  premises : VMEnvelopeAdherencePremises State Obs Placement
  localAdherence :
    LocalEnvelopeSoundness
      premises.localHypotheses.localEnvelope
      premises.localHypotheses.refRun
      premises.localHypotheses.vmRun :=
        vm_local_adherence_of_hypotheses premises.localHypotheses
  shardedAdherence :
    ShardedEnvelopeSoundness
      premises.shardedHypotheses.shardedEnvelope
      premises.shardedHypotheses.refRun
      premises.shardedHypotheses.vmRun :=
        vm_sharded_adherence_of_hypotheses premises.shardedHypotheses
  schedulerDeterminismLocal :
    ExchangeNormalization
      premises.localHypotheses.localEnvelope
      premises.localHypotheses.certifiedExchange :=
        scheduler_determinism_local_of_hypotheses premises.localHypotheses
  schedulerDeterminismSharded :
    ShardedExchangeNormalization
      premises.shardedHypotheses.shardedEnvelope
      premises.shardedHypotheses.certifiedExchange :=
        scheduler_determinism_sharded_of_hypotheses premises.shardedHypotheses

  -- Packaged VM Adherence Protocol: Adequacy Fields

  monotonicity :
    SpatialSubtypingMonotonicity premises.subtype premises.obligation :=
      vm_adherence_monotonicity_of_premises premises
  localAdequacy :
    VMObservationalAdequacyModuloEnvelope
      (EqEnvLocal premises.localHypotheses.localEnvelope)
      premises.localHypotheses.refRun
      premises.localHypotheses.vmRun :=
        vm_local_adequacy_of_premises premises
  shardedAdequacy :
    VMObservationalAdequacyModuloEnvelope
      (EqEnvShard premises.shardedHypotheses.shardedEnvelope)
/- ## Structured Block 5 -/
      premises.shardedHypotheses.refRun
      premises.shardedHypotheses.vmRun :=
        vm_sharded_adequacy_of_premises premises

  -- Packaged VM Adherence Protocol: Full-Abstraction Fields

  localFullAbstraction :
    EnvelopeFullAbstraction
      premises.localHypotheses.localEnvelope.toEnvelope.observe
      (EqEnvLocal premises.localHypotheses.localEnvelope) :=
        vm_local_full_abstraction_of_premises premises
  shardedFullAbstraction :
    EnvelopeFullAbstraction
      premises.shardedHypotheses.shardedEnvelope.toEnvelope.observe
      (EqEnvShard premises.shardedHypotheses.shardedEnvelope) :=
        vm_sharded_full_abstraction_of_premises premises
  capabilityMonotonicity :
    premises.guarantee premises.weakCapability →
    premises.guarantee premises.strongCapability :=
      vm_capability_monotonicity_of_premises premises

end Adequacy
end Runtime
