Constant CERT_INT_DISPATCH_SOUNDNESS
Source pub const CERT_INT_DISPATCH_SOUNDNESS: &str = "import CertPrelude\nimport SchemaCore\nimport PlanCheck\nimport PlanLower\n\nset_option maxRecDepth 100000\nset_option maxHeartbeats 2000000\n\nnamespace IntDispatchSoundness\nopen CertPrelude AverCert.Schema\n\n/-! ### Semantic evaluator and family invariant -/\n\ndef evalLeaf : IntDispatchLeaf \u{2192} Int \u{2192} Int\n | .proj, x => x\n | .hostOp .add k true, x => k + x\n | .hostOp .add k false, x => x + k\n | .hostOp .sub k true, x => k - x\n | .hostOp .sub k false, x => x - k\n\n/-- `EvalCascade S body tag fields n` is the semantic meaning of one admitted\n dispatch input. It relates the byte-origin plan to the existing source\n model without inventing a decoder for the abstract Int carrier. -/\ninductive EvalCascade {C : Nat} (S : CarrierSpec C) :\n IntDispatchCascade \u{2192} Nat \u{2192} List WVal \u{2192} Int \u{2192} Prop where\n | default (k : Int) (tag : Nat) (fields : List WVal) :\n EvalCascade S (.default k) tag fields k\n | hit (tyIdx : Nat) (leaf : IntDispatchLeaf) (rest : IntDispatchCascade)\n (fields : List WVal) (x : Int) (v : WVal)\n (hfield : fields[0]? = some v) (hrepr : S.Repr x v) :\n EvalCascade S (.test tyIdx leaf rest) tyIdx fields (evalLeaf leaf x)\n | miss (tyIdx tag : Nat) (leaf : IntDispatchLeaf) (rest : IntDispatchCascade)\n (fields : List WVal) (n : Int) (hne : tag \u{2260} tyIdx)\n (hrest : EvalCascade S rest tag fields n) :\n EvalCascade S (.test tyIdx leaf rest) tag fields n\n\ntheorem evalCascade_hit_inv {C : Nat} {S : CarrierSpec C}\n {tyIdx : Nat} {leaf : IntDispatchLeaf} {rest : IntDispatchCascade}\n {fields : List WVal} {n : Int}\n (h : EvalCascade S (.test tyIdx leaf rest) tyIdx fields n) :\n \u{2203} x v, fields[0]? = some v \u{2227} S.Repr x v \u{2227} n = evalLeaf leaf x := by\n cases h with\n | hit _ _ _ _ x v hfield hrepr => exact \u{27e8}x, v, hfield, hrepr, rfl\u{27e9}\n | miss _ _ _ _ _ _ hne _ => exact False.elim (hne rfl)\n\ntheorem evalCascade_miss_inv {C : Nat} {S : CarrierSpec C}\n {tyIdx tag : Nat} {leaf : IntDispatchLeaf} {rest : IntDispatchCascade}\n {fields : List WVal} {n : Int} (hne : tag \u{2260} tyIdx)\n (h : EvalCascade S (.test tyIdx leaf rest) tag fields n) :\n EvalCascade S rest tag fields n := by\n cases h with\n | hit _ _ _ _ _ _ _ _ => exact False.elim (hne rfl)\n | miss _ _ _ _ _ _ _ hrest => exact hrest\n\n/-- The template\'s stack invariant at a block boundary: a successful sub-block\n leaves one represented result above the unchanged incoming stack. -/\ndef StackOK {C : Nat} (S : CarrierSpec C) (n : Int) (base : List WVal) :\n Option Out \u{2192} Prop\n | some (.ok _ (w :: rest)) => rest = base \u{2227} S.Repr n w\n | _ => False\n\n/-- A block has the same `StackOK`-preserving property at every nesting depth. -/\ndef BlockOK {C : Nat} (S : CarrierSpec C)\n (host : HostTbl) (ar : Nat \u{2192} Option Nat) (callee : Callee)\n (n : Int) (base : List WVal) (instrs : List WInstr)\n (locals : List WVal) (stack : List WVal) : Prop :=\n \u{2200} out, wRunF host ar callee instrs locals stack = some out \u{2192}\n StackOK S n base (some out)\n\ntheorem finishRun_nil\n (host : HostTbl) (ar : Nat \u{2192} Option Nat) (callee : Callee)\n (r : Option Out) :\n (match r with\n | some (.ok locals stack) => wRunF host ar callee [] locals stack\n | some (.ret value) => some (.ret value)\n | none => none) = r := by\n cases r with\n | none => rfl\n | some out => cases out <;> simp [wRunF]\n\ntheorem popArgs_one (a : WVal) (rest : List WVal) :\n popArgs 1 (a :: rest) = some ([a], rest) := by\n simp [popArgs, List.take, List.drop]\n\ntheorem popArgs_two (b a : WVal) (rest : List WVal) :\n popArgs 2 (b :: a :: rest) = some ([a, b], rest) := by\n simp [popArgs, List.take, List.drop]\n\n/-! ### The branching arm, proved once -/\n\n/-- Both sub-blocks satisfy the same invariant; selecting either branch\n preserves it. This is the only proof that unfolds nested-block sequencing. -/\ntheorem blockOK_ifElse {C : Nat} (S : CarrierSpec C)\n (host : HostTbl) (ar : Nat \u{2192} Option Nat) (callee : Callee)\n (n : Int) (base : List WVal) (thenB elseB : List WInstr)\n (locals : List WVal) (stack : List WVal) (cond : Bool)\n (hbranch : BlockOK S host ar callee n base\n (if cond then thenB else elseB) locals stack) :\n BlockOK S host ar callee n base [.ifElse thenB elseB]\n locals (b32 cond :: stack) := by\n cases cond with\n | false =>\n intro out hrun\n cases hb : wRunF host ar callee elseB locals stack with\n | none => simp [wRunF, b32, hb] at hrun\n | some branchOut =>\n cases branchOut <;> simp [wRunF, b32, hb] at hrun\n all_goals subst out; exact hbranch _ (by simpa using hb)\n | true =>\n intro out hrun\n cases hb : wRunF host ar callee thenB locals stack with\n | none => simp [wRunF, b32, hb] at hrun\n | some branchOut =>\n cases branchOut <;> simp [wRunF, b32, hb] at hrun\n all_goals subst out; exact hbranch _ (by simpa using hb)\n\n/-! ### Host-slot hypotheses -/\n\ndef HostSlots (C : Nat) (host : HostTbl)\n (hostTable : List (HostRole \u{d7} Nat))\n (add sub : List WVal \u{2192} Option WVal) : Prop :=\n (\u{2200} idx, AverCert.PlanCheck.hostRoleIdx? hostTable .box = some idx \u{2192}\n host idx = some (1, boxRef C)) \u{2227}\n (\u{2200} idx, AverCert.PlanCheck.hostRoleIdx? hostTable .add = some idx \u{2192}\n host idx = some (2, add)) \u{2227}\n (\u{2200} idx, AverCert.PlanCheck.hostRoleIdx? hostTable .sub = some idx \u{2192}\n host idx = some (2, sub))\n\n/-! ### Leaf simulation -/\n\ntheorem simLeaf {C : Nat} (S : CarrierSpec C)\n (host : HostTbl) (ar : Nat \u{2192} Option Nat) (callee : Callee)\n (hostTable : List (HostRole \u{d7} Nat))\n (add sub : List WVal \u{2192} Option WVal)\n (hslots : HostSlots C host hostTable add sub)\n (hadd : \u{2200} a b va vb w, S.Repr a va \u{2192} S.Repr b vb \u{2192}\n add [va, vb] = some w \u{2192} S.Repr (a + b) w)\n (hsub : \u{2200} a b va vb w, S.Repr a va \u{2192} S.Repr b vb \u{2192}\n sub [va, vb] = some w \u{2192} S.Repr (a - b) w)\n (scrutineeLocal fieldLocal tyIdx : Nat)\n (locals : List WVal) (fields : List WVal) (x : Int) (v : WVal)\n (hslot : locals[scrutineeLocal]? = some (.structv tyIdx fields))\n (hfieldLocal : fieldLocal < locals.length)\n (hfield : fields[0]? = some v) (hrepr : S.Repr x v) :\n \u{2200} leaf instrs base,\n AverCert.PlanLower.lowerIntDispatchArm hostTable\n scrutineeLocal fieldLocal tyIdx leaf = some instrs \u{2192}\n BlockOK S host ar callee (evalLeaf leaf x) base instrs locals base := by\n intro leaf instrs base hlow\n cases leaf with\n | proj =>\n simp only [AverCert.PlanLower.lowerIntDispatchArm, Option.some.injEq] at hlow\n subst instrs\n have hset : (locals.set fieldLocal v)[fieldLocal]? = some v :=\n List.getElem?_set_self hfieldLocal\n simp [BlockOK, StackOK, wRunF, hslot, hfield, hset, evalLeaf, hrepr]\n | hostOp role k constFirst =>\n cases hb : AverCert.PlanCheck.hostRoleIdx? hostTable .box with\n | none => simp [AverCert.PlanLower.lowerIntDispatchArm, hb] at hlow\n | some boxIdx =>\n cases hh : AverCert.PlanCheck.hostRoleIdx? hostTable\n (AverCert.PlanCheck.intDispatchRoleHostRole role) with\n | none => simp [AverCert.PlanLower.lowerIntDispatchArm, hb, hh] at hlow\n | some hostIdx =>\n simp only [AverCert.PlanLower.lowerIntDispatchArm, hb, hh,\n Option.some.injEq] at hlow\n subst instrs\n have hset : (locals.set fieldLocal v)[fieldLocal]? = some v :=\n List.getElem?_set_self hfieldLocal\n have hbox := hslots.1 boxIdx hb\n cases role with\n | add =>\n have hhost := hslots.2.1 hostIdx hh\n cases constFirst with\n | false =>\n cases hop : add [v, carrierSmall C k] with\n | none => simp [BlockOK, StackOK, wRunF, hslot, hfield,\n hset, hbox, boxRef, hhost, popArgs_one, popArgs_two, hop]\n | some w =>\n have hw := hadd x k v (carrierSmall C k) w hrepr\n (S.smallIntro k) hop\n simp [BlockOK, StackOK, wRunF, hslot, hfield,\n hset, hbox, boxRef, hhost, popArgs_one, popArgs_two,\n hop, evalLeaf, hw]\n | true =>\n cases hop : add [carrierSmall C k, v] with\n | none => simp [BlockOK, StackOK, wRunF, hslot, hfield,\n hset, hbox, boxRef, hhost, popArgs_one, popArgs_two, hop]\n | some w =>\n have hw := hadd k x (carrierSmall C k) v w\n (S.smallIntro k) hrepr hop\n simp [BlockOK, StackOK, wRunF, hslot, hfield,\n hset, hbox, boxRef, hhost, popArgs_one, popArgs_two,\n hop, evalLeaf, hw]\n | sub =>\n have hhost := hslots.2.2 hostIdx hh\n cases constFirst with\n | false =>\n cases hop : sub [v, carrierSmall C k] with\n | none => simp [BlockOK, StackOK, wRunF, hslot, hfield,\n hset, hbox, boxRef, hhost, popArgs_one, popArgs_two, hop]\n | some w =>\n have hw := hsub x k v (carrierSmall C k) w hrepr\n (S.smallIntro k) hop\n simp [BlockOK, StackOK, wRunF, hslot, hfield,\n hset, hbox, boxRef, hhost, popArgs_one, popArgs_two,\n hop, evalLeaf, hw]\n | true =>\n cases hop : sub [carrierSmall C k, v] with\n | none => simp [BlockOK, StackOK, wRunF, hslot, hfield,\n hset, hbox, boxRef, hhost, popArgs_one, popArgs_two, hop]\n | some w =>\n have hw := hsub k x (carrierSmall C k) v w\n (S.smallIntro k) hrepr hop\n simp [BlockOK, StackOK, wRunF, hslot, hfield,\n hset, hbox, boxRef, hhost, popArgs_one, popArgs_two,\n hop, evalLeaf, hw]\n\n/-! ### Nested cascade simulation -/\n\ntheorem simCascade {C : Nat} (S : CarrierSpec C)\n (host : HostTbl) (ar : Nat \u{2192} Option Nat) (callee : Callee)\n (hostTable : List (HostRole \u{d7} Nat))\n (add sub : List WVal \u{2192} Option WVal)\n (hslots : HostSlots C host hostTable add sub)\n (hadd : \u{2200} a b va vb w, S.Repr a va \u{2192} S.Repr b vb \u{2192}\n add [va, vb] = some w \u{2192} S.Repr (a + b) w)\n (hsub : \u{2200} a b va vb w, S.Repr a va \u{2192} S.Repr b vb \u{2192}\n sub [va, vb] = some w \u{2192} S.Repr (a - b) w)\n (scrutineeLocal : Nat) (locals : List WVal)\n (tag : Nat) (fields : List WVal)\n (hslot : locals[scrutineeLocal]? = some (.structv tag fields)) :\n \u{2200} body pos first n instrs base,\n EvalCascade S body tag fields n \u{2192}\n pos + AverCert.PlanCheck.intDispatchArmCount body < locals.length \u{2192}\n (match body with | .default _ => first = false | .test _ _ _ => True) \u{2192}\n AverCert.PlanLower.lowerIntDispatchCascade hostTable scrutineeLocal\n pos first body = some instrs \u{2192}\n BlockOK S host ar callee n base instrs locals\n (if first then .structv tag fields :: base else base) := by\n intro body\n induction body with\n | default k =>\n intro pos first n instrs base hsem _hlen hfirst hlow\n cases hsem\n have hfirst\' : first = false := hfirst\n subst first\n cases hb : AverCert.PlanCheck.hostRoleIdx? hostTable .box with\n | none => simp [AverCert.PlanLower.lowerIntDispatchCascade, hb] at hlow\n | some boxIdx =>\n simp only [AverCert.PlanLower.lowerIntDispatchCascade, hb,\n Option.some.injEq] at hlow\n subst instrs\n have hbox := hslots.1 boxIdx hb\n simpa [BlockOK, StackOK, wRunF, hbox, boxRef, popArgs_one]\n using S.smallIntro k\n | test tyIdx leaf rest ih =>\n intro pos first n instrs base hsem hlen _hfirst hlow\n cases ha : AverCert.PlanLower.lowerIntDispatchArm hostTable\n scrutineeLocal (pos + 1) tyIdx leaf with\n | none => simp [AverCert.PlanLower.lowerIntDispatchCascade, ha] at hlow\n | some hitInstrs =>\n cases hr : AverCert.PlanLower.lowerIntDispatchCascade hostTable\n scrutineeLocal (pos + 1) false rest with\n | none => simp [AverCert.PlanLower.lowerIntDispatchCascade, ha, hr] at hlow\n | some restInstrs =>\n simp only [AverCert.PlanLower.lowerIntDispatchCascade, ha, hr,\n Option.some.injEq] at hlow\n subst instrs\n have hfieldLocal : pos + 1 < locals.length := by\n simp only [AverCert.PlanCheck.intDispatchArmCount] at hlen\n omega\n by_cases htag : tag = tyIdx\n \u{b7} subst tag\n obtain \u{27e8}x, v, hfield, hrepr, hn\u{27e9} := evalCascade_hit_inv hsem\n subst n\n have hhit := simLeaf S host ar callee hostTable add sub hslots\n hadd hsub scrutineeLocal (pos + 1) tyIdx locals fields x v\n hslot hfieldLocal hfield hrepr leaf hitInstrs base ha\n have hif := blockOK_ifElse S host ar callee\n (evalLeaf leaf x) base hitInstrs restInstrs locals base true\n (by simpa using hhit)\n cases first <;>\n simpa [BlockOK, StackOK, wRunF, hslot, b32] using hif\n \u{b7} have hrest := evalCascade_miss_inv htag hsem\n have hrestLen : pos + 1 +\n AverCert.PlanCheck.intDispatchArmCount rest < locals.length := by\n simp only [AverCert.PlanCheck.intDispatchArmCount] at hlen\n omega\n have htail := ih (pos + 1) false n restInstrs base hrest\n hrestLen (by cases rest <;> simp) hr\n have hif := blockOK_ifElse S host ar callee n base\n hitInstrs restInstrs locals base false (by simpa using htail)\n cases first <;>\n simp [BlockOK, StackOK, wRunF, hslot, b32, htag] at hif \u{22a2} <;>\n exact hif\n\n/-! ### Generic family certificate -/\n\ntheorem generic_int_dispatch_certified {C : Nat} (S : CarrierSpec C)\n (plan : IntDispatchRawPlan)\n (code : CodeTbl) (host : HostTbl) (self : Nat)\n (hostTable : List (HostRole \u{d7} Nat))\n (add sub : List WVal \u{2192} Option WVal)\n (hslots : HostSlots C host hostTable add sub)\n (hadd : \u{2200} a b va vb w, S.Repr a va \u{2192} S.Repr b vb \u{2192}\n add [va, vb] = some w \u{2192} S.Repr (a + b) w)\n (hsub : \u{2200} a b va vb w, S.Repr a va \u{2192} S.Repr b vb \u{2192}\n sub [va, vb] = some w \u{2192} S.Repr (a - b) w)\n (hroot : \u{2203} tyIdx leaf rest, plan.body = .test tyIdx leaf rest)\n (body : List WInstr)\n (hlow : AverCert.PlanLower.lowerIntDispatchBody hostTable plan = some body)\n (hself : code self = some {\n arity := 1,\n nlocals := AverCert.PlanCheck.intDispatchArmCount plan.body + 2,\n body := body }) :\n \u{2200} fuel tag fields n w,\n EvalCascade S plan.body tag fields n \u{2192}\n wFuncN code host (fuel + 1) self [.structv tag fields] = some w \u{2192}\n S.Repr n w := by\n intro fuel tag fields n w hsem hrun\n rcases hroot with \u{27e8}rootTy, rootLeaf, rootRest, hroot\u{27e9}\n simp only [wFuncN, hself] at hrun\n let nlocals := AverCert.PlanCheck.intDispatchArmCount plan.body + 2\n let scrutineeLocal := AverCert.PlanCheck.intDispatchArmCount plan.body + 1\n let locals : List WVal := [WVal.structv tag fields] ++\n List.replicate nlocals WVal.null\n let updated := locals.set scrutineeLocal (WVal.structv tag fields)\n have hslt : scrutineeLocal < locals.length := by\n simp [scrutineeLocal, locals, nlocals]\n have hslot : updated[scrutineeLocal]? = some (.structv tag fields) := by\n exact List.getElem?_set_self hslt\n have hlen : 0 + AverCert.PlanCheck.intDispatchArmCount plan.body <\n updated.length := by\n simp [updated, locals, nlocals]\n omega\n cases hcascade : AverCert.PlanLower.lowerIntDispatchCascade hostTable\n scrutineeLocal 0 true plan.body with\n | none => simp [AverCert.PlanLower.lowerIntDispatchBody, scrutineeLocal,\n hcascade] at hlow\n | some cascade =>\n simp only [AverCert.PlanLower.lowerIntDispatchBody, scrutineeLocal,\n hcascade, Option.some.injEq] at hlow\n subst body\n have hsim := simCascade S host (fun g => (code g).map (\u{b7}.arity))\n (fun g args => wFuncN code host fuel g args)\n hostTable add sub hslots hadd hsub scrutineeLocal updated tag fields hslot\n plan.body 0 true n cascade [] hsem hlen (by\n simp [hroot])\n hcascade\n change\n (match wRunF host (fun g => (code g).map (\u{b7}.arity))\n (fun g args => wFuncN code host fuel g args)\n ([.localGet 0, .localSet scrutineeLocal, .localGet scrutineeLocal] ++ cascade)\n locals [] with\n | some (.ok _ [value]) => some value\n | some (.ret value) => some value\n | _ => none) = some w at hrun\n simp only [List.cons_append, List.nil_append, wRunF] at hrun\n have hzero : locals[0]? = some (WVal.structv tag fields) := by\n simp [locals]\n have hslotRaw : (locals.set scrutineeLocal\n (WVal.structv tag fields))[scrutineeLocal]? =\n some (WVal.structv tag fields) :=\n List.getElem?_set_self hslt\n simp only [hzero, hslotRaw] at hrun\n change\n (match wRunF host (fun g => (code g).map (\u{b7}.arity))\n (fun g args => wFuncN code host fuel g args)\n cascade updated [WVal.structv tag fields] with\n | some (.ok _ [value]) => some value\n | some (.ret value) => some value\n | _ => none) = some w at hrun\n cases hr : wRunF host (fun g => (code g).map (\u{b7}.arity))\n (fun g args => wFuncN code host fuel g args)\n cascade updated [.structv tag fields] with\n | none => simp [hr] at hrun\n | some out =>\n cases out with\n | ret value =>\n simp [hr] at hrun\n have hfalse := hsim (.ret value) hr\n simp [StackOK] at hfalse\n | ok finalLocals stack =>\n cases stack with\n | nil => simp [hr] at hrun\n | cons value rest =>\n cases rest with\n | nil =>\n simp [hr] at hrun\n subst w\n have hok := hsim (.ok finalLocals [value]) hr\n exact hok.2\n | cons x xs => simp [hr] at hrun\n\n\nend IntDispatchSoundness\n";