The explicit causal state machine refines the certified finite controller execution.

def V7.Stage8Main.reportsTrace {d : ℕ} (reports : List (TrialReport d)) : List (Observation d)

The chronological observation list obtained by concatenating the trial reports.

Equations

• V7.Stage8Main.reportsTrace reports = List.flatMap V7.TrialReport.trace reports

@[simp]

theorem V7.Stage8Main.reportsTrace_append_singleton {d : ℕ} (reports : List (TrialReport d)) (report : TrialReport d) : reportsTrace (reports ++ [report]) = reportsTrace reports ++ report.trace

theorem V7.Stage8Main.reportsTrace_length {d : ℕ} (reports : List (TrialReport d)) : (reportsTrace reports).length = (List.map (fun (report : TrialReport d) => report.calls) reports).sum

theorem V7.Stage8Main.first_action_query_of_exec_nonempty {d : ℕ} (trial : LocalTrial d) (oracle : PairOracle d) (M D : ℝ) (cached : CachedPair d) (report : TrialReport d) (hexec : trial.Executes M D cached oracle report) (hne : report.trace ≠ []) : ∃ (x : Point d) (next : Observation d → trial.State), trial.action (trial.initial M D cached) = LocalTrialAction.query x next

theorem V7.Stage8Main.localTrial_run_to_done {d : ℕ} (oracle : PairOracle d) (data : RuntimeData d) (state : RuntimeControllerState d) (pre : List (Observation d)) {localFuel : ℕ} {machineState : (runtimeTrial data state).State} {localHistory : List (Observation d)} {report : TrialReport d} {finish : RuntimeFinish d} : (runtimeTrial data state).runFuel oracle localFuel machineState localHistory = some report → controllerStep data state report = RuntimeControllerRunResult.success finish → ∃ (methodFuel : ℕ), (currentMethod d).runFuel oracle methodFuel (CurrentMethodState.localTrial data state machineState localHistory) (pre ++ localHistory) = some { returned := finish.returned, queries := pre ++ report.trace }

theorem V7.Stage8Main.localTrial_run_to_next {d : ℕ} (oracle : PairOracle d) (data : RuntimeData d) (state state' : RuntimeControllerState d) (pre : List (Observation d)) {result : O3.RunResult d} {tailFuel localFuel : ℕ} {machineState : (runtimeTrial data state).State} {localHistory : List (Observation d)} {report : TrialReport d} : (runtimeTrial data state).runFuel oracle localFuel machineState localHistory = some report → controllerStep data state report = RuntimeControllerRunResult.exhausted state' → (currentMethod d).runFuel oracle tailFuel (CurrentMethodState.controllerReady data state') (pre ++ report.trace) = some result → ∃ (methodFuel : ℕ), (currentMethod d).runFuel oracle methodFuel (CurrentMethodState.localTrial data state machineState localHistory) (pre ++ localHistory) = some result

theorem V7.Stage8Main.controllerReady_run_to_done {d : ℕ} (data : RuntimeData d) (state : RuntimeControllerState d) (pre : List (Observation d)) (inst : PositiveInstance data.input.p d data.input.x0) {spec : LocalRunSpec data state inst} {finish : RuntimeFinish d} (hstep : controllerStep data state spec.report = RuntimeControllerRunResult.success finish) : ∃ (methodFuel : ℕ), (currentMethod d).runFuel inst.oracle methodFuel (CurrentMethodState.controllerReady data state) pre = some { returned := finish.returned, queries := pre ++ spec.report.trace }

theorem V7.Stage8Main.controllerReady_run_to_next {d : ℕ} (data : RuntimeData d) (state state' : RuntimeControllerState d) (pre : List (Observation d)) (inst : PositiveInstance data.input.p d data.input.x0) {spec : LocalRunSpec data state inst} {result : O3.RunResult d} {tailFuel : ℕ} (hstep : controllerStep data state spec.report = RuntimeControllerRunResult.exhausted state') (htail : (currentMethod d).runFuel inst.oracle tailFuel (CurrentMethodState.controllerReady data state') (pre ++ spec.report.trace) = some result) : ∃ (methodFuel : ℕ), (currentMethod d).runFuel inst.oracle methodFuel (CurrentMethodState.controllerReady data state) pre = some result

theorem V7.Stage8Main.causalController_refines {d : ℕ} (data : RuntimeData d) (inst : PositiveInstance data.input.p d data.input.x0) (hcached : data.cached.observation = O3.PairOracle.observe inst.oracle data.input.x0) (hlarge : data.input.eps < lpNorm (conjugateExponent data.input.p) (inst.oracle.gradient data.input.x0)) (publicPrefix : List (Observation d)) {controllerFuel : ℕ} {state : RuntimeControllerState d} {finish : RuntimeFinish d} : runController data inst hcached hlarge controllerFuel state = RuntimeControllerRunResult.success finish → ∃ (methodFuel : ℕ), (currentMethod d).runFuel inst.oracle methodFuel (CurrentMethodState.controllerReady data state) (publicPrefix ++ reportsTrace state.reports) = some { returned := finish.returned, queries := publicPrefix ++ reportsTrace finish.reports }