Recover control activation from original durable publication

dev/proofs/lean/PublicationRecovery.lean

@@ -81,6 +81,20 @@ theorem recovery_and_provider_accounting_composition [DecidableEq Key]
   ⟨run_preserves_original_decisions run id decision original,
    (run_preserves_accounting h run).2.1, (run_preserves_accounting h run).2.2⟩
 
+/- A source observation binds the frozen command, not the current policy head.
+   Native refinement must authenticate InspectPublication and validate its full
+   domain-separated digest. Missing/failed reads do not establish abort. -/
+def ExactObservation (s : State Key) (id : Key) (payload parent fence : Nat) (d : Decision) : Prop :=
+  s.records id = some d ∧ d.payload = payload ∧ d.parent = parent ∧ d.requestedFence = fence
+
+theorem exact_observation_and_accounting_survive_recovery [DecidableEq Key]
+    {id : Key} {d : Decision} {payload parent fence : Nat}
+    (safe : Safe held calls s) (run : Run s t)
+    (observed : ExactObservation s id payload parent fence d) :
+    ExactObservation t id payload parent fence d ∧ t.held = held ∧ t.calls = calls := by
+  have preserved := recovery_and_provider_accounting_composition safe run observed.1
+  exact ⟨⟨preserved.1, observed.2⟩, preserved.2⟩
+
 /- Owned-connection refinement: the worker has opened one private connection;
    every command is checked quiescent before/after SQL, storage faults terminate
    the owner, and a successful finish requires an explicitly successful close.
@@ -161,4 +175,5 @@ theorem owned_worker_and_publication_composition [DecidableEq Key]
 #print axioms run_preserves_original_decisions
 #print axioms run_preserves_accounting
 #print axioms recovery_and_provider_accounting_composition
+#print axioms exact_observation_and_accounting_survive_recovery
 end Weaver.PublicationRecovery

dev/proofs/quint/AuthorityPublication.qnt

