Report #20 — Shared-reference delegation in unindent 0.2.4

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/MasWag/crate-proofs report-20-source-1
git -C report-20-source-1 checkout --detach cabbee9506c6abcc2b9a42e7694ddc2ebdf7f07d
git -C report-20-source-1 submodule update --init --recursive --checkout
cd report-20-source-1/unindent/0.2.4/.work/build/default/x86_64-unknown-linux-gnu/proofs

lake build +Proofs.Delegation

printf '%s' 'import Aeneas
import Proofs.Delegation
set_option pp.all true
set_option pp.universes true
set_option pp.explicit true
set_option pp.fullNames true
set_option pp.notation false
set_option pp.proofs true
set_option pp.deepTerms true
set_option pp.maxSteps 10000000
-- proofs.rs adapter for Lean 4.35.0 / Aeneas be86ab0f.
-- Uses Lean'\''s environment, Meta telescope and pretty-printer, never source parsing.
open Lean Meta Elab Command
namespace ProofsProbe
meta def moduleOf (env : Environment) (n : Name) : String :=
  match env.getModuleIdxFor? n with
  | some idx => env.header.moduleNames[idx.toNat]!.toString
  | none => ""
meta def pretty (e : Expr) : MetaM String := do
  let s := (← ppExpr e).pretty
  if s.contains '\''⋯'\'' then
    throwError "Lean display contains an omission marker (or literal ⋯); refusing an incomplete proposition"
  if s.utf8ByteSize > 1000000 then throwError "Proposition exceeds 1,000,000-byte recording limit"
  return s
-- The full statement stays explicit; the inspection view uses Lean notation.
meta def readable (e : Expr) : MetaM String :=
  withOptions (fun o =>
    let o := o.setBool `pp.all false
    let o := o.setBool `pp.explicit false
    let o := o.setBool `pp.universes false
    o.setBool `pp.notation true) (pretty e)
-- Only a constant'\''s own tag grants a link; names in plain text are never guessed.
partial def segments (code : Widget.CodeWithInfos) (ref : Option Name := none) : Array Json :=
  match code with
  | .text text => #[Json.mkObj (([("text", toJson text)]) ++
      (ref.toList.map fun n => ("ref", toJson n.toString)))]
  | .append parts => parts.foldl (fun acc part => acc ++ segments part ref) #[]
  | .tag info part =>
    let ref := match info.info.val.info with
      | .ofTermInfo ti => ti.expr.constName?
      | _ => none
    segments part ref
meta def readableFields (key : String) (e : Expr) : MetaM (List (String × Json)) := do
  let text ← readable e
  let base := [(key, toJson text)]
  try
    let code ← withOptions (fun o =>
      let o := o.setBool `pp.all false
      let o := o.setBool `pp.explicit false
      let o := o.setBool `pp.universes false
      let o := o.setBool `pp.notation true
      o.setBool `pp.tagAppFns true) (Widget.ppExprTagged e)
    let parts := segments code
    let joined := String.join (parts.toList.map fun j =>
      (j.getObjValAs? String "text").toOption.getD "")
    if joined != text || parts.size > 10000 || joined.utf8ByteSize > 1000000 then
      return base
    return base ++ [(key ++ "_segments", toJson parts)]
  catch _ => return base
meta def inspect (n : Name) (ty : Expr) (manual : Bool) : MetaM (Option Json) := do
  let env ← getEnv
  forallTelescope ty fun xs conclusion => do
    let programExpr ← try
      let normalized ← Aeneas.Utils.normalizeLetBindings conclusion
      let (expr, _) ← Aeneas.Step.getStepSpecFunArgsExpr normalized
      pure (some expr)
    catch _ => pure none
    if programExpr.isNone && !manual then return none
    let full ← pretty ty
    let program ← match programExpr with
      | some expr => pure (toJson (← readable expr))
      | none => pure Json.null
    let head := toJson (programExpr.bind (·.getAppFn.constName?) |>.map Name.toString)
    let mut binders := #[]
    for x in xs do
      let d ← x.fvarId!.getDecl
      let prop ← isProp d.type
      binders := binders.push (Json.mkObj ((← readableFields "type" d.type) ++ [
        ("name", toJson d.userName.toString),
        ("kind", toJson (if d.binderInfo.isInstImplicit then "instance" else if prop then "hypothesis" else "variable")),
        ("binder", toJson (if d.binderInfo.isInstImplicit then "instance" else if d.binderInfo.isExplicit then "explicit" else "implicit"))]))
    if binders.size > 1000 then throwError "More than 1000 binders"
    let some ranges ← findDeclarationRanges? n | throwError "Missing theorem source range: {n}"
    let axioms ← Lean.collectAxioms n
    let constants := ty.getUsedConstants
    let mut definitions := #[]
    for nm in constants.extract 0 100 do
      let ranges ← findDeclarationRanges? nm
      definitions := definitions.push (Json.mkObj [
        ("name", toJson nm.toString), ("module", toJson (moduleOf env nm)),
        ("source", match ranges with
          | some r => Json.mkObj [("first_line", toJson r.range.pos.line), ("last_line", toJson r.range.endPos.line)]
          | none => Json.null)])
    return some (Json.mkObj ((← readableFields "conclusion" conclusion) ++ [
      ("version", toJson (1 : Nat)), ("theorem", toJson n.toString),
      ("module", toJson (moduleOf env n)), ("statement", toJson full),
      ("binders", toJson binders),
      ("program", program), ("program_head", head),
      ("axioms", toJson (axioms.map Name.toString)),
      ("first_line", toJson ranges.range.pos.line), ("last_line", toJson ranges.range.endPos.line),
      ("definitions", toJson definitions), ("definitions_truncated", toJson (decide (constants.size > 100))),
      ("translation_rerun", toJson false)]))
end ProofsProbe

run_cmd do
  let manual : Array Name := #[`unindent.Proofs.shared_unindent_spec]
  let localModules : Array String := #[]
  let roots : Array Name := #[]
  let env ← getEnv
  let mut closure : Array Name := #[]
  let mut pending := roots.toList
  while !pending.isEmpty do
    let m := pending.head!
    pending := pending.tail!
    if !closure.contains m then
      closure := closure.push m
      if let some idx := env.header.moduleNames.findIdx? (· == m) then
        pending := (env.header.moduleData[idx]!.imports.toList.map (·.module)) ++ pending
  let scope := closure.filter (fun m => localModules.contains m.toString)
  for n in manual do
    match env.find? n with
    | some (.thmInfo _) => pure ()
    | _ => throwError "Expected a theorem: {n}"
  for (n, ci) in env.constants.toList do
    let explicit := manual.contains n
    if explicit || scope.contains (ProofsProbe.moduleOf env n).toName then
      if let .thmInfo th := ci then
        let result ← liftTermElabM <| ProofsProbe.inspect n th.type explicit
        if let some value := result then
          liftIO <| IO.println ("proofs.rs:formal:" ++ value.compress)

