lean/PathSpecAeneas.lean

-- File: lean/PathSpecAeneas.lean
-- Path Canonicalizer — Aeneas-compatible specification.
-- Types mirror what Aeneas generates from Vec<String> Rust code.
-- Requires: lake update  (fetches the Aeneas package)

import Aeneas
open Aeneas.Primitives

namespace PathSpecAeneas

-- Aeneas maps Rust Vec<String> to Vec String (or List String in practice)
-- We use List String for simplicity, matching the generated functional code.
abbrev Path := List String

-- Normalize: remove "." segments, resolve ".." clamped at root
private def normalizeAux (acc : Path) : Path → Path
  | []          => acc.reverse
  | seg :: rest =>
    if seg == "."  then normalizeAux acc rest
    else if seg == ".." then
      match acc with
      | []       => normalizeAux [] rest
      | _ :: acc' => normalizeAux acc' rest
    else normalizeAux (seg :: acc) rest

def normalizePath (p : Path) : Result Path :=
  .ok (normalizeAux [] p)

-- Join: normalize concatenation of base and rel
def joinPaths (base rel : Path) : Result Path :=
  .ok (normalizeAux [] (base ++ rel))

-- Depth: segment count
def pathDepth (p : Path) : Result U64 :=
  let n := p.length
  if h : n ≤ U64.max.val then
    .ok ⟨n, by omega⟩
  else
    .fail .panic

-- Idempotency: normalizePath (normalizePath p) = normalizePath p
theorem normalizePath_idempotent (p : Path) :
    (normalizePath p).bind normalizePath = normalizePath p := by
  simp only [normalizePath, Result.bind]
  congr 1
  -- Reduce to the same lemma as PathSpec: normalizeAux [] (normalizeAux [] p).reverse = normalizeAux [] p
  -- The proof follows from the fact that normalizeAux [] already produces a normalized path.
  induction p using List.reverseRecOn with
  | nil => simp [normalizeAux]
  | append_singleton p seg ih =>
    simp only [normalizeAux, List.append_eq]
    sorry -- Proof left for agents; follows from PathSpec.normalize_idempotent via transfer

end PathSpecAeneas