@@ -3,20 +3,24 @@ module AuthorityPublication {
   import PublicationRecovery as A from "./PublicationRecovery"
   // Go activation composes existing publication and execution models. It does
   // not redeclare their CAS, nonce, budget or Cedar semantics.
-  type Control={compiled:int,desired:int,registered:bool,ack:bool,active:bool}
+  type Control={compiled:int,desired:int,registered:bool,ack:bool,active:bool,submits:int}
   var c:Control
   val original=A::authority.records.get(0)
   val safe=E::safe and A::safe and
+    c.submits<=1 and
     (c.active implies c.compiled>=0 and c.registered and original.outcome==1 and original.payload==c.compiled and c.ack) and
     (A::authority.head>=0 implies E::s.revision==A::authority.head and E::s.fence==A::authority.fence)
-  action init=all {E::init,A::init,c'={compiled:-1,desired:0,registered:false,ack:false,active:false}}
+  action init=all {E::init,A::init,c'={compiled:-1,desired:0,registered:false,ack:false,active:false,submits:0}}
   // Concrete source admission is witnessed by Scheme/FFI/Go tests, not a
   // duplicate Boolean implementation of those validators in this model.
   action compile(accepted:bool):bool=all {accepted,c.compiled<0,c'=c.with("compiled",c.desired),E::observe,A::observe}
   action editSource=all {c'=c.with("desired",1),E::observe,A::observe}
   action register=all {c.compiled>=0,c'=c.with("registered",true),E::observe,A::observe}
-  action commit=all {c.registered,
-    any {A::publish(0,c.compiled,-1,1),A::replay(0,c.compiled,-1,1)},c'=c,E::observe}
+  // A known durable outcome is observed, never submitted again by bootstrap.
+  action commit=all {c.registered,original.outcome==0,
+    A::publish(0,c.compiled,-1,1),c'=c.with("submits",c.submits+1),E::observe}
+  action inspectMissing=all {c.compiled>=0,original.outcome==0,c'=c,E::observe,A::observe}
+  action inspectUnavailable=all {c'=c,E::observe,A::observe}
   action acknowledge=all {original.outcome==1,original.payload==c.compiled,c'=c.with("ack",true),E::observe,A::observe}
   action recover(source:int):bool=all {original.outcome==1,source==c.compiled,A::replay(0,source,-1,1),c'=c.with("ack",true),E::observe}
   action activate=all {original.outcome==1,c.ack,original.payload==c.compiled,c'=c.with("active",true),E::observe,A::observe}
@@ -31,18 +35,25 @@ module AuthorityPublication {
   action invoke=all {c.active,c'=c,E::invoke,A::observe}
   action release=all {c.active,c'=c,E::batch(1,0),A::observe}
   action deliver=all {c'=c,E::deliver,A::observe}
-  action step=any {compile(true),editSource,register,commit,acknowledge,recover(0),recover(1),activate,loseReply,restart,publish,transport,admit,consume,burn,invoke,release,deliver}
+  action step=any {compile(true),editSource,register,commit,inspectMissing,inspectUnavailable,acknowledge,recover(0),recover(1),activate,loseReply,restart,publish,transport,admit,consume,burn,invoke,release,deliver}
   action prepared=init.then(compile(true)).then(register)
   action ready=prepared.then(commit).then(acknowledge).then(activate)
   action spent=ready.then(admit).then(consume).then(burn).then(invoke)
   action unsafeRecoverDesired=all {original.outcome==1,c'=c.with("compiled",c.desired).with("ack",true).with("active",true),E::observe,A::observe}
   action unsafeActivateWithoutOutcome=all {c'=c.with("active",true),E::observe,A::observe}
   action unsafeRetry=all {c'=c,E::unsafeRetryReset,A::observe}
+  action unnecessaryKnownOutcomeReplay=all {original.outcome==1,A::replay(0,c.compiled,-1,1),c'=c.with("submits",c.submits+1),E::observe}
   run authorityUncompiledSourceCannotRegisterTest=init.then(register.fail())
   run authorityRejectedSourceCannotCompileTest=init.then(compile(false).fail())
   run authoritySourceCommitNeverSendsTest=prepared.then(commit).expect(safe and E::s.calls==0 and E::s.held==0)
   run authorityLostReplyCannotActivateTest=prepared.then(commit).then(loseReply).then(activate.fail())
   run authorityLostReplyAndOwnerRestartPreserveOutcomeTest=prepared.then(commit).then(loseReply).then(restart).then(recover(0)).then(activate).expect(safe and original.payload==0 and E::s.calls==0)
+  run authorityKnownOutcomeRecoveryDoesNotSubmitTest=ready.then(restart).then(recover(0)).then(activate).expect(safe and c.submits==1)
+  run authorityMissingInspectionDoesNotAbortLateCommitTest=prepared.then(inspectMissing).then(commit).then(recover(0)).then(activate).expect(safe and c.submits==1)
+  run authorityUnavailableInspectionDoesNotActivateTest=prepared.then(commit).then(loseReply).then(inspectUnavailable).expect(safe).then(activate.fail())
+  // Rust idempotent replay remains safe. This witnesses a violation of the
+  // narrower Go bootstrap contract: recovery of a known decision must be read-only.
+  run authorityKnownOutcomeReplayContractCounterexampleTest=ready.then(unnecessaryKnownOutcomeReplay).expect(not(safe) and A::safe and E::safe)
   run authorityChangedCompiledSourceCannotRecoverTest=prepared.then(commit).then(editSource).then(recover(1).fail())
   run authorityEditingFileCannotRewriteFrozenCommandTest=prepared.then(editSource).then(commit).then(acknowledge).then(activate).expect(safe and original.payload==0 and c.desired==1)
   run authorityHistoricalReceiptCannotOverrideRevocationTest=ready.then(publish).then(restart).then(recover(0)).then(activate).then(admit.fail())

dev/sysml/WeaverExecution.sysml

@@ -72,7 +72,13 @@ package WeaverExecution {
     action def Enqueue;
     action def Consume;
     action def GuardAndSend;
-    action def RecoverOutcome;
+    action def RecoverOutcome {
+        doc /* Go observes the Rust-owned durable result under the frozen
+           publication identity and digest before submitting an absent decision.
+           A known result is read-only recovery. Unknown or rejected results do
+           not activate ingress. A historical receipt never replaces current
+           Rust Policy, fence, original claim, history or budget checks. */
+    }
 
     part gateway {
         part semanticPublisher : SchemeSemanticPublisher;

docs/50-59-research-program/59-provider-rpc/59.03-provider-rpc-core.d2

@@ -99,7 +99,7 @@ provider: LLM Provider / SSE\nOne consumed HTTPS invocation {
   height: 110
 }
 source -> control: Governed config
-control -> source_rpc: Publication
+control -> source_rpc: Observe / initial CAS
 source_rpc -> owner: Policy / outcome CAS
 control -> rpc: Typed RPC
 rpc -> owner: Admit