From 84202f8ad7f33f53367eafeea1002d2aa04d1524 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 15 Oct 2026 10:03:27 -0400 Subject: [PATCH] Prove conservative ownership checks for conditional drops Early compiler bodies can retain conditional drops after generic values have moved. Before admitting those drops, establish that the affected locals cannot still carry destruction obligations. Add a kernel-reducible ownership checker and its soundness theorem. Moves consume whole-local obligations; definitions restore uncertainty, and joins include every incoming path. Check complete acyclic control flow, including unwind edges and disconnected components. Prove that accepted candidates are empty under this model and silent under an explicit conditional-drop interpretation. Decode the pinned compiler's complete raw body in Lean. Reject unsupported syntax, cycles, and borrowed or projected candidate slots. Add direct kernel tests for transfers, overwrites, joins, cleanup, aliases, and schema mutations. Relating the decoder and drop interpretation to the compiler remains a separate correspondence premise. gherrit-pr-id: Gdfplsswvn7cgm7bugjeerqryd6uch4os Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/lean/DropJson.lean | 437 ++++++++++++++++++ verification/aeneas/lean/DropJsonTests.lean | 119 +++++ verification/aeneas/lean/DropOwnership.lean | 285 ++++++++++++ .../aeneas/lean/DropOwnershipTests.lean | 158 +++++++ 4 files changed, 999 insertions(+) create mode 100644 verification/aeneas/lean/DropJson.lean create mode 100644 verification/aeneas/lean/DropJsonTests.lean create mode 100644 verification/aeneas/lean/DropOwnership.lean create mode 100644 verification/aeneas/lean/DropOwnershipTests.lean diff --git a/verification/aeneas/lean/DropJson.lean b/verification/aeneas/lean/DropJson.lean new file mode 100644 index 0000000000..ee0d59f8c9 --- /dev/null +++ b/verification/aeneas/lean/DropJson.lean @@ -0,0 +1,437 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Lean +public import DropOwnership +@[expose] public section + +/-! +This decoder reads a complete Charon body, including its local declarations. +It accepts a deliberately small executable schema. Every operand is decoded in +evaluation order. It does not search JSON recursively for moves or accept an +externally supplied list of effects. + +Source spans, comments, statement IDs, types, generic arguments, and the static +trait reference in drop glue cannot carry executable operands in this schema. +Their payloads are explicitly ignored here. The ordinary admission audit still +checks operations, types, function identities, and all execution dependencies. +This decoder supplies only the additional ownership condition for erasing a +conditional drop, under the compiler correspondence premise of DropOwnership. +-/ + +namespace AeneasSpecs.DropJson + +open Lean DropOwnership + +abbrev Decode := Except String + +def require (condition : Bool) (message : String) : Decode Unit := + if condition then pure () else throw message + +def fields (j : Json) (names : List String) : Decode Unit := do + let obj ← j.getObj? + let actual := obj.toList.map Prod.fst + require (actual.length == names.length && actual.all names.contains) + "unexpected or missing object fields" + +def field := Json.getObjVal? + +def variant (j : Json) : Decode (String × Json) := do + let obj ← j.getObj? + match obj.toList with + | [kv] => pure kv + | _ => throw "expected one constructor" + +def tuple (j : Json) (n : Nat) : Decode (Array Json) := do + let a ← j.getArr? + require (a.size == n) "wrong constructor arity" + pure a + +def item (a : Array Json) (i : Nat) : Decode Json := + match a[i]? with + | some j => pure j + | none => throw "missing constructor argument" + +def localIndex (count : Nat) (j : Json) : Decode Nat := do + let i ← j.getNat? + require (i < count) "local index out of bounds" + pure i + +def globalRef (j : Json) : Decode Unit := do + fields j ["id", "generics"] + let _ ← (← field j "id").getNat? + -- Generic arguments describe types and constants, not runtime operands. + pure () + +def functionRef (j : Json) : Decode Unit := do + fields j ["kind", "generics"] + let (tag, value) ← variant (← field j "kind") + match tag with + | "Fun" => let _ ← value.getNat?; pure () + | "Trait" => + let args ← tuple value 2 + let _ ← (← item args 1).getNat? + -- The first argument is a static trait reference, not a place or operand. + pure () + | _ => throw "unsupported function reference" + +def directFunction (j : Json) : Decode Unit := do + let (tag, value) ← variant j + require (tag == "Regular") "unsupported executable function operand" + functionRef value + let (kind, _) ← variant (← field value "kind") + require (kind == "Fun") "only direct function calls are supported" + +def constant (j : Json) : Decode Unit := do + let (tag, value) ← variant j + require (tag == "Untagged") "unsupported constant wrapper" + let args ← tuple value 2 + let (kind, payload) ← variant (← item args 0) + -- The second argument is the static type of this constant. + match kind with + | "Global" => globalRef payload + | "Bool" => let _ ← payload.getBool?; pure () + | "Adt" => + let a ← tuple payload 2 + require (← item a 0).isNull "only unit constants are supported" + require (← (← item a 1).getArr?).isEmpty "only unit constants are supported" + | "Opaque" => + require ((← payload.getStr?) == "Missing metadata") "unsupported opaque constant" + | _ => throw "unsupported constant expression" + +structure Place where + root : Option Nat + whole : Bool + restricted : List Nat := [] + +def place : Nat → Nat → Json → Decode Place + | 0, _, _ => throw "place nesting limit exceeded" + | fuel + 1, count, j => do + fields j ["kind", "ty"] + let (tag, value) ← variant (← field j "kind") + match tag with + | "Local" => pure ⟨some (← localIndex count value), true, []⟩ + | "Global" => globalRef value; pure ⟨none, true, []⟩ + | "Projection" => + let args ← tuple value 2 + let base ← place fuel count (← item args 0) + -- Dereference is the only supported projection. Its base cannot be a + -- candidate local anywhere in the body, including disconnected code. + require ((← (← item args 1).getStr?) == "Deref") "unsupported place projection" + pure ⟨base.root, false, base.root.toList ++ base.restricted⟩ + | _ => throw "unsupported place constructor" + +structure Audit where + effects : List Effect := [] + restricted : List Nat := [] + +def Audit.append (a b : Audit) : Audit := + ⟨a.effects ++ b.effects, a.restricted ++ b.restricted⟩ + +def operand (fuel count : Nat) (j : Json) : Decode Audit := do + let (tag, value) ← variant j + match tag with + | "Move" | "Copy" => + let p ← place fuel count value + let effects := if tag == "Move" && p.whole then + p.root.toList.map Effect.consume else [] + pure ⟨effects, p.restricted⟩ + | "Const" => constant value; pure {} + | _ => throw "unsupported operand constructor" + +def destination (fuel count : Nat) (j : Json) : Decode Audit := do + let p ← place fuel count j + let effects := if p.whole then p.root.toList.map Effect.define else [] + pure ⟨effects, p.restricted⟩ + +def rvalue (fuel count : Nat) (j : Json) : Decode Audit := do + let (tag, value) ← variant j + match tag with + | "Use" => + let args ← tuple value 2 + require ((← (← item args 1).getStr?) == "Yes") "unsupported Use mode" + operand fuel count (← item args 0) + | "Ref" => + fields value ["place", "kind", "ptr_metadata"] + let kind ← (← field value "kind").getStr? + require (["Shared", "Mut"].contains kind) "unsupported reference kind" + let p ← place fuel count (← field value "place") + let metadata ← operand fuel count (← field value "ptr_metadata") + pure ⟨metadata.effects, p.root.toList ++ p.restricted ++ metadata.restricted⟩ + | "BinaryOp" => + let args ← tuple value 3 + require ((← (← item args 0).getStr?) == "Eq") "unsupported binary operation" + let left ← operand fuel count (← item args 1) + let right ← operand fuel count (← item args 2) + pure (left.append right) + | _ => throw "unsupported rvalue constructor" + +def simple (fuel count : Nat) (j : Json) : Decode Audit := do + let (tag, value) ← variant j + match tag with + | "StorageLive" | "StorageDead" => pure ⟨[.define (← localIndex count value)], []⟩ + | "Assign" => + let args ← tuple value 2 + let rhs ← rvalue fuel count (← item args 1) + let dest ← destination fuel count (← item args 0) + pure (rhs.append dest) + | "Borrowck" => + let (kind, p) ← variant value + require (kind == "FakeRead") "unsupported borrow-checking statement" + let p ← place fuel count p + pure ⟨[], p.restricted⟩ + | _ => throw "unsupported simple statement" + +def call (fuel count : Nat) (j : Json) : Decode Audit := do + fields j ["func", "args", "dest"] + directFunction (← field j "func") + let args ← (← field j "args").getArr? + let mut result : Audit := {} + for arg in args do + result := result.append (← operand fuel count arg) + -- Restoring the destination in this node precedes every normal and unwind + -- successor. Even an unwinding call cannot establish an empty destination. + pure (result.append (← destination fuel count (← field j "dest"))) + +def dropLocal (fuel count : Nat) (j : Json) : Decode Nat := do + require ((← (← field j "kind").getStr?) == "Conditional") "only conditional drops are supported" + let p ← place fuel count (← field j "place") + require p.whole "projected drop is unsupported" + let some root := p.root | throw "drop of a global is unsupported" + functionRef (← field j "fn_ptr") + pure root + +def abort (j : Json) : Decode Unit := do + match j with + | .str "UnwindTerminate" => pure () + | _ => + let (tag, path) ← variant j + require (tag == "Panic") "unsupported abort constructor" + let path ← path.getArr? + for part in path do + let (tag, args) ← variant part + require (tag == "Ident") "unsupported panic name component" + let args ← tuple args 2 + let _ ← (← item args 0).getStr? + let _ ← (← item args 1).getNat? + pure () + +def assertion (fuel count : Nat) (j : Json) : Decode Audit := do + fields j ["cond", "expected", "check_kind"] + let _ ← (← field j "expected").getBool? + require (← field j "check_kind").isNull "unsupported assertion check kind" + operand fuel count (← field j "cond") + +def wrapper (structured : Bool) (j : Json) : Decode Json := do + fields j (if structured then ["span", "id", "kind", "comments_before"] + else ["span", "kind", "comments_before"]) + if structured then + let _ ← (← field j "id").getNat? + field j "kind" + +structure Annotated where + node : Node + restricted : List Nat := [] + +def target (count : Nat) (j : Json) : Decode Nat := do + let i ← j.getNat? + require (i < count) "control target out of bounds" + pure i + +def switch (fuel count blocks : Nat) (j : Json) : Decode (Audit × List Nat) := do + fields j ["data", "branches"] + let successors ← (← field j "branches").getArr? + require (!successors.isEmpty) "empty switch successor list" + let successors ← successors.toList.mapM (target blocks) + let data ← field j "data" + fields data ["scrutinee", "branches", "fallback"] + let (tag, scrutinee) ← variant (← field data "scrutinee") + require (tag == "Value") "unsupported switch scrutinee" + let effects ← operand fuel count scrutinee + let branches ← (← field data "branches").getArr? + for branch in branches do + let branch ← tuple branch 2 + constant (← item branch 0) + let _ ← target successors.length (← item branch 1) + let _ ← target successors.length (← field data "fallback") + pure (effects, successors) + +def unstructured (fuel count : Nat) (j : Json) : Decode (List Annotated) := do + let blocks ← j.getArr? + require (!blocks.isEmpty) "empty unstructured body" + blocks.toList.mapM fun block => do + fields block ["statements", "terminator"] + let statements ← (← field block "statements").getArr? + let mut audit : Audit := {} + for statement in statements do + audit := audit.append (← simple fuel count (← wrapper false statement)) + let kind ← wrapper false (← field block "terminator") + match kind with + | .str "Return" | .str "UnwindResume" => + pure ⟨⟨audit.effects, none, []⟩, audit.restricted⟩ + | _ => + let (tag, value) ← variant kind + match tag with + | "Goto" => + fields value ["target"] + pure ⟨⟨audit.effects, none, [← target blocks.size (← field value "target")]⟩, audit.restricted⟩ + | "Abort" => abort value; pure ⟨⟨audit.effects, none, []⟩, audit.restricted⟩ + | "Call" => + fields value ["call", "target", "on_unwind"] + let total := audit.append (← call fuel count (← field value "call")) + let normal ← target blocks.size (← field value "target") + let unwind ← target blocks.size (← field value "on_unwind") + pure ⟨⟨total.effects, none, [normal, unwind]⟩, total.restricted⟩ + | "Drop" => + fields value ["kind", "place", "fn_ptr", "target", "on_unwind"] + let dropped ← dropLocal fuel count value + let normal ← target blocks.size (← field value "target") + let unwind ← target blocks.size (← field value "on_unwind") + pure ⟨⟨audit.effects, some dropped, [normal, unwind]⟩, audit.restricted⟩ + | "Switch" => + let (branchAudit, successors) ← switch fuel count blocks.size value + let total := audit.append branchAudit + pure ⟨⟨total.effects, none, successors⟩, total.restricted⟩ + | "Assert" => + fields value ["assert", "target", "on_unwind"] + let total := audit.append (← assertion fuel count (← field value "assert")) + let normal ← target blocks.size (← field value "target") + let unwind ← target blocks.size (← field value "on_unwind") + pure ⟨⟨total.effects, none, [normal, unwind]⟩, total.restricted⟩ + | _ => throw "unsupported unstructured terminator" + +abbrev Build := StateT (Array Annotated) Decode + +def emit (a : Annotated) : Build Nat := do + let nodes ← get + set (nodes.push a) + pure nodes.size + +-- The continuation is explicit. Abrupt exits ignore it. Statements after an +-- abrupt exit are still decoded and remain conservative disconnected nodes. +def structured : Nat → Nat → Json → List Nat → Build Nat + | 0, _, _, _ => throw "structured nesting limit exceeded" + | fuel + 1, count, block, continuation => do + fields block ["span", "id", "statements"] + let _ ← (← field block "id").getNat? + let statements ← (← field block "statements").getArr? + let mut next := continuation + for statement in statements.toList.reverse do + let kind ← wrapper true statement + let node ← match kind with + | .str "Return" | .str "UnwindResume" => emit ⟨⟨[], none, []⟩, []⟩ + | _ => do + let (tag, value) ← variant kind + match tag with + | "Abort" => abort value; emit ⟨⟨[], none, []⟩, []⟩ + | "Call" => + fields value ["call", "on_unwind"] + let audit ← call fuel count (← field value "call") + -- Falling through a cleanup is conservatively allowed to reach + -- the same continuation. Its actual abrupt exits never do so. + let unwind ← structured fuel count (← field value "on_unwind") next + emit ⟨⟨audit.effects, none, next ++ [unwind]⟩, audit.restricted⟩ + | "Drop" => + fields value ["kind", "place", "fn_ptr", "on_unwind"] + let dropped ← dropLocal fuel count value + let unwind ← structured fuel count (← field value "on_unwind") next + emit ⟨⟨[], some dropped, next ++ [unwind]⟩, []⟩ + | "Assert" => + fields value ["assert", "on_failure", "on_unwind"] + let audit ← assertion fuel count (← field value "assert") + abort (← field value "on_failure") + let unwind ← structured fuel count (← field value "on_unwind") next + emit ⟨⟨audit.effects, none, next ++ [unwind]⟩, audit.restricted⟩ + | _ => + -- Loop, Break, Continue, and every unknown constructor fail here. + let audit ← simple fuel count kind + emit ⟨⟨audit.effects, none, next⟩, audit.restricted⟩ + next := [node] + emit ⟨⟨[], none, next⟩, []⟩ + +def locals (j : Json) : Decode Nat := do + fields j ["arg_count", "locals"] + let args ← (← field j "arg_count").getNat? + let declarations ← (← field j "locals").getArr? + require (args < declarations.size) "invalid argument count" + for i in [:declarations.size] do + let declaration ← item declarations i + fields declaration ["index", "name", "span", "ty", "drop_flag_for"] + require ((← (← field declaration "index").getNat?) == i) "locals are not densely indexed" + require (← field declaration "drop_flag_for").isNull "drop flag locals are unsupported" + let name ← field declaration "name" + unless name.isNull do + let _ ← name.getStr? + pure declarations.size + +def topological (nodes : List Node) : Nat → List Nat → List Nat → Decode (List Nat) + | 0, remaining, order => + if remaining.isEmpty then pure order else throw "cyclic control flow" + | fuel + 1, remaining, order => do + if remaining.isEmpty then return order + let some chosen := remaining.find? (fun i => remaining.all fun predecessor => + match nodes[predecessor]? with + | some node => !node.successors.contains i + | none => false) | throw "cyclic control flow" + topological nodes fuel (remaining.erase chosen) (order ++ [chosen]) + +def reorder (count entry : Nat) (annotated : List Annotated) : Decode Graph := do + let nodes := annotated.map Annotated.node + let candidates := nodes.filterMap Node.candidateDrop + let restricted := annotated.flatMap Annotated.restricted + require (!(restricted.any candidates.contains)) "candidate local is projected or borrowed" + require (entry < nodes.length) "invalid entry node" + let order ← topological nodes nodes.length (List.range nodes.length) [] + let renamed ← order.mapM fun old => do + let some node := nodes[old]? | throw "invalid node permutation" + let successors ← node.successors.mapM fun successor => do + require (successor < nodes.length) "invalid graph successor" + pure (order.idxOf successor) + pure { node with successors := successors } + pure ⟨renamed, count, order.idxOf entry⟩ + +/-- Decode and check the complete executable schema before projecting effects. +The fixed nesting limit rejects exceptionally deep inputs rather than making +the executable decoder partial. Both structured and unstructured bodies are +reordered in Lean; every disconnected component participates in cycle checks. -/ +def decode (body : Json) : Except String Graph := do + let (tag, value) ← variant body + fields value ["span", "bound_body_regions", "locals", "body", "comments"] + let _ ← (← field value "bound_body_regions").getNat? + let count ← locals (← field value "locals") + match tag with + | "Unstructured" => reorder count 0 (← unstructured 4096 count (← field value "body")) + | "Structured" => + let (entry, nodes) ← (structured 4096 count (← field value "body") []).run #[] + reorder count entry nodes.toList + | _ => throw "unsupported body constructor" + +/-- This is the proposition evaluated by each kernel-checked snapshot theorem. -/ +def acceptBody (body : Json) : Bool := + match decode body with + | .error _ => false + | .ok graph => DropOwnership.accepted graph + +theorem accepted_of_decoded {body : Json} {graph : Graph} + (decoded : decode body = .ok graph) (checked : acceptBody body = true) : + DropOwnership.accepted graph = true := by + simpa [acceptBody, decoded] using checked + +/-- A certificate about a raw body entails the ownership theorem for the graph +produced by this decoder. The separate compiler correspondence premise must +relate source executions to that graph's modeled executions. -/ +theorem decoded_drop_empty {body : Json} {graph : Graph} + (decoded : decode body = .ok graph) (checked : acceptBody body = true) + {index slot : Nat} {owns : DropOwnership.Concrete} + (reached : DropOwnership.Reachable graph index owns) + (candidate : (graph.node index).candidateDrop = some slot) : + ¬ DropOwnership.execute (graph.node index).effects owns slot := + DropOwnership.accepted_drop_empty (accepted_of_decoded decoded checked) reached candidate + +end AeneasSpecs.DropJson diff --git a/verification/aeneas/lean/DropJsonTests.lean b/verification/aeneas/lean/DropJsonTests.lean new file mode 100644 index 0000000000..83eb15761f --- /dev/null +++ b/verification/aeneas/lean/DropJsonTests.lean @@ -0,0 +1,119 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +import DropJson + +namespace AeneasSpecs.DropJson.Tests + +open Lean + +set_option maxRecDepth 16384 +set_option maxHeartbeats 2000000 + +private def obj := Json.mkObj +private def arr (xs : List Json) := Json.arr xs.toArray +private def ctor (name : String) (value : Json) := obj [(name, value)] +private def slot (i : Nat) := obj [("kind", ctor "Local" (toJson i)), ("ty", .null)] +private def move (i : Nat) := ctor "Move" (slot i) +private def copy (i : Nat) := ctor "Copy" (slot i) +private def use (operand : Json) := ctor "Use" (arr [operand, .str "Yes"]) +private def assign (i : Nat) (rhs : Json) := ctor "Assign" (arr [slot i, rhs]) +private def statement (kind : Json) := obj + [("span", .null), ("kind", kind), ("comments_before", arr [])] +private def block (statements : List Json) (terminator : Json) := obj + [("statements", arr (statements.map statement)), ("terminator", statement terminator)] +private def goto (i : Nat) := ctor "Goto" (obj [("target", toJson i)]) +private def ret := block [] (.str "Return") +private def function := obj [("kind", ctor "Fun" 0), ("generics", .null)] +private def dropped (i : Nat) (normal unwind : Nat) (kind : String := "Conditional") := ctor "Drop" + (obj [("kind", .str kind), ("place", slot i), ("fn_ptr", function), + ("target", toJson normal), ("on_unwind", toJson unwind)]) +private def called (dest : Nat) (args : List Json) (normal unwind : Nat) := ctor "Call" + (obj [("call", obj [("func", ctor "Regular" function), ("args", arr args), ("dest", slot dest)]), + ("target", toJson normal), ("on_unwind", toJson unwind)]) +private def declarations := obj [("arg_count", 1), ("locals", arr + ((List.range 3).map fun i => obj [("index", toJson i), ("name", .null), ("span", .null), + ("ty", .null), ("drop_flag_for", .null)]))] +private def body (tag : String) (code : Json) := ctor tag (obj + [("span", .null), ("bound_body_regions", 0), ("locals", declarations), + ("body", code), ("comments", arr [])]) +private def ullbc (blocks : List Json) := body "Unstructured" (arr blocks) +private def projection (i : Nat) := obj + [("kind", ctor "Projection" (arr [slot i, .str "Deref"])), ("ty", .null)] +private def unitConstant := ctor "Const" (ctor "Untagged" + (arr [ctor "Adt" (arr [.null, arr []]), .null])) +private def boolConstant := ctor "Untagged" (arr [ctor "Bool" (.bool false), .null]) +private def branch (left right : Nat) := ctor "Switch" (obj + [("data", obj [("scrutinee", ctor "Value" (copy 0)), + ("branches", arr [arr [boolConstant, 0]]), ("fallback", 1)]), + ("branches", arr [toJson left, toJson right])]) + +example : acceptBody (ullbc [block [assign 0 (use (move 1))] (dropped 1 1 1), ret]) = true := by with_unfolding_all rfl +example : acceptBody (ullbc [block [] (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl +example : acceptBody (ullbc [block [assign 0 (use (copy 1))] (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl + +-- Assignment restores uncertainty after evaluating every operand, including a +-- self move. A later overwrite has the same conservative effect. +example : acceptBody (ullbc [block [assign 1 (use (move 1))] (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl +example : acceptBody (ullbc [block [assign 0 (use (move 1)), assign 1 (use unitConstant)] + (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl +example : acceptBody (ullbc [block [assign 0 (use (move 1)), ctor "StorageDead" 1] + (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl +example : acceptBody (ullbc [block [assign 0 (use (move 1)), ctor "StorageLive" 1] + (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl + +-- Every branch and unwind edge participates, including a call destination +-- whose old value had already been moved away. +example : acceptBody (ullbc [block [] (branch 1 2), + block [assign 0 (use (move 1))] (goto 3), block [] (goto 3), + block [] (dropped 1 4 4), ret]) = false := by with_unfolding_all rfl +example : acceptBody (ullbc [block [assign 0 (use (move 1))] (called 1 [] 1 2), ret, + block [] (dropped 1 1 1)]) = false := by with_unfolding_all rfl +example : acceptBody (ullbc [block [] (called 0 [move 1] 1 2), ret, + block [] (dropped 1 1 1)]) = true := by with_unfolding_all rfl + +-- Projecting or borrowing the candidate slot is forbidden throughout the +-- complete body, even if an earlier move would otherwise justify its drop. +example : acceptBody (ullbc [block [assign 0 (use (ctor "Move" (projection 1)))] + (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl +example : acceptBody (ullbc [block [assign 0 (use (move 1)), assign 2 (ctor "Ref" + (obj [("place", slot 1), ("kind", .str "Shared"), ("ptr_metadata", unitConstant)]))] + (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl +example : acceptBody (ullbc [block [assign 0 (use (move 1))] + (dropped 1 1 1 "Precise"), ret]) = false := by with_unfolding_all rfl +example : acceptBody (ullbc [block [assign 0 (use (move 1))] (dropped 1 1 1), ret, + block [] (goto 2)]) = false := by with_unfolding_all rfl +example : acceptBody (ullbc [ret, block [] (dropped 1 0 0)]) = false := by with_unfolding_all rfl + +-- Extra executable fields cannot hide an operand from the projection. +example : acceptBody (ullbc [block [assign 0 (obj + [("Use", arr [move 1, .str "Yes"]), ("hidden", move 2)])] + (dropped 1 1 1), ret]) = false := by with_unfolding_all rfl + +private def structuredStatement (kind : Json) := obj + [("span", .null), ("id", 0), ("kind", kind), ("comments_before", arr [])] +private def structuredBlock (statements : List Json) := obj + [("span", .null), ("id", 0), ("statements", arr (statements.map structuredStatement))] +private def llbc (statements : List Json) := body "Structured" (structuredBlock statements) +private def structuredDrop (i : Nat) := ctor "Drop" (obj + [("kind", .str "Conditional"), ("place", slot i), ("fn_ptr", function), + ("on_unwind", structuredBlock [.str "UnwindResume"])]) + +example : acceptBody (llbc [assign 0 (use (move 1)), structuredDrop 1, .str "Return"]) = true := by with_unfolding_all rfl + +-- The drop after Return is a disconnected conservative component. Connecting +-- it to the preceding move would manufacture an invalid empty fact. +example : acceptBody (llbc [assign 0 (use (move 1)), .str "Return", structuredDrop 1]) = false := by with_unfolding_all rfl +example : acceptBody (llbc [assign 0 (use (move 1)), .str "UnwindResume", structuredDrop 1]) = false := by with_unfolding_all rfl +example : acceptBody (llbc [assign 0 (use (move 1)), ctor "Abort" (.str "UnwindTerminate"), + structuredDrop 1]) = false := by with_unfolding_all rfl +example : acceptBody (llbc [ctor "Loop" (structuredBlock []), structuredDrop 1]) = false := by with_unfolding_all rfl +example : acceptBody (llbc [ctor "Break" 0, structuredDrop 1]) = false := by with_unfolding_all rfl +example : acceptBody (llbc [ctor "Continue" 0, structuredDrop 1]) = false := by with_unfolding_all rfl + +end AeneasSpecs.DropJson.Tests diff --git a/verification/aeneas/lean/DropOwnership.lean b/verification/aeneas/lean/DropOwnership.lean new file mode 100644 index 0000000000..cf329f1038 --- /dev/null +++ b/verification/aeneas/lean/DropOwnership.lean @@ -0,0 +1,285 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Std +@[expose] public section + +namespace AeneasSpecs.DropOwnership + +/-! +This module checks a small ownership model, not Rust's memory semantics. A +concrete state records destruction obligations; it says nothing about bytes +remaining in storage after a move. The caller must establish that its complete +body projection preserves evaluation order, all edges, and whole-slot effects. +It must also establish that an obligation-free conditional drop is silent in +the compiler interpretation. Those bridges are deliberately separate premises. + +Every source component and the designated entry can start with any obligations +on the declared locals. Consuming a whole slot removes its obligation; defining +it restores one. Consequently, an assignment must list RHS effects before the +destination definition. A call's destination must be defined on every successor, +including unwind. Slot reuse and storage markers restore uncertainty too. +-/ + +inductive Effect where + | consume (slot : Nat) + | define (slot : Nat) + deriving Repr, DecidableEq, Inhabited + +structure Node where + effects : List Effect := [] + candidateDrop : Option Nat := none + successors : List Nat := [] + deriving Repr, DecidableEq, Inhabited + +structure Graph where + nodes : List Node + localCount : Nat + entry : Nat := 0 + deriving Repr, DecidableEq, Inhabited + +def Graph.node (g : Graph) (index : Nat) : Node := + g.nodes[index]?.getD default + +def Effect.slot : Effect → Nat + | .consume slot | .define slot => slot + +/-- Abstract states are conservative sets, represented by finite lists. List +order and duplicate elements have no semantic significance. -/ +def applyEffect : Effect → List Nat → List Nat + | .consume slot, owns => owns.filter (· != slot) + | .define slot, owns => slot :: owns + +def transfer : List Effect → List Nat → List Nat + | [], owns => owns + | effect :: rest, owns => transfer rest (applyEffect effect owns) + +/-- A certificate gives the incoming may-own set at each node. It is untrusted: +`check` validates every obligation used by the soundness proof. -/ +abbrev Certificate := Nat → List Nat + +def IsRoot (g : Graph) (index : Nat) : Prop := + index = g.entry ∨ ∀ node ∈ g.nodes, index ∉ node.successors + +instance (g : Graph) (index : Nat) : Decidable (IsRoot g index) := + inferInstanceAs (Decidable + (index = g.entry ∨ ∀ node ∈ g.nodes, index ∉ node.successors)) + +/-- In addition to ownership closure, validate every slot and successor. The +strict successor order rejects cycles anywhere, even in a disconnected or +drop-free component. A candidate drop occurs after this node's ordered effects. +-/ +def NodeValid (g : Graph) (certificate : Certificate) (index : Nat) : Prop := + let node := g.node index + (∀ effect ∈ node.effects, effect.slot < g.localCount) ∧ + (∀ slot ∈ node.candidateDrop, + slot < g.localCount ∧ slot ∉ transfer node.effects (certificate index)) ∧ + (∀ next ∈ node.successors, + index < next ∧ next < g.nodes.length ∧ + ∀ slot ∈ transfer node.effects (certificate index), + slot ∈ certificate next) ∧ + (IsRoot g index → + ∀ slot ∈ List.range g.localCount, slot ∈ certificate index) + +instance (g : Graph) (certificate : Certificate) (index : Nat) : + Decidable (NodeValid g certificate index) := + inferInstanceAs (Decidable + ((∀ effect ∈ (g.node index).effects, effect.slot < g.localCount) ∧ + (∀ slot ∈ (g.node index).candidateDrop, + slot < g.localCount ∧ + slot ∉ transfer (g.node index).effects (certificate index)) ∧ + (∀ next ∈ (g.node index).successors, + index < next ∧ next < g.nodes.length ∧ + ∀ slot ∈ transfer (g.node index).effects (certificate index), + slot ∈ certificate next) ∧ + (IsRoot g index → + ∀ slot ∈ List.range g.localCount, slot ∈ certificate index))) + +def Valid (g : Graph) (certificate : Certificate) : Prop := + g.entry < g.nodes.length ∧ + ∀ index ∈ List.range g.nodes.length, NodeValid g certificate index + +instance (g : Graph) (certificate : Certificate) : + Decidable (Valid g certificate) := + inferInstanceAs (Decidable (g.entry < g.nodes.length ∧ + ∀ index ∈ List.range g.nodes.length, NodeValid g certificate index)) + +def check (g : Graph) (certificate : Certificate) : Bool := + decide (Valid g certificate) + +/-- Infer one finite certificate by forward propagation. Roots begin with all +locals; joins take union. The result still goes through `check`, so inference +needs no trusted solver and no completeness theorem. -/ +def infer (g : Graph) : Certificate := + (List.range g.nodes.length).foldl (fun incoming index => + let node := g.node index + let outgoing := transfer node.effects (incoming index) + fun next => if next ∈ node.successors then + outgoing ++ (incoming next).filter (fun slot => slot ∉ outgoing) + else incoming next) + (fun index => if IsRoot g index then List.range g.localCount else []) + +def accepted (g : Graph) : Bool := check g (infer g) + +/-- Every accepted edge advances its bounded node index. In particular, a path +cannot revisit a node, including through an exceptional edge. This condition +is checked for the whole graph rather than only for reachable drop sites. -/ +theorem checked_edge_forward {g : Graph} {certificate : Certificate} + (checked : check g certificate = true) {index next : Nat} + (inBounds : index < g.nodes.length) + (edge : next ∈ (g.node index).successors) : + index < next ∧ next < g.nodes.length := by + have valid : Valid g certificate := of_decide_eq_true checked + have closure := (valid.2 index (List.mem_range.mpr inBounds)).2.2.1 next edge + exact ⟨closure.1, closure.2.1⟩ + +theorem accepted_edge_forward {g : Graph} (checked : accepted g = true) + {index next : Nat} (inBounds : index < g.nodes.length) + (edge : next ∈ (g.node index).successors) : + index < next ∧ next < g.nodes.length := + checked_edge_forward checked inBounds edge + +/-! +The concrete semantics permits every initial subset of the declared locals. +It is intentionally independent of the inferred certificate. Branches choose +any listed successor, so the theorem includes ordinary and exceptional paths. +-/ + +abbrev Concrete := Nat → Prop + +def concreteEffect : Effect → Concrete → Concrete + | .consume slot, owns => fun other => owns other ∧ other ≠ slot + | .define slot, owns => fun other => other = slot ∨ owns other + +def execute : List Effect → Concrete → Concrete + | [], owns => owns + | effect :: rest, owns => execute rest (concreteEffect effect owns) + +def Covers (possible : List Nat) (owns : Concrete) : Prop := + ∀ slot, owns slot → slot ∈ possible + +theorem effect_covers (effect : Effect) {possible : List Nat} {owns : Concrete} + (covered : Covers possible owns) : + Covers (applyEffect effect possible) (concreteEffect effect owns) := by + cases effect with + | consume slot => + intro other obligation + simp only [concreteEffect] at obligation + simp only [applyEffect, List.mem_filter, bne_iff_ne, ne_eq] + exact ⟨covered other obligation.1, obligation.2⟩ + | define slot => + intro other obligation + simp only [concreteEffect] at obligation + simp only [applyEffect, List.mem_cons] + exact obligation.elim Or.inl (fun owned => Or.inr (covered other owned)) + +theorem transfer_covers (effects : List Effect) + {possible : List Nat} {owns : Concrete} (covered : Covers possible owns) : + Covers (transfer effects possible) (execute effects owns) := by + induction effects generalizing possible owns with + | nil => exact covered + | cons effect rest induction => + exact induction (effect_covers effect covered) + +inductive Reachable (g : Graph) : Nat → Concrete → Prop where + | root (index : Nat) (owns : Concrete) + (inBounds : index < g.nodes.length) (root : IsRoot g index) + (declared : ∀ slot, owns slot → slot < g.localCount) : + Reachable g index owns + | step {index next : Nat} {owns : Concrete} + (before : Reachable g index owns) + (edge : next ∈ (g.node index).successors) : + Reachable g next (execute (g.node index).effects owns) + +/-- Every concrete execution is contained in a checked incoming invariant. -/ +theorem checked_invariant {g : Graph} {certificate : Certificate} + (checked : check g certificate = true) {index : Nat} {owns : Concrete} + (reached : Reachable g index owns) : + index < g.nodes.length ∧ Covers (certificate index) owns := by + have valid : Valid g certificate := of_decide_eq_true checked + induction reached with + | root index owns inBounds root declared => + refine ⟨inBounds, ?_⟩ + intro slot obligation + exact (valid.2 index (List.mem_range.mpr inBounds)).2.2.2 root slot + (List.mem_range.mpr (declared slot obligation)) + | @step index next owns before edge induction => + have nodeValid := valid.2 index (List.mem_range.mpr induction.1) + have closure := nodeValid.2.2.1 next edge + refine ⟨closure.2.1, ?_⟩ + intro slot obligation + exact closure.2.2 slot (transfer_covers (g.node index).effects + induction.2 slot obligation) + +/-- The central guarantee: every candidate at every reached occurrence has no +destruction obligation after its preceding effects. This includes a root in a +disconnected component and a path chosen through an unwind successor. -/ +theorem checked_drop_empty {g : Graph} {certificate : Certificate} + (checked : check g certificate = true) {index slot : Nat} {owns : Concrete} + (reached : Reachable g index owns) + (candidate : (g.node index).candidateDrop = some slot) : + ¬ execute (g.node index).effects owns slot := by + have valid : Valid g certificate := of_decide_eq_true checked + have invariant := checked_invariant checked reached + have empty := (valid.2 index (List.mem_range.mpr invariant.1)).2.1 slot + (by simp [candidate]) + intro obligation + exact empty.2 (transfer_covers (g.node index).effects invariant.2 + slot obligation) + +theorem accepted_drop_empty {g : Graph} (checked : accepted g = true) + {index slot : Nat} {owns : Concrete} (reached : Reachable g index owns) + (candidate : (g.node index).candidateDrop = some slot) : + ¬ execute (g.node index).effects owns slot := + checked_drop_empty checked reached candidate + +/-! +This final relation states the conditional-drop interpretation assumed by the +semantic bridge: when no obligation exists, the operation returns the same +state silently; when one exists, it may invoke glue or unwind. The theorem +rules out both active alternatives for an accepted candidate. It does not +assert that an unconditional/precise drop has this interpretation. +-/ + +inductive DropOutcome where + | silent + | invokeGlue + | unwind + deriving Repr, DecidableEq + +inductive ConditionalDrop (slot : Nat) (before : Concrete) : + DropOutcome → Concrete → Prop where + | empty (absent : ¬ before slot) : ConditionalDrop slot before .silent before + | glue (present : before slot) (after : Concrete) : + ConditionalDrop slot before .invokeGlue after + | unwind (present : before slot) (after : Concrete) : + ConditionalDrop slot before .unwind after + +theorem empty_drop_iff {slot : Nat} {before after : Concrete} + {outcome : DropOutcome} (absent : ¬ before slot) : + ConditionalDrop slot before outcome after ↔ + outcome = .silent ∧ after = before := by + constructor + · intro step + cases step with + | empty => exact ⟨rfl, rfl⟩ + | glue present => exact False.elim (absent present) + | unwind present => exact False.elim (absent present) + · rintro ⟨rfl, rfl⟩ + exact .empty absent + +theorem accepted_drop_noop {g : Graph} (checked : accepted g = true) + {index slot : Nat} {owns after : Concrete} {outcome : DropOutcome} + (reached : Reachable g index owns) + (candidate : (g.node index).candidateDrop = some slot) : + ConditionalDrop slot (execute (g.node index).effects owns) outcome after ↔ + outcome = .silent ∧ after = execute (g.node index).effects owns := + empty_drop_iff (accepted_drop_empty checked reached candidate) + +end AeneasSpecs.DropOwnership diff --git a/verification/aeneas/lean/DropOwnershipTests.lean b/verification/aeneas/lean/DropOwnershipTests.lean new file mode 100644 index 0000000000..faee90fb71 --- /dev/null +++ b/verification/aeneas/lean/DropOwnershipTests.lean @@ -0,0 +1,158 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import DropOwnership +@[expose] public section + +namespace AeneasSpecs.DropOwnership.Tests + +/-! +These propositions are checked by the kernel. They exercise graph ownership +and validation; raw-schema, isolation, and exact-snapshot tests belong to the +decoder and admission integration. A missing effect below models Copy; the raw +decoder must distinguish that case from unsupported or omitted syntax. +-/ + +def moved : Graph := + { nodes := [{ effects := [.consume 0], candidateDrop := some 0 }] + localCount := 1 } + +example : accepted moved = true := by decide + +-- An argument still carries an obligation until a supported move consumes it. +example : accepted { + nodes := [{ candidateDrop := some 0 }], localCount := 1 } = false := by decide + +-- Copy leaves ownership unchanged, as does moving a different local. +example : accepted { + nodes := [{ effects := [.consume 1], candidateDrop := some 0 }] + localCount := 2 } = false := by decide + +-- Whole-local definitions restore ownership, after all RHS operand effects. +example : accepted { + nodes := [{ effects := [.consume 0, .define 0], candidateDrop := some 0 }] + localCount := 1 } = false := by decide + +-- In contrast, consuming the newly defined value really leaves the slot empty. +example : accepted { + nodes := [{ effects := [.define 0, .consume 0], candidateDrop := some 0 }] + localCount := 1 } = true := by decide + +-- Slot reuse, storage markers, and call destinations must be definitions. They +-- cannot establish empty ownership, even after an earlier move. +example : accepted { + nodes := [ + { effects := [.consume 0], successors := [1] }, + { effects := [.define 0], successors := [2] }, + { candidateDrop := some 0 }] + localCount := 1 } = false := by decide + +def joined (right : List Effect) : Graph := + { nodes := [ + { successors := [1, 2] }, + { effects := [.consume 0], successors := [3] }, + { effects := right, successors := [3] }, + { candidateDrop := some 0 }] + localCount := 1 } + +-- Every incoming branch must establish emptiness. Taking union at a join +-- preserves the obligation from an ordinary or exceptional failure path. +example : accepted (joined []) = false := by decide +example : accepted (joined [.consume 0]) = true := by decide +example : accepted (joined [.consume 0, .define 0]) = false := by decide + +-- A call defines its destination on normal and unwind successors alike. Its +-- preceding argument move does not justify dropping that destination. +example : accepted { + nodes := [ + { effects := [.consume 0, .define 0], successors := [1, 2] }, + {}, + { candidateDrop := some 0 }] + localCount := 1 } = false := by decide + +-- A disconnected component is independently seeded with every declared local. +example : accepted { + nodes := [ + { effects := [.consume 0], candidateDrop := some 0 }, + { candidateDrop := some 0 }] + localCount := 1 } = false := by decide + +example : accepted { + nodes := [ + { effects := [.consume 0], candidateDrop := some 0 }, + { effects := [.consume 0], candidateDrop := some 0 }] + localCount := 1 } = true := by decide + +-- A designated entry is seeded even when it also has incoming edges. The +-- body's entry cannot inherit a move from a disconnected predecessor. +example : accepted { + nodes := [ + { effects := [.consume 0], successors := [1] }, + { candidateDrop := some 0 }] + localCount := 1, entry := 1 } = false := by decide + +-- Reject cycles everywhere, including disconnected components without drops. +example : accepted { + nodes := [ + { effects := [.consume 0], candidateDrop := some 0 }, + { successors := [2] }, + { successors := [1] }] + localCount := 1 } = false := by decide + +example : accepted { + nodes := [{ + effects := [.consume 0] + candidateDrop := some 0 + successors := [0] }] + localCount := 1 } = false := by decide + +-- No invalid graph can gain acceptance through an empty iteration or default +-- lookup. This includes the entry, successors, move/define operands, and drops. +example : accepted { nodes := [], localCount := 1 } = false := by decide +example : accepted { nodes := [{}], localCount := 0, entry := 1 } = false := by decide +example : accepted { + nodes := [{ successors := [1] }], localCount := 0 } = false := by decide +example : accepted { + nodes := [{ effects := [.consume 1], candidateDrop := some 0 }] + localCount := 1 } = false := by decide +example : accepted { + nodes := [{ effects := [.define 1] }], localCount := 1 } = false := by decide +example : accepted { + nodes := [{ candidateDrop := some 1 }], localCount := 1 } = false := by decide +example : accepted { + nodes := [{ candidateDrop := some 0 }], localCount := 0 } = false := by decide + +-- Untrusted certificates cannot remove initial obligations or forget an +-- obligation when propagating an edge. This does not depend on `infer`. +example : check { + nodes := [{ candidateDrop := some 0 }], localCount := 1 } + (fun _ => []) = false := by decide + +example : check { + nodes := [{ successors := [1] }, { candidateDrop := some 0 }] + localCount := 1 } + (fun index => if index = 0 then [0] else []) = false := by decide + +-- Instantiate the semantic theorem with an arbitrary concrete initial state. +-- No test assumes the empty state that it is supposed to establish. +example (owns : Concrete) (declared : ∀ slot, owns slot → slot < 1) : + ¬ execute [.consume 0] owns 0 := by + have reached : Reachable moved 0 owns := + .root 0 owns (by decide) (Or.inl rfl) declared + exact accepted_drop_empty (by decide : accepted moved = true) reached rfl + +example (owns : Concrete) (declared : ∀ slot, owns slot → slot < 1) + (outcome : DropOutcome) (after : Concrete) : + ConditionalDrop 0 (execute [.consume 0] owns) outcome after ↔ + outcome = .silent ∧ after = execute [.consume 0] owns := by + have reached : Reachable moved 0 owns := + .root 0 owns (by decide) (Or.inl rfl) declared + exact accepted_drop_noop (by decide : accepted moved = true) reached rfl + +end AeneasSpecs.DropOwnership.Tests