Compile authenticated algebraic sources and quote complete cell proofs

HexManual/Chapters/HexRCF/RootTableQuote.lean

@@ -68,7 +68,7 @@ example :
 ```
 
 
-The fresh importing conformance module checks all 86 reachable example theorem
+The fresh importing conformance module checks all 103 reachable example theorem
 bodies and 14 definitions under the kernel producer guard, including private
 auxiliaries and the final witness. The complete axiom closure contains only
 `propext`, `Classical.choice` and `Quot.sound`. The stored polynomial request

HexRCF/HandlerTests/Admission.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+public import HexRCF.Tactic
+
+public section
+
+open Lean Meta
+namespace Hex.RCF.AdmissionTests
+opaque hidden : Nat := 13
+inductive Link where
+  | nil
+  | cons (tail : Link)
+private meta def reference (expression : Expr) : MetaM Bool := do
+  let expression ← instantiateMVars expression
+  if expression.hasExprMVar then return false
+  for name in expression.getUsedConstants do
+    for axiomName in ← collectAxioms name do
+      unless [``propext,``Classical.choice,``Quot.sound].contains axiomName do return false
+  return true
+run_meta do
+  withoutModifyingEnv do
+    let mut previous := mkConst ``hidden
+    let mut expressions := #[previous,mkConst ``Link,mkConst ``Link.rec,
+      mkConst ``Quot.mk [.zero],mkConst ``Classical.choice [.zero],
+      mkConst ``sorryAx [.zero],mkConst ``sorryAx [.succ .zero]]
+    for i in [:64] do
+      let value ← mkAppM ``Nat.add #[previous,previous]
+      let name := mkPrivateName (← getEnv) (← mkFreshUserName `diamond)
+      previous ← mkAuxDefinition name (mkConst ``Nat) value (compile := false)
+      if i % 8 == 0 then expressions := expressions.push previous
+    expressions := expressions.push (← mkAppM ``Nat.add #[previous,previous])
+    let value ← mkAppM ``Nat.add #[previous,mkNatLit 1]
+    let left ← mkAuxDefinition (mkPrivateName (← getEnv) (← mkFreshUserName `left))
+      (mkConst ``Nat) value (compile := false)
+    let right ← mkAuxDefinition (mkPrivateName (← getEnv) (← mkFreshUserName `right))
+      (mkConst ``Nat) value (compile := false)
+    expressions := expressions.push (← mkAppM ``Nat.add #[left,right])
+    expressions := expressions.push (← mkFreshExprMVar (mkConst ``True))
+    let forbidden := mkConst ``sorryAx [.zero]
+    expressions := expressions.push (mkApp (mkLambda `unused .default (← inferType forbidden)
+      (mkConst ``True.intro)) forbidden)
+    for expression in expressions do
+      let expected ← reference expression
+      let actual ← try
+        Hex.RCF.checkAxioms `forestProbe expression
+        pure true
+      catch _ => pure false
+      unless expected == actual do
+        throwError "forest and authoritative admission policies disagree: {expression}"
+    logInfo m!"forest/reference agree on {expressions.size} imported/local/opaque/inductive/shared/forbidden/unresolved cases"
+-- Reuse an identical declaration name across rolled-back environments. A
+-- previous successful check must not mask a later forbidden dependency, and
+-- a failed check must not poison a later valid declaration with that name.
+run_meta do
+  let reused := Name.mkSimple "__rcfForestEnvironmentProbe"
+  for forbidden in #[false,true,false] do
+    let saved ← saveState
+    try
+        let value ← if forbidden then mkSorry (mkConst ``Nat) false else pure (mkNatLit 3)
+        let root ← mkAuxDefinition reused (mkConst ``Nat) value (compile := false)
+        let shared ← mkAppM ``Nat.add #[root,root]
+        let expected ← reference shared
+        let actual ← try
+          Hex.RCF.checkAxioms `forestEnvironment shared
+          pure true
+        catch _ => pure false
+        unless expected == !forbidden && actual == expected do
+          throwError "admission retained results across an environment rollback"
+    finally
+      saved.restore
+  logInfo "forest admission follows all three rolled-back environments"
+end Hex.RCF.AdmissionTests

HexRCF/README.md

@@ -388,8 +388,32 @@ slots. It quotes a nonconstant scalar query, decodes a coefficient from that
 fact alone and proves its selected real value. Dependent branch proofs move
 by checked equality elimination; explicit replay functions remain abstract
 during conversion before instantiation. A fresh audit rechecks imported bodies
-with the unchanged producer guard. This does not supply the missing numerical
-signature equation or install the general tactic.
+with the unchanged producer guard. This does not install the general tactic.
+`RootHeader.quoteWith` reconstructs a root and independently parses its original
+raw subject through `RootReplay.readDescriptor_subject`. Their checked binding,
+quoted under one reflection budget, supplies the raw-root identity needed by a
+subsequent scalar packet. The [public consumer](../conformance/HexRCF/RootHeaderPacket.lean)
+constructs a new root/context, and the [coefficient consumer](../conformance/HexRCF/RootHeaderValues.lean)
+proves its selected real value and positivity without the old fixture's root
+identity. Canonical signature roundtrips use the existing public law at the
+actual encoded subject. `SignatureQuote.decoder` consumes the owner's public
+literal equation and a checked binding to the exact supplied signature. The
+new cubic packet retains frozen numerical node and nested-moment signatures;
+the [fresh signature tests](../conformance/HexRCF/FrozenSignatureProofs.lean)
+check distinct subjects and wrong bindings. This does not authenticate arbitrary
+registries or construct origin histories or deeper frozen root frames.
+`RootContext.packWith` assembles the actual native child from a closed retained
+parent and a checked descriptor, retaining the owner's serialization expression
+and checking its signature. The [ordinary-model regression](../conformance/HexRCF/RootContextConformance.lean)
+retains the coefficient's selected value and positive sign; its fresh audit
+also excludes serialization and graph encoding in the new packing bodies.
+This is checked typed-context construction, not fully frozen history assembly.
+`RootPrepare.prepareWith` retains a reconstructed descriptor and native context
+behind checked private definitions, with exact header and context equations.
+The [anonymous-reader regression](../conformance/HexRCF/RootPreparePacket.lean)
+composes its decoder with `ScalarPacket.quoteWith` to recover the original
+reader's equation. Header reconstruction, retention and replay share one
+request; its proof budget includes simplifier visits and generated expressions.
 `SectionQuote.finish` freshly reifies the original target and checks its matrix,
 valuation and ordered original-divisor identities before transporting a proof.
 The [fresh-source tests](../conformance/HexRCF/SectionProduceConformance.lean)

HexRCF/Tactic.lean

@@ -74,25 +74,58 @@ private meta opaque evalHandler (name : Name) : MetaM Handler
 private meta def ordinaryAxiom (name : Name) : Bool :=
   [``propext, ``Classical.choice, ``Quot.sound].contains name
 
+/-- Visit each local dependency once within one admission check. Imported
+closures use Lean's authoritative module inventories, including hidden bodies.
+The state is discarded before returning; no environment-sensitive cache persists. -/
+private meta partial def checkConstant (handler : Name) (environment : Environment)
+    (root current : Name) : StateRefT NameSet MetaM Unit := do
+  let seen : NameSet ← get
+  if seen.contains current then return
+  modify fun (seen : NameSet) => seen.insert current
+  if (environment.getModuleIdxFor? current).isSome then
+    for dependency in ← collectAxioms current do
+      unless ordinaryAxiom dependency do
+        throwError "rcf: handler {handler} proposed a proof using forbidden axiom {dependency} (through {root})"
+    return
+  let visit (expression : Expr) := expression.getUsedConstants.forM fun dependency =>
+    checkConstant handler environment root dependency
+  match environment.checked.get.find? current with
+  | some (.axiomInfo info) =>
+      unless ordinaryAxiom current do
+        throwError "rcf: handler {handler} proposed a proof using forbidden axiom {current} (through {root})"
+      visit info.type
+  | some (.defnInfo info) => visit info.type; visit info.value
+  | some (.thmInfo info) => visit info.type; visit info.value
+  | some (.opaqueInfo info) => visit info.type; visit info.value
+  | some (.quotInfo _) => pure ()
+  | some (.ctorInfo info) => visit info.type
+  | some (.recInfo info) => visit info.type
+  | some (.inductInfo info) =>
+      visit info.type
+      info.ctors.forM (checkConstant handler environment root)
+  | none => pure ()
+
 /-- Optional solvers may depend only on Lean's standard logical axioms.
 Imported dependency inventories also cover theorem bodies hidden by modules. -/
 meta def checkAxioms (name : Name) (proof : Expr) : MetaM Unit := do
-  let proof ← instantiateMVars proof
-  -- Universe metavariables do not hide declarations in an inventory probe.
-  -- Expression metavariables can hide arbitrary proof dependencies.
-  if proof.hasExprMVar then throwError "rcf: handler {name} returned an unresolved proof"
-  for constant in proof.getUsedConstants do
-    for dependency in ← collectAxioms constant do
-      unless ordinaryAxiom dependency do
-        throwError "rcf: handler {name} proposed a proof using forbidden axiom {dependency} (through {constant})"
+  profileitM Exception "rcf axiom dependency check" (← getOptions) do
+    let proof ← instantiateMVars proof
+    -- Universe metavariables do not hide declarations in an inventory probe.
+    -- Expression metavariables can hide arbitrary proof dependencies.
+    if proof.hasExprMVar then throwError "rcf: handler {name} returned an unresolved proof"
+    let environment ← getEnv
+    let _ ← (proof.getUsedConstants.forM fun constant =>
+      checkConstant name environment constant constant).run ({} : NameSet)
 
 /-- Screen closed expression data before native evaluation or proof acceptance.
 Local hypotheses remain permitted; unresolved and nonstandard dependencies do not. -/
 meta def checkExpr (name : Name) (expression : Expr) : MetaM Expr := do
   let expression ← instantiateMVars expression
   if expression.hasMVar then throwError "rcf: {name} contains unresolved metavariables"
   checkAxioms name expression
-  if (← getEnv).hasUnsafe expression then
+  let usesUnsafe ← profileitM Exception "rcf unsafe dependency check" (← getOptions) do
+    pure ((← getEnv).hasUnsafe expression)
+  if usesUnsafe then
     throwError "rcf: {name} uses an unsafe declaration"
   return expression
 
@@ -110,7 +143,9 @@ meta def checkProof (name : Name) (target proof : Expr)
   unless agrees do
     throwError "rcf: handler {name} proposed a proof of a different goal"
   checkAxioms name proof
-  if (← getEnv).hasUnsafe proof then
+  let usesUnsafe ← profileitM Exception "rcf unsafe dependency check" (← getOptions) do
+    pure ((← getEnv).hasUnsafe proof)
+  if usesUnsafe then
     throwError "rcf: handler {name} proposed a proof using an unsafe declaration"
   let proof ← profileitM Exception (category ++ " candidate check") (← getOptions) do
     withOptions (fun opts => debug.skipKernelTC.set (Elab.async.set opts false) false) do

adapters/HexRCF/RealCoefficients.lean

@@ -14,6 +14,8 @@ public meta import HexRCF.RealCoefficients.AlgebraicBounds
 public meta import HexRCF.RealCoefficients.Finite
 public meta import HexRCF.RealCoefficients.Reify
 public meta import HexRCF.RealCoefficients.Interpret
+public import HexRCF.RealCoefficients.TowerCompile
+public meta import HexRCF.RealCoefficients.TowerCompile
 public import HexRCF.RealCoefficients.RationalRoot
 public meta import HexRCF.RealCoefficients.RationalRoot
 public import HexRCF.RealCoefficients.RootAliases
@@ -24,6 +26,8 @@ public import HexRCF.RealCoefficients.Formula
 public import HexRCF.RealCoefficients.Field
 public import HexRCF.RealCoefficients.CommonPresentation
 public import HexRCF.RealCoefficients.SourceIdentity
+public meta import HexRCF.RealCoefficients.SourceIdentityQuote
+public import HexRCF.RealCoefficients.SourceBuild
 public import HexRCF.RealCoefficients.LiteralSign
 public import HexRCF.RealCoefficients.SignIndex
 public import HexRCF.RealCoefficients.FieldIndex
@@ -52,6 +56,12 @@ public meta import HexRCF.RealCoefficients.Quote
 public import HexRCF.RealCoefficients.RootReplay
 public import HexRCF.RealCoefficients.RootBuild
 public import HexRCF.RealCoefficients.RootQuote
+public import HexRCF.RealCoefficients.RowQuote
+public meta import HexRCF.RealCoefficients.RowQuote
+public meta import HexRCF.RealCoefficients.RootHeader
+public meta import HexRCF.RealCoefficients.RootPrepare
+public meta import HexRCF.RealCoefficients.RootContext
+public meta import HexRCF.RealCoefficients.SignatureQuote
 public meta import HexRCF.RealCoefficients.RootQuote
 public meta import HexRCF.RealCoefficients.RationalQuote
 public import HexRCF.RealCoefficients.ScalarQuote

adapters/HexRCF/RealCoefficients/CellOperations.lean

@@ -315,6 +315,34 @@ theorem formulaSector_eq (operations : Hex.RealClosure.Replay.Operations parent.
     formulaSector operations value roots cut values formula sectorFields[cut])
   return ⟨sections, fun cut => (sectors cut).sector, fun cut => (sectors cut).row⟩
 
+/-- Checked layout and pointwise row equations restore the complete dependent
+cell family. Original guards precede every layout and row read. -/
+theorem readCells_of_parts (operations : Hex.RealClosure.Replay.Operations parent.sign)
+    (value : ValueCodec parent.Value) (guards : List parent.Value)
+    (roots : RootReplay.Result p .negInf .posInf) (values : Fin n → parent.Value)
+    (formula : RealFormula.QF (n+1)) (packet : Codec.Json)
+    (fields : Vector Codec.Json 2)
+    (sectionFields : Vector Codec.Json roots.roots.length)
+    (sectorFields : Vector Codec.Json (roots.roots.length+1))
+    (sections : (i : Fin roots.roots.length) →
+      SelectedSigns (roots.roots.get i) (RepresentationSpecialize.prepare values formula))
+    (sectors : (cut : Fin (roots.roots.length+1)) → SectorReplay.Result roots cut values formula)
+    (guarded : guards.all (fun d => Decidable.decide (d ≠ 0)) = true)
+    (layout : Codec.tuple 2 packet = .ok fields)
+    (sectionLayout : Codec.tuple roots.roots.length fields[0] = .ok sectionFields)
+    (sectorLayout : Codec.tuple (roots.roots.length+1) fields[1] = .ok sectorFields)
+    (sectionChecked : ∀ i, formulaRow operations value (roots.roots.get i) values formula
+      sectionFields[i] = .ok (sections i))
+    (sectorChecked : ∀ cut, formulaSector operations value roots cut values formula
+      sectorFields[cut] = .ok (sectors cut)) :
+    readCells operations value guards roots values formula packet =
+      .ok ⟨sections, fun cut => (sectors cut).sector, fun cut => (sectors cut).row⟩ := by
+  have sectionRead := CellRead.collectWith_eq .binding _ _ sections sectionChecked
+  have sectorRead := CellRead.collectWith_eq .binding _ _ sectors sectorChecked
+  simp only [readCells, guarded, ite_true,
+    layout, sectionLayout, sectorLayout, CellRead.collect, sectionRead, sectorRead,
+    bind, Except.bind, pure, Except.pure]
+
 theorem readCells_eq (operations : Hex.RealClosure.Replay.Operations parent.sign)
     (value : ValueCodec parent.Value) (guards : List parent.Value)
     (roots : RootReplay.Result p .negInf .posInf) (values : Fin n → parent.Value)
@@ -387,6 +415,25 @@ theorem check_eq (operations : Hex.RealClosure.Replay.Operations parent.sign)
     check operations value values formula guards cert quantifier rootGraph cells =
       CompleteReplay.check value values formula guards cert quantifier rootGraph cells := by
   simp only [check, CompleteReplay.check, read_eq, fold_eq]
+
+/-- Compose independently checked root, cell and fold equations at the exact
+original packet. The dependent cell type retains the root reader's result. -/
+theorem check_of_parts (operations : Hex.RealClosure.Replay.Operations parent.sign)
+    (value : ValueCodec parent.Value) (values : Fin n → parent.Value)
+    (formula : RealFormula.QF (n+1)) (guards : List parent.Value)
+    (cert : RadicalCert parent.Value Signature) (quantifier : RealFormula.Quantifier)
+    (rootGraph cells : Codec.Json) (roots : RootReplay.Result cert.core .negInf .posInf)
+    (data : CellReplay.Evidence roots values formula) (verdict : Bool)
+    (rootChecked : RootReplay.readWith value guards cert.core .negInf .posInf
+      operations.one operations.add operations.sub operations.mul operations.natCast
+      operations.one_eq operations.add_eq operations.sub_eq operations.mul_eq operations.natCast_eq
+      rootGraph = .ok roots)
+    (cellsChecked : readCells operations value guards roots values formula cells = .ok data)
+    (foldChecked : fold operations values formula guards cert roots data quantifier = .ok verdict) :
+    check operations value values formula guards cert quantifier rootGraph cells = .ok verdict := by
+  simpa only [check, read, rootChecked, cellsChecked, bind, Except.bind, pure, Except.pure]
+    using foldChecked
+
 /-- The owner assembly API checks an optional success predicate. Only an
 accepted true verdict is a success; the public checker retains typed failures
 and the diagnostic false result. -/