CloneProbe.lean

import FrontierDerivative.DelayedResolver

/-!
# Fixed-port clone probe

The verified tuple encoding decodes logical stack `j` by reading label
component `j` and following port `j` at every historical node.  This module
checks that redirecting destination port `j` to source port `i` copies only
the new top: the historical walk resumes in coordinate `j`.

This is a counterexample to that obvious clone operation, not an impossibility
theorem for scaffolds or persistent stack cloning in another coordinate
doctrine.
-/

namespace FrontierDerivative.CloneProbe

open FPRD

/-- First compiler-shaped step: push `1` on stack 0 and `9` on stack 1. -/
def firstOps (j : Fin 2) : StackOp Nat :=
  if j = 0 then .push 1 else .push 9

def history1 : Scaffold 2 (Tuple 2 Nat) :=
  let base := Scaffold.base 2 (Tuple 2 Nat)
  base.append (newLabel base firstOps) (newTarget firstOps)

/-- Second compiler-shaped step: push `2` on stack 0 and keep stack 1. -/
def secondOps (j : Fin 2) : StackOp Nat :=
  if j = 0 then .push 2 else .keep

def history : Scaffold 2 (Tuple 2 Nat) :=
  history1.append (newLabel history1 secondOps) (newTarget secondOps)

theorem history1_backward : history1.Backward := by
  apply Scaffold.append_backward
  · exact Scaffold.base_backward 2 (Tuple 2 Nat)
  · exact newTarget_ne_self firstOps

/-- The source history is a well-directed scaffold built by the verified
compiler's own label/target formulas. -/
theorem history_backward : history.Backward := by
  apply Scaffold.append_backward
  · exact history1_backward
  · exact newTarget_ne_self secondOps

theorem source_before_clone : decode history 0 history.top = [2, 1] := by
  rw [decode_eq_decodeAux]
  native_decide

theorem destination_before_clone : decode history 1 history.top = [9] := by
  rw [decode_eq_decodeAux]
  native_decide

/-- Obvious attempted clone: copy source component 0 into every new component
and redirect every new port to the old source-0 root. -/
def naiveCloneLabel : Tuple 2 Nat :=
  fun _ => labelComp history history.top 0

def naiveCloneTarget : Fin 2 → Target 2 :=
  fun _ => .path [0]

def naiveClone : Scaffold 2 (Tuple 2 Nat) :=
  history.append naiveCloneLabel naiveCloneTarget

/-- The failed clone is still backward; its defect is coordinate switching,
not a forward edge or `SELF`. -/
theorem naiveClone_backward : naiveClone.Backward := by
  apply Scaffold.append_backward
  · exact history_backward
  · intro i
    simp [naiveCloneTarget]

theorem source_after_clone : decode naiveClone 0 naiveClone.top = [2, 1] := by
  rw [decode_eq_decodeAux]
  native_decide

/-- Destination gets the copied top `2`, then resumes component/port 1 at the
historical node and therefore reads `9` rather than source tail `1`. -/
theorem destination_after_clone : decode naiveClone 1 naiveClone.top = [2, 9] := by
  rw [decode_eq_decodeAux]
  native_decide

theorem naiveClone_not_copy :
    decode naiveClone 1 naiveClone.top ≠ decode naiveClone 0 naiveClone.top := by
  rw [destination_after_clone, source_after_clone]
  decide

#check history_backward
#check naiveClone_backward
#check naiveClone_not_copy

end FrontierDerivative.CloneProbe