import IrisExtractionAPI

/-! # IrisExtractionInstance

Concrete Iris extraction boundary with runtime erasure mappings. -/

/-
The Problem. Iris ghost state (invariants, fancy updates, ghost variables) is
proof-only and must be erased at runtime. Without explicit erasure, compiled code
would fail to typecheck or execute nonsensical operations.

Solution Structure. We use `@[implemented_by]` to map logical definitions to trivial
runtime implementations:
1. Fancy updates → identity (mask changes are proof-only)
2. Invariants → their content (no runtime bookkeeping)
3. Ghost ownership → `emp` (ghost state doesn't exist at runtime)
This is sound because Iris adequacy connects logical correctness to operational behavior.
-/

/-! ## Trust Boundary

This file is the **Iris extraction trust boundary**. It contains:

1. **Logical definitions**: Full Iris definitions used by the Lean kernel for
   proof checking (e.g., `fupd`, `inv`, `ghost_var`).

2. **Runtime erasure**: `@[implemented_by]` attributes that substitute trivial
   implementations at codegen/eval time.

## Erasure Laws (Audit Checklist)

Each `@[implemented_by]` follows the pattern:
- **Logical definition**: Full Iris machinery for proof checking
- **Runtime implementation**: Trivial/identity for execution

| Construct | Logical | Runtime | Justification |
|-----------|---------|---------|---------------|
| `fupd E₁ E₂ P` | Fancy update modality | `P` | Mask changes are proof-only |
| `uPredFupd E₁ E₂ P` | UPred fancy update | `P` | Same as above, at uPred level |
| `inv N P` | Invariant assertion | `P` | Invariant content only |
| `cinv N ct P` | Cancelable invariant | `P` | Invariant content only |
| `cancel_token_own ct` | Cancellation token | `emp` | Token is ghost ownership |
| `saved_prop_own γ P` | Saved proposition | `P` | Proposition content only |
| `ghost_var γ a` | Ghost variable | `emp` | Ghost ownership erased |
| `ghost_map_auth γ m` | Ghost map auth | `emp` | Ghost ownership erased |
| `ghost_map_elem γ k v` | Ghost map element | `emp` | Ghost ownership erased |

## Why This Is Sound

Ghost state in Iris is **proof-only by design**. From "Iris from the ground up":

> "Ghost state exists logically in the proof alongside the program execution
> but doesn't show up in the operational semantics or the running code."

The `@[implemented_by]` pattern implements this erasure:
- Proofs are checked against the full logical definitions
- Runtime execution uses the erased implementations
- The adequacy theorem connects logical correctness to operational behavior

## Audit Protocol

1. Verify each `@[implemented_by]` maps a ghost construct to its erased form
2. Run `just escape` — Iris hits should come only from this file
3. Run `lake build` — confirms type-correctness of the bridge
-/

set_option autoImplicit false

namespace Telltale

variable [ti : TelltaleIris]

/-! ## UPred Fancy Update Erasure

Fancy updates `|={E₁,E₂}=> P` allow mask-changing view shifts — logical
operations that open/close invariants. At runtime, mask manipulation is
purely logical framing, so we erase to identity.
-/

/-- Runtime implementation: fancy update erases to identity on `P`. -/
def uPredFupdImpl (_E₁ _E₂ : Mask) (P : iProp) : iProp := P

/-- Fancy update at UPred level.

**Logical**: Full Iris fancy update modality with mask tracking.
**Runtime**: Identity (masks are proof-only). -/
@[implemented_by uPredFupdImpl]
def uPredFupd (E₁ E₂ : Mask) (P : iProp) : iProp :=
  Iris.BaseLogic.uPred_fupd
    (GF := ti.GF) (M := ti.M) (F := ti.F) ti.W E₁ E₂ P

end Telltale

variable [ti : Telltale.TelltaleIris]

/-! ## iProp Connectives -/

namespace iProp

def entails (P Q : iProp) : Prop := @Iris.BI.BIBase.Entails _ _ P Q
def emp : iProp := @Iris.BI.BIBase.emp _ _
def sep (P Q : iProp) : iProp := @Iris.BI.BIBase.sep _ _ P Q
def wand (P Q : iProp) : iProp := @Iris.BI.BIBase.wand _ _ P Q
def pure (φ : Prop) : iProp := @Iris.BI.BIBase.pure _ _ φ
def later (P : iProp) : iProp := @Iris.BI.BIBase.later _ _ P
def persistently (P : iProp) : iProp := @Iris.BI.BIBase.persistently _ _ P
def «exist» {α : Type} (Φ : α → iProp) : iProp :=
  @Iris.BI.BIBase.«exists» _ _ α Φ
def «forall» {α : Type} (Φ : α → iProp) : iProp :=
  @Iris.BI.BIBase.«forall» _ _ α Φ

end iProp

/-! ## Big Separation over Maps -/

def big_sepM {K : Type _} {V : Type _} {M' : Type _ → Type _}
    [Iris.Std.FiniteMap K M'] (Φ : K → V → iProp) (m : M' V) : iProp :=
  Iris.BI.big_sepM (PROP := iProp) Φ m

/-! ## Entailment Helpers -/

private theorem entails_refl (P : iProp) : iProp.entails P P :=
  (Iris.BI.BIBase.BiEntails.rfl (P := P)).1

private theorem eq_entails {P Q : iProp} (h : P ⊣⊢ Q) : iProp.entails P Q := h.1

/-! ## Separation Logic Laws -/

theorem sep_comm (P Q : iProp) :
    iProp.entails (iProp.sep P Q) (iProp.sep Q P) :=
  eq_entails Iris.BI.sep_comm

theorem sep_assoc (P Q R : iProp) :
    iProp.entails (iProp.sep (iProp.sep P Q) R)
      (iProp.sep P (iProp.sep Q R)) :=
  eq_entails Iris.BI.sep_assoc

theorem sep_mono (P P' Q Q' : iProp) :
    iProp.entails P P' → iProp.entails Q Q' →
    iProp.entails (iProp.sep P Q) (iProp.sep P' Q') :=
  fun h1 h2 => Iris.BI.sep_mono h1 h2

theorem wand_intro (P Q R : iProp) :
    iProp.entails (iProp.sep P Q) R →
    iProp.entails P (iProp.wand Q R) :=
  fun h => Iris.BI.wand_intro h

theorem wand_elim (P Q : iProp) :
    iProp.entails (iProp.sep (iProp.wand P Q) P) Q := by
  simpa using (Iris.BI.wand_elim_l (P := P) (Q := Q))

theorem pure_intro (φ : Prop) (P : iProp) :
    φ → iProp.entails P (iProp.sep (iProp.pure φ) P) := by
  intro hφ
  have hEmp : iProp.entails P (iProp.sep iProp.emp P) :=
    Iris.BI.emp_sep.symm.1
  have hSep : iProp.entails (iProp.sep iProp.emp P) (iProp.sep (iProp.pure φ) P) :=
    Iris.BI.sep_mono (Iris.BI.pure_intro (P := iProp.emp) hφ) (entails_refl P)
  exact hEmp.trans hSep

theorem pure_elim (φ : Prop) (P : iProp) :
    (φ → iProp.entails iProp.emp P) → iProp.entails (iProp.pure φ) P :=
  fun h => Iris.BI.pure_elim' h

theorem persistently_idemp (P : iProp) :
    iProp.entails (iProp.persistently (iProp.persistently P))
      (iProp.persistently P) :=
  eq_entails Iris.BI.persistently_idem

theorem persistently_sep_dup (P : iProp) :
    iProp.entails (iProp.persistently P)
      (iProp.sep (iProp.persistently P) (iProp.persistently P)) :=
  eq_entails Iris.BI.persistently_sep_persistently.symm

/-! ## Basic Update Modality -/

def bupd (P : iProp) : iProp := Iris.BUpd.bupd P

theorem bupd_mono (P Q : iProp) :
    iProp.entails P Q → iProp.entails (_root_.bupd P) (_root_.bupd Q) :=
  fun h => Iris.BIUpdate.mono h

theorem bupd_intro (P : iProp) : iProp.entails P (_root_.bupd P) :=
  Iris.BIUpdate.intro

theorem bupd_trans (P : iProp) :
    iProp.entails (_root_.bupd (_root_.bupd P)) (_root_.bupd P) :=
  Iris.BIUpdate.trans

theorem bupd_frame_r (P Q : iProp) :
    iProp.entails (iProp.sep (_root_.bupd P) Q) (_root_.bupd (iProp.sep P Q)) :=
  Iris.BIUpdate.frame_r

/-! ## Big Separating Conjunction (Lists) -/

def big_sepL {α : Type} (Φ : α → iProp) : List α → iProp :=
  fun l => l.foldr (fun a acc => iProp.sep (Φ a) acc) iProp.emp

theorem big_sep_l_nil {α : Type} (Φ : α → iProp) :
    iProp.entails (big_sepL Φ []) iProp.emp :=
  entails_refl _

theorem big_sep_l_cons {α : Type} (Φ : α → iProp) (x : α) (l : List α) :
    iProp.entails (big_sepL Φ (x :: l)) (iProp.sep (Φ x) (big_sepL Φ l)) :=
  entails_refl _

theorem big_sep_l_app {α : Type} (Φ : α → iProp) (l₁ l₂ : List α) :
    iProp.entails (big_sepL Φ (l₁ ++ l₂))
      (iProp.sep (big_sepL Φ l₁) (big_sepL Φ l₂)) := by
  induction l₁ with
  | nil =>
    simp only [big_sepL, List.foldr, List.nil_append]
    exact Iris.BI.emp_sep.symm.1
  | cons x xs ih =>
    simp only [big_sepL, List.foldr, List.cons_append]
    refine (Iris.BI.sep_mono (entails_refl _) ih).trans ?_
    exact (Iris.BI.sep_assoc (P := Φ x)).symm.1

/-! ## Masks and Namespaces -/

namespace Mask

def top : Mask := fun _ => True
def empty : Mask := fun _ => False
def diff (E₁ E₂ : Mask) : Mask := fun x => E₁ x ∧ ¬E₂ x
def union (E₁ E₂ : Mask) : Mask := fun x => E₁ x ∨ E₂ x
def subseteq (E₁ E₂ : Mask) : Prop := ∀ x, E₁ x → E₂ x
def disjoint (E₁ E₂ : Mask) : Prop := ∀ x, ¬(E₁ x ∧ E₂ x)
def singleton (n : Nat) : Mask :=
  fun p => p = [Iris.Countable.encode n]

end Mask

namespace Namespace

def root : Telltale.Namespace := Iris.nroot
def append (N : Telltale.Namespace) (s : String) : Telltale.Namespace := Iris.ndot N s
def append_nat (N : Telltale.Namespace) (n : Nat) : Telltale.Namespace := Iris.ndot N n

end Namespace

def namespace_to_mask (N : Telltale.Namespace) : Mask := (Iris.nclose N).mem

/-! ## Fancy Update Modality

Fancy updates `|={E₁,E₂}=> P` are mask-changing view shifts that enable
atomic access to invariants. The mask tracks which invariants are "open"
(temporarily accessed) vs "closed" (protected).

**Logical behavior**: Opening invariant `N` removes it from the mask,
allowing access to its content. Closing restores it to the mask.

**Runtime behavior**: Masks are proof-only bookkeeping. The runtime
implementation is identity: `fupd E₁ E₂ P ↝ P`.
-/

/-- Runtime implementation: fancy update erases to identity on `P`. -/
def fupdImpl (_E₁ _E₂ : Mask) (P : iProp) : iProp := P

/-- Fancy update modality `|={E₁,E₂}=> P`.

**Logical**: Mask-changing view shift enabling invariant access.
**Runtime**: Identity (mask tracking is proof-only). -/
@[implemented_by fupdImpl]
def fupd (E₁ E₂ : Mask) (P : iProp) : iProp :=
  Telltale.uPredFupd E₁ E₂ P

theorem fupd_intro (E : Mask) (P : iProp) :
    iProp.entails P (_root_.fupd E E P) :=
  (Iris.BaseLogic.fupd_intro_mask (W := ti.W) E E (fun _ hx => hx) P).trans
    (Iris.BaseLogic.fupd_trans (W := ti.W) E E E P)

theorem fupd_mono (E₁ E₂ : Mask) (P Q : iProp) :
    iProp.entails P Q → iProp.entails (_root_.fupd E₁ E₂ P) (_root_.fupd E₁ E₂ Q) :=
  fun h => Iris.BaseLogic.fupd_mono (W := ti.W) E₁ E₂ h

theorem fupd_trans (E₁ E₂ E₃ : Mask) (P : iProp) :
    iProp.entails (_root_.fupd E₁ E₂ (_root_.fupd E₂ E₃ P)) (_root_.fupd E₁ E₃ P) :=
  Iris.BaseLogic.fupd_trans (W := ti.W) E₁ E₂ E₃ P

theorem fupd_frame_r (E₁ E₂ : Mask) (P Q : iProp) :
    iProp.entails (iProp.sep (_root_.fupd E₁ E₂ P) Q)
      (_root_.fupd E₁ E₂ (iProp.sep P Q)) :=
  Iris.BaseLogic.fupd_frame_r (W := ti.W) E₁ E₂ P Q

theorem fupd_mask_subseteq (E₁ E₂ : Mask) (hSub : Mask.subseteq E₂ E₁) :
    iProp.entails iProp.emp (_root_.fupd E₁ E₂ (_root_.fupd E₂ E₁ iProp.emp)) :=
  Iris.BaseLogic.fupd_mask_subseteq (W := ti.W) E₁ E₂ hSub

/-! ## Invariants

Invariants `inv N P` assert that proposition `P` is maintained throughout
execution. The namespace `N` identifies the invariant for mask tracking.

**Logical behavior**: An invariant can be "opened" to access `P` during
a fancy update, then must be "closed" by re-establishing `P`.

**Runtime behavior**: The invariant machinery is proof-only. At runtime,
we only care about the content `P`, so `inv N P ↝ P`.
-/

/-- Runtime implementation: invariant erases to its content `P`. -/
def invImpl (_N : Namespace) (P : iProp) : iProp := P

/-- Invariant assertion `inv N P`.

**Logical**: Persistent assertion that `P` is maintained, openable via fancy update.
**Runtime**: Just the content `P` (namespace/mask tracking is proof-only). -/
@[implemented_by invImpl]
def inv (N : Namespace) (P : iProp) : iProp :=
  Iris.BaseLogic.inv (M := ti.M) (F := ti.F) ti.W N P

theorem inv_persistent (N : Namespace) (P : iProp) :
    iProp.entails (_root_.inv N P) (iProp.persistently (_root_.inv N P)) :=
  Iris.BaseLogic.inv_persistent (W := ti.W) N P

/-! ## Cancelable Invariants

Cancelable invariants extend regular invariants with the ability to be
"canceled" (permanently closed) by consuming a cancellation token.

**Components**:
- `cinv N ct P`: The cancelable invariant assertion
- `cancel_token_own ct`: Ownership of the cancellation token

**Logical behavior**: Opening requires the token; canceling consumes it.
This enables patterns where an invariant is valid only for a limited
scope or until a specific event.

**Runtime behavior**: Both the invariant and token are proof-only.
The invariant erases to its content; the token erases to `emp`.
-/

/-! ## Cancelable Invariant Definitions -/

/-- Cancelable invariant token handle. -/
abbrev CancelToken := GhostName

/-- Runtime implementation: cancel token erases to `emp`. -/
def cancel_token_ownImpl (_ct : CancelToken) : iProp := iProp.emp

/-- Cancellation token ownership.

**Logical**: Fractional ownership of the cancellation capability.
**Runtime**: `emp` (ghost ownership has no runtime representation). -/
@[implemented_by cancel_token_ownImpl]
def cancel_token_own (_ct : CancelToken) : iProp :=
  Iris.BaseLogic.cinv_own (GF := ti.GF) (F := ti.F) ti.W _ct (1 : ti.F)

/-- Runtime implementation: cancelable invariant erases to content `P`. -/
def cinvImpl (_N : Namespace) (_ct : CancelToken) (P : iProp) : iProp := P

/-- Cancelable invariant `cinv N ct P`.

**Logical**: Invariant `P` that can be accessed with token `ct` and
eventually canceled by consuming the full token.
**Runtime**: Just the content `P` (token/namespace is proof-only). -/
@[implemented_by cinvImpl]
def cinv (N : Namespace) (_ct : CancelToken) (P : iProp) : iProp :=
  Iris.BaseLogic.cinv (GF := ti.GF) (M := ti.M) (F := ti.F) ti.W N _ct P

/-! ## Namespace and Allocation Lemmas -/

/-- Distinct `Nat` children of the same namespace are disjoint. -/
theorem namespace_disjoint (N : Namespace) (n₁ n₂ : Nat) (hNe : n₁ ≠ n₂) :
    Mask.disjoint (namespace_to_mask (Namespace.append_nat N n₁))
      (namespace_to_mask (Namespace.append_nat N n₂)) := by
  simpa [namespace_to_mask, Namespace.append_nat] using
    (Iris.ndot_ne_disjoint (A := Nat) N (x := n₁) (y := n₂) hNe)

/-- Allocate a cancelable invariant from `▷ P`. -/
theorem cinv_alloc :
  ∀ (N : Namespace) (E : Mask) (P : iProp),
    (∀ E' : Iris.GSet, ∃ i, ¬E'.mem i ∧ (namespace_to_mask N) i) →
    iProp.entails (iProp.later P)
      (fupd E E (iProp.exist fun ct =>
        iProp.sep (cinv N ct P) (cancel_token_own ct)))
  := by
    intro N E P hFresh
    simpa [cinv, cancel_token_own, namespace_to_mask] using
      (Iris.BaseLogic.cinv_alloc (GF := ti.GF) (M := ti.M) (F := ti.F) ti.W E N P hFresh)

/-! ## Access and Cancel Lemmas -/

/-- Open a cancelable invariant using its full cancel token. -/
theorem cinv_acc :
  ∀ (N : Namespace) (E : Mask) (ct : CancelToken) (P : iProp),
    Mask.subseteq (namespace_to_mask N) E →
    iProp.entails (iProp.sep (cinv N ct P) (cancel_token_own ct))
      (fupd E (Mask.diff E (namespace_to_mask N))
        (iProp.sep (iProp.later P)
          (iProp.sep (cancel_token_own ct)
            (iProp.wand (iProp.later P)
              (fupd (Mask.diff E (namespace_to_mask N)) E (iProp.pure True))))))
  := by
    intro N E ct P hSub
    let post :=
      fupd E (Mask.diff E (namespace_to_mask N))
        (iProp.sep (iProp.later P)
          (iProp.sep (cancel_token_own ct)
            (iProp.wand (iProp.later P)
              (fupd (Mask.diff E (namespace_to_mask N)) E (iProp.pure True)))))
    have hOpen :
        iProp.entails (cinv N ct P) (iProp.wand (cancel_token_own ct) post) := by
      simpa [post, cinv, cancel_token_own, namespace_to_mask, Mask.diff] using
        (Iris.BaseLogic.cinv_acc (GF := ti.GF) (M := ti.M) (F := ti.F) ti.W E N ct (1 : ti.F) P hSub)
    have hFrame :
        iProp.entails (iProp.sep (cinv N ct P) (cancel_token_own ct))
          (iProp.sep (iProp.wand (cancel_token_own ct) post) (cancel_token_own ct)) :=
      sep_mono (P:=cinv N ct P) (P':=iProp.wand (cancel_token_own ct) post)
        (Q:=cancel_token_own ct) (Q':=cancel_token_own ct)
        hOpen (entails_refl _)
    exact hFrame.trans (wand_elim _ _)

/-- Cancel/consume step for a cancelable invariant with its full token. -/
theorem cinv_cancel :
  ∀ (N : Namespace) (E : Mask) (ct : CancelToken) (P : iProp),
    Mask.subseteq (namespace_to_mask N) E →
    iProp.entails (iProp.sep (cinv N ct P) (cancel_token_own ct))
      (fupd E (Mask.diff E (namespace_to_mask N))
        (iProp.sep (iProp.later P)
          (iProp.sep (cancel_token_own ct)
            (iProp.wand (iProp.later P)
              (fupd (Mask.diff E (namespace_to_mask N)) E (iProp.pure True))))))
  := by
    intro N E ct P hSub
    exact cinv_acc N E ct P hSub
