pub const CERT_DISCHARGE_INT_DISPATCH: &str = "/-\nAcceptance-soundness wiring for integer dispatch.\n\nAcceptance supplies the checked plan, canonical host wiring, lowering, and\nexact code entry. The audited raw checker supplies the generic theorem\'s\nnon-default-root premise; only the independent domain/model face remains in\nthe semantic bridge.\n-/\nimport AcceptanceSoundnessCore\nimport IntDispatchSoundness\n\nopen AverCert\nopen AverCert.Schema\nopen AverCert.AcceptedArtifact\nopen CertPrelude\n\nnamespace AcceptanceSoundness\n\nprivate theorem intDispatchRoot_of_raw (plan : IntDispatchRawPlan)\n (hRaw : AverCert.PlanCheck.checkIntDispatchRawPlan plan = true) :\n \u{2203} tyIdx leaf rest, plan.body = .test tyIdx leaf rest := by\n cases hBody : plan.body with\n | default k =>\n simp [AverCert.PlanCheck.checkIntDispatchRawPlan, hBody] at hRaw\n | test tyIdx leaf rest =>\n exact \u{27e8}tyIdx, leaf, rest, rfl\u{27e9}\n\nprivate theorem hostRoleIdx_mem_pair\n (hostTable : List (HostRole \u{d7} Nat)) (role : HostRole) (idx : Nat)\n (hLookup : AverCert.PlanCheck.hostRoleIdx? hostTable role = some idx) :\n (role, idx) \u{2208} hostTable := by\n induction hostTable with\n | nil => simp [AverCert.PlanCheck.hostRoleIdx?] at hLookup\n | cons head rest ih =>\n rcases head with \u{27e8}headRole, headIdx\u{27e9}\n by_cases hRole : headRole = role\n \u{b7} subst headRole\n simp [AverCert.PlanCheck.hostRoleIdx?] at hLookup\n subst idx\n simp\n \u{b7} simp [AverCert.PlanCheck.hostRoleIdx?, hRole] at hLookup\n simp [ih hLookup]\n\nprivate def intDispatchExpectedSlot\n (C : Nat) (add sub mul : List WVal \u{2192} Option WVal) :\n HostRole \u{2192} Nat \u{d7} (List WVal \u{2192} Option WVal)\n | .box => (1, boxRef C)\n | .add => (2, add)\n | .mul => (2, mul)\n | .sub => (2, sub)\n\nprivate theorem canonicalSlot_of_lookup\n (C : Nat) (add sub mul : List WVal \u{2192} Option WVal)\n (hostTable : List (HostRole \u{d7} Nat))\n (hDistinct : AverCert.PlanCheck.hostTableIndicesDistinct hostTable = true)\n (role : HostRole) (idx : Nat)\n (hLookup : AverCert.PlanCheck.hostRoleIdx? hostTable role = some idx) :\n intDispatchCanonicalSlots C add sub mul hostTable idx =\n some (intDispatchExpectedSlot C add sub mul role) := by\n induction hostTable generalizing role idx with\n | nil => simp [AverCert.PlanCheck.hostRoleIdx?] at hLookup\n | cons head rest ih =>\n rcases head with \u{27e8}headRole, headIdx\u{27e9}\n simp only [AverCert.PlanCheck.hostTableIndicesDistinct,\n AverCert.PlanCheck.natListNoDup, List.map_cons,\n Bool.and_eq_true] at hDistinct\n rcases hDistinct with \u{27e8}hHeadFresh, hRestDistinct\u{27e9}\n by_cases hRole : headRole = role\n \u{b7} subst headRole\n simp [AverCert.PlanCheck.hostRoleIdx?] at hLookup\n subst idx\n cases role <;>\n simp [intDispatchCanonicalSlots, intDispatchExpectedSlot]\n \u{b7} have hTailLookup : AverCert.PlanCheck.hostRoleIdx? rest role = some idx := by\n simpa [AverCert.PlanCheck.hostRoleIdx?, hRole] using hLookup\n have hPairMem : (role, idx) \u{2208} rest :=\n hostRoleIdx_mem_pair rest role idx hTailLookup\n have hNe : idx \u{2260} headIdx := by\n intro hEq\n subst idx\n simp at hHeadFresh\n exact hHeadFresh role hPairMem\n change (if idx = headIdx then _ else\n intDispatchCanonicalSlots C add sub mul rest idx) = _\n rw [if_neg hNe]\n exact ih hRestDistinct role idx hTailLookup\n\nprivate theorem canonicalHostSlots\n (C : Nat) (add sub mul : List WVal \u{2192} Option WVal)\n (hostTable : List (HostRole \u{d7} Nat))\n (hDistinct : AverCert.PlanCheck.hostTableIndicesDistinct hostTable = true) :\n IntDispatchSoundness.HostSlots C\n (intDispatchCanonicalSlots C add sub mul hostTable) hostTable add sub := by\n constructor\n \u{b7} intro idx hLookup\n simpa [intDispatchExpectedSlot] using\n canonicalSlot_of_lookup C add sub mul hostTable hDistinct .box idx hLookup\n \u{b7} constructor\n \u{b7} intro idx hLookup\n simpa [intDispatchExpectedSlot] using\n canonicalSlot_of_lookup C add sub mul hostTable hDistinct .add idx hLookup\n \u{b7} intro idx hLookup\n simpa [intDispatchExpectedSlot] using\n canonicalSlot_of_lookup C add sub mul hostTable hDistinct .sub idx hLookup\n\n/-- The semantic face intentionally absent from `intDispatchPlanAccepted`.\nA represented source input must expose one runtime variant, `EvalCascade` must\nrelate that variant to the checked plan\'s Int result, and every representation\nof that result must satisfy the independently declared codomain/model relation. -/\ndef intDispatchSemanticBridge\n (claim : IntDispatchClaim) (plan : IntDispatchRawPlan) : Prop :=\n claim.obligation.policy = .simulatesModel \u{2227}\n \u{2200} (S : CarrierSpec claim.obligation.carrier)\n (x : claim.obligation.Dom) (vs : List WVal),\n claim.obligation.domRepr S x vs \u{2192}\n \u{2203} tag fields n,\n vs = [.structv tag fields] \u{2227}\n IntDispatchSoundness.EvalCascade S plan.body tag fields n \u{2227}\n \u{2200} w, S.Repr n w \u{2192}\n claim.obligation.codRepr S (claim.obligation.model x) w\n\ndef intDispatchSemanticBridges (artifact : ArtifactData) : Prop :=\n \u{2200} claim \u{2208} artifact.intDispatchClaims,\n \u{2200} plan,\n intDispatchPlanForExport claim.exportName\n artifact.manifest.intDispatchPlans = some plan \u{2192}\n intDispatchSemanticBridge claim plan\n\n/-- Byte/plan and generic-application half for one accepted Int-dispatch claim. -/\ntheorem intDispatch_accepted_call\n (artifact : ArtifactData)\n (hAcc : acceptedIntDispatchFragments artifact)\n (claim : IntDispatchClaim)\n (hMem : claim \u{2208} artifact.intDispatchClaims) :\n \u{2203} plan,\n intDispatchPlanForExport claim.exportName\n artifact.manifest.intDispatchPlans = some plan \u{2227}\n \u{2200} (S : CarrierSpec claim.obligation.carrier)\n (add sub mul stringEq : List WVal \u{2192} Option WVal)\n (stringConcat : Nat \u{2192} List WVal \u{2192} Option WVal),\n (\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) \u{2192}\n (\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) \u{2192}\n \u{2200} fuel tag fields n w,\n IntDispatchSoundness.EvalCascade S plan.body tag fields n \u{2192}\n wFuncN claim.obligation.code\n (claim.obligation.host add sub mul stringEq stringConcat)\n (fuel + 1) claim.obligation.self [.structv tag fields] = some w \u{2192}\n S.Repr n w := by\n have hClaim : intDispatchClaimAccepted artifact.modBytes artifact.modLen\n artifact.manifest claim := by\n exact allClaims_of_mem\n (intDispatchClaimAccepted artifact.modBytes artifact.modLen artifact.manifest)\n artifact.intDispatchClaims hAcc claim hMem\n unfold intDispatchClaimAccepted at hClaim\n cases hPlan : intDispatchPlanForExport claim.exportName\n artifact.manifest.intDispatchPlans with\n | none => simp [hPlan] at hClaim\n | some plan =>\n have hAccepted : intDispatchPlanAccepted\n artifact.modBytes artifact.modLen claim.exportNameBytes claim.exportName\n claim.carrier claim.hostTable plan claim.obligation := by\n simpa [hPlan] using hClaim\n rcases hAccepted with\n \u{27e8}_hExport, hCarrier, hRaw, hDistinct, hHost,\n body, codeEntry, binding, hLow, _hCodeEntry, _hExactBinding,\n hSelf, _hFuncType, hCode\u{27e9}\n have hCodeSelf : claim.obligation.code claim.obligation.self =\n some \u{27e8}1, AverCert.PlanCheck.intDispatchArmCount plan.body + 2,\n body\u{27e9} := by\n simpa [\u{2190} hSelf] using hCode\n have hHost\' : claim.obligation.host =\n intDispatchCanonicalHost claim.obligation.carrier claim.hostTable := by\n simpa [hCarrier] using hHost\n refine \u{27e8}plan, rfl, ?_\u{27e9}\n intro S add sub mul stringEq stringConcat hAdd hSub\n fuel tag fields n w hSem hRun\n have hSlots : IntDispatchSoundness.HostSlots claim.obligation.carrier\n (claim.obligation.host add sub mul stringEq stringConcat)\n claim.hostTable add sub := by\n rw [hHost\']\n exact canonicalHostSlots claim.obligation.carrier add sub mul\n claim.hostTable hDistinct\n exact IntDispatchSoundness.generic_int_dispatch_certified\n S plan claim.obligation.code\n (claim.obligation.host add sub mul stringEq stringConcat)\n claim.obligation.self claim.hostTable add sub hSlots hAdd hSub\n (intDispatchRoot_of_raw plan hRaw) body hLow hCodeSelf\n fuel tag fields n w hSem hRun\n\ntheorem intDispatch_claim_discharges\n (artifact : ArtifactData)\n (hAcc : acceptedIntDispatchFragments artifact)\n (claim : IntDispatchClaim)\n (hMem : claim \u{2208} artifact.intDispatchClaims)\n (hBridge : \u{2200} plan,\n intDispatchPlanForExport claim.exportName\n artifact.manifest.intDispatchPlans = some plan \u{2192}\n intDispatchSemanticBridge claim plan) :\n obligationHolds claim.obligation := by\n have hCall := intDispatch_accepted_call artifact hAcc claim hMem\n rcases hCall with \u{27e8}plan, hPlan, hGeneric\u{27e9}\n rcases hBridge plan hPlan with \u{27e8}hPolicy, hSemantic\u{27e9}\n rw [obligationHolds, hPolicy]\n intro S add sub mul stringEq stringConcat\n hAdd hSub _hMul _hStringEq _hStringConcat fuel x vs w hDom hRun\n rcases hSemantic S x vs hDom with\n \u{27e8}tag, fields, n, hVs, hCascade, hCod\u{27e9}\n subst vs\n cases fuel with\n | zero => simp [wFuncN] at hRun\n | succ fuel =>\n exact hCod w (hGeneric S add sub mul stringEq stringConcat hAdd hSub\n fuel tag fields n w hCascade hRun)\n\n/-- Per-obligation option-(b) discharge for a concrete Int-dispatch export.\nThe checked plan, canonical host table, lowering, and code binding are data;\n`hSemantic` is the intentionally residual source-model bridge emitted for the\nuser function. Unlike the option-(c) leaf theorems, the model is not replaced\nby a canonical evaluator: the bridge proves that the user\'s model agrees with\nthe byte-derived `EvalCascade` on every represented source constructor. -/\ntheorem intDispatch_canonical_discharges\n (exportName : String)\n (carrier self : Nat)\n (plan : IntDispatchRawPlan)\n (hostTable : List (HostRole \u{d7} Nat))\n (code : CodeTbl)\n (host :\n (List WVal \u{2192} Option WVal) \u{2192}\n (List WVal \u{2192} Option WVal) \u{2192}\n (List WVal \u{2192} Option WVal) \u{2192}\n (List WVal \u{2192} Option WVal) \u{2192}\n (Nat \u{2192} List WVal \u{2192} Option WVal) \u{2192} HostTbl)\n (Dom : Type)\n (domRepr : CarrierSpec carrier \u{2192} Dom \u{2192} List WVal \u{2192} Prop)\n (model : Dom \u{2192} Int)\n (hRaw : AverCert.PlanCheck.checkIntDispatchRawPlan plan = true)\n (hDistinct : AverCert.PlanCheck.hostTableIndicesDistinct hostTable = true)\n (hHost : \u{2200} add sub mul stringEq stringConcat,\n host add sub mul stringEq stringConcat =\n intDispatchCanonicalHost carrier hostTable\n add sub mul stringEq stringConcat)\n (body : List WInstr)\n (hLow : AverCert.PlanLower.lowerIntDispatchBody hostTable plan = some body)\n (hCode : code self = some {\n arity := 1,\n nlocals := AverCert.PlanCheck.intDispatchArmCount plan.body + 2,\n body := body })\n (hSemantic : \u{2200} (S : CarrierSpec carrier) (x : Dom) (vs : List WVal),\n domRepr S x vs \u{2192}\n \u{2203} tag fields n,\n vs = [.structv tag fields] \u{2227}\n IntDispatchSoundness.EvalCascade S plan.body tag fields n \u{2227}\n \u{2200} w, S.Repr n w \u{2192} intRepr S (model x) w) :\n Obligation.holds\n ({ export_ := exportName\n policy := .simulatesModel\n carrier := carrier\n code := code\n host := host\n self := self\n Dom := Dom\n Cod := Int\n domRepr := domRepr\n codRepr := fun S n w => intRepr S n w\n model := model } : Obligation) := by\n intro S add sub mul stringEq stringConcat\n hAdd hSub _hMul _hStringEq _hStringConcat fuel x vs w hDom hRun\n rcases hSemantic S x vs hDom with\n \u{27e8}tag, fields, n, hVs, hCascade, hCod\u{27e9}\n subst vs\n cases fuel with\n | zero => simp [wFuncN] at hRun\n | succ fuel =>\n have hSlots : IntDispatchSoundness.HostSlots carrier\n (host add sub mul stringEq stringConcat) hostTable add sub := by\n rw [hHost]\n exact canonicalHostSlots carrier add sub mul hostTable hDistinct\n have hGeneric := IntDispatchSoundness.generic_int_dispatch_certified\n S plan code (host add sub mul stringEq stringConcat) self\n hostTable add sub hSlots hAdd hSub\n (intDispatchRoot_of_raw plan hRaw) body hLow hCode\n exact hCod w (hGeneric fuel tag fields n w hCascade hRun)\n\n/-- Complete family slice under the residual semantic bridge. -/\ntheorem intDispatch_discharges\n (artifact : ArtifactData)\n (hAcc : acceptedIntDispatchFragments artifact)\n (hSemantic : intDispatchSemanticBridges artifact) :\n \u{2200} o \u{2208} artifact.intDispatchClaims.map (\u{b7}.obligation), obligationHolds o := by\n intro o hObligation\n rcases List.mem_map.mp hObligation with \u{27e8}claim, hMem, rfl\u{27e9}\n exact intDispatch_claim_discharges artifact hAcc claim hMem\n (hSemantic claim hMem)\n\nend AcceptanceSoundness\n";