RecipientExecution.lean

1 import MachineTheory.Recipient
2 
3 /-!
4 # Fixed recipient executions
5 
6 A recipient's run function takes only its own background and the common artifact.
7 The hidden case indexes required results and limits, not an extra interpreter input.
8 Outcome flags, returned work and peak-space counters belong to a stipulated finite
9 execution contract. This is not a universal semantics for arbitrary host software.
10 -/
11 namespace Komorebi.MachineTheory.RecipientExecution
12 
13 structure Result (Y : Type*) where
14   output : Y
15   work : ℕ
16   peakSpace : ℕ
17   deriving DecidableEq
18 
19 inductive Outcome (Y : Type*) where
20   | completed (r : Result Y)
21   | timeout
22   | malformed
23   deriving DecidableEq
24 
25 structure Audience (X C I : Type*) (B Y : I → Type*) where
26   background : ∀ i, X → B i
27   target : ∀ i, X → Y i
28   run : ∀ i, B i → C → Outcome (Y i)
29   permitted : I → X → C → Prop
30   workLimit : I → X → ℕ
31   spaceLimit : I → X → ℕ
32 
33 namespace Audience
34 variable {X C I : Type*} {B Y : I → Type*}
35 
36 /-- Each recipient must succeed on the SAME artifact with its INSTALLED interpreter. -/
37 def Accepts (R : Audience X C I B Y) (x : X) (c : C) : Prop :=
38   ∀ i, R.permitted i x c ∧ ∃ v,
39     R.run i (R.background i x) c = Outcome.completed v ∧
40     v.output = R.target i x ∧ v.work ≤ R.workLimit i x ∧
41     v.peakSpace ≤ R.spaceLimit i x
42 
43 theorem accepts_result (R : Audience X C I B Y) {x : X} {c : C}
44     (h : R.Accepts x c) (i : I) : ∃ v,
45     R.run i (R.background i x) c = Outcome.completed v ∧
46     v.output = R.target i x ∧ v.work ≤ R.workLimit i x ∧
47     v.peakSpace ≤ R.spaceLimit i x := (h i).2
48 
49 theorem no_timeout (R : Audience X C I B Y) {x : X} {c : C}
50     (i : I) (h : R.run i (R.background i x) c = Outcome.timeout) : ¬ R.Accepts x c := by
51   intro ha
52   obtain ⟨v, hv, _⟩ := R.accepts_result ha i
53   rw [h] at hv
54   cases hv
55 
56 theorem no_malformed (R : Audience X C I B Y) {x : X} {c : C}
57     (i : I) (h : R.run i (R.background i x) c = Outcome.malformed) : ¬ R.Accepts x c := by
58   intro ha
59   obtain ⟨v, hv, _⟩ := R.accepts_result ha i
60   rw [h] at hv
61   cases hv
62 
63 theorem no_work_overrun (R : Audience X C I B Y) {x : X} {c : C}
64     (i : I) (v : Result (Y i))
65     (hr : R.run i (R.background i x) c = Outcome.completed v)
66     (hcost : R.workLimit i x < v.work) : ¬ R.Accepts x c := by
67   intro ha
68   obtain ⟨w, hw, _, hc, _⟩ := R.accepts_result ha i
69   have he : w = v := Outcome.completed.inj (hw.symm.trans hr)
70   subst w
71   exact Nat.not_le_of_gt hcost hc
72 
73 theorem no_space_overrun (R : Audience X C I B Y) {x : X} {c : C}
74     (i : I) (v : Result (Y i))
75     (hr : R.run i (R.background i x) c = Outcome.completed v)
76     (hcost : R.spaceLimit i x < v.peakSpace) : ¬ R.Accepts x c := by
77   intro ha
78   obtain ⟨w, hw, _, _, hc⟩ := R.accepts_result ha i
79   have he : w = v := Outcome.completed.inj (hw.symm.trans hr)
80   subst w
81   exact Nat.not_le_of_gt hcost hc
82 
83 theorem no_permission (R : Audience X C I B Y) {x : X} {c : C}
84     (i : I) (h : ¬ R.permitted i x c) : ¬ R.Accepts x c :=
85   fun ha => h (ha i).1
86 
87 /-- The source theorem instantiated at output, permission and budget success. -/
88 theorem common_artifact_iff (R : Audience X C I B Y) {H : Type*} (α : X → H) :
89     (∃ f : Attained α → C, ∀ x, R.Accepts x (f (record α x))) ↔
90       ∀ h : Attained α, ∃ c, ∀ x, α x = h.val → R.Accepts x c :=
91   Recipient.encoder_exists_iff α R.Accepts
92 
93 /-- Minimum image and minimum meeting codebook coincide for actual fixed recipients. -/
94 theorem minimum_codebook [Fintype X] (R : Audience X C I B Y) {H : Type*} {α : X → H}
95     (h : Recipient.Feasible α R.Accepts) :
96     Recipient.minImageSize h = Recipient.minCoverSize h :=
97   Recipient.minimum_image_eq_cover h
98 
99 /-- Tightening a requirement can preserve or reduce feasibility, never create it. -/
100 theorem acceptance_monotone {H : Type*} (α : X → H) (ok₁ ok₂ : X → C → Prop)
101     (stronger : ∀ x c, ok₂ x c → ok₁ x c) :
102     Recipient.Feasible α ok₂ → Recipient.Feasible α ok₁ := by
103   rintro ⟨f, hf⟩
104   exact ⟨f, fun x => stronger x _ (hf x)⟩
105 
106 theorem minimum_monotone [Fintype X] {H : Type*} {α : X → H} {ok₁ ok₂ : X → C → Prop}
107     (stronger : ∀ x c, ok₂ x c → ok₁ x c)
108     (h₁ : Recipient.Feasible α ok₁) (h₂ : Recipient.Feasible α ok₂) :
109     Recipient.minImageSize h₁ ≤ Recipient.minImageSize h₂ := by
110   obtain ⟨f, hf, he⟩ := Recipient.minImage_attained h₂
111   exact (Recipient.minImage_le h₁ f (fun x => stronger x _ (hf x))).trans_eq he
112 
113 end Audience
114 end Komorebi.MachineTheory.RecipientExecution

Back to source controls