run_cmd do
  let theorem_name := `unindent.Proofs.shared_unindent_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: unindent.Proofs.shared_unindent_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in unindent.Proofs.shared_unindent_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:unindent.Proofs.shared_unindent_spec"
' | lake env lean --stdin

Checks out the recorded source commit from GitHub. Install the report’s tool version before running.

Source on GitHub · SARIF with logs (.json)

Recorded run

Completed · 1 checks passed · 0 failed

2026-11-03T23:47:14.461323772+00:00 · 188.5 seconds · Exit code 0

Recorded on the author’s machine.

=== stdout ===
✔ [1796/1799] Built Wrapper (15s)
✔ [1797/1799] Built Unindent (24s)
ℹ [1798/1799] Built Proofs.CountSpaces (41s)
info: Proofs/CountSpaces.lean:97:0: 'UnindentProof.countSpaces_total_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [1799/1799] Built Proofs.Delegation (35s)
Build completed successfully (1799 jobs).

$ lake env lean --stdin (proofs.rs formal extraction and axiom audit)
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"T","type":"Type","type_segments":[{"text":"Type"}]},{"binder":"implicit","kind":"variable","name":"O","type":"Type","type_segments":[{"text":"Type"}]},{"binder":"explicit","kind":"variable","name":"inst","type":"unindent.unindent.Unindent T O","type_segments":[{"ref":"unindent.unindent.Unindent","text":"unindent.unindent.Unindent"},{"text":" "},{"text":"T"},{"text":" "},{"text":"O"}]},{"binder":"explicit","kind":"variable","name":"self","type":"T","type_segments":[{"text":"T"}]},{"binder":"explicit","kind":"variable","name":"post","type":"O → Prop","type_segments":[{"text":"O"},{"text":" → "},{"text":"Prop"}]},{"binder":"explicit","kind":"hypothesis","name":"h","type":"∃ out, inst.unindent self = Aeneas.Std.Result.ok out ∧ post out","type_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"text":"inst"},{"text":"."},{"ref":"unindent.unindent.Unindent.unindent","text":"unindent"},{"text":" "},{"text":"self"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"post"},{"text":" "},{"text":"out"}]}],"conclusion":"∃ out, unindent.Shared0T.Insts.UnindentUnindentUnindent.unindent inst self = Aeneas.Std.Result.ok out ∧ post out","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"unindent.Shared0T.Insts.UnindentUnindentUnindent.unindent","text":"unindent.Shared0T.Insts.UnindentUnindentUnindent.unindent"},{"text":" "},{"text":"inst"},{"text":" "},{"text":"self"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"post"},{"text":" "},{"text":"out"}],"definitions":[{"module":"Wrapper","name":"unindent.unindent.Unindent","source":{"first_line":23,"last_line":27}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Wrapper","name":"unindent.unindent.Unindent.unindent","source":{"first_line":27,"last_line":27}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Wrapper","name":"unindent.Shared0T.Insts.UnindentUnindentUnindent.unindent","source":{"first_line":29,"last_line":37}}],"definitions_truncated":false,"first_line":9,"last_line":13,"module":"Proofs.Delegation","program":null,"program_head":null,"statement":"∀ {T O : Type} (inst : unindent.unindent.Unindent.{0, 0} T O) (self : T) (post : O → Prop)\n  (h :\n    @Exists.{1} O fun (out : O) =>\n      And\n        (@Eq.{1} (Aeneas.Std.Result.{0} O) (@unindent.unindent.Unindent.unindent.{0, 0} T O inst self)\n          (@Aeneas.Std.Result.ok.{0} O out))\n        (post out)),\n  @Exists.{1} O fun (out : O) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} O)\n        (@unindent.Shared0T.Insts.UnindentUnindentUnindent.unindent.{0, 0} T O inst self)\n        (@Aeneas.Std.Result.ok.{0} O out))\n      (post out)","theorem":"unindent.Proofs.shared_unindent_spec","translation_rerun":false,"version":1}

=== stderr ===