From 825b52e2c009a3a5dcf71954d2a2cd1a32869145 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 29 Jul 2026 06:05:49 +0000 Subject: [PATCH 1/6] Prove arbitrary propagator traces end to end --- HexInterval/Experiment/PayloadArena.lean | 4 +- HexInterval/Experiment/Propagator.lean | 13 +- HexInterval/Experiment/SemanticReplay.lean | 884 ++++++++++++++++-- HexInterval/SPEC/hex-interval.md | 68 +- .../HexInterval/PropagatorE2EConformance.lean | 753 +++++++++++++++ .../SemanticReplayConformance.lean | 83 +- lakefile.lean | 2 +- progress/20260729T060457Z.md | 48 + 8 files changed, 1747 insertions(+), 108 deletions(-) create mode 100644 conformance/HexInterval/PropagatorE2EConformance.lean create mode 100644 progress/20260729T060457Z.md diff --git a/HexInterval/Experiment/PayloadArena.lean b/HexInterval/Experiment/PayloadArena.lean index 9ac39260c..380a14fc6 100644 --- a/HexInterval/Experiment/PayloadArena.lean +++ b/HexInterval/Experiment/PayloadArena.lean @@ -52,7 +52,7 @@ structure Entry where role : Role schema : Nat body : List Nat - deriving Repr + deriving DecidableEq, Repr /-- The immutable dispatch address for semantic replay. `rule.schema` is the handler/theorem compatibility epoch; this structure's numeric `schema` is a @@ -85,7 +85,7 @@ the aggregate body bound independent of later arena size. -/ structure Arena where entries : Array Entry bodyCells : Nat - deriving Repr + deriving DecidableEq, Repr namespace Arena diff --git a/HexInterval/Experiment/Propagator.lean b/HexInterval/Experiment/Propagator.lean index 64c051a52..2b8b7c5d1 100644 --- a/HexInterval/Experiment/Propagator.lean +++ b/HexInterval/Experiment/Propagator.lean @@ -65,20 +65,20 @@ structure Operation where key : OpKey inputs : List DomainId output : DomainId - deriving Repr + deriving DecidableEq, Repr /-- One instruction in a typed single-assignment expression DAG. -/ structure Node where domain : DomainId op : OpId args : List NodeId - deriving Repr + deriving DecidableEq, Repr /-- Immutable base expression program. -/ structure Program where operations : Array Operation nodes : Array Node - deriving Repr + deriving DecidableEq, Repr namespace Program @@ -370,7 +370,7 @@ structure Action where kind : ActionKind effort : Nat inputs : List SeenVersion - deriving Repr + deriving DecidableEq, Repr /-- Immutable fact view supplied with an action. -/ structure Snapshot (Fact : Type) where @@ -761,7 +761,7 @@ or payload. -/ inductive FactCause (Fact : Type) where | rule (action : Action) (proposed : Fact) (payload : PayloadId) | transport (equality : EqualityId) (source : SeenVersion) - deriving Repr + deriving DecidableEq, Repr /-- One retained fact provenance record. -/ structure FactEvent (Fact : Type) where @@ -771,6 +771,7 @@ structure FactEvent (Fact : Type) where fact : Fact version : Nat cause : FactCause Fact + deriving DecidableEq, Repr /-- Canonical unordered endpoint pair for one generated equality. -/ structure EqualityPair where @@ -797,6 +798,7 @@ structure EqualityEdge where generation : Nat origin : Action payload : PayloadId + deriving DecidableEq, Repr def equalityPair (left right : NodeId) : EqualityPair := if left.index <= right.index then { first := left, second := right } @@ -826,6 +828,7 @@ structure InstanceEvent where instance and repeated references to the same canonical link. -/ equalities : List EqualityId payload : PayloadId + deriving DecidableEq, Repr /-- Live state of the function-agnostic scheduler. -/ structure Engine (Fact : Type) where diff --git a/HexInterval/Experiment/SemanticReplay.lean b/HexInterval/Experiment/SemanticReplay.lean index 0bc98e858..d16f3d7d6 100644 --- a/HexInterval/Experiment/SemanticReplay.lean +++ b/HexInterval/Experiment/SemanticReplay.lean @@ -20,11 +20,11 @@ certificate type, decoder, and theorem builder for each fact schema. The generic registry dispatches only on the exact `(RuleKey, role, schema)` stored in an immutable payload entry. -This is not yet a complete trace checker. It fixes the interfaces needed by -that checker without pretending that format validation establishes semantic -soundness. In particular, rule replay proves the proposed fact, while a -separate fact-domain schema proves that intersecting the previous and proposed -facts produced the installed fact. +Format validation does not establish semantic soundness. Fact schemas prove +proposed facts, instance schemas prove conservative program extension, and +equality schemas prove transport for the exact admitted edge. A separate +fact-domain schema proves that intersecting the previous and proposed facts +produced the installed fact. -/ namespace Hex.Interval.Experiment.SemanticReplay @@ -35,6 +35,18 @@ open Propagator PayloadArena structure NodeFact (Fact : Type) where node : NodeId fact : Fact + deriving DecidableEq + +namespace NodeFact + +theorem extensionality (left right : NodeFact Fact) + (node : left.node = right.node) (fact : left.fact = right.fact) : + left = right := by + cases left + cases right + simp_all + +end NodeFact /-- Inputs owned by the caller, rather than reconstructed from an untrusted trace. Making this value an explicit parameter of every replay context binds @@ -54,6 +66,14 @@ structure Semantics (Fact : Type) where Value : Type models : Program -> (NodeId -> Value) -> Prop holds : Program -> (NodeId -> Value) -> NodeFact Fact -> Prop + /-- Fact interpretation is stable when an equality schema proves that two + expression nodes have the same semantic value. -/ + transport : + ∀ (program : Program) (valuation : NodeId -> Value) + (left right : NodeId) (fact : Fact), + valuation left = valuation right -> + holds program valuation { node := left, fact } -> + holds program valuation { node := right, fact } namespace Semantics @@ -66,6 +86,21 @@ def Entails (semantics : Semantics Fact) (program : Program) semantics.holds program valuation assumption) -> semantics.holds program valuation conclusion +/-- A package-owned expression extension is semantically conservative when +every valuation of the old program has a valuation of the new program which +agrees on every old expression node. An instance schema proves this stronger +property rather than merely acknowledging that an instance payload exists. -/ +def Extends (semantics : Semantics Fact) (before after : Program) : Prop := + ∀ valuation, semantics.models before valuation -> + ∃ extended, semantics.models after extended ∧ + ∀ node, node.index < before.nodes.size -> extended node = valuation node + +/-- Semantic equality of two nodes in one checked program. -/ +def Equivalent (semantics : Semantics Fact) (program : Program) + (left right : NodeId) : Prop := + ∀ valuation, semantics.models program valuation -> + valuation left = valuation right + end Semantics /-- A proof packaged in `Type`, so a computational checker may return it in @@ -74,25 +109,53 @@ structure Evidence (claim : Prop) : Type where proof : claim /-- Proposition that the caller's program is an exact prefix of the program -being replayed. A future untrusted trace validator must construct this -witness; schemas may consume it but cannot choose a different base program. -/ +being replayed. The suffix witnesses make this constructible by a transparent +checker over untrusted arrays; schemas may consume it but cannot choose a +different base program. -/ structure ProgramPrefix (base extended : Program) : Prop where - operationSize : base.operations.size ≤ extended.operations.size - nodeSize : base.nodes.size ≤ extended.nodes.size - operationAt : - ∀ index, index < base.operations.size -> - extended.operations[index]? = base.operations[index]? - nodeAt : - ∀ index, index < base.nodes.size -> - extended.nodes[index]? = base.nodes[index]? + operationSuffix : + ∃ suffix, extended.operations.toList = base.operations.toList ++ suffix + nodeSuffix : + ∃ suffix, extended.nodes.toList = base.nodes.toList ++ suffix namespace ProgramPrefix theorem refl (program : Program) : ProgramPrefix program program := - { operationSize := Nat.le_refl _ - nodeSize := Nat.le_refl _ - operationAt := fun _ _ => rfl - nodeAt := fun _ _ => rfl } + { operationSuffix := ⟨[], by simp⟩ + nodeSuffix := ⟨[], by simp⟩ } + +def suffix? [DecidableEq α] : + (expected values : List α) -> + Option { suffix : List α // values = expected ++ suffix } + | [], values => some ⟨values, rfl⟩ + | _ :: _, [] => none + | head :: rest, actual :: values => + if equal : actual = head then + match suffix? rest values with + | none => none + | some suffix => + some + ⟨suffix, by + subst actual + simpa only [List.cons_append] using + congrArg (List.cons head) suffix.property⟩ + else + none + +/-- Transparently construct exact prefix evidence from two untrusted program +snapshots. -/ +def check? (base extended : Program) : + Option (Evidence (ProgramPrefix base extended)) := + match suffix? base.operations.toList extended.operations.toList with + | none => none + | some operations => + match suffix? base.nodes.toList extended.nodes.toList with + | none => none + | some nodes => + some + { proof := + { operationSuffix := ⟨operations, operations.property⟩ + nodeSuffix := ⟨nodes, nodes.property⟩ } } end ProgramPrefix @@ -105,6 +168,24 @@ structure RuleFactContext (input : CheckerInput Fact) (action : Action) where assumptions : List (NodeFact Fact) proposed : NodeFact Fact +/-- Exact structural context for one admitted instantiation. The executable +engine supplies the event and the two chronological program snapshots; the +payload entry fixes `action` to the immutable package invocation which +proposed it. -/ +structure InstanceContext (input : CheckerInput Fact) (action : Action) where + before : Program + after : Program + basePrefix : ProgramPrefix input.baseProgram before + event : InstanceEvent + +/-- Exact semantic context for transporting one fact over an admitted +equality. Equality packages prove the transport theorem for the fact domain; +the generic replay loop never interprets either endpoint's function. -/ +structure EqualityContext (input : CheckerInput Fact) (action : Action) where + program : Program + basePrefix : ProgramPrefix input.baseProgram program + edge : EqualityEdge + /-- The fact-domain proof boundary is intentionally independent of all function-rule schemas. `proveMeet` must establish semantic intersection for the exact installed fact; merely proving the proposal is insufficient. @@ -128,6 +209,15 @@ structure FactDomainSchema (semantics : Semantics Fact) where (semantics.holds program valuation { node, fact := installed } ↔ semantics.holds program valuation { node, fact := previous } ∧ semantics.holds program valuation { node, fact := proposed }))) + /-- Close a requested result from a fact which may be strictly stronger. + Final replay must not require representation equality with the goal. -/ + proveImplies : + (program : Program) -> (node : NodeId) -> + (stronger requested : Fact) -> + Option (Evidence + (∀ valuation, semantics.models program valuation -> + semantics.holds program valuation { node, fact := stronger } -> + semantics.holds program valuation { node, fact := requested })) /-- An immutable, existentially packed theorem schema owned by one rule. @@ -154,20 +244,61 @@ def key (packed : PackedFactSchema semantics) : ReplayKey := end PackedFactSchema +/-- An existentially packed, package-owned proof for one expression +instantiation recipe. -/ +structure PackedInstanceSchema (semantics : Semantics Fact) where + rule : RuleKey + schema : Nat + Certificate : Type + decode : List Nat -> Option Certificate + replay : + (input : CheckerInput Fact) -> (action : Action) -> + (context : InstanceContext input action) -> Certificate -> + Option (Evidence (semantics.Extends context.before context.after)) + +namespace PackedInstanceSchema + +def key (packed : PackedInstanceSchema semantics) : ReplayKey := + { rule := packed.rule, role := .instance, schema := packed.schema } + +end PackedInstanceSchema + +/-- An existentially packed, package-owned proof for one admitted equality +recipe. Its theorem is the exact transport step used by chronological fact +replay, so equality payload coverage is semantic rather than cosmetic. -/ +structure PackedEqualitySchema (semantics : Semantics Fact) where + rule : RuleKey + schema : Nat + Certificate : Type + decode : List Nat -> Option Certificate + replay : + (input : CheckerInput Fact) -> (action : Action) -> + (context : EqualityContext input action) -> Certificate -> + Option (Evidence + (semantics.Equivalent context.program context.edge.left context.edge.right)) + +namespace PackedEqualitySchema + +def key (packed : PackedEqualitySchema semantics) : ReplayKey := + { rule := packed.rule, role := .equality, schema := packed.schema } + +end PackedEqualitySchema + /-- Cache-free semantic declarations contributed by one function package. Package order is the same as in the checked executable registry supplied to `Registry.build`; this lets assembly reject a theorem schema attributed to a different package even when both packages reuse the same numeric schema. -/ structure Package (semantics : Semantics Fact) where factSchemas : Array (PackedFactSchema semantics) + instanceSchemas : Array (PackedInstanceSchema semantics) := #[] + equalitySchemas : Array (PackedEqualitySchema semantics) := #[] -/-- Exact executable replay declarations covered or deliberately deferred by -the current semantic protocol. Fact formats have bidirectional coverage: -every key here has exactly one checker. Instance and equality formats remain -visible rather than being silently treated as checked. -/ +/-- Exact executable replay declarations covered by semantic schemas. Every +key in each role has exactly one package-owned checker. -/ structure Coverage where factFormats : Array ReplayKey - deferredFormats : Array ReplayKey + instanceFormats : Array ReplayKey + equalityFormats : Array ReplayKey deriving Repr /-- Semantic assembly failures retain the exact replay address and package @@ -183,98 +314,222 @@ inductive BuildError where structure Registry (semantics : Semantics Fact) where private mk :: factSchemas : Array (PackedFactSchema semantics) + instanceSchemas : Array (PackedInstanceSchema semantics) + equalitySchemas : Array (PackedEqualitySchema semantics) + coverage : Coverage + +/-- Transparent theorem dispatcher used by kernel replay. Unlike the sealed +search-paired `Registry`, its constructor need not be a trust boundary: +forging one cannot manufacture any `Evidence`, because every packed schema's +dependent result still has to prove its exact context. `buildPackages` is the +checked constructor used by the tactic and conformance fixtures. -/ +structure KernelRegistry (semantics : Semantics Fact) where + factSchemas : Array (PackedFactSchema semantics) + instanceSchemas : Array (PackedInstanceSchema semantics) + equalitySchemas : Array (PackedEqualitySchema semantics) coverage : Coverage namespace Registry private def make (factSchemas : Array (PackedFactSchema semantics)) + (instanceSchemas : Array (PackedInstanceSchema semantics)) + (equalitySchemas : Array (PackedEqualitySchema semantics)) (coverage : Coverage) : Registry semantics := - { factSchemas, coverage } + { factSchemas, instanceSchemas, equalitySchemas, coverage } + +def containsFactKey (schemas : Array (PackedFactSchema semantics)) + (key : ReplayKey) : Bool := + schemas.any fun schema => schema.key == key -private def containsKey (schemas : Array (PackedFactSchema semantics)) +def containsInstanceKey + (schemas : Array (PackedInstanceSchema semantics)) (key : ReplayKey) : Bool := schemas.any fun schema => schema.key == key -private def addSchemas (schemas : Array (PackedFactSchema semantics)) : +def containsEqualityKey + (schemas : Array (PackedEqualitySchema semantics)) + (key : ReplayKey) : Bool := + schemas.any fun schema => schema.key == key + +def addFactSchemas (schemas : Array (PackedFactSchema semantics)) : List (PackedFactSchema semantics) -> Except BuildError (Array (PackedFactSchema semantics)) | [] => pure schemas | schema :: rest => - if containsKey schemas schema.key then + if containsFactKey schemas schema.key then + throw (BuildError.duplicateSchema schema.key) + else + addFactSchemas (schemas.push schema) rest + +def addInstanceSchemas + (schemas : Array (PackedInstanceSchema semantics)) : + List (PackedInstanceSchema semantics) -> + Except BuildError (Array (PackedInstanceSchema semantics)) + | [] => pure schemas + | schema :: rest => + if containsInstanceKey schemas schema.key then + throw (BuildError.duplicateSchema schema.key) + else + addInstanceSchemas (schemas.push schema) rest + +def addEqualitySchemas + (schemas : Array (PackedEqualitySchema semantics)) : + List (PackedEqualitySchema semantics) -> + Except BuildError (Array (PackedEqualitySchema semantics)) + | [] => pure schemas + | schema :: rest => + if containsEqualityKey schemas schema.key then throw (BuildError.duplicateSchema schema.key) else - addSchemas (schemas.push schema) rest + addEqualitySchemas (schemas.push schema) rest -private def packageCoverage (package : Propagator.Package Fact) : Coverage := +def packageCoverage (package : Propagator.Package Fact) : Coverage := package.handlers.foldl (fun coverage handler => handler.replayFormats.foldl (fun coverage format => let key := format.replayKey handler.registration.key - if format.role == .fact then - { coverage with factFormats := coverage.factFormats.push key } - else - { coverage with - deferredFormats := coverage.deferredFormats.push key }) + match format.role with + | .fact => + { coverage with factFormats := coverage.factFormats.push key } + | .instance => + { coverage with + instanceFormats := coverage.instanceFormats.push key } + | .equality => + { coverage with + equalityFormats := coverage.equalityFormats.push key }) coverage) - { factFormats := #[], deferredFormats := #[] } + { factFormats := #[], instanceFormats := #[], equalityFormats := #[] } -private def checkOwners (package : Nat) (formats : Array ReplayKey) : +def checkFactOwners (package : Nat) (formats : Array ReplayKey) : List (PackedFactSchema semantics) -> Except BuildError PUnit | [] => pure ⟨⟩ | schema :: schemas => if formats.any (fun key => key == schema.key) then - checkOwners package formats schemas + checkFactOwners package formats schemas + else + throw (.unownedSchema package schema.key) + +def checkInstanceOwners (package : Nat) (formats : Array ReplayKey) : + List (PackedInstanceSchema semantics) -> Except BuildError PUnit + | [] => pure ⟨⟩ + | schema :: schemas => + if formats.any (fun key => key == schema.key) then + checkInstanceOwners package formats schemas + else + throw (.unownedSchema package schema.key) + +def checkEqualityOwners (package : Nat) (formats : Array ReplayKey) : + List (PackedEqualitySchema semantics) -> Except BuildError PUnit + | [] => pure ⟨⟩ + | schema :: schemas => + if formats.any (fun key => key == schema.key) then + checkEqualityOwners package formats schemas else throw (.unownedSchema package schema.key) -private def checkCoverage (package : Nat) +def checkFactCoverage (package : Nat) (schemas : Array (PackedFactSchema semantics)) : List ReplayKey -> Except BuildError PUnit | [] => pure ⟨⟩ | key :: keys => - if containsKey schemas key then - checkCoverage package schemas keys + if containsFactKey schemas key then + checkFactCoverage package schemas keys + else + throw (.missingSchema package key) + +def checkInstanceCoverage (package : Nat) + (schemas : Array (PackedInstanceSchema semantics)) : + List ReplayKey -> Except BuildError PUnit + | [] => pure ⟨⟩ + | key :: keys => + if containsInstanceKey schemas key then + checkInstanceCoverage package schemas keys + else + throw (.missingSchema package key) + +def checkEqualityCoverage (package : Nat) + (schemas : Array (PackedEqualitySchema semantics)) : + List ReplayKey -> Except BuildError PUnit + | [] => pure ⟨⟩ + | key :: keys => + if containsEqualityKey schemas key then + checkEqualityCoverage package schemas keys else throw (.missingSchema package key) -private def addPackages (index : Nat) - (schemas : Array (PackedFactSchema semantics)) (coverage : Coverage) : +def addPackages (index : Nat) + (facts : Array (PackedFactSchema semantics)) + (instances : Array (PackedInstanceSchema semantics)) + (equalities : Array (PackedEqualitySchema semantics)) + (coverage : Coverage) : List (Propagator.Package Fact) -> List (Package semantics) -> - Except BuildError (Array (PackedFactSchema semantics) × Coverage) - | [], [] => pure (schemas, coverage) + Except BuildError + (Array (PackedFactSchema semantics) × + Array (PackedInstanceSchema semantics) × + Array (PackedEqualitySchema semantics) × Coverage) + | [], [] => pure (facts, instances, equalities, coverage) | executable :: executables, package :: packages => do let owned := packageCoverage executable - checkOwners index owned.factFormats package.factSchemas.toList - checkCoverage index package.factSchemas owned.factFormats.toList - let schemas ← addSchemas schemas package.factSchemas.toList + checkFactOwners index owned.factFormats package.factSchemas.toList + checkInstanceOwners index owned.instanceFormats package.instanceSchemas.toList + checkEqualityOwners index owned.equalityFormats package.equalitySchemas.toList + checkFactCoverage index package.factSchemas owned.factFormats.toList + checkInstanceCoverage index package.instanceSchemas owned.instanceFormats.toList + checkEqualityCoverage index package.equalitySchemas owned.equalityFormats.toList + let facts ← addFactSchemas facts package.factSchemas.toList + let instances ← addInstanceSchemas instances package.instanceSchemas.toList + let equalities ← addEqualitySchemas equalities package.equalitySchemas.toList let coverage := { factFormats := coverage.factFormats ++ owned.factFormats - deferredFormats := - coverage.deferredFormats ++ owned.deferredFormats } - addPackages (index + 1) schemas coverage executables packages + instanceFormats := coverage.instanceFormats ++ owned.instanceFormats + equalityFormats := coverage.equalityFormats ++ owned.equalityFormats } + addPackages (index + 1) facts instances equalities coverage + executables packages | executables, packages => throw (.packageCount executables.length packages.length) +/-- Transparent semantic assembly directly against the immutable executable +package declarations. This is the kernel-replay entry point: opaque compiled +search registries are deliberately not a soundness dependency. -/ +def buildPackages (executable : Array (Propagator.Package Fact)) + (packages : Array (Package semantics)) : + Except BuildError (KernelRegistry semantics) := do + if executable.size != packages.size then + throw (.packageCount executable.size packages.size) + let (factSchemas, instanceSchemas, equalitySchemas, coverage) ← + addPackages 0 #[] #[] #[] + { factFormats := #[], instanceFormats := #[], equalityFormats := #[] } + executable.toList packages.toList + pure { factSchemas, instanceSchemas, equalitySchemas, coverage } + /-- Assemble schemas against one checked executable registry without retaining its mutable package caches. Package positions establish ownership, exact -`ReplayKey`s establish dispatch, and every executable fact format must have -exactly one checker. Unsupported instance and equality formats are returned -in `Registry.coverage.deferredFormats`. -/ +`ReplayKey`s establish dispatch, and every executable format in every role +must have exactly one checker. -/ opaque build (executable : Propagator.Registry Fact) (packages : Array (Package semantics)) : Except BuildError (Registry semantics) := do if executable.packages.size != packages.size then throw (.packageCount executable.packages.size packages.size) - let (factSchemas, coverage) ← - addPackages 0 #[] { factFormats := #[], deferredFormats := #[] } + let (factSchemas, instanceSchemas, equalitySchemas, coverage) ← + addPackages 0 #[] #[] #[] + { factFormats := #[], instanceFormats := #[], equalityFormats := #[] } executable.packages.toList packages.toList - pure (make factSchemas coverage) + pure (make factSchemas instanceSchemas equalitySchemas coverage) def findFact? (registry : Registry semantics) (key : ReplayKey) : Option (PackedFactSchema semantics) := registry.factSchemas.toList.find? fun schema => schema.key == key +def findInstance? (registry : Registry semantics) (key : ReplayKey) : + Option (PackedInstanceSchema semantics) := + registry.instanceSchemas.toList.find? fun schema => schema.key == key + +def findEquality? (registry : Registry semantics) (key : ReplayKey) : + Option (PackedEqualitySchema semantics) := + registry.equalitySchemas.toList.find? fun schema => schema.key == key + /-- Decode and replay one immutable fact entry under the exact selected schema. Equality and instantiation roles cannot accidentally reach a fact schema because lookup compares the full replay key. @@ -294,14 +549,100 @@ def dispatchFact {Fact : Type} {semantics : Semantics Fact} | some certificate => packed.replay input entry.origin context certificate +/-- Decode and replay one exact instance entry. -/ +def dispatchInstance {Fact : Type} {semantics : Semantics Fact} + (registry : Registry semantics) (input : CheckerInput Fact) + (entry : Entry) (context : InstanceContext input entry.origin) : + Option (Evidence (semantics.Extends context.before context.after)) := + match registry.findInstance? entry.replayKey with + | none => none + | some packed => + match packed.decode entry.body with + | none => none + | some certificate => + packed.replay input entry.origin context certificate + +/-- Decode and replay one exact equality entry. -/ +def dispatchEquality {Fact : Type} {semantics : Semantics Fact} + (registry : Registry semantics) (input : CheckerInput Fact) + (entry : Entry) (context : EqualityContext input entry.origin) : + Option (Evidence + (semantics.Equivalent context.program context.edge.left context.edge.right)) := + match registry.findEquality? entry.replayKey with + | none => none + | some packed => + match packed.decode entry.body with + | none => none + | some certificate => + packed.replay input entry.origin context certificate + end Registry +namespace KernelRegistry + +def findFact? (registry : KernelRegistry semantics) (key : ReplayKey) : + Option (PackedFactSchema semantics) := + registry.factSchemas.toList.find? fun schema => schema.key == key + +def findInstance? (registry : KernelRegistry semantics) (key : ReplayKey) : + Option (PackedInstanceSchema semantics) := + registry.instanceSchemas.toList.find? fun schema => schema.key == key + +def findEquality? (registry : KernelRegistry semantics) (key : ReplayKey) : + Option (PackedEqualitySchema semantics) := + registry.equalitySchemas.toList.find? fun schema => schema.key == key + +def dispatchFact {Fact : Type} {semantics : Semantics Fact} + (registry : KernelRegistry semantics) (input : CheckerInput Fact) + (entry : Entry) (context : RuleFactContext input entry.origin) : + Option (Evidence + (semantics.Entails context.program context.assumptions context.proposed)) := + match registry.findFact? entry.replayKey with + | none => none + | some packed => + match packed.decode entry.body with + | none => none + | some certificate => + packed.replay input entry.origin context certificate + +def dispatchInstance {Fact : Type} {semantics : Semantics Fact} + (registry : KernelRegistry semantics) (input : CheckerInput Fact) + (entry : Entry) (context : InstanceContext input entry.origin) : + Option (Evidence (semantics.Extends context.before context.after)) := + match registry.findInstance? entry.replayKey with + | none => none + | some packed => + match packed.decode entry.body with + | none => none + | some certificate => + packed.replay input entry.origin context certificate + +def dispatchEquality {Fact : Type} {semantics : Semantics Fact} + (registry : KernelRegistry semantics) (input : CheckerInput Fact) + (entry : Entry) (context : EqualityContext input entry.origin) : + Option (Evidence + (semantics.Equivalent context.program context.edge.left context.edge.right)) := + match registry.findEquality? entry.replayKey with + | none => none + | some packed => + match packed.decode entry.body with + | none => none + | some certificate => + packed.replay input entry.origin context certificate + +end KernelRegistry + /-! ## Prefix-only access to untrusted trace data -/ /-- Untrusted retained replay data. The caller-owned base program, initial facts, and target are intentionally absent; they remain in `CheckerInput`. -/ structure Trace (Fact : Type) where program : Program + /-- Program snapshots in chronological order, including the caller's base + program at index zero and `program` as the final entry. -/ + programs : Array Program := #[] + instances : Array InstanceEvent := #[] + equalities : Array EqualityEdge := #[] events : Array (FactEvent Fact) arena : Arena @@ -349,24 +690,423 @@ def factAt? {Fact : Type} {semantics : Semantics Fact} end Trace -/-! ## Deliberate boundary of this canary +/-! ## Transparent chronological trace checker -/ + +/-- Caller-owned version-zero assumptions, in exact base-node order. -/ +def initialContextFrom (index : Nat) : List Fact -> List (NodeFact Fact) + | [] => [] + | fact :: facts => + { node := { index }, fact } :: initialContextFrom (index + 1) facts + +def initialContext (input : CheckerInput Fact) : List (NodeFact Fact) := + initialContextFrom 0 input.initialFacts.toList + +/-- A list member carrying its membership proof in `Type`. -/ +structure Member (items : List α) where + value : α + proof : value ∈ items + +def findNodeMember? (node : NodeId) : + (items : List (NodeFact Fact)) -> Option (Member items) + | [] => none + | fact :: facts => + if fact.node == node then + some { value := fact, proof := List.Mem.head _ } + else + match findNodeMember? node facts with + | none => none + | some member => + some { value := member.value, proof := List.Mem.tail _ member.proof } + +/-- One chronologically established fact, together with its theorem from the +caller-owned initial context. -/ +structure ProvenFact (semantics : Semantics Fact) (program : Program) + (assumptions : List (NodeFact Fact)) where + nodeFact : NodeFact Fact + version : Nat + evidence : Evidence (semantics.Entails program assumptions nodeFact) + +namespace ProvenFact + +def find? (seen : SeenVersion) : + List (ProvenFact semantics program assumptions) -> + Option (ProvenFact semantics program assumptions) + | [] => none + | proven :: facts => + if proven.nodeFact.node == seen.node && proven.version == seen.version then + some proven + else + find? seen facts + +theorem holdsOfMem {Fact : Type} {semantics : Semantics Fact} + {program : Program} {assumptions : List (NodeFact Fact)} + (proven : List (ProvenFact semantics program assumptions)) + (valuation : NodeId -> semantics.Value) + (model : semantics.models program valuation) + (initial : ∀ assumption, assumption ∈ assumptions -> + semantics.holds program valuation assumption) + (fact : NodeFact Fact) + (member : fact ∈ proven.map + (fun item : ProvenFact semantics program assumptions => item.nodeFact)) : + semantics.holds program valuation fact := by + induction proven with + | nil => simp at member + | cons head tail induction => + simp only [List.map_cons, List.mem_cons] at member + rcases member with equal | member + · subst fact + exact head.evidence.proof valuation model initial + · exact induction member + +end ProvenFact + +/-- An admitted equality whose exact package-owned theorem has replayed. -/ +structure ProvenEquality (semantics : Semantics Fact) (program : Program) where + edge : EqualityEdge + evidence : + Evidence (semantics.Equivalent program edge.left edge.right) + +def expectedNewNodes (before after : Program) : List NodeId := + (List.range (after.nodes.size - before.nodes.size)).map + (fun offset => { index := before.nodes.size + offset }) + +def instanceEqualitiesValid (equalities : Array EqualityEdge) + (event : InstanceEvent) : Bool := + event.equalities.all fun equalityId => + (equalities[equalityId.index]?).any fun edge => edge.origin == event.origin + +def replayInstances {Fact : Type} {semantics : Semantics Fact} + (registry : KernelRegistry semantics) (input : CheckerInput Fact) + (trace : Trace Fact) (index : Nat) : + List InstanceEvent -> Option PUnit + | [] => some ⟨⟩ + | event :: events => do + let before ← trace.programs[index]? + let after ← trace.programs[index + 1]? + if before.operations != after.operations || + event.programVersion != index + 1 || + event.origin.programVersion != index || + event.newNodes != expectedNewNodes before after || + !instanceEqualitiesValid trace.equalities event then + none + else + let basePrefix ← ProgramPrefix.check? input.baseProgram before + let stepPrefix ← ProgramPrefix.check? before after + let entry ← trace.arena.entry? event.payload .instance + if entry.origin != event.origin then none else + let context : InstanceContext input entry.origin := + { before + after + basePrefix := basePrefix.proof + event } + let _ ← registry.dispatchInstance input entry context + let _ := stepPrefix + replayInstances registry input trace (index + 1) events + +def equalityOwned (instances : Array InstanceEvent) + (id : EqualityId) (edge : EqualityEdge) : Bool := + instances.any fun event => + event.origin == edge.origin && event.equalities.contains id + +def replayEqualities {Fact : Type} {semantics : Semantics Fact} + (registry : KernelRegistry semantics) (input : CheckerInput Fact) + (trace : Trace Fact) (basePrefix : ProgramPrefix input.baseProgram trace.program) : + Nat -> List EqualityEdge -> + Option (Array (ProvenEquality semantics trace.program)) + | _, [] => some #[] + | index, edge :: edges => do + let id : EqualityId := { index } + if !equalityOwned trace.instances id edge then none else + let entry ← trace.arena.entry? edge.payload .equality + if entry.origin != edge.origin then none else + let context : EqualityContext input entry.origin := + { program := trace.program + basePrefix + edge } + let evidence ← registry.dispatchEquality input entry context + let rest ← replayEqualities registry input trace basePrefix + (index + 1) edges + pure (#[{ edge, evidence }] ++ rest) + +def replayStructure {Fact : Type} {semantics : Semantics Fact} + (registry : KernelRegistry semantics) (input : CheckerInput Fact) + (trace : Trace Fact) : + Option + (Evidence (ProgramPrefix input.baseProgram trace.program) × + Array (ProvenEquality semantics trace.program)) := do + if trace.programs.size != trace.instances.size + 1 || + trace.programs[0]? != some input.baseProgram || + trace.programs[trace.instances.size]? != some trace.program then + none + else + let finalPrefix ← ProgramPrefix.check? input.baseProgram trace.program + let _ ← replayInstances registry input trace 0 trace.instances.toList + let equalities ← replayEqualities registry input trace finalPrefix.proof + 0 trace.equalities.toList + pure (finalPrefix, equalities) + +def resolveFact {Fact : Type} {semantics : Semantics Fact} + (domain : FactDomainSchema semantics) (input : CheckerInput Fact) + (trace : Trace Fact) (assumptions : List (NodeFact Fact)) + (proven : List (ProvenFact semantics trace.program assumptions)) + (seen : SeenVersion) : + Option (ProvenFact semantics trace.program assumptions) := + if seen.version == 0 then + if seen.node.index < input.baseProgram.nodes.size then + match findNodeMember? seen.node assumptions with + | none => none + | some member => + some + { nodeFact := member.value + version := 0 + evidence := + { proof := by + intro valuation model initial + exact initial member.value member.proof } } + else + match nodeProof : trace.program.node? seen.node with + | none => none + | some instruction => + some + { nodeFact := { node := seen.node, fact := domain.top instruction.domain } + version := 0 + evidence := + { proof := by + intro valuation model _ + exact domain.topSound trace.program valuation seen.node + instruction nodeProof model } } + else + ProvenFact.find? seen proven + +def discharge {Fact : Type} {semantics : Semantics Fact} + (program : Program) (assumptions : List (NodeFact Fact)) + (premises : List (ProvenFact semantics program assumptions)) + (conclusion : NodeFact Fact) + (evidence : + Evidence (semantics.Entails program + (premises.map (fun item => item.nodeFact)) conclusion)) : + Evidence (semantics.Entails program assumptions conclusion) := + { proof := by + intro valuation model initial + exact evidence.proof valuation model fun fact member => + ProvenFact.holdsOfMem premises valuation model initial fact member } + +def installFact {Fact : Type} {semantics : Semantics Fact} + (domain : FactDomainSchema semantics) (program : Program) + (assumptions : List (NodeFact Fact)) + (previous : ProvenFact semantics program assumptions) + (proposed : ProvenFact semantics program assumptions) + (event : FactEvent Fact) : + Option (ProvenFact semantics program assumptions) := + if previousNode : previous.nodeFact.node = event.node then + if proposedNode : proposed.nodeFact.node = event.node then + if event.previous.node != event.node || + event.version != event.previous.version + 1 then + none + else do + let meet ← domain.proveMeet program event.node previous.nodeFact.fact + proposed.nodeFact.fact event.fact + pure + { nodeFact := { node := event.node, fact := event.fact } + version := event.version + evidence := + { proof := by + intro valuation model initial + have previousHolds : + semantics.holds program valuation + { node := event.node, fact := previous.nodeFact.fact } := by + have factEq : previous.nodeFact = + { node := event.node, fact := previous.nodeFact.fact } := by + exact NodeFact.extensionality _ _ previousNode rfl + rw [← factEq] + exact previous.evidence.proof valuation model initial + have proposedHolds : + semantics.holds program valuation + { node := event.node, fact := proposed.nodeFact.fact } := by + have factEq : proposed.nodeFact = + { node := event.node, fact := proposed.nodeFact.fact } := by + exact NodeFact.extensionality _ _ proposedNode rfl + rw [← factEq] + exact proposed.evidence.proof valuation model initial + exact (meet.proof valuation model).mpr + ⟨previousHolds, proposedHolds⟩ } } + else + none + else + none + +def factFromRule {Fact : Type} {semantics : Semantics Fact} + (registry : KernelRegistry semantics) (domain : FactDomainSchema semantics) + (input : CheckerInput Fact) + (trace : Trace Fact) (basePrefix : ProgramPrefix input.baseProgram trace.program) + (assumptions : List (NodeFact Fact)) + (proven : List (ProvenFact semantics trace.program assumptions)) + (event : FactEvent Fact) (action : Action) (proposed : Fact) + (payload : PayloadId) : + Option (ProvenFact semantics trace.program assumptions) := do + if event.programVersion != action.programVersion then none else + let premises ← action.inputs.mapM + (resolveFact (Fact := Fact) (semantics := semantics) + domain input trace assumptions proven) + let entry ← trace.arena.entry? payload .fact + if entry.origin != action then none else + let context : RuleFactContext input entry.origin := + { program := trace.program + basePrefix + assumptions := premises.map (fun item => item.nodeFact) + proposed := { node := event.node, fact := proposed } } + let evidence ← registry.dispatchFact input entry context + pure + { nodeFact := context.proposed + version := event.version + evidence := discharge trace.program assumptions premises + context.proposed evidence } + +def transportFact {Fact : Type} {semantics : Semantics Fact} + (trace : Trace Fact) + (assumptions : List (NodeFact Fact)) + (equalities : Array (ProvenEquality semantics trace.program)) + (source : ProvenFact semantics trace.program assumptions) + (target : NodeId) (equalityId : EqualityId) : + Option (ProvenFact semantics trace.program assumptions) := do + let equality ← equalities[equalityId.index]? + let proposed : NodeFact Fact := { node := target, fact := source.nodeFact.fact } + if forward : + equality.edge.left = source.nodeFact.node ∧ equality.edge.right = target then + pure + { nodeFact := proposed + version := source.version + evidence := + { proof := by + intro valuation model initial + let equal := equality.evidence.proof valuation model + have values : + valuation source.nodeFact.node = valuation target := by + simpa [forward.1, forward.2] using equal + exact semantics.transport trace.program valuation + source.nodeFact.node target source.nodeFact.fact values + (source.evidence.proof valuation model initial) } } + else if reverse : + equality.edge.right = source.nodeFact.node ∧ equality.edge.left = target then + pure + { nodeFact := proposed + version := source.version + evidence := + { proof := by + intro valuation model initial + let equal := (equality.evidence.proof valuation model).symm + have values : + valuation source.nodeFact.node = valuation target := by + simpa [reverse.1, reverse.2] using equal + exact semantics.transport trace.program valuation + source.nodeFact.node target source.nodeFact.fact values + (source.evidence.proof valuation model initial) } } + else + none + +def replayEvents {Fact : Type} {semantics : Semantics Fact} + (registry : KernelRegistry semantics) (domain : FactDomainSchema semantics) + (input : CheckerInput Fact) (trace : Trace Fact) + (basePrefix : ProgramPrefix input.baseProgram trace.program) + (assumptions : List (NodeFact Fact)) + (equalities : Array (ProvenEquality semantics trace.program)) : + List (FactEvent Fact) -> + List (ProvenFact semantics trace.program assumptions) -> + Option (List (ProvenFact semantics trace.program assumptions)) + | [], proven => some proven + | event :: events, proven => do + let previous ← resolveFact domain input trace assumptions proven event.previous + if (ProvenFact.find? + { node := event.node, version := event.version } proven).isSome then + none + else + let proposed ← + match event.cause with + | .rule action fact payload => + factFromRule registry domain input trace basePrefix assumptions + proven event action fact payload + | .transport equality sourceVersion => do + let source ← + resolveFact domain input trace assumptions proven sourceVersion + transportFact trace assumptions equalities source event.node equality + let installed ← installFact domain trace.program assumptions + previous proposed event + replayEvents registry domain input trace basePrefix assumptions equalities + events (installed :: proven) + +/-- Transparently replay an explicit, untrusted trace. Search may run through +opaque compiled session operations, but soundness depends only on this +kernel-reducible pass and the proof terms returned by package-owned schemas. + +The result certifies the requested bound under the complete checked program +from the caller's exact version-zero assumptions. -/ +def check {Fact : Type} [DecidableEq Fact] {semantics : Semantics Fact} + (registry : KernelRegistry semantics) (domain : FactDomainSchema semantics) + (input : CheckerInput Fact) (trace : Trace Fact) : + Option (Evidence + (semantics.Entails trace.program (initialContext input) input.target)) := do + if input.initialFacts.size != input.baseProgram.nodes.size then none else + let (basePrefix, equalities) ← replayStructure registry input trace + let assumptions := initialContext input + let proven ← replayEvents registry domain input trace basePrefix.proof assumptions + equalities trace.events.toList [] + match proven.find? (fun fact => fact.nodeFact.node == input.target.node) with + | none => + match findNodeMember? input.target.node assumptions with + | some member => + if targetNode : member.value.node = input.target.node then + let implication ← domain.proveImplies trace.program input.target.node + member.value.fact input.target.fact + some + { proof := by + intro valuation model initial + have stronger : + semantics.holds trace.program valuation + { node := input.target.node, fact := member.value.fact } := by + have factEq : member.value = + { node := input.target.node, fact := member.value.fact } := by + exact NodeFact.extensionality _ _ targetNode rfl + rw [← factEq] + exact initial member.value member.proof + exact implication.proof valuation model stronger } + else + none + | none => none + | some target => + if targetNode : target.nodeFact.node = input.target.node then + let implication ← domain.proveImplies trace.program input.target.node + target.nodeFact.fact input.target.fact + some + { proof := by + intro valuation model initial + have stronger : + semantics.holds trace.program valuation + { node := input.target.node, fact := target.nodeFact.fact } := by + have factEq : target.nodeFact = + { node := input.target.node, fact := target.nodeFact.fact } := by + exact NodeFact.extensionality _ _ targetNode rfl + rw [← factEq] + exact target.evidence.proof valuation model initial + exact implication.proof valuation model stronger } + else + none + +/-! ## Remaining production work A complete checker still has to validate, in one forward pass: -* exact base-prefix preservation and initial-fact length; -* chronological versions, `previous` links, and action-input resolution using - only the already-checked event prefix; -* package-owned instance and equality schemas for the explicitly deferred - non-fact `ReplayFormat` declarations, including proof of every appended - instruction and admitted equality; -* composition of the rule entailment and fact-domain meet evidence into an - installed-fact theorem; and -* final closure of `CheckerInput.target`. - -Those obligations are intentionally not represented by a Boolean labelled -“checked” here. The next Mathlib vertical should instantiate this protocol -with the existing fixed centered example, while leaving its `Center.Prim` and -`EqRecipe` local rather than promoting either to a central function language. +* resource envelopes for trace sizes and theorem-schema decoding work; +* exact reconstruction of instance substitutions, products, and equality + ownership, plus per-event program-snapshot linkage, from proposed recipes + instead of accepting those fields only after their package schema has + checked them; +* contradiction certificates and branch/split composition; and +* a frontend quotation format which emits the transparent `Trace` value from + an opaque, untrusted search run. + +The next Mathlib vertical should instantiate this protocol with the centered +example while leaving its function language and equality recipes local rather +than promoting either to a central engine enumeration. -/ end Hex.Interval.Experiment.SemanticReplay diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 33d48fe90..9e079be2f 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1060,25 +1060,51 @@ Package caches may record the failed attempt because they remain non-semantic. The format API validates representation shape only; it does not itself attest that a body proves the proposed interval fact, instance, or equality. The cache-free semantic replay protocol separately assembles theorem schemas -package-for-package against one sealed executable registry. Its constructor is -private, and its checked builder requires exact bidirectional coverage between -fact schemas and executable fact formats on the complete +package-for-package. Its sealed search-paired registry requires exact +bidirectional coverage for all three roles on the complete `(RuleKey, role, schema)` key. Thus a checker from another package cannot be -selected merely because two rules reuse a numeric schema. Instance and -equality formats are reported explicitly as deferred rather than silently -treated as checked. - -A Mathlib companion must instantiate those abstract schemas, decode each -frozen entry independently of package cache state, and recheck the -corresponding rule theorem. It remains an explicit compatibility -obligation—not a property enforced by the representation validator—that a -different callback implementation under an existing versioned rule schema -leave every retained payload semantically replayable. Whether production -retains these existential snapshots, compiles a dispatch table, adds typed -decoders, supports hot replacement, or uses another lookup structure remains -experimental. The older direct registry and engine interfaces remain -available for search experiments, but proof-producing execution goes through -the session. +selected merely because two rules reuse a numeric schema. Fact schemas prove +the proposed fact from the exact watched versions; instance schemas prove that +the admitted program extension is semantically conservative; equality schemas +prove semantic equality of the exact admitted endpoints. + +Kernel replay does not trust or unfold the opaque compiled search session. +The tactic must quote an explicit trace containing chronological program +snapshots, instance events, equality edges, fact events, and the frozen arena. +A transparent `KernelRegistry` is checked directly against the immutable +executable package declarations. Its constructor is intentionally not a +soundness boundary: even a forged table cannot manufacture `Evidence`, because +each existential schema must return a proof whose dependent type contains the +exact decoded context. The transparent forward checker verifies base/final +program binding, prefix extensions, every instance and equality payload, +fact-version and previous-link chronology, action inputs from the already +proved prefix, package rule entailment, fact-domain meet evidence, equality +transport, and a domain-owned implication from the strongest installed fact +to the possibly weaker requested target. + +The implemented Mathlib conformance vertical recognizes `x * (1 - x)`, +instantiates the package-local auxiliary function +`x ↦ 1/4 - (x - 1/2)^2`, admits a package-owned equality, propagates +`[0, 1/4]`, transports it to the original product, and kernel-checks the final +upper bound. A separate compiled guard checks that the private policy session +currently emits the quoted trace; this reachability test is not used as the +mathematical proof. The instance schema's conservative-extension witness then +lifts the result from the checked extended program back to every valuation of +the caller's original four-node program. + +This remains an experiment rather than the production checker. Trace-size and +decoder-work envelopes, exact generic reconstruction of instance +substitutions/products and per-event program-snapshot linkage, contradiction +certificates, split-tree composition, and the tactic quotation format are +still open. It is also an explicit +compatibility obligation—not a property enforced by the representation +validator—that a different callback implementation under an existing +versioned rule schema leave every retained payload semantically replayable. +Whether production retains existential snapshots, compiles a dispatch table, +adds typed decoders, supports hot replacement, or uses another lookup +structure remains experimental. The older direct registry and engine +interfaces remain available for search experiments, but proof-producing +execution goes through a session and transparent replay. `PolicySession.Session` is the corresponding proof-producing policy canary. Its checked start stores one bundle containing the engine, policy, and arena @@ -1315,8 +1341,10 @@ Each frozen entry stores its originating action, semantic role, numeric payload schema, and uninterpreted `List Nat` body. It derives the rule owner only from `origin.key`, avoiding two stored identities which could disagree. The session now performs package-owned format lookup and bounded body-shape -validation under the full `(RuleKey, role, schema)` key. Typed decoding, typed -atom encodings, byte limits, and semantic replay are still missing. +validation under the full `(RuleKey, role, schema)` key. The transparent +semantic-replay experiment decodes all three roles and returns kernel proof +terms, but production typed atom encodings, byte limits, trace resource +envelopes, and tactic quotation are still missing. The first real dyadic packages declare payload schema `0` separately for each fact, instance, or equality handler. Each body validator accepts exactly the empty list and rejects every trailing cell; the rule key still distinguishes diff --git a/conformance/HexInterval/PropagatorE2EConformance.lean b/conformance/HexInterval/PropagatorE2EConformance.lean new file mode 100644 index 000000000..e2c4a8296 --- /dev/null +++ b/conformance/HexInterval/PropagatorE2EConformance.lean @@ -0,0 +1,753 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +import HexInterval.Experiment.PolicySession +import HexInterval.Experiment.SemanticReplay +import Mathlib.Data.Real.Basic +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Ring + +/-! +# Arbitrary propagator end-to-end proof canary + +A package recognizes `x * (1 - x)`, instantiates the opaque auxiliary function +`x ↦ 1/4 - (x - 1/2)^2`, admits the package-owned equality between those +expressions, propagates `[0, 1/4]` through the auxiliary node, and transports +that bound back to the original product. + +The policy-session guard exercises compiled search and checks that it emitted +the quoted trace below. The theorem at the end does not trust that search +run: ordinary kernel reduction replays the explicit trace through exact +fact/instance/equality schemas and produces a proof of the final real bound. +The generic engine and replay loop contain no branch for multiplication, +centering, real arithmetic, or these operation keys. +-/ + +namespace Hex.Interval.PropagatorE2EConformance + +open Experiment Propagator PayloadArena PolicySession SemanticReplay + +noncomputable section + +/-! ## Package-local expression language and fact domain -/ + +def real : DomainId := { index := 0 } + +def sourceKey : OpKey := { name := "e2e.source" } +def oneKey : OpKey := { name := "e2e.one" } +def subKey : OpKey := { name := "e2e.sub" } +def mulKey : OpKey := { name := "e2e.mul" } +def centeredKey : OpKey := { name := "e2e.centered-product" } + +def centeredForwardKey : RuleKey := { name := "e2e.centered.forward" } +def centeredInstantiateKey : RuleKey := { name := "e2e.centered.instantiate" } + +def operations : Array Operation := + #[{ key := sourceKey, inputs := [], output := real }, + { key := oneKey, inputs := [], output := real }, + { key := subKey, inputs := [real, real], output := real }, + { key := mulKey, inputs := [real, real], output := real }, + { key := centeredKey, inputs := [real], output := real }] + +def node (index : Nat) : NodeId := { index } + +def instruction (operation : Nat) (args : List NodeId := []) : Node := + { domain := real, op := { index := operation }, args } + +def baseProgram : Program := + { operations + nodes := + #[instruction 0, + instruction 1, + instruction 2 [node 1, node 0], + instruction 3 [node 0, node 2]] } + +def extendedProgram : Program := + { baseProgram with + nodes := baseProgram.nodes.push (instruction 4 [node 0]) } + +inductive Fact where + | top + | unit + | quarter + | upperQuarter + deriving DecidableEq, Repr + +namespace Fact + +def Allows : Fact -> ℝ -> Prop + | .top, _ => True + | .unit, value => 0 ≤ value ∧ value ≤ 1 + | .quarter, value => 0 ≤ value ∧ value ≤ (1 : ℝ) / 4 + | .upperQuarter, value => value ≤ (1 : ℝ) / 4 + +end Fact + +def narrow : Fact -> Fact -> NarrowResult Fact + | current, proposed => + if current == proposed then + .noChange + else + match current, proposed with + | .top, fact => .improved fact + | _, .top => .noChange + | .quarter, .upperQuarter => .noChange + | .upperQuarter, .quarter => .improved .quarter + | _, _ => .malformed 1 + +def searchDomain : Propagator.FactDomain Fact := + { top := fun _ => .top + narrow := fun _ => narrow } + +/-! ## Function-specific executable package -/ + +def centeredForward : Registration := + { key := centeredForwardKey + head := centeredKey + kind := .forward + watches := [.argument 0] + writes := [.result] } + +def centeredInstantiate : Registration := + { key := centeredInstantiateKey + head := mulKey + kind := .instantiate + watches := [] + writes := [] + watchesProgram := true } + +def factLabel : PayloadId := { index := 0 } +def instanceLabel : PayloadId := { index := 0 } +def equalityLabel : PayloadId := { index := 1 } + +def emptyFormat (role : Role) : ReplayFormat := + { role + schema := 0 + validateBody := fun body => body.isEmpty } + +def recognizesCentered (request : RuleRequest Fact) : Bool := + request.program.programVersion == request.action.programVersion && + request.program.operationKey? request.action.node == some mulKey && + match request.program.node? request.action.node with + | some product => + product.args == [node 0, node 2] && + request.program.operationKey? (node 2) == some subKey && + match request.program.node? (node 2) with + | some gap => + gap.args == [node 1, node 0] && + request.program.operationKey? (node 1) == some oneKey + | none => false + | none => false + +def invokeInstantiate (request : RuleRequest Fact) : Plan Fact := + if recognizesCentered request then + { outcome := + .success [] + [.instantiate + { key := 1 + triggers := [node 3, node 0, node 2, node 1] + claimedGeneration := 1 + nodes := + [{ domain := real + op := { index := 4 } + args := [.existing (node 0)] }] + equalities := + [{ left := .existing (node 3) + right := .proposed 0 + payload := equalityLabel }] + payload := instanceLabel }] + { visitedEntries := 9, estimatedProofNodes := 1 } + drafts := + [{ label := instanceLabel, role := .instance, schema := 0, body := [] }, + { label := equalityLabel, role := .equality, schema := 0, body := [] }] } + else + { outcome := .inapplicable, drafts := [] } + +def invokeForward (request : RuleRequest Fact) : Plan Fact := + match request.inputs, request.writes with + | [{ node := input, fact := .unit, .. }], [target] => + if input == node 0 && target == node 4 then + { outcome := + .success + [{ node := target, fact := .quarter, payload := factLabel }] + [] { arithmeticWork := 1, estimatedProofNodes := 1 } + drafts := + [{ label := factLabel, role := .fact, schema := 0, body := [] }] } + else + { outcome := .failed 2, drafts := [] } + | _, _ => { outcome := .inapplicable, drafts := [] } + +def runtimePackage : Propagator.Package Fact := + { Cache := Unit + cache := () + operations + handlers := + #[Handler.statelessPlanned centeredForward invokeForward + #[emptyFormat .fact], + Handler.statelessPlanned centeredInstantiate invokeInstantiate + #[emptyFormat .instance, emptyFormat .equality]] } + +def runtimePackages : Array (Propagator.Package Fact) := #[runtimePackage] + +/-! ## Opaque search run and quoted trace -/ + +def endpointLimit : EndpointLimit := + { maxEndpointHeight := 8, maxAlignmentShift := 8 } + +def engineLimits : Propagator.Limits := + { maxOperations := 5 + maxNodes := 5 + maxRules := 2 + maxRegistryEntries := 16 + maxReplayFormats := 3 + maxArity := 2 + maxApplications := 2 + maxQueueEntries := 16 + maxActions := 8 + maxAcceptedFacts := 4 + maxRetainedSuggestions := 2 + maxEffort := 0 + maxObservationValue := 16 + maxDiagnosticValue := 16 + maxOutcomeCandidates := 1 + maxOutcomeSuggestions := 1 + maxProposalItems := 5 + maxInstances := 1 + maxGeneration := 1 + maxEqualities := 1 + splitEndpointLimit := endpointLimit } + +def policyLimits : Propagator.Policy.Limits := + { maxDecisions := 8 + maxTraversal := 256 + maxLiveOffers := 16 } + +def arenaLimits : PayloadArena.Limits := + { maxEntries := 3 + maxBodyCells := 0 + maxAtom := 0 + maxSchema := 0 + maxUses := 7 } + +def limits : PolicySession.Limits := + { engine := engineLimits, policy := policyLimits, arena := arenaLimits } + +def start? : Option (PolicySession.Session Fact) := + match PolicySession.Session.start searchDomain baseProgram runtimePackages + #[.unit, .top, .top, .top] limits with + | .ok session => some session + | .error _ => none + +inductive Command where + | invoke (key : RuleKey) + | instantiate + | equality + +def commandMatches : Command -> Propagator.Policy.OfferView -> Bool + | .invoke key, { key := .invoke source, .. } => source.rule == key + | .instantiate, { key := .instantiate source _, .. } => + source.rule == centeredInstantiateKey + | .equality, { key := .equality _, .. } => true + | _, _ => false + +def selection? (session : PolicySession.Session Fact) (command : Command) : + Option (Propagator.Policy.Selection × PolicySession.Session Fact) := + match session.view with + | .ready view viewed => + match view.offers.toList.find? (commandMatches command) with + | none => none + | some offer => + some + ({ scope := view.scope + serial := view.serial + programVersion := view.programVersion + id := offer.id + expected := offer.key }, + viewed) + | .resource _ _ | .contradiction _ | .invalidSession _ => none + +def execute? (session : PolicySession.Session Fact) (command : Command) : + Option (PolicySession.Session Fact) := do + let (selection, viewed) ← selection? session command + match command, viewed.choose (.select selection) with + | .invoke _, .rule _ _ next => some next + | .instantiate, .instance _ (.instanceAdmitted [fresh]) next => + if fresh == node 4 then some next else none + | .equality, .equality _ observation next => + if observation.outcome == .improved then some next else none + | _, _ => none + +def searchResult? : Option (PolicySession.Session Fact) := do + let start ← start? + let afterDiscovery ← execute? start (.invoke centeredInstantiateKey) + let afterInstance ← execute? afterDiscovery .instantiate + let afterForward ← execute? afterInstance (.invoke centeredForwardKey) + execute? afterForward .equality + +def instantiateAction : Action := + { serial := 0 + programVersion := 0 + application := { index := 0 } + rule := { index := 1 } + key := centeredInstantiateKey + node := node 3 + kind := .instantiate + effort := 0 + inputs := [] } + +def forwardAction : Action := + { serial := 1 + programVersion := 1 + application := { index := 1 } + rule := { index := 0 } + key := centeredForwardKey + node := node 4 + kind := .forward + effort := 0 + inputs := [{ node := node 0, version := 0 }] } + +def instanceEvent : InstanceEvent := + { programVersion := 1 + origin := instantiateAction + family := 1 + substitution := [node 3] + products := [node 4] + newNodes := [node 4] + generation := 1 + equalities := [{ index := 0 }] + payload := { index := 0 } } + +def equalityEdge : EqualityEdge := + { left := node 3 + right := node 4 + generation := 1 + origin := instantiateAction + payload := { index := 1 } } + +def forwardEvent : FactEvent Fact := + { programVersion := 1 + node := node 4 + previous := { node := node 4, version := 0 } + fact := .quarter + version := 1 + cause := .rule forwardAction .quarter { index := 2 } } + +def transportEvent : FactEvent Fact := + { programVersion := 1 + node := node 3 + previous := { node := node 3, version := 0 } + fact := .quarter + version := 1 + cause := .transport { index := 0 } { node := node 4, version := 1 } } + +def instanceEntry : Entry := + { origin := instantiateAction, role := .instance, schema := 0, body := [] } + +def equalityEntry : Entry := + { origin := instantiateAction, role := .equality, schema := 0, body := [] } + +def factEntry : Entry := + { origin := forwardAction, role := .fact, schema := 0, body := [] } + +def quotedArena : Arena := + { entries := #[instanceEntry, equalityEntry, factEntry] + bodyCells := 0 } + +def quotedTrace : Trace Fact := + { program := extendedProgram + programs := #[baseProgram, extendedProgram] + instances := #[instanceEvent] + equalities := #[equalityEdge] + events := #[forwardEvent, transportEvent] + arena := quotedArena } + +def wrongRoleTrace : Trace Fact := + { quotedTrace with + arena := + { entries := + #[instanceEntry, { equalityEntry with role := .fact }, factEntry] + bodyCells := 0 } } + +def wrongKeyTrace : Trace Fact := + { quotedTrace with + arena := + { entries := + #[instanceEntry, { equalityEntry with schema := 1 }, factEntry] + bodyCells := 0 } } + +def futureAction : Action := + { forwardAction with + inputs := [{ node := node 4, version := 1 }] } + +def futureEvent : FactEvent Fact := + { forwardEvent with + cause := .rule futureAction .quarter { index := 2 } } + +def futureTrace : Trace Fact := + { quotedTrace with + events := #[futureEvent, transportEvent] + arena := + { entries := + #[instanceEntry, equalityEntry, { factEntry with origin := futureAction }] + bodyCells := 0 } } + +def forgedMeetEvent : FactEvent Fact := + { forwardEvent with fact := .upperQuarter } + +def forgedMeetTrace : Trace Fact := + { quotedTrace with events := #[forgedMeetEvent, transportEvent] } + +-- Compiled search is only an untrusted trace producer. This guard confirms +-- the current policy route emits the separately quoted certificate. +#guard + match searchResult? with + | none => false + | some session => + session.state.engine.program == quotedTrace.program && + session.state.engine.instanceHistory == quotedTrace.instances && + session.state.engine.equalities == quotedTrace.equalities && + session.state.engine.history == quotedTrace.events && + session.arena == quotedTrace.arena + +/-! ## Package-owned mathematical semantics -/ + +def centeredValue (x : ℝ) : ℝ := + (1 : ℝ) / 4 - (x - (1 : ℝ) / 2) ^ 2 + +def BaseEquations (valuation : NodeId -> ℝ) : Prop := + valuation (node 1) = 1 ∧ + valuation (node 2) = valuation (node 1) - valuation (node 0) ∧ + valuation (node 3) = valuation (node 0) * valuation (node 2) + +def ExtendedEquations (valuation : NodeId -> ℝ) : Prop := + BaseEquations valuation ∧ + valuation (node 4) = centeredValue (valuation (node 0)) + +def Models (program : Program) (valuation : NodeId -> ℝ) : Prop := + (program = baseProgram ∧ BaseEquations valuation) ∨ + (program = extendedProgram ∧ ExtendedEquations valuation) + +def semantics : Semantics Fact := + { Value := ℝ + models := Models + holds := fun _ valuation fact => fact.fact.Allows (valuation fact.node) + transport := by + intro _ valuation left right fact equal holds + change fact.Allows (valuation right) + rw [← equal] + exact holds } + +theorem base_ne_extended : baseProgram ≠ extendedProgram := by + decide + +theorem modelsBase (valuation : NodeId -> ℝ) : + Models baseProgram valuation -> BaseEquations valuation := by + intro model + rcases model with ⟨_, equations⟩ | ⟨equal, _⟩ + · exact equations + · exact False.elim (base_ne_extended equal) + +theorem modelsExtended (valuation : NodeId -> ℝ) : + Models extendedProgram valuation -> ExtendedEquations valuation := by + intro model + rcases model with ⟨equal, _⟩ | ⟨_, equations⟩ + · exact False.elim (base_ne_extended equal.symm) + · exact equations + +theorem centeredExtends : semantics.Extends baseProgram extendedProgram := by + intro valuation model + let extended : NodeId -> ℝ := + fun current => + if current = node 4 then centeredValue (valuation (node 0)) + else valuation current + refine ⟨extended, ?_, ?_⟩ + · right + refine ⟨rfl, ?_⟩ + constructor + · rcases modelsBase valuation model with ⟨one, gap, product⟩ + constructor + · simpa [extended, node] using one + constructor + · simpa [extended, node] using gap + · simpa [extended, node] using product + · simp [extended, node] + · intro current before + have different : current ≠ node 4 := by + intro equal + subst current + simp [baseProgram, node] at before + simp [extended, different] + +theorem centeredIdentity (valuation : NodeId -> ℝ) + (equations : ExtendedEquations valuation) : + valuation (node 3) = valuation (node 4) := by + rcases equations with ⟨⟨one, gap, product⟩, centered⟩ + rw [product, gap, one, centered] + simp only [centeredValue] + ring + +theorem centeredBounds (x : ℝ) (bounds : 0 ≤ x ∧ x ≤ 1) : + Fact.quarter.Allows (centeredValue x) := by + constructor + · have product : 0 ≤ x * (1 - x) := + mul_nonneg bounds.1 (sub_nonneg.mpr bounds.2) + have identity : centeredValue x = x * (1 - x) := by + simp only [centeredValue] + ring + rw [identity] + exact product + · have square : 0 ≤ (x - (1 : ℝ) / 2) ^ 2 := sq_nonneg _ + simp only [centeredValue] + linarith + +theorem forwardEntails : + semantics.Entails extendedProgram + [{ node := node 0, fact := .unit }] + { node := node 4, fact := .quarter } := by + intro valuation model assumptions + have input := + assumptions { node := node 0, fact := .unit } (List.Mem.head _) + change Fact.unit.Allows (valuation (node 0)) at input + change Fact.quarter.Allows (valuation (node 4)) + rw [(modelsExtended valuation model).2] + exact centeredBounds _ input + +inductive UnitCertificate where + | unit + +def decodeUnit : List Nat -> Option UnitCertificate + | [] => some .unit + | _ :: _ => none + +def factSchema : PackedFactSchema semantics := + { rule := centeredForwardKey + schema := 0 + Certificate := UnitCertificate + decode := decodeUnit + replay := fun _ action context _ => + if actionProof : action = forwardAction then + if programProof : context.program = extendedProgram then + if assumptionsProof : + context.assumptions = [{ node := node 0, fact := .unit }] then + if proposedProof : + context.proposed = { node := node 4, fact := .quarter } then + some + { proof := by + rw [programProof, assumptionsProof, proposedProof] + exact forwardEntails } + else none + else none + else none + else none } + +def instanceSchema : PackedInstanceSchema semantics := + { rule := centeredInstantiateKey + schema := 0 + Certificate := UnitCertificate + decode := decodeUnit + replay := fun _ action context _ => + if actionProof : action = instantiateAction then + if beforeProof : context.before = baseProgram then + if afterProof : context.after = extendedProgram then + if eventProof : context.event = instanceEvent then + some + { proof := by + rw [beforeProof, afterProof] + exact centeredExtends } + else none + else none + else none + else none } + +def equalitySchema : PackedEqualitySchema semantics := + { rule := centeredInstantiateKey + schema := 0 + Certificate := UnitCertificate + decode := decodeUnit + replay := fun _ action context _ => + if actionProof : action = instantiateAction then + if programProof : context.program = extendedProgram then + if edgeProof : context.edge = equalityEdge then + some + { proof := by + rw [programProof, edgeProof] + intro valuation model + exact centeredIdentity valuation (modelsExtended valuation model) } + else none + else none + else none } + +def semanticPackage : SemanticReplay.Package semantics := + { factSchemas := #[factSchema] + instanceSchemas := #[instanceSchema] + equalitySchemas := #[equalitySchema] } + +def semanticPackages : Array (SemanticReplay.Package semantics) := + #[semanticPackage] + +def meetEvidence (previous proposed installed : Fact) : + Option (Evidence + (∀ value : ℝ, installed.Allows value ↔ + previous.Allows value ∧ proposed.Allows value)) := + match previous, proposed, installed with + | .top, fact, actual => + if equal : actual = fact then + some + { proof := by + subst actual + intro + simp [Fact.Allows] } + else none + | fact, .top, actual => + if equal : actual = fact then + some + { proof := by + subst actual + intro + simp [Fact.Allows] } + else none + | .quarter, .upperQuarter, .quarter => + some + { proof := by + intro + simp only [Fact.Allows] + constructor + · intro bounds + exact ⟨bounds, bounds.2⟩ + · intro bounds + exact bounds.1 } + | .upperQuarter, .quarter, .quarter => + some + { proof := by + intro + simp only [Fact.Allows] + constructor + · intro bounds + exact ⟨bounds.2, bounds⟩ + · intro bounds + exact bounds.2 } + | left, right, actual => + if same : left = right ∧ actual = left then + some + { proof := by + rcases same with ⟨rfl, rfl⟩ + intro + simp } + else none + +def proofDomain : FactDomainSchema semantics := + { top := fun _ => .top + topSound := by + intro _ _ _ _ _ _ + trivial + proveMeet := fun _ node previous proposed installed => do + let evidence ← meetEvidence previous proposed installed + pure + { proof := by + intro valuation _ + exact evidence.proof (valuation node) } + proveImplies := fun _ node stronger requested => + match stronger, requested with + | _, .top => + some + { proof := by + intro _ _ _ + trivial } + | .quarter, .upperQuarter => + some + { proof := by + intro valuation _ stronger + exact stronger.2 } + | left, right => + if equal : left = right then + some + { proof := by + subst right + intro _ _ holds + exact holds } + else none } + +def checkerInput : CheckerInput Fact := + { baseProgram + initialFacts := #[.unit, .top, .top, .top] + target := { node := node 3, fact := .upperQuarter } } + +def acceptsTrace (trace : Trace Fact) : Bool := + match SemanticReplay.Registry.buildPackages runtimePackages semanticPackages with + | .error _ => false + | .ok registry => + (SemanticReplay.check registry proofDomain checkerInput trace).isSome + +def checked? : + Option (Evidence + (semantics.Entails extendedProgram + (initialContext checkerInput) checkerInput.target)) := + match SemanticReplay.Registry.buildPackages runtimePackages semanticPackages with + | .error _ => none + | .ok registry => + SemanticReplay.check registry proofDomain checkerInput quotedTrace + +theorem checked_isSome : checked?.isSome = true := by + decide +kernel + +theorem rejects_wrong_role : acceptsTrace wrongRoleTrace = false := by + decide +kernel + +theorem rejects_wrong_key : acceptsTrace wrongKeyTrace = false := by + decide +kernel + +theorem rejects_future_reference : acceptsTrace futureTrace = false := by + decide +kernel + +theorem rejects_forged_meet : acceptsTrace forgedMeetTrace = false := by + decide +kernel + +/-- The kernel-checked result: for every real valuation satisfying the quoted +expression program, `0 ≤ x ≤ 1` implies `x * (1 - x) ≤ 1/4`. -/ +theorem product_le_quarter : + semantics.Entails extendedProgram + (initialContext checkerInput) checkerInput.target := by + match result : checked? with + | some evidence => exact evidence.proof + | none => + have accepted := checked_isSome + simp [result] at accepted + +/-- The checked extension is conservative, so the result also applies to +every valuation of the original four-node program. -/ +theorem base_product_le_quarter : + semantics.Entails baseProgram + (initialContext checkerInput) checkerInput.target := by + intro valuation model initial + obtain ⟨extended, extendedModel, agreement⟩ := + centeredExtends valuation model + have extendedInitial : + ∀ assumption, assumption ∈ initialContext checkerInput -> + semantics.holds extendedProgram extended assumption := by + intro assumption member + have before : assumption.node.index < baseProgram.nodes.size := by + have listed := member + simp [initialContext, initialContextFrom, checkerInput] at listed + rcases listed with equal | equal | equal | equal + all_goals subst assumption + all_goals decide + have holds := initial assumption member + have equal := agreement assumption.node before + change assumption.fact.Allows (valuation assumption.node) at holds + change assumption.fact.Allows (extended assumption.node) + rw [equal] + exact holds + have result := + product_le_quarter extended extendedModel extendedInitial + have equal := agreement (node 3) (by decide) + change Fact.upperQuarter.Allows (extended (node 3)) at result + change Fact.upperQuarter.Allows (valuation (node 3)) + rw [equal] at result + exact result + +end + +end Hex.Interval.PropagatorE2EConformance diff --git a/conformance/HexInterval/SemanticReplayConformance.lean b/conformance/HexInterval/SemanticReplayConformance.lean index 692fd0315..8adacbbe3 100644 --- a/conformance/HexInterval/SemanticReplayConformance.lean +++ b/conformance/HexInterval/SemanticReplayConformance.lean @@ -46,7 +46,12 @@ def Models (meanings : List UnaryMeaning) (program : Program) def semantics (meanings : List UnaryMeaning) : Semantics Fact := { Value := Nat models := Models meanings - holds := fun _ valuation fact => fact.fact.Allows (valuation fact.node) } + holds := fun _ valuation fact => fact.fact.Allows (valuation fact.node) + transport := by + intro _ valuation left right fact equal holds + change fact.Allows (valuation right) + rw [← equal] + exact holds } def real : DomainId := { index := 0 } def sourceKey : OpKey := { name := "semantic-replay.source" } @@ -156,6 +161,9 @@ inductive LeftCertificate where inductive RightCertificate where | pair +inductive EqualityCertificate where + | unit + def decodeLeft : List Nat -> Option LeftCertificate | [101] => some .unit | _ => none @@ -164,6 +172,10 @@ def decodeRight : List Nat -> Option RightCertificate | [202, 203] => some .pair | _ => none +def decodeEquality : List Nat -> Option EqualityCertificate + | [303] => some .unit + | _ => none + def leftSchema : PackedFactSchema (semantics meanings) := { rule := leftRuleKey schema := 7 @@ -180,15 +192,33 @@ def rightSchema : PackedFactSchema (semantics meanings) := replay := fun input action context _ => replayUnary rightMeaning rightMeaning_mem input action context } +def rightEqualitySchema : PackedEqualitySchema (semantics meanings) := + { rule := rightRuleKey + schema := 8 + Certificate := EqualityCertificate + decode := decodeEquality + replay := fun _ _ context _ => + if endpointProof : context.edge.left = context.edge.right then + some + { proof := by + intro valuation _ + exact congrArg valuation endpointProof } + else + none } + def leftProofs : SemanticReplay.Package (semantics meanings) := { factSchemas := #[leftSchema] } def rightProofs : SemanticReplay.Package (semantics meanings) := - { factSchemas := #[rightSchema] } + { factSchemas := #[rightSchema] + equalitySchemas := #[rightEqualitySchema] } def noProofs : SemanticReplay.Package (semantics meanings) := { factSchemas := #[] } +def rightFactOnlyProofs : SemanticReplay.Package (semantics meanings) := + { factSchemas := #[rightSchema] } + def duplicateLeftProofs : SemanticReplay.Package (semantics meanings) := { factSchemas := #[leftSchema, leftSchema] } @@ -393,7 +423,8 @@ def rightContext (entry : Entry) : RuleFactContext checkerInput entry.origin := (rightContext fixture.rightEntry)).isSome && fixture.registry.coverage.factFormats == #[leftSchema.key, rightSchema.key] && - fixture.registry.coverage.deferredFormats == + fixture.registry.coverage.instanceFormats.isEmpty && + fixture.registry.coverage.equalityFormats == #[rightEqualityFormat.replayKey rightRuleKey] | none => false @@ -418,8 +449,9 @@ def rightContext (entry : Entry) : RuleFactContext checkerInput entry.origin := | _ => false | none => false --- Fact coverage is bidirectional: omitting a checker is a precise assembly --- error, while the equality format remains explicitly deferred. +-- Coverage is bidirectional in every role: omitting the right package loses +-- both its fact and equality checker, with the first missing exact key +-- reported deterministically. #guard match executable? with | some executable => @@ -429,6 +461,19 @@ def rightContext (entry : Entry) : RuleFactContext checkerInput entry.origin := | _ => false | none => false +-- Non-fact coverage is equally exact: supplying the right fact theorem but +-- omitting its declared equality theorem reports that equality replay key. +#guard + match executable? with + | some executable => + match SemanticReplay.Registry.build executable + #[leftProofs, rightFactOnlyProofs] with + | .error (.missingSchema package key) => + package == 1 && + key == rightEqualityFormat.replayKey rightRuleKey + | _ => false + | none => false + -- Package position and the complete replay key prevent a checker contributed -- by the right package from being installed as the left package's schema, -- even though both packages deliberately use fact schema number seven. @@ -451,8 +496,8 @@ def rightContext (entry : Entry) : RuleFactContext checkerInput entry.origin := (rightContext wrong)).isNone | none => false --- Exact dispatch includes the role. The currently deferred equality address --- cannot reach the fact theorem at the same rule. +-- Exact dispatch includes the role. The checked equality address cannot +-- reach the fact theorem at the same rule. #guard match fixture? with | some fixture => @@ -502,7 +547,29 @@ def factDomain : FactDomainSchema (semantics meanings) := some { proof := by intro valuation _ - exact evidence.proof (valuation node) } } + exact evidence.proof (valuation node) } + proveImplies := fun _ node stronger requested => + match stronger, requested with + | _, .top => + some + { proof := by + intro + intro + intro + trivial } + | .top, .exact _ => none + | .exact actual, .exact expected => + if equal : actual = expected then + some + { proof := by + intro valuation + intro + intro holds + change valuation node = expected + change valuation node = actual at holds + simpa [equal] using holds } + else + none } example : (factDomain.proveMeet program (node 1) .top (.exact 4) (.exact 4)).isSome = true := by diff --git a/lakefile.lean b/lakefile.lean index a4ac64c4b..f858f100b 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -302,7 +302,7 @@ lean_lib HexRCFProofProbeScientific where -- `*_emit_fixtures` exes below, carrying `srcDir := "conformance"`. lean_lib HexConformance where srcDir := "conformance" - globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexInterval.Conformance, `HexInterval.CenterConformance, `HexInterval.ScaleConformance, `HexInterval.PropagatorConformance, `HexInterval.StructureViewConformance, `HexInterval.PolicyConformance, `HexInterval.PolicyFrontierConformance, `HexInterval.PolicyDriverConformance, `HexInterval.PackageRegistryConformance, `HexInterval.DyadicIntervalConformance, `HexInterval.DyadicRulesConformance, `HexInterval.PayloadArenaConformance, `HexInterval.PayloadSessionConformance, `HexInterval.PolicySessionConformance, `HexInterval.SemanticReplayConformance, `HexLLL.Conformance, `HexMatrix.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexNumberField.Conformance, `HexNumberFieldTower.Conformance, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRCF.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexResultant.Conformance, `HexRoots.Conformance].map Glob.one + globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexInterval.Conformance, `HexInterval.CenterConformance, `HexInterval.ScaleConformance, `HexInterval.PropagatorConformance, `HexInterval.StructureViewConformance, `HexInterval.PolicyConformance, `HexInterval.PolicyFrontierConformance, `HexInterval.PolicyDriverConformance, `HexInterval.PackageRegistryConformance, `HexInterval.DyadicIntervalConformance, `HexInterval.DyadicRulesConformance, `HexInterval.PayloadArenaConformance, `HexInterval.PayloadSessionConformance, `HexInterval.PolicySessionConformance, `HexInterval.SemanticReplayConformance, `HexInterval.PropagatorE2EConformance, `HexLLL.Conformance, `HexMatrix.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexNumberField.Conformance, `HexNumberFieldTower.Conformance, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRCF.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexResultant.Conformance, `HexRoots.Conformance].map Glob.one -- Public umbrellas intentionally contain only the supported API. Executable -- examples and regression tests are compiled through this separate target so diff --git a/progress/20260729T060457Z.md b/progress/20260729T060457Z.md new file mode 100644 index 000000000..fd4143983 --- /dev/null +++ b/progress/20260729T060457Z.md @@ -0,0 +1,48 @@ +# Arbitrary-propagator semantic replay vertical + +## Accomplished + +- Restacked the semantic-replay experiment onto the private policy-owned + payload session. +- Replaced deferred non-fact coverage with exact package-owned fact, + instantiation, and equality schemas under the full + `(RuleKey, role, schema)` dispatch key. +- Added a transparent kernel replay registry checked directly against immutable + executable package declarations, without making the opaque compiled search + registry a soundness dependency. +- Added transparent chronological replay for quoted program snapshots, + instantiation events, equality edges, frozen payload entries, rule facts, + equality transport, fact-domain meet proofs, and final domain-owned + subsumption. +- Added the decisive real-valued canary: a private policy session recognizes + `x * (1 - x)`, instantiates the package-local centered function, admits its + equality, propagates `[0, 1/4]`, freezes all three evidence roles, and + transports the result to the original product. +- Separated the compiled reachability guard from the mathematical theorem. + Ordinary kernel replay proves the extended-program bound, and the checked + conservative-extension witness proves the corresponding result for every + valuation of the original four-node program. +- Added kernel-reducible rejection tests for a forged meet, a future fact + reference, a wrong payload role, and a wrong replay-key schema. +- Updated the SPEC only for the implemented replay contracts and recorded + remaining production gaps. +- Built `HexIntervalExperiment`, + `HexInterval.PropagatorE2EConformance`, + `HexInterval.SemanticReplayConformance`, and + `HexInterval.PolicySessionConformance`; the conformance target manifest and + banned-token scan are clean. + +## Current frontier + +The generic arbitrary-propagator checker and centered-product theorem are +locally green as one milestone. The implementation does not inspect function +keys or arithmetic facts in the engine or generic replay loop. + +## Next step + +Review and land this milestone on the tightened lower stack, then add the +independent sine-oddness package canary as a separate stacked change. + +## Blockers + +None. From da4e7c9bb46710f42f127752e16f89c85c76a406 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 29 Jul 2026 06:32:30 +0000 Subject: [PATCH 2/6] Lift propagator proofs to the caller program --- HexInterval/Experiment/SemanticReplay.lean | 320 ++++++++++++------ HexInterval/SPEC/hex-interval.md | 36 +- .../HexInterval/PropagatorE2EConformance.lean | 168 +++++---- .../SemanticReplayConformance.lean | 99 ++++-- progress/20260729T063212Z.md | 46 +++ 5 files changed, 475 insertions(+), 194 deletions(-) create mode 100644 progress/20260729T063212Z.md diff --git a/HexInterval/Experiment/SemanticReplay.lean b/HexInterval/Experiment/SemanticReplay.lean index d16f3d7d6..9e747a982 100644 --- a/HexInterval/Experiment/SemanticReplay.lean +++ b/HexInterval/Experiment/SemanticReplay.lean @@ -194,6 +194,22 @@ Returning a proof in `Option` permits a computational companion checker to reject malformed facts. It does not trust the scheduler's `narrow` result. -/ structure FactDomainSchema (semantics : Semantics Fact) where top : DomainId -> Fact + /-- A fact about a modeled old expression node has the same meaning after a + conservative program extension when the extended model agrees at that node. + Function packages may add arbitrary new nodes over the program's declared + operation table; this is the sole generic locality law needed to transport + caller assumptions and the requested result across those additions. -/ + holdsPrefix : + ∀ (before after : Program) + (valuation extended : NodeId -> semantics.Value) + (fact : NodeFact Fact), + ProgramPrefix before after -> + semantics.models before valuation -> + semantics.models after extended -> + fact.node.index < before.nodes.size -> + extended fact.node = valuation fact.node -> + (semantics.holds before valuation fact ↔ + semantics.holds after extended fact) topSound : ∀ (program : Program) (valuation : NodeId -> semantics.Value) (node : NodeId) (instruction : Node), @@ -646,50 +662,6 @@ structure Trace (Fact : Type) where events : Array (FactEvent Fact) arena : Arena -namespace Trace - -/-- Read an event only when its index is strictly before the replay cursor. -Even if the untrusted array contains a future entry, it is inaccessible. -/ -def eventAt? (trace : Trace Fact) (cursor index : Nat) : Option (FactEvent Fact) := - if index < cursor then trace.events[index]? else none - -def findVersionPrefix? (events : Array (FactEvent Fact)) (seen : SeenVersion) : - Nat -> Nat -> Option Fact - | 0, _ => none - | cursor + 1, index => - match events[index]? with - | none => none - | some event => - if event.node == seen.node && event.version == seen.version then - some event.fact - else - findVersionPrefix? events seen cursor (index + 1) - -/-- Resolve a positive fact version from a bounded event prefix. This helper -never falls back to the engine's mutable current fact slot. -/ -def eventFactAt? (trace : Trace Fact) (cursor : Nat) - (seen : SeenVersion) : Option Fact := - if seen.version == 0 then none - else findVersionPrefix? trace.events seen cursor 0 - -/-- Resolve a fact exactly as replay will: base version zero comes from the -caller's immutable initial facts, generated version zero is semantic top, and -positive versions can inspect only the already-checked event prefix. -/ -def factAt? {Fact : Type} {semantics : Semantics Fact} - (domain : FactDomainSchema semantics) - (input : CheckerInput Fact) (trace : Trace Fact) - (cursor : Nat) (seen : SeenVersion) : Option Fact := - if seen.version == 0 then - if seen.node.index < input.baseProgram.nodes.size then - input.initialFacts[seen.node.index]? - else do - let instruction ← trace.program.node? seen.node - pure (domain.top instruction.domain) - else - trace.eventFactAt? cursor seen - -end Trace - /-! ## Transparent chronological trace checker -/ /-- Caller-owned version-zero assumptions, in exact base-node order. -/ @@ -701,6 +673,20 @@ def initialContextFrom (index : Nat) : List Fact -> List (NodeFact Fact) def initialContext (input : CheckerInput Fact) : List (NodeFact Fact) := initialContextFrom 0 input.initialFacts.toList +theorem initialContextFrom_node_lt (facts : List Fact) (index : Nat) + (nodeFact : NodeFact Fact) + (member : nodeFact ∈ initialContextFrom index facts) : + nodeFact.node.index < index + facts.length := by + induction facts generalizing index with + | nil => simp [initialContextFrom] at member + | cons fact facts induction => + simp only [initialContextFrom, List.mem_cons] at member + rcases member with equal | member + · subst nodeFact + simp + · have later := induction (index := index + 1) member + simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using later + /-- A list member carrying its membership proof in `Type`. -/ structure Member (items : List α) where value : α @@ -766,6 +752,53 @@ structure ProvenEquality (semantics : Semantics Fact) (program : Program) where evidence : Evidence (semantics.Equivalent program edge.left edge.right) +/-- One package-checked conservative extension step. Keeping the semantic +evidence is essential: structural prefix checks alone do not show that a +valuation of the caller's expression graph extends to the added nodes. -/ +structure ProvenExtension (semantics : Semantics Fact) where + before : Program + after : Program + programPrefix : ProgramPrefix before after + evidence : Evidence (semantics.Extends before after) + +namespace ProgramPrefix + +theorem nodeSize_le (programPrefix : ProgramPrefix before after) : + before.nodes.size ≤ after.nodes.size := by + rcases programPrefix.nodeSuffix with ⟨suffix, equal⟩ + have lengths := congrArg List.length equal + simp only [Array.length_toList, List.length_append] at lengths + rw [lengths] + exact Nat.le_add_right _ _ + +end ProgramPrefix + +namespace Semantics + +theorem extendsRefl (semantics : Semantics Fact) (program : Program) : + semantics.Extends program program := by + intro valuation model + exact ⟨valuation, model, fun _ _ => rfl⟩ + +theorem extendsTrans (semantics : Semantics Fact) + (programPrefix : ProgramPrefix before middle) + (first : Evidence (semantics.Extends before middle)) + (second : Evidence (semantics.Extends middle after)) : + semantics.Extends before after := by + intro valuation model + obtain ⟨middleValuation, middleModel, agreesFirst⟩ := + first.proof valuation model + obtain ⟨extended, extendedModel, agreesSecond⟩ := + second.proof middleValuation middleModel + refine ⟨extended, extendedModel, ?_⟩ + intro node oldNode + calc + extended node = middleValuation node := + agreesSecond node (Nat.lt_of_lt_of_le oldNode programPrefix.nodeSize_le) + _ = valuation node := agreesFirst node oldNode + +end Semantics + def expectedNewNodes (before after : Program) : List NodeId := (List.range (after.nodes.size - before.nodes.size)).map (fun offset => { index := before.nodes.size + offset }) @@ -778,8 +811,8 @@ def instanceEqualitiesValid (equalities : Array EqualityEdge) def replayInstances {Fact : Type} {semantics : Semantics Fact} (registry : KernelRegistry semantics) (input : CheckerInput Fact) (trace : Trace Fact) (index : Nat) : - List InstanceEvent -> Option PUnit - | [] => some ⟨⟩ + List InstanceEvent -> Option (List (ProvenExtension semantics)) + | [] => some [] | event :: events => do let before ← trace.programs[index]? let after ← trace.programs[index + 1]? @@ -799,9 +832,45 @@ def replayInstances {Fact : Type} {semantics : Semantics Fact} after basePrefix := basePrefix.proof event } - let _ ← registry.dispatchInstance input entry context - let _ := stepPrefix - replayInstances registry input trace (index + 1) events + let evidence ← registry.dispatchInstance input entry context + let rest ← replayInstances registry input trace (index + 1) events + pure + ({ before + after + programPrefix := stepPrefix.proof + evidence } :: rest) + +/-- Compose a checked chronological list of package-owned extension steps. +The endpoint comparisons are transparent checks over untrusted trace data; +the semantic result is built only from the proofs returned by the packages. -/ +def composeExtensions {Fact : Type} {semantics : Semantics Fact} + (base final : Program) : + List (ProvenExtension semantics) -> + Option (Evidence (semantics.Extends base final)) + | [] => + if equal : base = final then + some + { proof := by + subst final + exact semantics.extendsRefl base } + else + none + | step :: steps => + if starts : step.before = base then + match composeExtensions step.after final steps with + | none => none + | some rest => + let programPrefix : ProgramPrefix base step.after := by + rw [← starts] + exact step.programPrefix + let first : Evidence (semantics.Extends base step.after) := + { proof := by + rw [← starts] + exact step.evidence.proof } + some + { proof := semantics.extendsTrans programPrefix first rest } + else + none def equalityOwned (instances : Array InstanceEvent) (id : EqualityId) (edge : EqualityEdge) : Bool := @@ -832,7 +901,8 @@ def replayStructure {Fact : Type} {semantics : Semantics Fact} (registry : KernelRegistry semantics) (input : CheckerInput Fact) (trace : Trace Fact) : Option - (Evidence (ProgramPrefix input.baseProgram trace.program) × + (Evidence (semantics.Extends input.baseProgram trace.program) × + Evidence (ProgramPrefix input.baseProgram trace.program) × Array (ProvenEquality semantics trace.program)) := do if trace.programs.size != trace.instances.size + 1 || trace.programs[0]? != some input.baseProgram || @@ -840,10 +910,11 @@ def replayStructure {Fact : Type} {semantics : Semantics Fact} none else let finalPrefix ← ProgramPrefix.check? input.baseProgram trace.program - let _ ← replayInstances registry input trace 0 trace.instances.toList + let steps ← replayInstances registry input trace 0 trace.instances.toList + let extension ← composeExtensions input.baseProgram trace.program steps let equalities ← replayEqualities registry input trace finalPrefix.proof 0 trace.equalities.toList - pure (finalPrefix, equalities) + pure (extension, finalPrefix, equalities) def resolveFact {Fact : Type} {semantics : Semantics Fact} (domain : FactDomainSchema semantics) (input : CheckerInput Fact) @@ -1034,62 +1105,109 @@ def replayEvents {Fact : Type} {semantics : Semantics Fact} replayEvents registry domain input trace basePrefix assumptions equalities events (installed :: proven) +/-- Replay fact and equality events after the structural pass has established +the final program prefix and all package-owned equality theorems. -/ +def replayFinal {Fact : Type} {semantics : Semantics Fact} + (registry : KernelRegistry semantics) (domain : FactDomainSchema semantics) + (input : CheckerInput Fact) (trace : Trace Fact) + (basePrefix : ProgramPrefix input.baseProgram trace.program) + (equalities : Array (ProvenEquality semantics trace.program)) : + Option (Evidence + (semantics.Entails trace.program (initialContext input) input.target)) := do + let assumptions := initialContext input + let proven ← replayEvents registry domain input trace basePrefix assumptions + equalities trace.events.toList [] + match proven.find? (fun fact => fact.nodeFact.node == input.target.node) with + | none => + match findNodeMember? input.target.node assumptions with + | some member => + if targetNode : member.value.node = input.target.node then + let implication ← domain.proveImplies trace.program input.target.node + member.value.fact input.target.fact + some + { proof := by + intro valuation model initial + have stronger : + semantics.holds trace.program valuation + { node := input.target.node, fact := member.value.fact } := by + have factEq : member.value = + { node := input.target.node, fact := member.value.fact } := by + exact NodeFact.extensionality _ _ targetNode rfl + rw [← factEq] + exact initial member.value member.proof + exact implication.proof valuation model stronger } + else + none + | none => none + | some target => + if targetNode : target.nodeFact.node = input.target.node then + let implication ← domain.proveImplies trace.program input.target.node + target.nodeFact.fact input.target.fact + some + { proof := by + intro valuation model initial + have stronger : + semantics.holds trace.program valuation + { node := input.target.node, fact := target.nodeFact.fact } := by + have factEq : target.nodeFact = + { node := input.target.node, fact := target.nodeFact.fact } := by + exact NodeFact.extensionality _ _ targetNode rfl + rw [← factEq] + exact target.evidence.proof valuation model initial + exact implication.proof valuation model stronger } + else + none + /-- Transparently replay an explicit, untrusted trace. Search may run through opaque compiled session operations, but soundness depends only on this kernel-reducible pass and the proof terms returned by package-owned schemas. -The result certifies the requested bound under the complete checked program -from the caller's exact version-zero assumptions. -/ -def check {Fact : Type} [DecidableEq Fact] {semantics : Semantics Fact} +Unlike an extended-program-only checker, the result is a theorem about the +caller's original expression graph. The checker composes every package-owned +`Extends` proof, transports the caller's initial facts to the final graph, +replays the trace there, and transports the requested old-node fact back. -/ +def check {Fact : Type} {semantics : Semantics Fact} (registry : KernelRegistry semantics) (domain : FactDomainSchema semantics) (input : CheckerInput Fact) (trace : Trace Fact) : Option (Evidence - (semantics.Entails trace.program (initialContext input) input.target)) := do - if input.initialFacts.size != input.baseProgram.nodes.size then none else - let (basePrefix, equalities) ← replayStructure registry input trace - let assumptions := initialContext input - let proven ← replayEvents registry domain input trace basePrefix.proof assumptions - equalities trace.events.toList [] - match proven.find? (fun fact => fact.nodeFact.node == input.target.node) with - | none => - match findNodeMember? input.target.node assumptions with - | some member => - if targetNode : member.value.node = input.target.node then - let implication ← domain.proveImplies trace.program input.target.node - member.value.fact input.target.fact - some - { proof := by - intro valuation model initial - have stronger : - semantics.holds trace.program valuation - { node := input.target.node, fact := member.value.fact } := by - have factEq : member.value = - { node := input.target.node, fact := member.value.fact } := by - exact NodeFact.extensionality _ _ targetNode rfl - rw [← factEq] - exact initial member.value member.proof - exact implication.proof valuation model stronger } - else - none - | none => none - | some target => - if targetNode : target.nodeFact.node = input.target.node then - let implication ← domain.proveImplies trace.program input.target.node - target.nodeFact.fact input.target.fact - some - { proof := by - intro valuation model initial - have stronger : - semantics.holds trace.program valuation - { node := input.target.node, fact := target.nodeFact.fact } := by - have factEq : target.nodeFact = - { node := input.target.node, fact := target.nodeFact.fact } := by - exact NodeFact.extensionality _ _ targetNode rfl - rw [← factEq] - exact target.evidence.proof valuation model initial - exact implication.proof valuation model stronger } - else - none + (semantics.Entails input.baseProgram (initialContext input) input.target)) := do + if sizeEqual : input.initialFacts.size = input.baseProgram.nodes.size then + if targetOld : input.target.node.index < input.baseProgram.nodes.size then + let (extension, basePrefix, equalities) ← replayStructure registry input trace + let final ← replayFinal registry domain input trace basePrefix.proof equalities + some + { proof := by + intro valuation model initial + obtain ⟨extended, extendedModel, agreement⟩ := + extension.proof valuation model + have extendedInitial : + ∀ assumption, assumption ∈ initialContext input -> + semantics.holds trace.program extended assumption := by + intro assumption member + have inFacts : + assumption.node.index < input.initialFacts.toList.length := by + simpa using + initialContextFrom_node_lt input.initialFacts.toList 0 + assumption member + have inBase : + assumption.node.index < input.baseProgram.nodes.size := by + simpa [sizeEqual] using inFacts + exact + (domain.holdsPrefix input.baseProgram trace.program + valuation extended assumption basePrefix.proof + model extendedModel inBase + (agreement assumption.node inBase)).mp + (initial assumption member) + have result := final.proof extended extendedModel extendedInitial + exact + (domain.holdsPrefix input.baseProgram trace.program + valuation extended input.target basePrefix.proof + model extendedModel targetOld + (agreement input.target.node targetOld)).mpr result } + else + none + else + none /-! ## Remaining production work diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 9e079be2f..db2be7cee 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1082,6 +1082,18 @@ proved prefix, package rule entailment, fact-domain meet evidence, equality transport, and a domain-owned implication from the strongest installed fact to the possibly weaker requested target. +Replay retains every instance schema's `Extends before after` theorem and +composes the chronological chain rather than treating those proofs as +validation-only acknowledgements. The fact-domain interface supplies the one +locality law needed at this boundary: for valuations which model the old and +extended programs, a fact about an in-bounds old node has the same meaning when +the two valuations agree at that node. +The checker uses the composed extension to transport the caller's exact +version-zero assumptions into the final graph, proves the target there, and +transports the target back. Its result type is consequently an entailment over +the caller's `baseProgram`, and it rejects a target outside that base prefix; +no companion-specific post-processing theorem is needed to close the gap. + The implemented Mathlib conformance vertical recognizes `x * (1 - x)`, instantiates the package-local auxiliary function `x ↦ 1/4 - (x - 1/2)^2`, admits a package-owned equality, propagates @@ -1089,11 +1101,25 @@ instantiates the package-local auxiliary function upper bound. A separate compiled guard checks that the private policy session currently emits the quoted trace; this reachability test is not used as the mathematical proof. The instance schema's conservative-extension witness then -lifts the result from the checked extended program back to every valuation of -the caller's original four-node program. - -This remains an experiment rather than the production checker. Trace-size and -decoder-work envelopes, exact generic reconstruction of instance +participates in the generic composed lift back to every valuation of the +caller's original four-node program. The conformance file also instantiates a +concrete base valuation and derives the ordinary inequality +`x * (1 - x) ≤ 1/4`, preventing a vacuous model encoding from passing as an +end-to-end theorem. + +Program extension currently appends nodes only. Every operation signature a +package may instantiate, including an auxiliary operation unused by the base +node array, is declared in the frontend program's immutable operation table at +session start. Packages resolve its snapshot-local `OpId` from the stable +`OpKey`; neither package assembly order nor a hardcoded compact identifier is +authoritative. Dynamic operation-table growth remains an open design rather +than an implemented capability. + +This remains an experiment rather than the production checker. Its complete +program snapshot per instance and repeated prefix scans are a correctness +canary, not a scalable trace format; a delta-encoded, indexed replay experiment +must measure and replace that representation. Trace-size and decoder-work +envelopes, exact generic reconstruction of instance substitutions/products and per-event program-snapshot linkage, contradiction certificates, split-tree composition, and the tactic quotation format are still open. It is also an explicit diff --git a/conformance/HexInterval/PropagatorE2EConformance.lean b/conformance/HexInterval/PropagatorE2EConformance.lean index e2c4a8296..2990c97c0 100644 --- a/conformance/HexInterval/PropagatorE2EConformance.lean +++ b/conformance/HexInterval/PropagatorE2EConformance.lean @@ -30,8 +30,6 @@ namespace Hex.Interval.PropagatorE2EConformance open Experiment Propagator PayloadArena PolicySession SemanticReplay -noncomputable section - /-! ## Package-local expression language and fact domain -/ def real : DomainId := { index := 0 } @@ -123,10 +121,10 @@ def factLabel : PayloadId := { index := 0 } def instanceLabel : PayloadId := { index := 0 } def equalityLabel : PayloadId := { index := 1 } -def emptyFormat (role : Role) : ReplayFormat := +def taggedFormat (role : Role) (tag : Nat) : ReplayFormat := { role schema := 0 - validateBody := fun body => body.isEmpty } + validateBody := fun body => body == [tag] } def recognizesCentered (request : RuleRequest Fact) : Bool := request.program.programVersion == request.action.programVersion && @@ -161,8 +159,8 @@ def invokeInstantiate (request : RuleRequest Fact) : Plan Fact := payload := instanceLabel }] { visitedEntries := 9, estimatedProofNodes := 1 } drafts := - [{ label := instanceLabel, role := .instance, schema := 0, body := [] }, - { label := equalityLabel, role := .equality, schema := 0, body := [] }] } + [{ label := instanceLabel, role := .instance, schema := 0, body := [1] }, + { label := equalityLabel, role := .equality, schema := 0, body := [2] }] } else { outcome := .inapplicable, drafts := [] } @@ -175,7 +173,7 @@ def invokeForward (request : RuleRequest Fact) : Plan Fact := [{ node := target, fact := .quarter, payload := factLabel }] [] { arithmeticWork := 1, estimatedProofNodes := 1 } drafts := - [{ label := factLabel, role := .fact, schema := 0, body := [] }] } + [{ label := factLabel, role := .fact, schema := 0, body := [3] }] } else { outcome := .failed 2, drafts := [] } | _, _ => { outcome := .inapplicable, drafts := [] } @@ -186,9 +184,9 @@ def runtimePackage : Propagator.Package Fact := operations handlers := #[Handler.statelessPlanned centeredForward invokeForward - #[emptyFormat .fact], + #[taggedFormat .fact 3], Handler.statelessPlanned centeredInstantiate invokeInstantiate - #[emptyFormat .instance, emptyFormat .equality]] } + #[taggedFormat .instance 1, taggedFormat .equality 2]] } def runtimePackages : Array (Propagator.Package Fact) := #[runtimePackage] @@ -227,8 +225,8 @@ def policyLimits : Propagator.Policy.Limits := def arenaLimits : PayloadArena.Limits := { maxEntries := 3 - maxBodyCells := 0 - maxAtom := 0 + maxBodyCells := 3 + maxAtom := 3 maxSchema := 0 maxUses := 7 } @@ -344,17 +342,17 @@ def transportEvent : FactEvent Fact := cause := .transport { index := 0 } { node := node 4, version := 1 } } def instanceEntry : Entry := - { origin := instantiateAction, role := .instance, schema := 0, body := [] } + { origin := instantiateAction, role := .instance, schema := 0, body := [1] } def equalityEntry : Entry := - { origin := instantiateAction, role := .equality, schema := 0, body := [] } + { origin := instantiateAction, role := .equality, schema := 0, body := [2] } def factEntry : Entry := - { origin := forwardAction, role := .fact, schema := 0, body := [] } + { origin := forwardAction, role := .fact, schema := 0, body := [3] } def quotedArena : Arena := { entries := #[instanceEntry, equalityEntry, factEntry] - bodyCells := 0 } + bodyCells := 3 } def quotedTrace : Trace Fact := { program := extendedProgram @@ -369,14 +367,28 @@ def wrongRoleTrace : Trace Fact := arena := { entries := #[instanceEntry, { equalityEntry with role := .fact }, factEntry] - bodyCells := 0 } } + bodyCells := 3 } } def wrongKeyTrace : Trace Fact := { quotedTrace with arena := { entries := #[instanceEntry, { equalityEntry with schema := 1 }, factEntry] - bodyCells := 0 } } + bodyCells := 3 } } + +def wrongBodyTrace : Trace Fact := + { quotedTrace with + arena := + { entries := + #[instanceEntry, equalityEntry, { factEntry with body := [2] }] + bodyCells := 3 } } + +def wrongInstanceBodyTrace : Trace Fact := + { quotedTrace with + arena := + { entries := + #[{ instanceEntry with body := [2] }, equalityEntry, factEntry] + bodyCells := 3 } } def futureAction : Action := { forwardAction with @@ -414,6 +426,8 @@ def forgedMeetTrace : Trace Fact := /-! ## Package-owned mathematical semantics -/ +noncomputable section + def centeredValue (x : ℝ) : ℝ := (1 : ℝ) / 4 - (x - (1 : ℝ) / 2) ^ 2 @@ -515,18 +529,18 @@ theorem forwardEntails : rw [(modelsExtended valuation model).2] exact centeredBounds _ input -inductive UnitCertificate where - | unit +inductive TaggedCertificate where + | tagged -def decodeUnit : List Nat -> Option UnitCertificate - | [] => some .unit - | _ :: _ => none +def decodeTag (expected : Nat) : List Nat -> Option TaggedCertificate + | [actual] => if actual == expected then some .tagged else none + | _ => none def factSchema : PackedFactSchema semantics := { rule := centeredForwardKey schema := 0 - Certificate := UnitCertificate - decode := decodeUnit + Certificate := TaggedCertificate + decode := decodeTag 3 replay := fun _ action context _ => if actionProof : action = forwardAction then if programProof : context.program = extendedProgram then @@ -546,8 +560,8 @@ def factSchema : PackedFactSchema semantics := def instanceSchema : PackedInstanceSchema semantics := { rule := centeredInstantiateKey schema := 0 - Certificate := UnitCertificate - decode := decodeUnit + Certificate := TaggedCertificate + decode := decodeTag 1 replay := fun _ action context _ => if actionProof : action = instantiateAction then if beforeProof : context.before = baseProgram then @@ -565,8 +579,8 @@ def instanceSchema : PackedInstanceSchema semantics := def equalitySchema : PackedEqualitySchema semantics := { rule := centeredInstantiateKey schema := 0 - Certificate := UnitCertificate - decode := decodeUnit + Certificate := TaggedCertificate + decode := decodeTag 2 replay := fun _ action context _ => if actionProof : action = instantiateAction then if programProof : context.program = extendedProgram then @@ -640,6 +654,11 @@ def meetEvidence (previous proposed installed : Fact) : def proofDomain : FactDomainSchema semantics := { top := fun _ => .top + holdsPrefix := by + intro _ _ valuation extended fact _ _ _ _ agreement + change fact.fact.Allows (valuation fact.node) ↔ + fact.fact.Allows (extended fact.node) + rw [agreement] topSound := by intro _ _ _ _ _ _ trivial @@ -675,15 +694,21 @@ def checkerInput : CheckerInput Fact := initialFacts := #[.unit, .top, .top, .top] target := { node := node 3, fact := .upperQuarter } } -def acceptsTrace (trace : Trace Fact) : Bool := +def acceptsInputTrace (input : CheckerInput Fact) (trace : Trace Fact) : Bool := match SemanticReplay.Registry.buildPackages runtimePackages semanticPackages with | .error _ => false | .ok registry => - (SemanticReplay.check registry proofDomain checkerInput trace).isSome + (SemanticReplay.check registry proofDomain input trace).isSome + +def acceptsTrace (trace : Trace Fact) : Bool := + acceptsInputTrace checkerInput trace + +def generatedTargetInput : CheckerInput Fact := + { checkerInput with target := { node := node 4, fact := .quarter } } def checked? : Option (Evidence - (semantics.Entails extendedProgram + (semantics.Entails baseProgram (initialContext checkerInput) checkerInput.target)) := match SemanticReplay.Registry.buildPackages runtimePackages semanticPackages with | .error _ => none @@ -699,16 +724,27 @@ theorem rejects_wrong_role : acceptsTrace wrongRoleTrace = false := by theorem rejects_wrong_key : acceptsTrace wrongKeyTrace = false := by decide +kernel +theorem rejects_wrong_body : acceptsTrace wrongBodyTrace = false := by + decide +kernel + +theorem rejects_wrong_instance_body : + acceptsTrace wrongInstanceBodyTrace = false := by + decide +kernel + theorem rejects_future_reference : acceptsTrace futureTrace = false := by decide +kernel theorem rejects_forged_meet : acceptsTrace forgedMeetTrace = false := by decide +kernel -/-- The kernel-checked result: for every real valuation satisfying the quoted -expression program, `0 ≤ x ≤ 1` implies `x * (1 - x) ≤ 1/4`. -/ +theorem rejects_generated_target : + acceptsInputTrace generatedTargetInput quotedTrace = false := by + decide +kernel + +/-- The kernel checker itself composes the package-owned conservative +extension proof and returns a theorem about the caller's original graph. -/ theorem product_le_quarter : - semantics.Entails extendedProgram + semantics.Entails baseProgram (initialContext checkerInput) checkerInput.target := by match result : checked? with | some evidence => exact evidence.proof @@ -716,37 +752,49 @@ theorem product_le_quarter : have accepted := checked_isSome simp [result] at accepted -/-- The checked extension is conservative, so the result also applies to -every valuation of the original four-node program. -/ +/-- Compatibility name emphasizing that no generated node occurs in the +theorem returned by the generic checker. -/ theorem base_product_le_quarter : semantics.Entails baseProgram - (initialContext checkerInput) checkerInput.target := by - intro valuation model initial - obtain ⟨extended, extendedModel, agreement⟩ := - centeredExtends valuation model - have extendedInitial : + (initialContext checkerInput) checkerInput.target := + product_le_quarter + +/-- A concrete valuation of the caller's four-node expression graph. This +turns the structural replay theorem into the ordinary inequality a tactic user +would see and demonstrates that the checked model context is inhabited. -/ +def baseValuation (x : ℝ) : NodeId -> ℝ := + fun current => + if current = node 0 then x + else if current = node 1 then 1 + else if current = node 2 then 1 - x + else if current = node 3 then x * (1 - x) + else 0 + +theorem baseValuation_models (x : ℝ) : + Models baseProgram (baseValuation x) := by + left + refine ⟨rfl, ?_⟩ + simp [BaseEquations, baseValuation, node] + +/-- Human-facing consequence of the arbitrary-propagator trace. The proof +calls the theorem returned by the generic checker; it does not invoke a +separate arithmetic tactic to establish the upper bound. -/ +theorem product_le_quarter_raw (x : ℝ) (lower : 0 ≤ x) (upper : x ≤ 1) : + x * (1 - x) ≤ (1 : ℝ) / 4 := by + have initial : ∀ assumption, assumption ∈ initialContext checkerInput -> - semantics.holds extendedProgram extended assumption := by + semantics.holds baseProgram (baseValuation x) assumption := by intro assumption member - have before : assumption.node.index < baseProgram.nodes.size := by - have listed := member - simp [initialContext, initialContextFrom, checkerInput] at listed - rcases listed with equal | equal | equal | equal - all_goals subst assumption - all_goals decide - have holds := initial assumption member - have equal := agreement assumption.node before - change assumption.fact.Allows (valuation assumption.node) at holds - change assumption.fact.Allows (extended assumption.node) - rw [equal] - exact holds + simp [initialContext, initialContextFrom, checkerInput] at member + rcases member with equal | equal | equal | equal + · subst assumption + exact ⟨lower, upper⟩ + all_goals subst assumption + all_goals trivial have result := - product_le_quarter extended extendedModel extendedInitial - have equal := agreement (node 3) (by decide) - change Fact.upperQuarter.Allows (extended (node 3)) at result - change Fact.upperQuarter.Allows (valuation (node 3)) - rw [equal] at result - exact result + product_le_quarter (baseValuation x) (baseValuation_models x) initial + change Fact.upperQuarter.Allows (baseValuation x (node 3)) at result + simpa [Fact.Allows, baseValuation, node] using result end diff --git a/conformance/HexInterval/SemanticReplayConformance.lean b/conformance/HexInterval/SemanticReplayConformance.lean index 8adacbbe3..9491d6cc0 100644 --- a/conformance/HexInterval/SemanticReplayConformance.lean +++ b/conformance/HexInterval/SemanticReplayConformance.lean @@ -537,6 +537,11 @@ def meetEvidence (previous proposed installed : Fact) : def factDomain : FactDomainSchema (semantics meanings) := { top := fun _ => .top + holdsPrefix := by + intro _ _ valuation extended fact _ _ _ _ agreement + change fact.fact.Allows (valuation fact.node) ↔ + fact.fact.Allows (extended fact.node) + rw [agreement] topSound := by intro _ _ _ _ _ _ trivial @@ -575,34 +580,72 @@ example : (factDomain.proveMeet program (node 1) .top (.exact 4) (.exact 4)).isS true := by decide -def event (version value : Nat) : FactEvent Fact := - { programVersion := 0 - node := node 1 - previous := { node := node 1, version := version - 1 } - fact := .exact value - version - cause := .rule leftAction (.exact value) { index := 0 } } +/-! ## Conservative-extension chain composition -/ -def trace (arena : Arena) : Trace Fact := - { program - events := #[event 1 4, event 2 5] - arena } - -/-- A future event is physically present but inaccessible before its cursor. -/ -example (arena : Arena) : - (trace arena).eventFactAt? 1 { node := node 1, version := 2 } = none := by - rfl - -example (arena : Arena) : - (trace arena).eventFactAt? 2 { node := node 1, version := 2 } = - some (.exact 5) := by - rfl - -/-- Version zero for a base node comes from the caller-owned initial facts, -not from the untrusted trace. -/ -example (arena : Arena) : - (trace arena).factAt? factDomain checkerInput 0 - { node := node 0, version := 0 } = some (.exact 3) := by - rfl +namespace ExtensionChain + +def base : Program := + { operations := program.operations + nodes := #[instruction 0] } + +def middle : Program := + { operations := program.operations + nodes := #[instruction 0, instruction 1 [node 0]] } + +def final : Program := program + +def trivialSemantics : Semantics Fact := + { Value := Unit + models := fun _ _ => True + holds := fun _ _ _ => True + transport := by intros; trivial } + +theorem basePrefix : ProgramPrefix base middle := + { operationSuffix := ⟨[], rfl⟩ + nodeSuffix := ⟨[instruction 1 [node 0]], rfl⟩ } + +theorem middlePrefix : ProgramPrefix middle final := + { operationSuffix := ⟨[], rfl⟩ + nodeSuffix := ⟨[instruction 2 [node 0]], rfl⟩ } + +theorem extendsAny (before after : Program) : + trivialSemantics.Extends before after := by + intro valuation _ + exact ⟨valuation, trivial, fun _ _ => rfl⟩ + +def first : ProvenExtension trivialSemantics := + { before := base + after := middle + programPrefix := basePrefix + evidence := { proof := extendsAny base middle } } + +def second : ProvenExtension trivialSemantics := + { before := middle + after := final + programPrefix := middlePrefix + evidence := { proof := extendsAny middle final } } + +def composed? : + Option (Evidence (trivialSemantics.Extends base final)) := + composeExtensions base final [first, second] + +theorem composed_isSome : composed?.isSome = true := by + decide +kernel + +theorem rejects_reversed_chain : + (composeExtensions base final [second, first]).isSome = false := by + decide +kernel + +theorem accepts_empty_identity : + (composeExtensions base base + ([] : List (ProvenExtension trivialSemantics))).isSome = true := by + decide +kernel + +theorem rejects_empty_gap : + (composeExtensions base final + ([] : List (ProvenExtension trivialSemantics))).isSome = false := by + decide +kernel + +end ExtensionChain end Hex.Interval.SemanticReplayConformance diff --git a/progress/20260729T063212Z.md b/progress/20260729T063212Z.md new file mode 100644 index 000000000..67da0d44b --- /dev/null +++ b/progress/20260729T063212Z.md @@ -0,0 +1,46 @@ +# Generic base-program replay lift + +## Accomplished + +- Retained every package-owned conservative-extension theorem during instance + replay and composed the chronological base-to-final chain. +- Added the fact-domain locality law needed to transport old-node facts across + arbitrary program extensions whose valuations agree at that node. +- Pinned two-step extension composition, reversed-chain rejection, the + zero-step identity, and rejection of an empty chain with unequal endpoints. +- Restricted fact locality to modeled old/new valuations and an in-bounds old + node, preserving the possibility of genuinely program-relative fact + semantics. +- Removed the unused alternate cursor lookup path so chronological replay has + one implementation: the proved-event accumulator used by the checker. +- Documented that instantiation appends nodes over a predeclared immutable + operation table; dynamic operation-table growth is not implemented. +- Changed the transparent checker to return an entailment over the caller's + original program and to reject targets outside that base graph. +- Moved the executable search guard outside the noncomputable mathematical + section, replaced empty proof bodies with role-specific decoded tokens, and + added negative checks for forged fact and instance bodies plus a generated- + node target. +- Derived the ordinary real inequality `0 ≤ x → x ≤ 1 → + x * (1 - x) ≤ 1/4` from the generic checker result under a concrete, + inhabited model of the original expression graph. +- Updated the SPEC to distinguish the now-closed generic lift obligation from + the still-open scalable delta-trace and resource-envelope experiments. +- Built the experiment, end-to-end, semantic-replay, and policy-session + targets; the conformance manifest, diff check, and banned-token scan pass. + +## Current frontier + +The centered arbitrary-propagator canary now obtains its original-program +theorem directly from the generic checker. The proof path has no known +soundness defect. The branch is still based on the older lower stack. + +## Next step + +Restack the isolated lift onto the refreshed semantic-replay and policy-session +chain, rebuild, then publish the stacked PR. + +## Blockers + +None. Full program snapshots and repeated prefix scans remain deliberately +unoptimized experimental representations, not correctness blockers. From 518bc31d88a33a3c8fe369d7f9bc8ea03d173969 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 29 Jul 2026 07:22:38 +0000 Subject: [PATCH 3/6] Specify arbitrary-scope contractor framework Record the session handoff in progress/20260729T072155Z.md. --- HexInterval/SPEC/hex-interval.md | 305 ++++++++++++++++++++++++++++++- progress/20260729T072155Z.md | 40 ++++ 2 files changed, 340 insertions(+), 5 deletions(-) create mode 100644 progress/20260729T072155Z.md diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index db2be7cee..370cb5fe2 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -564,8 +564,29 @@ ordered read list, and an ordered write list. The dependency index maps each read node to the concrete applications that must wake when its fact changes. The scheduler sees only these concrete identifiers; it does not inspect an operation key to infer that, for example, addition reads two arguments or a -contractor writes one of them. Later shape rules may propose validated -cross-node applications without changing the scheduler protocol. +contractor writes one of them. + +Head-local slots are the compact fast path, not the complete contractor model. +The production application table also admits a compiled arbitrary-scope +contractor application. Such an application has a stable versioned contractor +key, an optional structural anchor, a validated semantic scope, and explicit +ordered read and write node lists. Its scope may cover several constraints or +otherwise unrelated parts of the expression DAG; it need not be encoded as the +arguments of an artificial operation node. Every fact on which its answer +depends occurs in its read list, and every candidate target occurs in its write +list. A bounded matcher or frontend declaration supplies the initial binding; +the engine checks node visibility, domains, duplicate ports, scope, and all +structural limits before compiling the ordinary dependency entries. + +Head-local and arbitrary-scope applications use the same `Action`, +request/reply, freshness, atomic update, observation, and replay protocol. +This lets a package expose elementary forward and backward projections through +relative slots while also exposing a whole-constraint HC4 traversal, an +interval-Newton system contractor, or another coordinated box contractor. +Instantiation may propose a validated arbitrary-scope application or derived +constraint as well as new expression nodes and equality edges. The exact +proposal representation remains open, but cross-node contractors are a +first-class application form rather than a future exception to the scheduler. The current arbitrary-propagator experiment gives each request a bounded, immutable `ProgramView` containing the exact program version, operation table, @@ -1068,6 +1089,18 @@ the proposed fact from the exact watched versions; instance schemas prove that the admitted program extension is semantically conservative; equality schemas prove semantic equality of the exact admitted endpoints. +The production assembly boundary is one coherent checked package snapshot. +For every versioned rule which can execute, that snapshot contains or +atomically pairs its operation signatures, registration or contractor matcher, +callback route, cache policy, payload formats, freezing limits, and semantic +replay schemas. A runtime-only handler cannot enter a proof-producing session, +and a semantic schema with no executable owner cannot be selected by search. +Whether package authors fill one record or a builder seals separately compiled +runtime and companion halves remains open; the public result and its +bidirectional coverage check are one authority boundary. Hot replacement is +valid only when every retained payload remains covered by the exact old +versioned schema. + Kernel replay does not trust or unfold the opaque compiled search session. The tactic must quote an explicit trace containing chronological program snapshots, instance events, equality edges, fact events, and the frozen arena. @@ -1180,6 +1213,18 @@ dependency merely because engine-owned admission may CSE one of their outputs. Compiled structural patterns or more selective operation-key triggers remain alternatives to compare once the behavior is established. +The upgrade path is an indexed structural-watch declaration rather than a +larger collection of booleans. Candidate watch classes include exact operation +keys, bounded compiled patterns, equality or constraint additions, and a +whole-program fallback. Program extension records the bounded classes of its +new structure and wakes only matching registrations; fact-dependent triggers +still use their ordinary explicit fact reads. A compiled-pattern arm returns +validated bindings and a bounded match certificate, while the full +`ProgramView` arm remains the reference oracle. The representation, pattern +language, and index are experiments, but selective extension wakeup, +deterministic bounded enumeration, and the unrestricted fallback are required +capabilities. + 1. The solver produces an `Action` naming a program snapshot, concrete rule application, anchor, declared input fact versions, effort, and action kind. 2. The external function-package registry executes the routed callback and @@ -1211,6 +1256,24 @@ alternatives to compare once the behavior is established. program and caller-supplied version-zero fact array rather than attempting to recover either from the extended program or narrowed current slots. +Atomic multi-output replies have one exact proof contract. Every candidate in +the batch is interpreted against the same pre-reply program snapshot and exact +watched fact versions. Its replay schema proves the proposed fact from those +facts and the program model independently of every other candidate in the +batch. The engine then derives the installed fact by meeting that proposal with +the target's exact preceding fact. Therefore accepting, rejecting, or finding +one sibling candidate redundant cannot invalidate another sibling's proof. +The engine preflights and commits all improving installed facts before issuing +the deduplicated union of wakeups, so no callback can observe a half-installed +batch. + +This first contract deliberately forbids an implicit dependency on an earlier +candidate in reply order. A future contractor which benefits from sequential +intermediate facts must return an explicit bounded micro-trace whose internal +references and order are replayed, rather than relying on list position or the +engine's transaction order. Comparing independent candidates with such +micro-traces is an open proof-size experiment. + The executable `Engine.factAt?` is the replay lookup invariant. Version zero of a base-program node resolves from the caller's immutable `initialFacts`; version zero of an appended node resolves to `FactDomain.top` at that node's @@ -1384,6 +1447,9 @@ package-local identifier reaches its retained provenance. Its monotone a terminal-state claim. The exported `Session.complete` predicate additionally requires a live session and no retained retry or instantiation. At a FIFO fixed point this predicate is the sole gate between saturated and incomplete. +For the canary's current head-local registry this is the `configured` closure +profile described below; production completion also records the selected +profile and includes every compiled arbitrary-scope application it names. Package `failed`/`resourceLimit` results, malformed evidence, dropped narrowing suggestions, and unprocessed retained narrowing therefore cannot be laundered into saturation. @@ -1446,6 +1512,52 @@ targeted shaving, interval Newton, and a global split. Which strength to apply is empirical and may depend on occurrence counts, derivative influence, observed contraction, and proof cost. +### Contractor families and transferable RealPaver design + +RealPaver supplies concrete algorithms to translate and compare, not an API to +copy wholesale. Its base contractor declares an arbitrary variable scope, +contracts an interval box, and reports `Empty`, `Feasible`, `Inner`, or +`Maybe` ([source](https://github.com/realpaver/realpaver/blob/f9d422354c67daf9fcc292ff599acbe8d66cceec/src/realpaver/Contractor.hpp#L30-L64)). +Its dependency pool indexes contractors by every variable in their scope, and +the propagator requeues affected contractors after a sufficient box reduction +([pool](https://github.com/realpaver/realpaver/blob/f9d422354c67daf9fcc292ff599acbe8d66cceec/src/realpaver/ContractorPool.hpp#L29-L82), +[worklist](https://github.com/realpaver/realpaver/blob/f9d422354c67daf9fcc292ff599acbe8d66cceec/src/realpaver/IntervalPropagator.cpp#L83-L145)). +Hex's arbitrary-scope application and dependency index are the proof-producing +counterpart, while its claims and exact fact deltas replace an unverified +status code and floating-point width test. + +The following remain competing registered methods and policy actions: + +- HC4 performs one upward interval evaluation through a constraint expression + followed by backward projection to its leaves + ([interface](https://github.com/realpaver/realpaver/blob/f9d422354c67daf9fcc292ff599acbe8d66cceec/src/realpaver/ContractorHC4Revise.hpp#L29-L56), + [implementation](https://github.com/realpaver/realpaver/blob/f9d422354c67daf9fcc292ff599acbe8d66cceec/src/realpaver/FlatFunction.cpp#L807-L835)). + Hex can express this either as elementary head-local rules reaching a + worklist fixed point or as one composite contractor with an atomic box + reply. +- BC4 first applies HC4 and then uses BC3 only for variables with multiple + occurrences in the constraint + ([source](https://github.com/realpaver/realpaver/blob/f9d422354c67daf9fcc292ff599acbe8d66cceec/src/realpaver/ContractorBC4Revise.hpp#L30-L67)). + Occurrence counts and repeated-node structure are therefore useful bounded + matcher outputs or policy features, not semantics embedded in the scheduler. +- CID slices one variable, runs the complete underlying contractor on every + slice, discards inconsistent slices, and hulls every variable over the + survivors + ([source](https://github.com/realpaver/realpaver/blob/f9d422354c67daf9fcc292ff599acbe8d66cceec/src/realpaver/ContractorVarCID.cpp#L66-L99)). + Its Hex analogue is a local branch certificate inside `shave`, not a global + solver split. +- ACID orders variable-level 3B/CID work using derivative influence and adapts + how many contractors it invokes across learning and exploitation phases + ([source](https://github.com/realpaver/realpaver/blob/f9d422354c67daf9fcc292ff599acbe8d66cceec/src/realpaver/ContractorACID.hpp#L30-L50)). + This is an explicit policy-state experiment below, never mutable + memoization hidden inside a callback. + +RealPaver's floating relative-width tolerances are scheduling heuristics, not +logical closure criteria for Hex. Every accepted logical strengthening, +including a strictness change at an unchanged endpoint, enters the fact state +and wakes its declared dependencies. Exact bounded scores may still decide +whether a small improvement justifies another expensive contractor call. + Whether `ActionKind` is only a policy/provenance label or also constrains the constructors a callback may return remains open. The current experiment allows, for example, an instantiation suggestion from any successfully routed handler; @@ -1470,6 +1582,24 @@ reply into the policy observation. Dropping a retry or instantiation marks propagation incomplete, while dropping only split advice preserves fixed-point completeness. +These outcome tags are control observations, never mathematical +classifications. A contractor report may separately carry theorem-backed +claims with their own role-specific payloads. The first required claims are: + +- `contradiction`: no valuation satisfies the exact program relation and + request facts in this scope; and +- `inner`: every valuation in the exact current input box satisfies the + registered constraint or goal relation named by the application. + +A contradiction may alternatively be reconstructed from incompatible proved +facts after ordinary intersection. `noChange` is not `inner`, `inapplicable` +is not contradiction, and `resourceLimit` proves nothing about the box. +RealPaver's additional `Feasible` classification motivates a possible future +existence claim, but Hex accepts one only with an explicit replayed witness or +existence certificate; a nonempty contracted box is not such a proof. Claims, +fact candidates, and suggestions may share an atomic report, but each has +independent payload coverage and resource accounting. + The base `Program` is static after validation. Generic cheap alternates may be present before search, and `rewrite` only changes which form in the current validated snapshot is scheduled. Adaptive range reduction or a Taylor @@ -1499,6 +1629,23 @@ Shrinking an input does not require a rule to discard all earlier work. Cache reuse is a performance feature only. Every returned fact still receives a new or reused sound justification. +Adaptive strategy state is separate from this memo cache. Learning that a +contractor, variable, effort, or subdivision pattern has recently been useful +may change which eligible action runs next; it must not silently change the +candidate returned by an otherwise identical request. The first candidate +places RealPaver-ACID-style learning and exploitation in `Policy.State`, using +engine-owned observations of actual fact deltas and declared work. A more +modular package-owned advisor remains an experiment, but any state which +changes applicability or facts has an explicit version included in action +freshness and an explicit wakeup rule. + +Strategy state also has declared branch ownership. A child either receives a +documented persistent policy snapshot, starts from a documented reset state, +or uses observations keyed by the complete semantic scope; it never inherits +history accidentally through a shared cache. Its decisions use bounded exact +features and are replayable as search choices, while proof replay remains +independent of them. + ## Propagation state Each live branch contains: @@ -1526,6 +1673,22 @@ suppressed work, and peak live queue before selecting a default. Multi-output outcomes install every accepted fact before waking this union, so they do not manufacture stale work against their own half-installed state. +Self-revisitation is explicit. Once an application is selected it is no longer +marked queued; if its atomic reply strengthens a node that the same application +reads, the ordinary dependency wakeup may enqueue it again. This is the safe +default for one-step elementary propagation and for contractors such as a +single HC4 revision which need not be idempotent. The scheduler never excludes +the current application merely because it caused the change. + +A composite contractor may instead report that its output box is locally +closed under a named method and effort. That report is bound to the exact +post-reply facts and closure profile; it is not inferred from `ActionKind`, +from absence of a large width reduction, or from `noChange`. Whether a checked +local-closure certificate can safely suppress the immediate self-wakeup, or +whether it should remain only a policy hint followed by one confirming call, +is an experiment. An unverified hint may affect priority but cannot justify a +saturation result. + The initial `balancedV1` candidate runs all cheap forward rules once in program order and then drains the dependency worklist. It also runs zero-cost contradiction checks after every accepted fact. More expensive improvement and @@ -1533,6 +1696,24 @@ split actions start only after this cheap fixed point, unless a rule marks a singularity that requires an immediate split. This staging is policy behavior, not an engine soundness condition. +Saturation is always relative to a named closure profile carried by the result. +The first profiles to compare are: + +- `cheap`: equality transport and every enabled head-local forward/backward + application at its initial effort are quiescent; +- `contractor`: `cheap` plus a named, versioned set of arbitrary-scope + contractor methods and effort levels is quiescent; and +- `configured`: no invocation, equality, retry, instantiation, or other + narrowing action admitted by the run configuration remains live. + +These are statements about a finite registry and configuration, not +mathematical completeness of interval reasoning. Optional global splits do not +prevent propagation saturation in the current scope. A dropped, dismissed, +failed, resource-limited, stale, or unprocessed action required by the selected +profile yields `unknown` or a weaker recorded profile; an empty queue alone +does not upgrade the claim. The exact profile encoding and whether arbitrary +profiles are data or a small versioned enumeration remain open. + Backward propagation uses the same worklist. A contractor is valid only when its soundness theorem says that it preserves every assignment satisfying the current constraints. When proving a goal by contradiction, the frontend may @@ -1546,6 +1727,27 @@ counterexample-box diagnostics. A public best-bound theorem is replayed from pre-assumption facts or from a separate bound search, never by leaking a conditional fact into the parent scope. +### Immediate contractor-granularity experiment + +The next framework experiment uses the same validated expression program, +initial facts, fact domain, function-package theorems, and resource envelopes +in two arms: + +1. compile elementary head-local forward and backward applications and drain + the incremental dependency worklist to the selected closure profile; and +2. compile one arbitrary-scope HC4-style application per constraint, perform + an upward evaluation and backward projection inside the callback, and + return the resulting box as one atomic multi-output report. + +Both arms replay ordinary kernel proofs and are tested first on the named HC4 +and loop fixtures below. They compare final facts or a documented containment +relation, contradictions and inner claims, callback invocations, fact meets, +watcher visits, self-revisits, accepted deltas, frozen payload entries and +bytes, backwards-sliced proof nodes, and checker work. Mixed and policy-selected +hybrids remain possible outcomes. The experiment chooses contractor +granularity; it neither selects nor depends on a rational working-endpoint +representation. + ## Search policy The policy affects success and performance, never validity. In particular it @@ -2187,6 +2389,17 @@ structure FactId where scope : ScopeId index : Nat +structure ClaimId where + scope : ScopeId + index : Nat + +structure ConstraintId where + index : Nat + +inductive ClaimKind + | contradiction + | inner (constraint : ConstraintId) + inductive EqualityRef | edge (edge : EqEdgeId) | source (source : SourceId) @@ -2199,9 +2412,16 @@ inductive Derivation | splitAssumption (parent : ScopeId) (side : SplitSide) (node : NodeId) (cut : Dyadic) +structure ClaimDerivation where + rule : RuleKey + inputs : Array FactId + kind : ClaimKind + payload : PayloadId + inductive Close | goal (facts : Array FactId) | contradiction (lower upper : FactId) + | claim (claim : ClaimId) inductive BranchTree | leaf (scope : ScopeId) (close : Close) @@ -2221,6 +2441,12 @@ upper cut `node <= cut`; the right child receives the strict lower cut `cut < node`. The branch-tree validator checks these relationships, unique parentage, acyclicity, and that every leaf has a closing witness. +Claim identifiers are scope-qualified in the same way and index a separate +bounded claim-derivation table. Closing from one replays its exact rule, +request facts, relation identity, and payload. A contradiction claim closes +the scope; an inner claim closes only the exact registered constraint or goal +relation named in that leaf. A control outcome never creates a `ClaimId`. + `transportEq` preserves side, value, and strictness while moving a fact across a proved equality. Validation checks that the equality is visible in the fact's scope, that its endpoints match the input and target nodes in one of the @@ -2297,6 +2523,10 @@ marked pixels are explicitly `unknown`. No finite algorithm can always decide intersection with every pixel boundary, so unresolved pixels are part of the honest interface rather than rendered as proved occupancy. +An arbitrary-scope contractor may classify a whole tile or connected group of +columns at once. An `inner` claim can discharge a universal region test, while +a `present` pixel still requires the separate existence evidence above. + Pixel rectangles use an exact, documented boundary convention, preferably half-open cells with a separately closed outer viewport. Open cuts matter: they decide whether a graph lying exactly on a pixel boundary belongs to one @@ -2346,6 +2576,11 @@ composition of consecutive steps. The interval engine contributes checked facts and replayable dependencies to those theorems; successful numerical search alone never asserts that a solution exists. +This application is one reason arbitrary-scope contractors are part of the +base framework: a Picard, Jacobian, invariant, or event contractor may update a +coordinated time/state/parameter box atomically rather than masquerading as a +unary scalar operation. + This downstream use argues for keeping the present abstractions: - domains and facts must extend beyond one scalar endpoint representation, @@ -2418,6 +2653,61 @@ their declared cost inside a scheduler bound. The required Lean-only profile covers every interval shape and operation with typical, boundary, and adversarial inputs. In particular it includes: +### Named contractor challenge fixtures + +The contractor-granularity experiment and later policy experiments use a +stable named corpus translated from RealPaver's primary sources. RealPaver's +binary floating-point intervals are not oracle values for Hex: the translations +use exact endpoints, preserve Hex open/unbounded semantics, and prove their +own expected facts. + +- `hc4-quadratic` translates `(x + y)^2 - 2*z + 2 = 0`. From + `x ∈ [-10,15]`, `y ∈ [-20,5]`, and `z ∈ [-10,11/2]`, the composite reference + revision returns exactly `x ∈ [-8,15]`, `y ∈ [-18,5]`, + `z ∈ [1,11/2]`; the elementary closure arm must establish at least those + bounds and may soundly be tighter under its named profile. With `x` + initially whole, the reference result is exactly `x ∈ [-8,23]`, + `y ∈ [-20,5]`, and `z ∈ [1,11/2]`. The `z ∈ [-10,0]` variant proves + contradiction. For `(x + y)^2 - 2*z + 2 ≥ 0` with `x ∈ [2,4]`, + `y ∈ [3,10]`, and `z ∈ [0,6]`, the result is a theorem-backed inner-box + claim, not merely `noChange`. These are the cases in RealPaver's + [`ctc_hc4_test.cpp`](https://github.com/realpaver/realpaver/blob/f9d422354c67daf9fcc292ff599acbe8d66cceec/test/ctc_hc4_test.cpp). +- `hc4-loop` uses `x^2 - x = 0` from `x ∈ [0,10]`, whose hull-consistent + closure approaches the exact solution hull `[0,1]`. Coarse, medium, and fine + exact Hex profiles must respectively return sound enclosures no wider than + `[0,43/40]`, `[0,2019/2000]`, and `[0,5003/5000]`, matching or improving the + source test's documented outer targets without adopting its relative-width + stopping rule. The `x ∈ [3/2,10]` variant is not allowed to stop after an + inconclusive first revision: self-revisitation must eventually prove + contradiction under its configured exact closure profile. A coupled variant + uses `y = x^2` and `x^2 + y^2 = 2` from `x,y ∈ [0,10]` to test reactivation + between two arbitrary-scope contractors and increasingly tight enclosures + of the unique nonnegative solution `(1,1)`: its coarse exact target puts both + variables inside `[0,707107/500000]`, and its fine target puts both inside + `[99999999/100000000,1000000001/1000000000]`. RealPaver's tolerance ladder + supplies these challenge targets, not Hex's stopping rule + ([source](https://github.com/realpaver/realpaver/blob/f9d422354c67daf9fcc292ff599acbe8d66cceec/test/ctc_loop_test.cpp)). +- `robot-2r` translates the inverse-kinematics system with + `q1,q2 ∈ [-π,π]`, link lengths `9/2` and `3`, and target + `(x,y) = (23/4,17/4)`. It tests sine and cosine packages, shared + `q1 + q2`, periodic backward projection, disconnected solution regions, + semantic split landmarks, and multi-solution branch coverage + ([source](https://github.com/realpaver/realpaver/blob/f9d422354c67daf9fcc292ff599acbe8d66cceec/examples/2r-robot.rp)). +- `trigexp-10` translates the sparse ten-variable cubic, sine, and exponential + chain from RealPaver. It is primarily a dependency, arbitrary-scope + contractor, cache, and policy stress test: changing one variable should not + rescan unrelated graph structure + ([source](https://github.com/realpaver/realpaver/blob/f9d422354c67daf9fcc292ff599acbe8d66cceec/benchmarks/csp/Trigexp1-10.rp)). + +Hex-specific companions require `sin x = 0` on `(0,π)` to prove +contradiction, while the same equation on `[0,π]` must preserve its endpoint +solutions. The equation `x⁻¹ = 0` at `x = 0` must remain satisfiable under +Lean's total inverse. These cases prevent a contractor translated from a +conventional numeric library from erasing strict endpoints or silently +replacing Lean's total inverse with a partial reciprocal. + +### General conformance matrix + - all four finite endpoint closure combinations; - equal endpoints in all closure combinations; - empty, singleton, one-sided unbounded, and whole intervals; @@ -2567,9 +2857,10 @@ The Mathlib-free benchmark target measures: - bounded-instantiation saturation over useful, duplicate, and deliberately explosive trigger families, recording generated nodes, equality edges, suppressed instances, and proof-slice retention; -- HC4-style propagation and local-shaving traces over translated small - RealPaver-shaped dependency graphs, without importing their floating-point - semantics; +- the elementary-worklist and composite-HC4 arms over `hc4-quadratic`, + `hc4-loop`, and the coupled system, followed by local-shaving traces and the + larger `robot-2r` and `trigexp-10` dependency graphs, without importing + RealPaver's floating-point semantics or stopping tolerances; - branch creation and isolated updates for `Array` copy-on-write, persistent paged-trie, chunked-vector, and trail/rollback candidates, crossing program sizes 20, 50, and 500 with 8, 100, and 1,000 leaves; @@ -2618,6 +2909,10 @@ local test profile. They do not enter this Mathlib-free benchmark target. [Arb: efficient arbitrary-precision midpoint-radius interval arithmetic](https://arxiv.org/abs/1611.02831). - Oliver Flatt and Pavel Panchekha, [An interval arithmetic for robust error estimation](https://arxiv.org/abs/2107.05784). +- Raphaël Chenouard and Laurent Granvilliers, + [RealPaver 1.1](https://joss.theoj.org/papers/10.21105/joss.09331), + with the [versioned source](https://github.com/realpaver/realpaver/tree/f9d422354c67daf9fcc292ff599acbe8d66cceec) + used for contractor and challenge-fixture references above. - [IBEX contractor documentation](https://ibex-team.github.io/ibex-lib/contractor.html) and [strategy documentation](https://ibex-team.github.io/ibex-lib/strategy.html). - [IntervalArithmetic.jl construction and exact input guidance](https://juliaintervals.github.io/IntervalArithmetic.jl/stable/manual/construction/). diff --git a/progress/20260729T072155Z.md b/progress/20260729T072155Z.md new file mode 100644 index 000000000..15180e039 --- /dev/null +++ b/progress/20260729T072155Z.md @@ -0,0 +1,40 @@ +# Arbitrary-scope contractor framework SPEC + +## Accomplished + +- Made compiled arbitrary-scope contractor applications first-class alongside + head-local result/argument registrations, with the same dependency, + transaction, policy, and replay protocol. +- Specified independent pre-snapshot proofs for atomic multi-output replies + and an explicit micro-trace option for future sequential contractor results. +- Separated theorem-backed contradiction and inner-box claims from control + outcomes, and extended the derivation sketch with scoped claim closure. +- Defined conservative self-revisitation, explicit local-closure reporting, and + named cheap, contractor, and configured saturation profiles. +- Kept adaptive learning state in an explicit strategy/policy layer distinct + from memo caches, including branch ownership and versioned dependencies. +- Required coherent runtime and semantic package assembly and described the + indexed structural-watch upgrade path from whole-program wakeups. +- Added primary-source RealPaver mappings for HC4, BC4, CID, and ACID, plus + exact named HC4, loop, coupled-system, robot, Trigexp, sine-boundary, and + total-inverse challenge fixtures. +- Made the immediate framework experiment compare elementary worklist + propagation with a composite HC4-style contractor under identical facts, + proof schemas, and resource accounting. + +## Current frontier + +The SPEC now treats arbitrary function and box contractors as the main +framework problem. The executable engine still implements only head-local +applications; arbitrary-scope compilation, claim payload roles, named closure +profiles, and the two-arm HC4 experiment remain to be implemented. + +## Next step + +Implement the smallest arbitrary-scope application vertical and run both +contractor-granularity arms on `hc4-quadratic`, then add the loop/revisit cases +before selecting a default granularity. + +## Blockers + +None. From 92afdf4b04a86661d1c3a27d13e80bd1c8f7a0df Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 29 Jul 2026 07:29:45 +0000 Subject: [PATCH 4/6] Refresh arbitrary propagator proof integration Progress: progress/20260729T072925Z.md --- HexInterval/SPEC/hex-interval.md | 21 +++++++++++ .../HexInterval/PropagatorE2EConformance.lean | 9 +++-- .../SemanticReplayConformance.lean | 2 +- progress/20260729T072925Z.md | 37 +++++++++++++++++++ 4 files changed, 64 insertions(+), 5 deletions(-) create mode 100644 progress/20260729T072925Z.md diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 370cb5fe2..68b3e3f7e 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -783,6 +783,20 @@ which deliberately says nothing about retained suggestions or propagation completeness. A separate policy canary consumes the exact engine-issued drop plan and records the lost instantiation as incomplete. +Depth is only the first recoverable per-suggestion refusal. The contractor +experiment must classify resource limits by ownership: a malformed proposal +invalidates its reply; a valid proposal which is individually unaffordable +under a configured local node, equality, application, or queue allowance may +be dropped with an exact reason while independent candidates commit and the +scope becomes incomplete; exhaustion of storage already consumed by the live +branch may remain a hard engine-resource stop. In particular, a multi-node +function instantiation should not terminate an otherwise useful reply merely +because it crosses `maxNodes` when the same situation can be identified before +retention. The exact split among `maxNodes`, `maxInstances`, `maxEqualities`, +`maxApplications`, and `maxQueueEntries` is an implementation experiment, but +every limit has one documented disposition and no refused narrowing work may +be mistaken for saturation. + The general experiment activates proposed equality edges as indexed, replayable search contractors: improving either endpoint wakes transport in the other direction, and admission of a new edge considers both current @@ -1987,6 +2001,13 @@ dropped from the engine's bounded retained prefix, or tombstoned by a failed freshness guard. `Suggestion.affectsClosure` is the single classification used for all three paths, while `Engine.keptSuggestions` and `Engine.droppedSuggestions` define the exact shared retention boundary. +The engine returns this exact admission plan to the policy wrapper so the +wrapper never repeats structural classification against a possibly different +snapshot. The policy observation is nevertheless payload-erased: it exposes +semantic suggestion keys, kept/dropped disposition, and drop reasons such as +capacity or structural depth, never raw payload identifiers or complete +`InstantiationRequest`s. Search behavior must not depend on arbitrary +proof-arena numbering. Declining an invocation, equality contractor, retry, or instantiation makes the run incomplete; declining a split does not, because it changes proof search rather than the propagation closure of the current scope. An empty diff --git a/conformance/HexInterval/PropagatorE2EConformance.lean b/conformance/HexInterval/PropagatorE2EConformance.lean index 2990c97c0..e5caad3c4 100644 --- a/conformance/HexInterval/PropagatorE2EConformance.lean +++ b/conformance/HexInterval/PropagatorE2EConformance.lean @@ -146,8 +146,6 @@ def invokeInstantiate (request : RuleRequest Fact) : Plan Fact := .success [] [.instantiate { key := 1 - triggers := [node 3, node 0, node 2, node 1] - claimedGeneration := 1 nodes := [{ domain := real op := { index := 4 } @@ -209,12 +207,13 @@ def engineLimits : Propagator.Limits := maxRetainedSuggestions := 2 maxEffort := 0 maxObservationValue := 16 - maxDiagnosticValue := 16 + maxDiagnosticValue := 256 maxOutcomeCandidates := 1 maxOutcomeSuggestions := 1 maxProposalItems := 5 maxInstances := 1 maxGeneration := 1 + maxNodeDepth := 8 maxEqualities := 1 splitEndpointLimit := endpointLimit } @@ -224,8 +223,10 @@ def policyLimits : Propagator.Policy.Limits := maxLiveOffers := 16 } def arenaLimits : PayloadArena.Limits := - { maxEntries := 3 + { maxEntries := 7 maxBodyCells := 3 + maxDrafts := 7 + maxDraftCells := 3 maxAtom := 3 maxSchema := 0 maxUses := 7 } diff --git a/conformance/HexInterval/SemanticReplayConformance.lean b/conformance/HexInterval/SemanticReplayConformance.lean index 9491d6cc0..ef51cb97c 100644 --- a/conformance/HexInterval/SemanticReplayConformance.lean +++ b/conformance/HexInterval/SemanticReplayConformance.lean @@ -580,7 +580,7 @@ example : (factDomain.proveMeet program (node 1) .top (.exact 4) (.exact 4)).isS true := by decide -/-! ## Conservative-extension chain composition -/ +/-! # Conservative-extension chain composition -/ namespace ExtensionChain diff --git a/progress/20260729T072925Z.md b/progress/20260729T072925Z.md new file mode 100644 index 000000000..4fa5ea751 --- /dev/null +++ b/progress/20260729T072925Z.md @@ -0,0 +1,37 @@ +# Arbitrary-propagator proof integration refresh + +## Accomplished + +- Joined the final policy-session and semantic-replay branches without + duplicating either implementation, then rebased the end-to-end propagator + proof and arbitrary-scope contractor SPEC work onto that combined base. +- Migrated the end-to-end instance request to engine-owned generation and + structural dependencies, added the final node-depth and payload-draft + envelopes, and raised the registry diagnostic envelope to its declared + dispatch-code floor. +- Preserved both policy-session and semantic-replay targets in the combined + Lake graph and fixed the rebased documentation-header hierarchy. +- Folded independent review findings into the SPEC: the authoritative engine + suggestion plan reaches policy only through a payload-erased observation, + and recoverable local contractor refusals are distinguished from hard + branch-storage exhaustion. +- `lake build HexIntervalExperiment HexInterval.PropagatorE2EConformance + HexInterval.SemanticReplayConformance HexInterval.PolicySessionConformance`, + the Lean line-count lint, and `git diff --check` pass without warnings. + +## Current frontier + +The generic checker now composes arbitrary package-owned extension proofs and +returns the requested theorem over the caller's original program on the final +framework stack. The contractor SPEC and named RealPaver challenge corpus are +in the same integration branch. + +## Next step + +Restack the sine package, migrate its runtime callback to stable-key operation +resolution, run an independent review of the arbitrary-prefix sine theorem, +and open the integration and sine PRs. + +## Blockers + +None. From 79d04f407417d39dbf63907fc3f78f1120073e4c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 29 Jul 2026 09:20:53 +0000 Subject: [PATCH 5/6] docs(interval): specify arbitrary propagator framework --- HexInterval/SPEC/hex-interval.md | 1136 +++++++++++++++++++++++------- progress/20260729T091623Z.md | 33 + 2 files changed, 922 insertions(+), 247 deletions(-) create mode 100644 progress/20260729T091623Z.md diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 68b3e3f7e..e09afe166 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -45,6 +45,14 @@ The design must satisfy all of the following. not appear in the generated proof. 8. No part of the implementation, conformance suite, benchmark, or tactic fallback uses `native_decide`. +9. A function package may install an arbitrary propagator over an ordered set + of existing and newly instantiated expressions. Its read/write scope need + not be the arguments of one arithmetic node, and it uses the same queue, + policy, resource, and replay machinery as built-in local propagation. +10. Structural matching, propagation, improvement, instantiation, local + refinement, and proof-level subdivision are independently schedulable. + Their selection schemes are replaceable and upgradeable without changing + the package soundness theorems. The fixed contracts are semantic: exact enclosures, independent strictness, safe failure, replayable provenance, deterministic resource accounting, and @@ -125,6 +133,58 @@ This SPEC presently approves no `@[extern]` planner hook. Adding one requires a SPEC revision naming its versioned symbol and candidate schema, shape validator, checker soundness theorem, and native absence/rejection fallback. +## Generic fact-domain contract + +The propagation engine is parameterized by an opaque `Fact` type. It does not +inspect interval endpoints, widths, rational numerators, or the mathematical +meaning of a domain. The executable `v0` boundary is intentionally small: + +```lean +inductive NarrowResult (Fact : Type) + | noChange + | improved (fact : Fact) + | contradiction (fact : Fact) + | malformed (code : Nat) + | resourceLimit (resource : Nat) + +structure FactDomain (Fact : Type) where + top : DomainId → Fact + narrow : DomainId → Fact → Fact → NarrowResult Fact +``` + +`narrow d current candidate` is the engine-owned installation operation. A +callback proposes `candidate`; it never installs a fact directly. `improved` +and `contradiction` return the canonical installed meet with `current`, while +`noChange` means that the canonical current fact already contains all useful +information in the candidate. `malformed` rejects a representation error and +`resourceLimit` reports exact domain-owned arithmetic refusal. Both are +distinct from mathematical inapplicability and from an engine storage limit. +The operation is deterministic under its explicit resource envelope and may +not hide an unbounded normalization or a `native_decide` fallback. + +The Mathlib companion supplies the semantic side of this interface. For a +program model `ρ`, node `n`, and fact `f`, write `ModelsFact ρ n f`. Replay +requires the following laws, specialized by `DomainId`: + +- `top` is satisfied by every well-typed value; +- a returned installed fact denotes the conjunction of the preceding fact + and the proposed fact, or a sound strengthening of that conjunction; +- `contradiction` carries replay evidence that the two proved inputs cannot be + satisfied together; +- facts about an old node are stable under a conservative program/network + extension which preserves that node's interpretation; and +- the strongest retained fact used to close a goal entails the exact + caller-requested target fact. + +The executable narrowing result is still untrusted search data: companion +replay proves the candidate from the rule payload and then applies the +domain's meet law. A future fact domain may add bounded equality, +canonicalization, significance, or policy-feature extraction hooks. Such a +hook can suppress scheduling or provide ranking data, but it cannot silently +discard a logical strengthening or change the replay laws above. The first +real-valued domain below—strict/non-strict dyadic cuts with unbounded ends—is +one instance of this generic contract, not the scheduler's type. + ## Interval representation The semantic shape is intentionally small. The exact constructors and the @@ -527,11 +587,14 @@ settle the public representation. The frontend first reifies terms into a typed single-assignment base program. Each instruction refers only to earlier instruction identifiers. Common subexpression elimination occurs before search, so the array is also a compact -encoding of an expression DAG. The base is immutable after validation. A -separate, bounded extension mechanism may add proved-relevant expressions as -search discovers useful shapes; eager pre-materialization, epochal extension, -and fully append-only extension are candidates to compare rather than a choice -already frozen here. +encoding of an expression DAG. The caller's base remains an immutable prefix. +A separate, bounded transition may atomically add proved-relevant expressions, +equality contractors, and arbitrary-scope propagator applications as search +discovers useful shapes. Once an engine identifier has been exposed, later +transitions never renumber or replace it. Eager pre-materialization, epochal +storage, chunked arenas, and physically incremental storage remain candidates +to compare, but every candidate must implement this logical append-only +identity contract. Conceptually: @@ -544,10 +607,16 @@ structure Node where structure Program where operations : Array OpKey nodes : Array Node - consumers : Array (Array NodeId) + +structure Network where + program : Program equalities : Array EqEdge + applications : Array Application ``` +Consumer/watcher tables are deterministic derived indexes over the network; +they are not semantic program data and need not appear in a certificate. + An `OpKey` identifies the semantic operation at a node, including its domain signature and normalization variant. An `OpId` is only a compact index into the program's operation table. A `RuleKey` instead identifies one propagation @@ -566,17 +635,37 @@ The scheduler sees only these concrete identifiers; it does not inspect an operation key to infer that, for example, addition reads two arguments or a contractor writes one of them. +Every registration declares a `BindingKind`. A `local` registration derives +its ports from bounded result/argument slots at each matching head node. A +`scoped` registration is dormant until the frontend or a structural matcher +supplies a concrete `ScopeBinding`; a `ProposedScope.rule` must resolve to such +a scope-capable registration. Local binding is the compact fast path, while +both forms compile to the same application interface. + Head-local slots are the compact fast path, not the complete contractor model. The production application table also admits a compiled arbitrary-scope contractor application. Such an application has a stable versioned contractor -key, an optional structural anchor, a validated semantic scope, and explicit -ordered read and write node lists. Its scope may cover several constraints or -otherwise unrelated parts of the expression DAG; it need not be encoded as the -arguments of an artificial operation node. Every fact on which its answer -depends occurs in its read list, and every candidate target occurs in its write -list. A bounded matcher or frontend declaration supplies the initial binding; -the engine checks node visibility, domains, duplicate ports, scope, and all -structural limits before compiling the ordinary dependency entries. +key, a structural anchor in the current experiment, and explicit ordered read +and write node lists. Its scope may cover several constraints or otherwise +unrelated parts of the expression DAG; it need not be encoded as the arguments +of an artificial operation node. Every fact on which its answer depends occurs +in its read list, and every candidate target occurs in its write list. A +bounded matcher or frontend declaration supplies the initial binding. The +engine checks rule ownership, anchor/head compatibility, node visibility, +write authorization, and structural limits; the owning package separately vetoes +bindings which do not fit its semantic contractor schema. That package check +protects the callback contract but is not proof: the companion still replays +the contractor theorem. An anchor-free production form remains a possible +generalization, but it must supply an equally explicit structural identity. + +Read ports have two roles which the production representation must not +conflate. Their ordered semantic projection may repeat a node—for example the +two arguments of `x * x`—while the dependency index wakes the application once +per changed node. Duplicate writes remain rejected until an explicit same- +target merge rule is specified. The current `v0` scope record rejects repeated +reads as a simplifying representation restriction; experiments must compare +it with separate ordered role ports and a deduplicated wake set before this API +is frozen. Head-local and arbitrary-scope applications use the same `Action`, request/reply, freshness, atomic update, observation, and replay protocol. @@ -584,12 +673,19 @@ This lets a package expose elementary forward and backward projections through relative slots while also exposing a whole-constraint HC4 traversal, an interval-Newton system contractor, or another coordinated box contractor. Instantiation may propose a validated arbitrary-scope application or derived -constraint as well as new expression nodes and equality edges. The exact -proposal representation remains open, but cross-node contractors are a -first-class application form rather than a future exception to the scheduler. +constraint as well as new expression nodes and equality edges. The exercised +proposal form names a stable rule key, an anchor reference, and ordered read +and write references; each reference may target an old node or a node proposed +by the same atomic event. Cross-node contractors are therefore a first-class +application form rather than a future exception to the scheduler. + +Here “contractor scope” means the ordered structural binding of one +application. It is distinct from the proof/search `ScopeId` used below for a +root state or split branch; a contractor binding is visible in exactly the +proof scopes where its nodes and evidence are visible. The current arbitrary-propagator experiment gives each request a bounded, -immutable `ProgramView` containing the exact program version, operation table, +immutable `ProgramView` containing the exact network version, operation table, SSA node table, per-node theorem-instantiation generations, and per-node structural expression depths. It contains no facts. The engine constructs it only from a validated state already covered by the @@ -614,19 +710,22 @@ places engine-owned generation accounting can see it; merely calling `ProgramView.node?` on an arbitrary identifier does not make that node a generation dependency. Anchor-local inspection adds no wakeup beyond the declared fact slots; a rule -which reads the whole view declares `watchesProgram`, making program extension +which reads the whole view declares `watchesProgram`, making network extension an explicit dependency. -`ProgramView.programVersion` equals the engine-owned version in the action for -that invocation. An append-only extension creates subsequent requests with -the new arrays and version. An anchor-local proposal may remain fresh when its -concrete application and declared fact versions are unchanged; admission still -resolves references, CSE hits, types, equalities, and generation against the -current validated program. A `watchesProgram` action instead requires the exact -program version: extension stales its old proposal and requeues the existing -application to obtain a fresh view. A meaning-changing application replacement -or watched-fact change also makes an action stale. Policy selections made -against a current snapshot retain their separate exact program-version guard. +`ProgramView.programVersion` equals the engine-owned propagation-network +version in the action for that invocation. The current field name is broader +than expression nodes: a fresh scope-only application advances it even when +the node array is unchanged. An append-only extension creates subsequent +requests with the new network and version. An anchor-local proposal may remain +fresh when its concrete application and declared fact versions are unchanged; +admission still resolves references, CSE hits, types, equalities, and generation +against the current validated program. A `watchesProgram` action instead +requires the exact network version: extension stales its old proposal and +requeues the existing application to obtain a fresh view. A meaning-changing +application replacement or watched-fact change also makes an action stale. +Policy selections made against a current snapshot retain their separate exact +network-version guard. The external registry assigns meaning to keys such as product, difference, or a distinguished constant. The engine supplies only exact lookups and never embeds those meanings. @@ -684,20 +783,50 @@ ordinary interval facts. Typical uses include: - introducing derivative, range-reduction, or function-specific alternate expressions only after their input range makes them useful; - instantiating a monotonicity theorem by adding product or difference nodes - that were absent from the original goal. + that were absent from the original goal; and +- installing a coordinated contractor only when the expressions which form + its nonlocal read/write box have appeared. An instantiation proposal is retained under the selected action's versioned `RuleKey`; its own `key : Nat` is only an untrusted family label for replay and is not canonical authority. The proposal contains new SSA instructions, -equality or derived-fact recipes, and their opaque replay payloads. The engine +equality or derived-fact recipes, arbitrary-scope application drafts, and +their opaque replay payloads. The engine derives the canonical substitution from the selected action's anchor, declared input facts, and existing nodes explicitly referenced by those instructions and recipes. +The exercised structural shape is: + +```lean +inductive NodeRef + | existing (node : NodeId) + | proposed (index : Nat) + +structure ProposedScope where + rule : RuleKey + anchor : NodeRef + watches : List NodeRef + writes : List NodeRef + +structure InstantiationRequest where + key : Nat + nodes : List ProposedNode + equalities : List ProposedEquality + scopes : List ProposedScope + payload : PayloadId +``` + +Scope references are resolved only after draft-node CSE, against the final +prospective program, so a port may name a fresh node or a proposed node which +CSE-reuses an older one. Scope application CSE preserves one output identifier +per proposal occurrence while appending each genuinely fresh binding once. + For every suggestion which still has retained capacity, reply admission first resolves its complete uncapped draft, checks operation arities and domains, -topological order, scope visibility and equality endpoints, and applies the -same CSE rule used by final admission. Only after that full structural check +topological order, scope visibility and equality endpoints, validates every +old and proposed scope through the owning package, and applies the same CSE +rule used by final admission. Only after that full structural check does it compare `maxNodeDepth` with the freshly appended depth suffix; existing program depths were validated when their snapshot was created. A malformed request returns the named `ReplyError.malformedProposal` and invalidates the @@ -711,26 +840,38 @@ rather than rerunning structural validation. Losing an instantiation marks policy completeness false, so the filtered reply cannot manufacture saturation. Once retained capacity is exhausted, the remaining suffix is dropped without structural validation, as it cannot enter live state. Full -admission revalidates a selected proposal against the current -append-only program before atomically updating consumer and rule indexes and -retaining opaque recipe identifiers. Policy view construction consequently -checks freshness and engine-owned generation without repeating draft -resolution. +admission revalidates a selected proposal against the current append-only +network before atomically appending bindings, applications, consumers, facts, +equalities, and opaque recipe identifiers. Policy view construction checks +freshness, the current package veto, and engine-owned generation. Whether a +future implementation caches a sealed validation witness instead of repeating +this bounded check is an optimization question. The request has no package-claimed generation field. Policy sees the engine-computed generation in the semantic offer key, and the accepted instance records that same value for replay. Production must freeze every referenced recipe value before replay. Base nodes have theorem-instantiation -generation zero. The production representation may record generation per -theorem instance or per generated product; that choice remains open below. In -either case, a new expression is not trusted merely because a trigger matched. - -The authoritative references are the action substitution and old nodes named -explicitly as existing inputs by proposed drafts or equalities. A proposed node -remains an output of the theorem instance when it CSE-hits an already -materialized node: storage reuse cannot manufacture a proof dependency. Thus -the same append-stable proposal has the same logical generation before and -after an unrelated CSE-producing extension. +generation zero. Every application exposes an immutable creation generation; +whether that value is stored inline or derived from its immutable origin event +is a physical representation choice. Assigning one event generation to all +new products or retaining finer per-product provenance remains open. In either +case, a new expression is not trusted merely because a trigger matched. + +The authoritative recurrence starts from the generation frozen into the +application which emitted the action. It then takes the maximum with the +action substitution, old nodes named explicitly by proposed drafts, +equalities, or scopes, and old nodes reached when a proposed equality endpoint +or scope port CSE-resolves to existing storage. Explicit structural equality +and application inputs contribute the creation generation of their own +network events. A proposed expression used +only as an output remains an output of the theorem instance when it CSE-hits +an already materialized node: storage reuse alone cannot manufacture a proof +dependency. Once that resolved expression becomes an equality endpoint or +scope port, however, later propagation may consume the old fact, so its +generation is causal. Freezing the application's creation generation is also +essential for a scope-only causal chain whose next scope mentions only +generation-zero nodes; the second event still has generation two and is +rejected by an exact generation-one cap. The current centered-product D2 vertical is deliberately narrower than this general recurrence. Its `Center.inferredGeneration` only recognizes one @@ -745,14 +886,106 @@ The general propagation experiment uses the same admission boundary with opaque operations. A selected proposal is resolved against an immutable operation table, checked for typed SSA order, CSE'd against old and newly proposed nodes, assigned an engine-recomputed generation, and committed -atomically with rebuilt rule and watcher indexes. Its two-step canary adds -`g (f x)` and then `h (g (f x))`; newly registered rules run through the +atomically to an append-only application arena. The reference trace schema +`v0` orders startup scoped bindings before node-major/rule-minor local +applications, then orders each event's fresh scoped applications before local +applications induced by that event's new node suffix. This exact within-event +order is a versioned encoding choice, not a mathematical invariant: a future +schema may choose another deterministic order if it records and replays the +event delta. Every older `ApplicationId`, dirty bit, pending action, and policy +clock remains fixed. Watcher arrays may be rebuilt in the +prototype, but every old dependency entry remains in its old relative order; +a new application may appear before an older equality watcher, so prefix +stability is neither promised nor required. Its two-step canary adds +`g (f x)` and then `h (g (f x))`; newly compiled applications run through the ordinary request/reply path, producing generations one and two. Exact node, generation, structural-depth, application, queue, instance, equality, and proposal-list limits are independent, and failure retains the preceding -snapshot. The current hot storage uses linear reference CSE and rebuilds -indexes after an extension; that validates the state transition but does not -select the production CSE or incremental-index representation. +snapshot. The current hot storage still uses linear reference and application +CSE and may rebuild watcher indexes; that validates the state transition but +does not select the production CSE or incremental-index representation. It +must never recover the application arena by recompiling the binding log: +dynamic scopes and same-event local applications interleave, and creation +generation is application data. + +Several representation questions deliberately remain open: whether every +scope needs an anchor, whether the package veto is a Boolean or a typed bounded +match certificate, whether a package may canonicalize more bindings than exact +ordered identity, how watcher indexes become incremental, and how an obsolete +dynamic application is tombstoned without recycling its identifier. None of +these choices should constrain the replaceable policy for propagation, +strengthening, instantiation, or subdivision before measurements require it. + +#### Structural matching and instantiation triggers + +Instantiation is a first-class bounded producer of network structure, not a +special callback convention. A package may register a structural watch for an +anchor operation, one or more newly added operation keys, an equality or +constraint class, a bounded compiled pattern, or the whole-network fallback. +The exact pattern language remains experimental; the following behavior does +not: + +In `v0`, a structural matcher is an ordinary concrete application, usually +with `ActionKind.instantiate`. It has a stable `ApplicationId`, anchor, and +structural-watch declaration, and its structural wakeups enter the same +queue, `Action`, freshness, policy, and resource accounting as fact-driven +work. A future separate `MatcherId` is possible only if work-item identity, +budgets, replay, and scheduling are extended explicitly; there is no hidden +side scheduler. + +1. The engine wakes a matcher with an immutable network version and either the + relevant append delta or a bounded snapshot view. The delta contains stable + identifiers for newly visible nodes, equalities, and applications. +2. For a compiled matcher, the engine owns the cursor, visited-key accounting, + and exhaustion bit. The package supplies semantic filtering and proposals + for engine-enumerated bindings. An unrestricted package callback may return + a bounded batch and a continuation hint, but its own cost or completeness + claim is not trusted. +3. The engine derives a stable, versioned exact structural key from each + resolved match and its complete structural footprint; a package family + label is bounded metadata only. Any old node which influences the match occurs as an + anchor, declared fact read, or explicit reference in the proposal. A used + equality or application is likewise an explicit structural input to the + originating action/event, with its stable identifier and creation version + or generation. Admission checks that it is already visible, the causal + recurrence includes it, and proof slicing retains its creator and evidence. + Hidden traversal cannot create an unrecorded generation, freshness, or + replay dependency. +4. One match may atomically propose expression nodes, equality edges, and + arbitrary-scope applications. This is the instantiation mechanism needed + when the appearance of one shaped expression makes another expression or a + coordinated contractor useful. +5. The engine resolves references, performs CSE, validates package-owned + bindings, and deduplicates the exact structural result. Matcher-provided + identifiers, costs, completeness claims, and proof payloads are never + admission authority. A callback establishes exhaustion only through an + engine-checkable bounded enumeration certificate. +6. If fuel, traversal, retention, or capacity prevents the remaining match + suffix from being considered, that wakeup is incomplete. An empty queue is + not reported as propagation closure until every closure-relevant matcher + wakeup is complete or its omitted work has been proved redundant. + +An unexhausted engine cursor re-enqueues the same matcher application without +waiting for another fact or network change. The cursor epoch participates in +offer freshness and resource state. If admitting one batch extends the +network, the next action must either advance an append-stable certified cursor +or restart under the new snapshot while remembering already resolved keys; it +must not loop forever on the first CSE duplicate. Restart versus incremental +advance remains an experiment, but losing the unseen suffix is recorded as +incomplete. + +For a fixed snapshot, delta, engine cursor, and budget, certified enumeration +is deterministic. The engine may index watches by operation key or compiled +pattern, but it must preserve the same match stream and exact accounting as a +bounded reference enumerator. `ProgramView` is the current expression-only +oracle for discovering useful hints, but a raw whole-view callback does not by +itself establish exhaustive closure; +equality- and application-sensitive watches receive their matched stable IDs +through the separate network-delta interface rather than gaining unrestricted +fact access. Selective indexes, cached bounded match certificates, and +incremental e-matching are experiments against this contract. Integration +with `grind` is deliberately outside the present plan, although the trigger +and cursor model is designed so such a frontend need not change the engine. For inspection and mutation-cost experiments this provisional `Engine` is an exposed record. Consequently, its raw module does not enforce an authority @@ -761,14 +994,17 @@ production engine must hide its constructor and expose checked observations and transitions; making one transition opaque would not provide that encapsulation and would obstruct ordinary-kernel theorems about admission. -One atomic theorem instantiation initially assigns a single instantiation -generation to all helper nodes it introduces: one plus the maximum generation -of every node in the authoritative action substitution or explicitly named as -an existing input by a draft or equality. Proposed products are outputs, even -when CSE reuses their storage, so selection order cannot raise their logical -generation or change success at an exact generation cap. This measures -theorem-instantiation depth rather than expression-tree depth. Per-product or -multiple-provenance generation remains a possible refinement. +One atomic theorem instantiation initially has one event generation: one plus +the maximum of the emitting application's creation generation and every node +in the authoritative action substitution or explicitly named as an existing +input by a draft, equality, or scope after resolution, together with every +explicit structural input's creation generation. The event records that +generation, and every newly created node and application receives it. Proposed +products are outputs even when CSE reuses their storage, so selection order +cannot raise their logical generation or change success at an exact generation +cap. This measures theorem-instantiation depth rather than expression-tree +depth. Per-product or multiple-provenance generation remains a possible +refinement. Structural expression depth is a separate engine invariant: nullary nodes have depth zero; every fresh non-nullary node has one plus the maximum depth of its @@ -786,17 +1022,29 @@ plan and records the lost instantiation as incomplete. Depth is only the first recoverable per-suggestion refusal. The contractor experiment must classify resource limits by ownership: a malformed proposal invalidates its reply; a valid proposal which is individually unaffordable -under a configured local node, equality, application, or queue allowance may -be dropped with an exact reason while independent candidates commit and the -scope becomes incomplete; exhaustion of storage already consumed by the live -branch may remain a hard engine-resource stop. In particular, a multi-node -function instantiation should not terminate an otherwise useful reply merely -because it crosses `maxNodes` when the same situation can be identified before -retention. The exact split among `maxNodes`, `maxInstances`, `maxEqualities`, -`maxApplications`, and `maxQueueEntries` is an implementation experiment, but +under a configured local node, equality, scope-port, application, or queue +allowance may be dropped with an exact reason while independent candidates +commit and the scope becomes incomplete; exhaustion of storage already +consumed by the live branch may remain a hard engine-resource stop. In +particular, a multi-node function instantiation should not terminate an +otherwise useful reply merely because it crosses `maxNodes` when the same +situation can be identified before retention. The exact split among +`maxNodes`, `maxInstances`, `maxEqualities`, `maxApplications`, +`maxScopeNodes`, `maxStructuralInputs`, and `maxQueueEntries` is an implementation experiment, but every limit has one documented disposition and no refused narrowing work may be mistaken for saturation. +`maxScopeNodes` independently bounds each ordered read list and each ordered +write list; local slots remain bounded by operation arity. +`maxStructuralInputs` independently bounds the equality/application footprint +retained by one matcher action, offer, and replay event. +`maxProposalItems` separately bounds the number of proposed scopes. Start-time +count and port envelopes are checked before structural or package-specific +scope validation. Oversized dynamic syntax is rejected before retention; +policy-view semantic-surface exhaustion is a distinct policy resource result. +Generated-scope metrics count applications actually appended, not repeated or +CSE-reused proposal outputs. + The general experiment activates proposed equality edges as indexed, replayable search contractors: improving either endpoint wakes transport in the other direction, and admission of a new edge considers both current @@ -900,15 +1148,35 @@ the same endpoint pair with different scopes or proof costs. A production table may separate one canonical transport link from several evidence records; the first experiment may retain the first deterministic evidence. +Each replay-facing instance event also records the exact resolved scope +bindings in proposal order, the fresh binding subset, `scopeOutputs` in +proposal order (including CSE hits and repetitions), and +`newScopeApplications`. Local applications induced by the event's fresh node +suffix are reconstructed as `newLocalApplications`. In trace schema `v0` the +exact next arena suffix is + +```text +newScopeApplications ++ newLocalApplications +``` + +An append-only binding audit log alone is insufficient: dynamically created +scopes and local applications interleave, and every application exposes an +immutable creation generation. Replay must reject a binding/application +mismatch, a forged output identifier, a moved old identifier, a wrong local +suffix, or a claimed fresh application which is not the next arena entry. + Structural instance identity includes canonical unordered equality endpoint -pairs as well as the originating rule, engine-derived substitution, and -resolved products. An untrusted family label remains replay metadata but does -not manufacture a new network extension. Equality resolution +pairs and the exact resolved scope-binding list, as well as the originating +rule, engine-derived substitution, and resolved products. An untrusted family +label remains replay metadata but does not manufacture a new network +extension. Equality resolution returns the identifiers of reused links as well as newly appended links, so a pure-equality instance is replayable and cannot collide with an empty -extension. If every proposed node CSE-hits and every equality already exists, -admission reports a duplicate without advancing the program snapshot or -consuming an instance slot. Scope becomes part of this identity when branches are introduced. +extension. A fresh scope-only application is likewise a real extension and +may return an empty new-node list. Only when every proposed node CSE-hits, +every equality already exists, and every proposed scope application already +exists does admission report a duplicate without advancing the propagation- +network version or consuming an instance slot. Structurally admitted equality evidence is search-active but not trusted: failure to reconstruct it rejects the eventual proof, just as a malformed function-rule payload does. @@ -926,11 +1194,14 @@ reference checker rather than a production storage decision. The next general trace representation exposes an endpoint-erased structural skeleton. It records operation tags and operand references, literal slots, trigger provenance and recomputed generations, proposal/deduplication keys, -equality edges, derivation references, caller-bound source/target slots, and -structural budgets, but not endpoint values. Endpoint backends may be compared -only when their accepted certificates erase to the identical skeleton. This -prevents Core rational normalization or dyadic projection cost from being -misreported as scheduler or storage cost. +equality edges, exact scope bindings, scoped and local application identifiers +and creation generations, derivation references, caller-bound source/target +slots, and structural budgets, but not endpoint values. Its independent caps +include scope count, scope-port count, application-arena size, and network- +event count, together with structural inputs per action/event. Endpoint backends may be compared only when their accepted +certificates erase to the identical skeleton. This prevents endpoint-specific +normalization or projection cost from being misreported as scheduler or +storage cost. Production experiments compare exact-index array, arena, and chunked layouts against the list reference in both compiled and ordinary-kernel replay. Every @@ -941,9 +1212,10 @@ storage steps remains empirical, but a certificate-supplied cost is never trusted. Instantiation is explicitly budgeted by new nodes, new equality edges, rule -applications, theorem-generation, structural node depth, and retained payload -bytes. A canonical key consisting of the rule, substitution, scope, and -generated expression prevents duplicate instances. Candidate traversal and +applications, ordered scope-port length, theorem-generation, structural node +depth, and retained payload bytes. A versioned exact structural key consisting of the rule, +substitution, contractor bindings, and generated expression/equality outputs +prevents duplicate instances. Candidate traversal and insertion order are deterministic. If a branch-local fact triggers a semantically branch-independent expression, the node may be shared globally while the resulting fact and conditional equality remain branch-scoped. @@ -954,16 +1226,16 @@ The initial feasibility comparison has three arms: 1. eagerly materialize every alternate admitted by the node/form budgets; 2. run bounded instantiation between propagation epochs, then validate and - freeze a new program snapshot; + freeze a new network snapshot; 3. append nodes lazily during search with incremental dependency updates. The corpus measures program size, duplicate instances, useful-instance ratio, search time, and replay size. Safe budget exhaustion leaves the already -validated program and facts usable. +validated network and facts usable. #### Instantiation certificate boundary -The proof-facing checker treats the proposed program extension, recipe +The proof-facing checker treats the proposed network extension, recipe witnesses, equality edges, propagation facts, and selected result index as untrusted certificate data. The caller separately supplies the immutable base snapshot boundary, initial source rows, requested target row, and every @@ -1050,6 +1322,42 @@ precision ladder against its arithmetic endpoint-height limit; otherwise a configuration known in advance to exceed the backend limit is rejected at start rather than advertised as compatible. +Every scoped handler also supplies a package-owned binding preflight; the +production default is fail-closed. `Registry.acceptsBinding` routes a concrete +binding through its exact `RuleKey`, checks that the flattened registration +still agrees with the owning handler, and invokes that package predicate. A +checked session installs the routed predicate in the engine, so the same veto +governs start-time bindings, reply retention, policy-key refresh, and final +dynamic admission. The current reference rechecks every existing binding +against every prospective final program rather than silently assuming that +the predicate is append-monotone. This is fail-closed and useful for finding +bad package assumptions, but it is not a satisfactory production composition +rule: one non-monotone package could otherwise veto every unrelated extension. + +Generic structural validation and package validation are independent. The +generic engine checks identifiers, port uniqueness, head compatibility, +visibility, and resource limits; the owner decides whether that exact ordered +projection instantiates its contractor schema. This Boolean veto is search +admissibility, not proof. Replay receives the exact binding and reconstructs +the package theorem. Package validation has its own traversal/fuel charge and +may inspect only its declared bounded structural footprint; an uncharged +whole-program scan is not permitted. + +Before the binding API is frozen, experiments must choose at least one +compositional contract: + +- an accepted binding carries a bounded footprint and an append-stability + theorem or sealed match certificate, so unrelated extensions preserve it; + or +- extension may invalidate and tombstone an application through an explicit + replayed transition, with stable identifier, watcher, queue, and + completeness semantics. + +Rechecking a bounded certificate, requiring a package monotonicity theorem, +and replacing the Boolean veto with a typed binding witness remain open +representations of the first contract. Tombstoned identifiers are never +recycled under the second. + `Registry.invokePlanned` cross-checks the flattened registration, routed handler metadata, and structural projection of an engine-produced request before entering the callback, then replaces only the selected package's cache. It @@ -1116,22 +1424,31 @@ valid only when every retained payload remains covered by the exact old versioned schema. Kernel replay does not trust or unfold the opaque compiled search session. -The tactic must quote an explicit trace containing chronological program -snapshots, instance events, equality edges, fact events, and the frozen arena. +The tactic must quote an explicit trace containing chronological network- +extension events, the application arena or equivalent checked +deltas, equality edges, fact events, and the frozen payload arena. A scope-only +event may retain the identical expression program while advancing the network +version. A transparent `KernelRegistry` is checked directly against the immutable executable package declarations. Its constructor is intentionally not a soundness boundary: even a forged table cannot manufacture `Evidence`, because each existential schema must return a proof whose dependent type contains the exact decoded context. The transparent forward checker verifies base/final -program binding, prefix extensions, every instance and equality payload, -fact-version and previous-link chronology, action inputs from the already -proved prefix, package rule entailment, fact-domain meet evidence, equality -transport, and a domain-owned implication from the strongest installed fact -to the possibly weaker requested target. - -Replay retains every instance schema's `Extends before after` theorem and -composes the chronological chain rather than treating those proofs as -validation-only acknowledgements. The fact-domain interface supplies the one +program binding, expression-prefix extensions, every network-event delta, +scope binding, scoped/local application suffix, creation generation, instance +and equality payload, fact-version and previous-link chronology, and action +inputs from the already proved prefix. Before invoking a package theorem for a +fact, it resolves the action's exact application and binding and checks that +the application already existed. It then checks package rule entailment, +fact-domain meet evidence, equality transport, and a domain-owned implication +from the strongest installed fact to the possibly weaker requested target. + +Replay retains every instance schema's expression-level +`Program.Extends before after` theorem and composes the chronological chain +rather than treating those proofs as validation-only acknowledgements. A +scope-only or equality-only event may have reflexive `Program.Extends`, but its +network delta is still checked and advances application/equality chronology. +The fact-domain interface supplies the one locality law needed at this boundary: for valuations which model the old and extended programs, a fact about an in-bounds old node has the same meaning when the two valuations agree at that node. @@ -1154,22 +1471,23 @@ concrete base valuation and derives the ordinary inequality `x * (1 - x) ≤ 1/4`, preventing a vacuous model encoding from passing as an end-to-end theorem. -Program extension currently appends nodes only. Every operation signature a -package may instantiate, including an auxiliary operation unused by the base -node array, is declared in the frontend program's immutable operation table at -session start. Packages resolve its snapshot-local `OpId` from the stable -`OpKey`; neither package assembly order nor a hardcoded compact identifier is -authoritative. Dynamic operation-table growth remains an open design rather -than an implemented capability. +The expression `Program` currently grows only by appending nodes; one enclosing +network event may also append equalities and applications. Every operation +signature a package may instantiate, including an auxiliary operation unused +by the base node array, is declared in the frontend program's immutable +operation table at session start. Packages resolve its snapshot-local `OpId` +from the stable `OpKey`; neither package assembly order nor a hardcoded compact +identifier is authoritative. Dynamic operation-table or executable-registry +growth remains an open design rather than an implemented capability. This remains an experiment rather than the production checker. Its complete program snapshot per instance and repeated prefix scans are a correctness canary, not a scalable trace format; a delta-encoded, indexed replay experiment must measure and replace that representation. Trace-size and decoder-work -envelopes, exact generic reconstruction of instance -substitutions/products and per-event program-snapshot linkage, contradiction -certificates, split-tree composition, and the tactic quotation format are -still open. It is also an explicit +envelopes, exact generic reconstruction of instance substitutions/products, +binding outputs, scoped/local application suffixes, and per-event network +linkage, contradiction certificates, split-tree composition, and the tactic +quotation format are still open. It is also an explicit compatibility obligation—not a property enforced by the representation validator—that a different callback implementation under an existing versioned rule schema leave every retained payload semantically replayable. @@ -1230,7 +1548,7 @@ alternatives to compare once the behavior is established. The upgrade path is an indexed structural-watch declaration rather than a larger collection of booleans. Candidate watch classes include exact operation keys, bounded compiled patterns, equality or constraint additions, and a -whole-program fallback. Program extension records the bounded classes of its +whole-program fallback. Network extension records the bounded classes of its new structure and wakes only matching registrations; fact-dependent triggers still use their ordinary explicit fact reads. A compiled-pattern arm returns validated bindings and a bounded match certificate, while the full @@ -1239,8 +1557,9 @@ language, and index are experiments, but selective extension wakeup, deterministic bounded enumeration, and the unrestricted fallback are required capabilities. -1. The solver produces an `Action` naming a program snapshot, concrete rule - application, anchor, declared input fact versions, effort, and action kind. +1. The solver produces an `Action` naming a propagation-network snapshot, + concrete rule application, anchor, declared input fact versions, effort, + and action kind. 2. The external function-package registry executes the routed callback and owns its private cache; the Mathlib companion is responsible for semantic replay, not hot-loop dispatch. @@ -1271,7 +1590,7 @@ capabilities. to recover either from the extended program or narrowed current slots. Atomic multi-output replies have one exact proof contract. Every candidate in -the batch is interpreted against the same pre-reply program snapshot and exact +the batch is interpreted against the same pre-reply network snapshot and exact watched fact versions. Its replay schema proves the proposed fact from those facts and the program model independently of every other candidate in the batch. The engine then derives the installed fact by meeting that proposal with @@ -1504,10 +1823,11 @@ The protocol distinguishes the following actions. - `shave`: temporarily slice one input, run a bounded contractor on each slice, discard slices proved inconsistent, and return the hull of survivors with a local branch certificate. -- `instantiate`: propose validated new expression nodes and their proof - recipes from a matched shape. +- `instantiate`: propose one atomic set of validated expression nodes, + equalities, arbitrary-scope applications, and proof recipes from a matched + shape. - `rewrite`: activate a proved alternate expression and equality edge already - present in the current validated program snapshot. + present in the current validated network snapshot. - `regularize`: create bounded-height working views without deleting stronger facts. - `split`: create proof branches by adding complementary cuts for one node. @@ -1614,9 +1934,19 @@ existence certificate; a nonempty contracted box is not such a proof. Claims, fact candidates, and suggestions may share an atomic report, but each has independent payload coverage and resource accounting. -The base `Program` is static after validation. Generic cheap alternates may be -present before search, and `rewrite` only changes which form in the current -validated snapshot is scheduled. Adaptive range reduction or a Taylor +A constraint-producing registration declares an optional stable +`RelationKey`, copied into every concrete application's semantic key. An +`inner` report names that exact relation and is admitted only when it matches +the selected application; a bare numeric claim or a relation borrowed from a +different application is rejected before payload commit. Replay resolves the +same relation through the checked application and package schema before +applying the inner theorem. + +The caller's base `Program` prefix and operation table are static after +validation, while bounded network events may append expression nodes, +equalities, and applications. Generic cheap alternates may be present before +search, and `rewrite` only changes which form in the current validated snapshot +is scheduled. Adaptive range reduction or a Taylor polynomial may instead remain inside a rule-specific payload and return a fact about an existing node. Dynamic instantiation is never unchecked mutation: it uses the validation, dependency-update, scope, generation, and replay contract @@ -1672,10 +2002,10 @@ Each live branch contains: - the branch assumptions introduced by splits; - step, endpoint-height, trace-size, depth, and leaf counters. -A stronger fact enqueues only consumers and reverse rules that depend on the -changed side. The default implementation does not run repeated whole-program -passes. A pass remains a useful diagnostic grouping, but the algorithm is an -incremental worklist. +A stronger fact enqueues only the applications whose declared read list names +the changed node, together with equality work watching that node. The default +implementation does not run repeated whole-program passes. A pass remains a +useful diagnostic grouping, but the algorithm is an incremental worklist. The reference propagation queue coalesces a concrete application while it is already dirty. Several changed inputs therefore produce one registry call on @@ -1687,6 +2017,16 @@ suppressed work, and peak live queue before selecting a default. Multi-output outcomes install every accepted fact before waking this union, so they do not manufacture stale work against their own half-installed state. +The reference dependency index enumerates application watchers in ascending +stable `ApplicationId` order, followed by equality watchers in ascending +`EqualityId` order. Dynamic extension preserves every old watcher entry in its +old relative order, but not necessarily as a prefix: a new application may +appear before an older equality on the same node. This is a deterministic +index invariant, not a scheduling priority. New equality and application work +becomes eligible atomically; FIFO order remains a reference trace while an +external policy may rank propagation, retry, instantiation, refinement, and +subdivision through stable semantic keys. + Self-revisitation is explicit. Once an application is selected it is no longer marked queued; if its atomic reply strengthens a node that the same application reads, the ordinary dependency wakeup may enqueue it again. This is the safe @@ -1703,11 +2043,12 @@ whether it should remain only a policy hint followed by one confirming call, is an experiment. An unverified hint may affect priority but cannot justify a saturation result. -The initial `balancedV1` candidate runs all cheap forward rules once in program -order and then drains the dependency worklist. It also runs zero-cost -contradiction checks after every accepted fact. More expensive improvement and -split actions start only after this cheap fixed point, unless a rule marks a -singularity that requires an immediate split. This staging is policy behavior, +The initial `balancedV1` candidate runs all cheap forward rules once in +canonical initial application order and then drains the dependency worklist. +It also runs zero-cost contradiction checks after every accepted fact. More +expensive improvement and split actions start only after this cheap fixed +point, unless a rule marks a singularity that requires an immediate split. +This staging is policy behavior, not an engine soundness condition. Saturation is always relative to a named closure profile carried by the result. @@ -1765,14 +2106,17 @@ representation. ## Search policy The policy affects success and performance, never validity. In particular it -does not construct an `Action`: action serials, program snapshots, concrete -applications, and input versions are engine-owned authority. The engine owns a -bounded frontier of offers and the policy returns only the stable identity and -canonical key of one offer it observed. In the sketch below, -`InstantiationSemanticKey` is the payload-erased canonical family, -engine-computed generation, proposed-operation/reference graph, and unordered -equality-pair key. Replay-facing trigger metadata is deliberately absent; -`PolicyFeature` is a bounded exact integer key/value; and frontier events are +does not construct an `Action`: action serials, propagation-network snapshots, +concrete applications, and input versions are engine-owned authority. The +engine owns a bounded frontier of offers and the policy returns only the stable +identity and versioned exact structural key of one offer it observed. In the sketch below, +`InstantiationSemanticKey` is the payload-erased family, +engine-computed generation, ordered node and equality drafts, and ordered +proposed scopes. Each scope retains its rule, anchor reference, and ordered +reads and writes. The first version deliberately preserves proposal order; +canonical equivalence beyond exact binding identity remains an experiment. +Replay-facing trigger metadata is deliberately absent; +`PolicyFeature` is a versioned bounded exact integer key/value; and frontier events are engine-issued additions, refreshes, tombstones, and observations: ```lean @@ -1783,15 +2127,46 @@ structure PolicyKey where structure OfferId where index : Nat +structure RelationKey where + name : String + schema : Nat + +inductive StructuralInputKey + | equality (edge : EqualityId) + | application (application : ApplicationId) + +structure ApplicationSemanticKey where + rule : RuleKey + anchor : NodeId + binding : BindingKind + watches : List NodeId + writes : List NodeId + relation : Option RelationKey + structure InvocationKey where scope : ScopeId programVersion : Nat application : ApplicationId - rule : RuleKey - anchor : NodeId + semantic : ApplicationSemanticKey kind : ActionKind effort : Nat + generation : Nat inputs : List SeenVersion + structuralInputs : List StructuralInputKey + matcherEpoch : Option Nat + +structure ProposedScopeKey where + rule : RuleKey + anchor : NodeRef + watches : List NodeRef + writes : List NodeRef + +structure InstantiationSemanticKey where + family : Nat + generation : Nat + nodes : List ProposedNodeKey + equalities : List ProposedEqualityKey + scopes : List ProposedScopeKey structure EqualityWorkKey where scope : ScopeId @@ -1814,9 +2189,16 @@ inductive OfferKey | split (source : InvocationKey) (node : NodeId) (point : Dyadic) (reason : SplitReason) +inductive FeatureProvenance + | engineMeasured + | packageHint + structure PolicyFeature where - key : Nat - value : Int + owner : String + schema : Nat + field : Nat + provenance : FeatureProvenance + value : Int structure ObservationSummary where outcome : Nat @@ -1832,7 +2214,12 @@ structure EngineBudgetView where actions : Nat acceptedFacts : Nat nodes : Nat + applications : Nat equalities : Nat + retainedSuggestions : Nat + instances : Nat + queueEntries : Nat + generation : Nat branches : Nat structure FactDelta (Fact : Type) where @@ -1848,11 +2235,19 @@ inductive OutcomeTag | resourceLimit (budget : Nat) | failed (code : Nat) +inductive ClaimKind + | contradiction + | inner (relation : RelationKey) + +structure ClaimObservation where + kind : ClaimKind + schema : Nat + structure RuleObservation (Fact : Type) where invocation : InvocationKey outcome : OutcomeTag changes : Array (FactDelta Fact) - contradiction : Bool + claims : Array ClaimObservation cost : CostObservation suggestionPlan : SuggestionPlan emittedSuggestions : Array OfferId @@ -1922,13 +2317,32 @@ structure Policy (Fact : Type) where choose : PolicyBudget → State → PolicyStep State ``` +For structural matcher work, `structuralInputs` is the engine-derived exact +footprint, canonically ordered by input kind and stable identifier. It prevents +two matches over different equality/application evidence from sharing an +offer key. `matcherEpoch` identifies the engine-owned cursor epoch; an +unexhausted matcher requeue at unchanged fact/network versions therefore has +distinct freshness authority. Both fields are copied into the selected action +and replay event. Cursor internals remain engine state and are not trusted +proof data. + +Feature ownership is explicit. Engine-measured features—queue age, actual +fact changes, admitted structure, and charged work—cannot be forged by a +package. Package hints live in the package's stable namespace and schema and +are advisory only. A function package may expose incomparable method offers +for retry, refinement, instantiation, local shaving, or global splitting; +their effort and feature values need not share a scale with another package. +Changing a feature's meaning requires a schema change. Feature-count and +extraction-work caps apply before policy code sees the array. + The policy state, like rule-private caches, may have an arbitrary Lean type and is owned by the external driver. `Policy.State.select` rechecks the decision -serial, scope, program version, offer identifier, complete canonical key, -eligibility, and budgets. It alone freezes current input versions and creates -a registry `Action`, runs an engine equality contractor, admits a selected -instance, or emits an endpoint-resource-checked `SplitPlan`. The current driver -stops and returns that plan; it does not create branches or establish that the +serial, scope, network version, offer identifier, complete expected key, +eligibility, current package scope veto, and budgets. It alone freezes current +input versions and creates a registry `Action`, runs an engine equality +contractor, admits a selected instance, or emits an endpoint-resource-checked +`SplitPlan`. The current driver stops and returns that plan; it does not create +branches or establish that the point is interior. A future scope/branch layer must validate domain-specific interiority and construct complementary child assumptions. A stale, fabricated, or transplanted selection changes no facts, program, frontier @@ -1939,13 +2353,16 @@ Dirty concrete applications create or refresh invocation offers. Any structurally accepted bounded rule report may create engine-indexed retry, instantiation, and split offers; the policy cannot supply their structural payloads. Removing an offer emits a tombstone event, so stable identifiers do -not require an ever-growing live frontier. Program extension invalidates -exact-snapshot instantiation offers, refreshes dirty invocation offers, rechecks -retry and split offers under their variant-specific guards, and inserts offers -for new applications and equality jobs atomically with the extension. +not require an ever-growing live frontier. A network extension tombstones +`watchesProgram` exact-snapshot instantiation offers. Anchor-local +instantiation offers are revalidated and may survive when their application, +fact inputs, explicit references, and package binding remain fresh. The same +transition refreshes dirty invocation offers, rechecks retry and split offers +under their variant-specific guards, and inserts offers for new applications +and equality jobs atomically with the extension. A selected retry prepares a fresh action carrying the bounded effort override; it does not mutate the compiled application's registration baseline, so later -append-only program validation still compares an immutable application prefix. +append-only network validation still compares an immutable application prefix. Each completed rule selection produces an engine-owned observation containing the outcome class, actual admitted fact deltas, contradiction status, emitted @@ -1978,15 +2395,30 @@ checked against `maxObservationValue`; candidate, suggestion, and proposal counts have separate structural caps, and negative identifiers have their own diagnostic cap. The current event protocol has no general encoded-byte cap. -It may be cleaner to normalize the registry result as one bounded `RuleReport` -containing an outcome tag, candidate list, suggestion list, and cost. That +The semantic registry boundary is one bounded `RuleReport`, regardless of +whether the first Lean encoding uses one structure or several constructors. It +contains exactly: + +- one control outcome tag; +- an atomic list of proposed fact candidates; +- theorem-backed claims such as `contradiction` or `inner`; +- retry, refinement, instantiation, local-shaving, or global-split + suggestions; and +- exact logical cost observations. + +Every candidate, claim, and suggestion has independent role-specific payload +coverage. The complete report is structurally preflighted before any fact, +payload, suggestion, or cache-visible semantic state commits. This envelope allows `noChange` to recommend a stronger effort or landmark split without -encoding itself as `success` with no candidates. This is an open protocol -experiment; negative mathematical information is never inferred from a -resource limit or failed rule. An accepted `resourceLimit` or `failed` report -clears the request/reply latch and remains an exact policy observation, but it -also marks propagation incomplete: consuming that application did not -establish either successful contraction or mathematical inapplicability. +encoding itself as `success` with an empty candidate list. The physical sum +type, sharing between payloads, and support for explicit contractor +micro-traces remain open; the semantic fields and atomicity do not. + +Negative mathematical information is never inferred from a resource limit or +failed rule. An accepted `resourceLimit` or `failed` report clears the +request/reply latch and remains an exact policy observation, but it also marks +propagation incomplete: consuming that application did not establish either +successful contraction or mathematical inapplicability. Reply rejection, engine-resource exhaustion, or fact-domain-resource exhaustion has the same status when it clears the pending latch. A mismatched reply which preserves that exact pending action remains resubmittable and does @@ -2021,6 +2453,17 @@ The shown first interface supplies the authoritative bounded scan frontier in each `PolicyView`; transition events let the policy update historical state without reconstructing it. Its traversal budget is cumulative across views, not merely a per-view size check, and counts inactive backing slots honestly. +Fixed backing counts are checked before semantic-key construction. Validated +applications and retained proposals cache their logical key-surface counts, +so a one-step-short limit does not first walk a large scope. Live application +keys charge both ordered read and write projections; matcher keys also charge +their structural-input footprint and cursor epoch. Retained instantiation keys +charge their node/equality/scope records and nested references. This is a deterministic +logical semantic-surface budget, not a claim about compiler-level list visits, +package callback work, CSE work, or physical index maintenance; those require +separate declared counters and benchmarks. Generation remaining is computed +from committed instance events, so a scope-only or equality-only event is not +invisible merely because it created no node. The decision budget does not suppress a read-only view: after the last allowed decision the driver may still use its separately charged traversal budget to distinguish a genuinely empty frontier from live work that must be reported as @@ -2091,14 +2534,16 @@ discarded without that penalty remains an open policy question. Freshness is offer-specific. An invocation or retry compares the concrete application and relevant current input versions. An anchor-local rule remains fresh across an unrelated append-only extension. A `watchesProgram` rule also -requires the exact program version: extension stales its old offer and requeues +requires the exact network version: extension stales its old offer and requeues the application against the new snapshot. Instantiation shape is validated -before retention; offer construction rechecks freshness and authoritative -generation without resolving the draft again, and selection repeats full -admission against the current append-only program. A split compares its scope, -target fact version, and endpoint resource bound; an unrelated append-only -program extension need not stale it. Domain-specific interiority belongs to -the later scope/branch validator which constructs the complementary children. +before retention; offer construction rechecks freshness, current package scope +veto, and authoritative generation against the current resolved draft, and +selection repeats full admission against the current append-only network. +Caching a sealed equivalent witness is an open optimization. A split compares +its scope, target fact version, and endpoint resource bound; an unrelated +append-only network extension need not stale it. Domain-specific interiority +belongs to the later scope/branch validator which constructs the complementary +children. Proactive invalidation is an optimization, so selection always rechecks the conditions it owns. @@ -2198,12 +2643,13 @@ is only a reproducibility aid. The normative requirements on any release default are smaller than one particular scoring formula. -- For a fixed validated program, registry contents, configuration, and Lean +- For a fixed validated network, registry contents, configuration, and Lean environment, offer choice under a step budget is deterministic. - Candidate maps are traversed in canonical sorted order. The final tie-break - includes action kind, `NodeId`, versioned `RuleKey`, input fact versions, + compares the complete `ApplicationSemanticKey`, action kind, input fact + versions, structural inputs and matcher epoch, complete instantiation key, equality endpoints and endpoint versions, effort, generation, and split - point; hash-table order and freshly allocated identifiers are not + descriptor; hash-table order and freshly allocated identifiers are not tie-breakers. - Scores use bounded integer or exact arithmetic with specified saturation, never `Float` or host timing. @@ -2309,13 +2755,55 @@ free variable. Splitting a derived node is useful when several occurrences share that node, though contractors are needed to transfer the cut to its arguments. +#### Atomic branch transition: next framework milestone + +Returning a prepared `SplitPlan` is not the branch implementation. Before any +further rational-backend work, the framework must exercise one complete +branch transition and replay it. Selection of a plan performs one prospective +transaction: + +1. Recheck the parent scope, network version, target node, target fact version, + split descriptor, domain-owned resource envelope, and domain-specific + interiority condition. +2. Ask the fact/branch companion for complementary child assumptions and a + replay theorem showing that every parent valuation belongs to at least one + child. For real `v1`, these are `t ≤ m` and `m < t`; a future domain may use + a different opaque, versioned split descriptor. +3. Create both child scopes with explicit visibility watermarks for nodes, + equalities, applications, payloads, and facts. A child cannot cite a sibling + event or structure created after its watermark. +4. Define inheritance for function-package caches and policy state. Pure + performance caches may be copied, shared immutably, or reset; semantic + state must be represented by replayed network/fact events. No mutable cache + cell is shared unsafely between sibling searches. +5. Charge global branch/tree resources and each child's local queue, retained- + offer, instantiation, application, trace, and endpoint allowances before + either child becomes visible. Any failure leaves the parent and both child + identifiers uncommitted. +6. Record one branch event containing the parent snapshot, exact child + assumptions and scopes, split payload, and child identifiers. Replay checks + this event before consuming either child trace, proves every required child, + and combines their conclusions with the coverage theorem. + +Per-branch engine snapshots, persistent arenas, copy-on-write pages, and a +trail/rollback store remain comparison arms. The invariant is logical +isolation plus atomic creation, not a particular storage representation. A +global best-bound search additionally records which unconditional parent fact +or fully closed branch tree justifies the reported bound; it never exports a +fact conditional on only one child. + ### Budgets and termination Every search is finite because the configuration bounds: - reified base nodes, dynamically generated nodes and equality edges, - instantiation actions and generation depth, and alternate forms per original - node; + instantiation actions and scope-only causal generation depth, and alternate + forms per original node; +- scoped-application proposals, ordered read and write ports per scope, + concrete application-arena size, queue growth, and retained suggestions; +- structural-matcher wakeups, visited match keys, batch size, cursor storage, + bounded enumeration-certificate work, and structural inputs retained per + action/offer/event; - accepted actions; - rule invocations and maximum effort; - solver split depth and number of leaves; @@ -2324,6 +2812,7 @@ Every search is finite because the configuration bounds: precision; - retained trace nodes, frozen payload entries and bytes, kernel-checker work, and estimated proof nodes; +- cumulative policy decisions, live offers, and logical semantic-key surface; - optional wall-clock time. `maxEndpointHeight` is measured after canonical dyadic normalization as the bit @@ -2340,22 +2829,17 @@ numerator bits, encoded exponent bits, exponent magnitude, and actual shifted integer work so experiments can replace the aggregate metric without weakening the preflight resource guard. -Every backend in the D2 comparison implements a common exact endpoint-cost and -preflight interface. The rational candidate at minimum charges normalized -numerator and denominator bit lengths, predicts cross-multiplication and -regularization work before allocating the enlarged integers, and returns the -same distinct `resourceLimit` outcome when its configured bound is exceeded. -Backend-specific numbers need not be numerically identical to dyadic height, -but each must prevent an ostensibly small encoded exponent or denominator from +Every active endpoint backend implements a common exact endpoint-cost and +preflight interface. Backend-specific numbers need not be numerically +identical to dyadic height, but each must prevent a compact encoding from bypassing the actual arithmetic-work budget and must expose its components in telemetry. -For serialized rational certificates, entry counts and encoded integer byte -lengths are checked before arbitrary-precision decoding. After decoding, -numerator and denominator size checks precede the nonzero-denominator and -coprimality checks; no gcd, shift, or cross-product is attempted before its -input-size preflight. Per-operation temporary arithmetic and aggregate checker -work are budgeted separately from retained endpoint size. +If the deferred rational comparison resumes, its candidate additionally +charges normalized numerator and denominator sizes and preflights +cross-multiplication, gcd, regularization, encoded bytes, and decoder work +before allocation. Those requirements do not add rational operations to the +generic scheduler or gate the current framework profile. For the dyadic candidate, before an exact comparison or arithmetic action the engine computes the required alignment shift without performing it. If it @@ -2366,7 +2850,8 @@ may instead return a separately justified outward-regularized candidate within budget when regularization actually helps. Existing stronger facts are never deleted to satisfy the limit, and an oversized result is reported distinctly from `noChange`. The rational candidate applies the common exact-cost preflight -above to cross-multiplication and denominator growth instead. +above to cross-multiplication and denominator growth if that deferred +comparison resumes. Retained endpoint height and temporary arithmetic work are distinct limits. For subtraction, every endpoint-alignment pair needed by an interval rule is @@ -2377,7 +2862,8 @@ mantissa bit lengths and the signed sum of exponents before constructing the product, then checks the canonical result. Using the signed exponent sum is important: it admits cheap cancellation such as a tiny power of two times its inverse while still rejecting a genuinely oversized product. Comparable -preflight-before-allocation obligations apply to rational cross-products. +preflight-before-allocation obligations would apply to rational cross-products +in the deferred backend. Payload limits are enforced when an accepted recipe is frozen. Deduplicated tables are counted once in the immutable arena. A one-node derivation cannot @@ -2397,6 +2883,42 @@ do not close the original goal. `interval_bound` can therefore replay a real theorem from an `unknown` search; diagnostics never present a branch-local cut as a context-wide fact. +## Tactic and package frontend + +A user-visible function package contributes one coherent, versioned bundle: + +- stable `OpKey`s and their typed signatures; +- stable `RuleKey`s, local/scoped binding declarations, structural watches, + runtime callbacks, and bounded cache/configuration preflight; +- replay payload roles and decoders; and +- companion theorems proving every fact candidate, claim, instantiation, + equality, and split form the package may emit. + +The tactic assembles selected bundles first, then reifies the goal and local +hypotheses against their exact operation table. Reification performs shared +subexpression elimination, records open/closed/unbounded source facts, and +keeps unrecognized expressions opaque unless a caller supplies a sound source +fact for them. A package is never discovered recursively by typeclass search +while bounding a node. Attributes, explicit registry builders, and generated +bundle tables remain frontend experiments; the checked bundle snapshot and +stable keys are the semantic boundary. + +Search executes only the Mathlib-free callbacks. On success the tactic quotes +the caller-owned base program, source assumptions, requested target, selected +network/fact/branch events, and the backwards slice of frozen payloads needed +by that target. It does not quote failed probes, cache contents, discarded +offers, or the whole search state. The Mathlib companion reconstructs the +package theorems, composes conservative extensions and branch coverage, and +returns an ordinary proof term. Search execution, quotation, and replay have +separate budgets, and none may fall back to `native_decide`. + +Package upgrade is explicit: changing operation meaning, binding semantics, +payload decoding, or a replay theorem changes the corresponding schema. A +new implementation may retain a schema only when every old retained payload +has exactly the same meaning. This permits new enclosure methods and policy +features without making existing proof traces depend on the current default +search strategy. + ## Derivation trace The search log may be large, but the returned derivation is a backwards slice @@ -2417,27 +2939,57 @@ structure ClaimId where structure ConstraintId where index : Nat +structure ConstraintEntry where + relation : RelationKey + application : ApplicationId + inductive ClaimKind | contradiction | inner (constraint : ConstraintId) inductive EqualityRef - | edge (edge : EqEdgeId) + | edge (edge : EqualityId) | source (source : SourceId) +structure ActionRef where + scope : ScopeId + networkVersion : Nat + application : ApplicationId + kind : ActionKind + effort : Nat + generation : Nat + inputs : Array FactId + structuralInputs : Array StructuralInputKey + matcherEpoch : Option Nat + +structure NetworkEvent where + networkVersion : Nat + origin : ActionRef + family : Nat + generation : Nat + products : Array NodeId + newNodes : Array NodeId + equalities : Array EqualityId + newEqualities : Array EqualityId + bindings : Array ScopeBinding + newBindings : Array ScopeBinding + scopeOutputs : Array ApplicationId + newScopeApplications : Array ApplicationId + newLocalApplications : Array ApplicationId + payload : PayloadId + inductive Derivation | source (source : SourceId) - | rule (rule : RuleKey) (inputs : Array FactId) (payload : PayloadId) + | rule (action : ActionRef) (payload : PayloadId) | transportEq (equality : EqualityRef) (input : FactId) (target : NodeId) | weaken (input : FactId) (cut : Cut) | splitAssumption (parent : ScopeId) (side : SplitSide) (node : NodeId) (cut : Dyadic) structure ClaimDerivation where - rule : RuleKey - inputs : Array FactId - kind : ClaimKind - payload : PayloadId + action : ActionRef + kind : ClaimKind + payload : PayloadId inductive Close | goal (facts : Array FactId) @@ -2467,6 +3019,10 @@ bounded claim-derivation table. Closing from one replays its exact rule, request facts, relation identity, and payload. A contradiction claim closes the scope; an inner claim closes only the exact registered constraint or goal relation named in that leaf. A control outcome never creates a `ClaimId`. +The trace's checked constraint table maps each `ConstraintId` to a +`RelationKey` and concrete application. Inner-claim admission, application +semantic identity, and replay must all agree on that entry; the compact index +has no meaning by itself. `transportEq` preserves side, value, and strictness while moving a fact across a proved equality. Validation checks that the equality is visible in the @@ -2480,10 +3036,12 @@ contextual equality transfer have an explicit replay step. The branch tree refers to shared derivations. Facts established before a split are stored once in the ancestor scope. Within a branch, repeated uses of one fact refer to one identifier. Backwards slicing starts from every leaf's -`Close`, retains the necessary ancestor facts and split assumptions, and -discards all other probes. The Mathlib companion turns this representation -into nested `let`, `have`, and case bindings so Lean's elaborator and kernel -also see the sharing. +`Close`, retains the necessary ancestor facts, split assumptions, and creator +`NetworkEvent` for every referenced node, equality, and application, and +discards all other probes. A scope-only creator event therefore survives the +slice even though it introduced no expression node. The Mathlib companion +turns this representation into nested `let`, `have`, and case bindings so +Lean's elaborator and kernel also see the sharing. `ProofPlan.byContradiction` tells replay to introduce the negated target in a fresh counterexample scope before replaying its tree. Its `SourceId` cannot be @@ -2494,9 +3052,11 @@ best-bound certificate always uses `direct`, so a failed contradiction attempt cannot leak its temporary assumption. The trace never contains a proof of its own validity. It is untrusted data. -The companion registration for each `RuleKey` reconstructs the corresponding -theorem application or checks a rule-specific certificate. A trace is paired -with its immutable payload arena and operation table. Replay rejects an +The exact application named by a rule or claim derivation resolves its +`RuleKey`, anchor, ordered semantic ports, creation generation, and prior +creator event. The companion registration for that key reconstructs the +corresponding theorem application or checks a rule-specific certificate. A +trace is paired with its immutable payload arena and operation table. Replay rejects an unknown rule version, wrong payload schema, dangling payload identifier, or scope violation. @@ -2547,6 +3107,10 @@ honest interface rather than rendered as proved occupancy. An arbitrary-scope contractor may classify a whole tile or connected group of columns at once. An `inner` claim can discharge a universal region test, while a `present` pixel still requires the separate existence evidence above. +Adaptive tile creation may atomically append tile expressions and the scoped +contractor which consumes them; a scope-only event is useful when the tile +expressions already exist. The image certificate replays those binding events +rather than trusting renderer-created application identifiers. Pixel rectangles use an exact, documented boundary convention, preferably half-open cells with a separately closed outer viewport. Open cuts matter: @@ -2590,6 +3154,10 @@ coefficients and remainder, invariants, and event functions. Instantiation can introduce derivative and Taylor expressions only when a step method needs them; function-local refinement can subdivide a remainder calculation, while a solver split represents genuinely alternative state boxes or event cases. +The same event may install a Picard, Jacobian, invariant, or event contractor +over newly introduced expressions. Long chains of slabs and event scopes +therefore exercise append-stable applications and causal generation even when +one step adds no new scalar expression. The eventual ODE companion remains responsible for the mathematical theorems: existence, uniqueness when claimed, enclosure of the solution tube, and @@ -2608,7 +3176,7 @@ This downstream use argues for keeping the present abstractions: either through vector/box facts or coordinated scalar nodes; - operation keys and propagator caches must remain opaque to the scheduler; - expression instantiation, equality transport, scoped facts, and exact - resource limits must work over many consecutive program extensions; and + resource limits must work over many consecutive network extensions; and - policy observations must distinguish local refinement from global branching and proof cost from numerical gain. @@ -2619,18 +3187,38 @@ design with its own SPEC. ## Complexity contract -Let `n` be the number of program nodes, `e` the number of argument-to-consumer -edges, `q` the number of queued candidates, and `b` the number of live branch -states. - -- Program validation and initial dependency construction are `O(n + e)`. -- One worklist update is proportional to the number of rules attached to the - changed node and its consumers. The scheduler does not scan all `n` nodes - after every fact. +Let `n` be the number of program nodes, `r` the number of registrations, `a` +the number of concrete applications, `p` the total number of declared ports, +`m` the number of engine-enumerated structural candidate bindings, `s` the +number of installed scoped bindings, `q` the number of queued candidates, and +`b` the number of live branch states. + +- Once concrete bindings are known, dependency construction is proportional + to `a + p` plus equality endpoints. Binding discovery has its own declared + cost: the current simple local compiler scans node/registration pairs, and + the dynamic reference rebuilds watcher arrays after extension. A production + incremental index should update in proportion to newly appended + applications and ports while preserving the same stable identifiers and + deterministic watcher relation. +- A bounded reference matcher is proportional to the charged candidate keys + and structural references it visits, summarized by `m`; its cursor and + exhaustion certificate make that work explicit. An indexed matcher also + charges delta classification and index maintenance and must emit the same + stream. No package callback may hide an unbounded structural scan behind + one reported match. +- The current fail-closed admission arm rechecks `s` routed package binding + predicates plus their declared bounded footprint work against each + prospective program. Cached typed witnesses or proved append stability are + the experiments intended to make unrelated extension validation + incremental; this `O(s)` reference cost is reported until then. +- One worklist update is proportional to the applications and equality edges + watching the changed node. The scheduler does not scan all `n` nodes after + every fact. - Fact comparison and contradiction checks use exact endpoint comparison. For the dyadic candidate, integer cost is proportional to effective endpoint - height and the permitted exponent-alignment shift; a rational candidate must - declare and benchmark its corresponding exact-arithmetic cost. + height and the permitted exponent-alignment shift. A deferred rational + candidate must declare and benchmark its corresponding exact-arithmetic cost + when that comparison resumes. - Branch storage must make child creation and isolated updates cheap at the program sizes and leaf counts in the corpus; it must not silently copy all `n` fact slots at every split once that cost dominates. Candidate @@ -2727,34 +3315,11 @@ Lean's total inverse. These cases prevent a contractor translated from a conventional numeric library from erasing strict endpoints or silently replacing Lean's total inverse with a partial reciprocal. -### General conformance matrix +### Required framework conformance + +This profile gates the arbitrary-propagator engine independently of the +chosen endpoint backend. It includes: -- all four finite endpoint closure combinations; -- equal endpoints in all closure combinations; -- empty, singleton, one-sided unbounded, and whole intervals; -- table-driven empty laws: every unary operation and `regularize` preserve - empty; binary image operations and intersection absorb it; hull has it as an - identity; splitting it returns two empty pieces; `pow empty n = empty` even - at zero, while `pow I 0 = {1}` for every nonempty `I`; -- intersection and hull at equal open and closed cuts; -- split coverage at an endpoint and an interior point; -- negation and addition closure propagation; -- multiplication by singleton zero, by a nonsingleton interval containing - zero, and by unbounded intervals, with exact endpoint-attainment flags; -- the distinct cases `mul empty whole = empty`, `mul {0} whole = {0}`, and - `mul whole {0} = {0}`; -- `abs`, `min`, and `max` with tied open and closed extrema; -- precision-indexed reciprocal and division for `{3}`, positive, negative, - singleton-zero, one-sided-zero, and sign-crossing inputs; -- powers on negative, mixed-sign, open-zero, and singleton inputs; -- rational-to-dyadic projection at exact and inexact values, including the - strict cut gained by moving a closed source outward; -- canonical raw rational tables, including negative numerators and canonical - `0 / 1`, and rejection of zero denominators, noncoprime equivalent - encodings, unused oversized entries, excessive projection shifts, and - one-step-over-budget cross-products before allocation; -- regularization idempotence, outward containment, moved closed cuts, and - exact-grid open cuts; - a dependency worklist in which one fact wakes only the affected consumers; - opaque unary chains, fan-out with a ternary join, and forward/backward rule cycles in which the expression DAG remains acyclic; @@ -2763,6 +3328,23 @@ replacing Lean's total inverse with a partial reciprocal. - an atomic multi-output outcome, repeated-operand watcher deduplication, projected-input enforcement, and rejection of an undeclared write or a mismatched delayed reply without state mutation; +- start-time and dynamically proposed arbitrary scopes with nonlocal ordered + reads and writes, same-event node/equality/scope admission, a genuine scope- + only admission, immediate execution, self-revisitation, and exact package + veto of a structurally valid but semantically reordered projection before + retention and final admission; +- two successive dynamic admissions with proposal-order outputs containing an + existing scope, a fresh scope, and a repeated fresh scope; old application + identifiers and queue bits remain fixed, fresh scopes precede same-event + local applications, and a mixed equality/application watcher table preserves + every old entry as a subsequence rather than claiming prefix stability; +- one-step-short and exact scope-port, application, queue, generation, and + logical policy-surface bounds with complete rollback, including a generation- + one scope which proposes a distinct base-node-only scope and is rejected by + `maxGeneration = 1`; +- replay rejection of forged scope-binding/application-identifier pairs, + incorrect fresh subsets, and an action which cites an application before its + creation event; - package-major registry assembly with two handlers sharing a `Nat` cache, independently appended packages using `List Nat` and `Bool` caches, exact route and final-program signature checks, external required signatures, @@ -2800,6 +3382,18 @@ replacing Lean's total inverse with a partial reciprocal. depth-four proposal is dropped under an exact `maxNodeDepth = 3` cap without aborting unrelated rule processing; the raw driver reports queue saturation, not policy completeness; +- a structural matcher whose engine-owned cursor enumerates deterministic + multi-batch matches; one-step-short visit, cursor, batch, and certificate + limits preserve the cursor and mark closure incomplete, while an unsupported + package `complete` hint cannot manufacture saturation; +- reference and indexed matchers produce the same exact match stream, and an + equality/application-delta wake records those stable structural inputs, + includes their creation generation, and retains their creator events during + replay; +- one snapshot contains two useful structural matches; admitting the first + extends the network, after which the cursor/restart rule must still admit the + second or record its omission as incomplete, without repeatedly selecting + the first CSE duplicate; - one mixed reply in which a candidate fact, an affordable instantiation, and a later retry survive an over-depth instantiation between them; the loss is counted and policy completeness becomes false; @@ -2845,7 +3439,7 @@ replacing Lean's total inverse with a partial reciprocal. - derivation slicing that removes failed probes and unused facts; - branch validation that rejects sibling fact references and mutable or dangling payloads; -- program-extension validation that rejects bad topology, duplicate canonical +- network-extension validation that rejects bad topology, duplicate canonical keys, invisible branch-local nodes, invalid equality endpoints, and an instantiation beyond each generation budget; - deterministic deduplication of two rules proposing the same expression and @@ -2853,8 +3447,46 @@ replacing Lean's total inverse with a partial reciprocal. - two successive opaque instantiations which add absent expressions, activate their registered propagators, recompute generations one and two, and leave the previous snapshot intact at each one-step-short limit; +- one small sine package over an arbitrary caller-owned base prefix: an + initial forward enclosure, a stronger effort retry, a strict/open-endpoint + case, and a package-owned range-reduction or split suggestion all pass + through the ordinary arbitrary-propagator protocol; any introduced + expression, equality, or scope is replayed, and ordinary-kernel companion + replay proves the caller's real-valued target without `native_decide`; - budget exhaustion returning `unknown` with a nonempty diagnostic record. +### Required dyadic real-v1 conformance + +This separate profile instantiates the generic fact-domain interface used by +the first real-valued tactic. It does not define scheduler architecture: + +- all four finite endpoint closure combinations and equal endpoints in every + closure combination; +- empty, singleton, one-sided unbounded, and whole intervals; +- table-driven empty laws for unary and binary operations, intersection, + hull, splitting, and powers, including `pow empty 0 = empty` and + `pow I 0 = {1}` for nonempty `I`; +- intersection and hull at equal open and closed cuts; +- split coverage at an endpoint and an interior point; +- negation, addition, multiplication, `abs`, `min`, and `max`, including + zero, unbounded, tied-extremum, and endpoint-attainment cases; +- precision-indexed reciprocal and division for positive, negative, + singleton-zero, one-sided-zero, and sign-crossing inputs; +- powers on negative, mixed-sign, open-zero, and singleton inputs; and +- regularization idempotence, outward containment, moved closed cuts, and + exact-grid open cuts. + +### Deferred rational-backend conformance + +These tests are retained as a possible later backend comparison. They do not +gate the current framework, subdivision, or non-polynomial milestones: + +- rational-to-dyadic projection at exact and inexact values, including the + strict cut gained by moving a closed source outward; and +- canonical raw rational tables, including negative numerators and canonical + `0 / 1`, plus rejection of zero denominators, noncoprime encodings, unused + oversized entries, excessive shifts, and pre-allocation budget overflow. + The `ci` profile cross-checks finite arithmetic against an independent Python implementation using exact `Fraction` corner calculations and explicit endpoint-attainment flags. `python-flint` Arb is reserved for the companion's @@ -2869,10 +3501,10 @@ compiled fixture emitters and compare their serialized results outside Lean. ## Benchmarks -The Mathlib-free benchmark target measures: +### Framework benchmarks + +The active Mathlib-free benchmark target measures: -- `intersect`, `mul`, and `regularize` over effective endpoint height and - exponent-alignment distance; - worklist saturation over synthetic chain, fan-out, and shared-diamond programs; - bounded-instantiation saturation over useful, duplicate, and deliberately @@ -2886,13 +3518,23 @@ The Mathlib-free benchmark target measures: paged-trie, chunked-vector, and trail/rollback candidates, crossing program sizes 20, 50, and 500 with 8, 100, and 1,000 leaves; - policy selection over the number of available actions; -- derivation slicing over total log size and retained proof size; -- the same centered-product DAG under compiled Core `Rat` planning and - transparent canonical-table replay, separating planning, endpoint - interning, serialization, bounded decoding, table validation, and compiled - replay; an external build-only probe measures ordinary-kernel replay of the - same certificate, with dyadic-valued sources, `1 / 3`-valued sources, and a - denominator-height ladder. +- derivation slicing over total log size and retained proof size. + +### Dyadic real-v1 backend benchmarks + +- `intersect`, `mul`, and `regularize` over effective endpoint height and + exponent-alignment distance; and +- function-package replay cost over the same framework traces used by the + generic scheduler benchmarks. + +### Deferred rational-backend benchmarks + +When rational work resumes, a separate non-gating target may run the same +centered-product skeleton under compiled Core `Rat` planning and transparent +canonical-table replay, separating planning, endpoint interning, +serialization, bounded decoding, validation, and ordinary-kernel replay. Its +dyadic-valued, `1 / 3`-valued, and denominator-height cases do not block the +current framework or non-polynomial acceptance gates. The opaque-forest logical-count canary starts from a saturated set of disconnected unary chains and tightens one root. With four depth-eight chains, diff --git a/progress/20260729T091623Z.md b/progress/20260729T091623Z.md new file mode 100644 index 000000000..ea1b6754d --- /dev/null +++ b/progress/20260729T091623Z.md @@ -0,0 +1,33 @@ +# Interval arbitrary-propagator SPEC + +## Accomplished + +- Refocused the SPEC on the generic arbitrary-function framework and moved + rational conformance/benchmarks into a deferred, non-gating backend track. +- Specified the generic fact-domain boundary, arbitrary local/scoped + applications, dynamic instantiation, engine-owned structural matching, + exact network/application replay events, package-owned binding validation, + causal generation, and policy-surface accounting. +- Made one complete atomic branch transition and a replayed sine package the + next framework acceptance gates before any rational-backend milestone. +- Added tactic/package extension, verified-graph, ODE, and conformance + contracts while preserving open representation and scheduling questions. +- Rebuilt the experiment, end-to-end propagation, semantic replay, and policy + session targets successfully. + +## Current frontier + +The document now states the framework contract independently of dyadic or +rational arithmetic. The executable dynamic-scope experiment lives in the +stacked scope PR and its binding/application deltas still need to be consumed +by the generic replay implementation. + +## Next step + +Land the SPEC revision, then implement the engine-owned structural matcher +cursor and the atomic two-child branch transition before resuming endpoint- +backend comparisons. + +## Blockers + +None. From 47b4f8ffda9193597c01ceb2370767fbb52627d7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 29 Jul 2026 09:55:13 +0000 Subject: [PATCH 6/6] docs(interval): fix matcher generation contract Specify the frozen reference cursor and CSE-order independence. Progress: progress/20260729T095501Z.md --- HexInterval/SPEC/hex-interval.md | 42 ++++++++++++++++++++------------ progress/20260729T095501Z.md | 29 ++++++++++++++++++++++ 2 files changed, 56 insertions(+), 15 deletions(-) create mode 100644 progress/20260729T095501Z.md diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index e09afe166..4a4912427 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -860,15 +860,16 @@ case, a new expression is not trusted merely because a trigger matched. The authoritative recurrence starts from the generation frozen into the application which emitted the action. It then takes the maximum with the action substitution, old nodes named explicitly by proposed drafts, -equalities, or scopes, and old nodes reached when a proposed equality endpoint -or scope port CSE-resolves to existing storage. Explicit structural equality -and application inputs contribute the creation generation of their own -network events. A proposed expression used -only as an output remains an output of the theorem instance when it CSE-hits -an already materialized node: storage reuse alone cannot manufacture a proof -dependency. Once that resolved expression becomes an equality endpoint or -scope port, however, later propagation may consume the old fact, so its -generation is causal. Freezing the application's creation generation is also +equalities, or scopes. Explicit structural equality and application inputs +contribute the creation generation of their own network events. A proposed +expression remains an output of the theorem instance when it CSE-hits an +already materialized node, including when that proposed output is also an +equality endpoint or scope port: storage reuse cannot manufacture a proof +dependency or make the cap depend on admission order. A package which means +to depend on an already available node names it as `existing`, rather than +reconstructing it as a proposed output. Later fact propagation through an +equality or scoped application retains its own fact and application +provenance. Freezing the emitting application's creation generation is essential for a scope-only causal chain whose next scope mentions only generation-zero nodes; the second event still has generation two and is rejected by an exact generation-one cap. @@ -974,6 +975,17 @@ must not loop forever on the first CSE duplicate. Restart versus incremental advance remains an experiment, but losing the unseen suffix is recorded as incomplete. +The first reference-cursor arm freezes three append-only ceilings per epoch: +nodes, then equality edges, then concrete applications, each in ascending +stable-identifier order. Its constant-size cursor stores the exhausted prefix, +frozen ceiling, offset, epoch, and cumulative visits. A batch never scans past +that ceiling even if its first match causes network growth; after exhaustion, +renewal exposes exactly the appended suffix. Every enumerated input carries +its engine-owned creation generation, a one-short visit limit leaves the +cursor unchanged, and no package-facing field can assert exhaustion. This +transparent linear arm is a conformance oracle for later indexes, not a +commitment to scanning three full arrays in production. + For a fixed snapshot, delta, engine cursor, and budget, certified enumeration is deterministic. The engine may index watches by operation key or compiled pattern, but it must preserve the same match stream and exact accounting as a @@ -997,14 +1009,14 @@ encapsulation and would obstruct ordinary-kernel theorems about admission. One atomic theorem instantiation initially has one event generation: one plus the maximum of the emitting application's creation generation and every node in the authoritative action substitution or explicitly named as an existing -input by a draft, equality, or scope after resolution, together with every +input by a draft, equality, or scope, together with every explicit structural input's creation generation. The event records that generation, and every newly created node and application receives it. Proposed -products are outputs even when CSE reuses their storage, so selection order -cannot raise their logical generation or change success at an exact generation -cap. This measures theorem-instantiation depth rather than expression-tree -depth. Per-product or multiple-provenance generation remains a possible -refinement. +products are outputs even when CSE reuses their storage, including proposed +equality endpoints and scope ports, so selection order cannot raise their +logical generation or change success at an exact generation cap. This +measures theorem-instantiation depth rather than expression-tree depth. +Per-product or multiple-provenance generation remains a possible refinement. Structural expression depth is a separate engine invariant: nullary nodes have depth zero; every fresh non-nullary node has one plus the maximum depth of its diff --git a/progress/20260729T095501Z.md b/progress/20260729T095501Z.md new file mode 100644 index 000000000..f26142164 --- /dev/null +++ b/progress/20260729T095501Z.md @@ -0,0 +1,29 @@ +# Matcher cursor and CSE generation contract + +## Accomplished + +- Made theorem-instantiation generation independent of whether a proposed + output is stored freshly or CSE-reuses an older node, including proposed + equality endpoints and scope ports. +- Kept the emitting application's creation generation as an authoritative + input, so scope-only creation chains cannot reset their logical depth. +- Specified the first reference matcher arm: frozen node/equality/application + suffixes, engine-owned generations, cumulative visits, exact renewal, and no + package-provided completion claim. +- Rebuilt the experiment, end-to-end replay, semantic replay, and policy + session targets successfully. + +## Current frontier + +The SPEC now agrees with the dynamic-scope implementation fix and the +standalone matcher cursor experiment. + +## Next step + +Consume matcher inputs and cursor epochs in scheduler actions, policy keys, +generation inference, and replay events after the lower scope and proof stacks +are combined. + +## Blockers + +None.