Skip to content

proof: bridge owned resources into frame couplings (#1990) #2402

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Th0rgal wants to merge 1 commit into
base: main
Choose a base branch
from
Open

proof: bridge owned resources into frame couplings (#1990) #2402

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
49 changes: 40 additions & 9 deletions Compiler/Proofs/Frames.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -474,6 +474,18 @@ def Supported (c : Coupling Abs) (support : List Resource) : Prop :=
∀ ⦃st s : RuntimeState⦄ ⦃a : Abs⦄,
(∀ r, r ∈ support → OwnedEq r st s) → c.Inv st a → c.Inv s a

/-- The canonical coupling for one owned resource. Its abstract state is a
snapshot of the concrete runtime state, but the invariant observes only `r`.
Clients can compose these couplings and later replace the snapshot with a
domain-specific abstraction via `SegmentSimWithFields.weaken`. -/
def owned (r : Resource) : Coupling RuntimeState where
Inv st snapshot := OwnedEq r snapshot st

/-- A resource coupling is supported by precisely the resource it observes. -/
theorem owned_supported (r : Resource) : Supported (owned r) [r] := by
intro st s snapshot hsame hinv
exact Resource.ownedEq_trans hinv (hsame r (by simp))

theorem supported_mono {c : Coupling Abs} {support support' : List Resource}
(hs : Supported c support)
(hsub : ∀ r, r ∈ support → r ∈ support') :
Expand Down Expand Up @@ -611,6 +623,23 @@ theorem frame_writeFootprint {fields : List Field} {c : Coupling Abs}
SegmentSimWithFields fields c prog _root_.id :=
frame hsupport (stmtListWritesOnly_writeFootprint hfp) hdisj

/-- Computed frame rule specialized to the canonical coupling for one resource.
This removes the support boilerplate from the common case where a proof needs
to carry one untouched concrete observation across a generated segment. -/
theorem frame_owned_writeFootprint {fields : List Field} {r : Resource}
{prog : List Stmt} {written : List Resource}
(hfp : Stmt.writeFootprintList prog = some written)
(hdisj : ∀ w, w ∈ written → Disjoint r w) :
SegmentSimWithFields fields (Coupling.owned r) prog _root_.id :=
frame_writeFootprint
(Coupling.owned_supported r)
hfp
(by
intro observed hobserved
simp at hobserved
subst observed
exact hdisj)

/-- Combine a local simulation with a framed invariant for untouched resources. -/
theorem and_frame {fields : List Field}
{localCoupling : Coupling Abs} {framed : Coupling Beta}
Expand Down Expand Up @@ -879,15 +908,17 @@ theorem execStmt_letVar_preserves_selector_calldata
(st s : RuntimeState) (name : String) (e : Expr)
(h : execStmt [] st (.letVar name e) = .continue s) :
PreservesSelectorCalldata st s := by
rw [show execStmt [] st (.letVar name e) = (match evalExpr [] st e with
| some resolved => .continue { st with bindings := bindValue st.bindings name resolved }
| none => .revert) from rfl] at h
cases hev : evalExpr [] st e with
| none => rw [hev] at h; exact absurd h (by simp)
| some _ =>
rw [hev] at h
injection h with hh; subst hh
exact And.intro rfl rfl
have hsim : SegmentSim (Coupling.owned .static) [.letVar name e] _root_.id :=
SegmentSimWithFields.frame_owned_writeFootprint
(by rfl)
(by
intro w hw
simp at hw
subst w
trivial)
have hexec : execStmtList [] st [.letVar name e] = .continue s := by
simp [execStmtList, h]
exact hsim (Resource.ownedEq_refl .static st) hexec

theorem execStmt_mstore_preserves_selector_calldata
(st s : RuntimeState) (off val : Expr)
Expand Down
4 changes: 3 additions & 1 deletion PrintAxioms.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2022,6 +2022,7 @@ end Verity.AxiomAudit
Compiler.Proofs.Frames.stmtListWritesOnly_writeFootprint
Compiler.Proofs.Frames.execStmt_frame_rule_writeFootprint
Compiler.Proofs.Frames.execStmts_frame_rule_writeFootprint
Compiler.Proofs.Frames.Coupling.owned_supported
Compiler.Proofs.Frames.Coupling.supported_mono
Compiler.Proofs.Frames.Coupling.supported_and
Compiler.Proofs.Frames.Coupling.iterFrom_zero
Expand All @@ -2033,6 +2034,7 @@ end Verity.AxiomAudit
Compiler.Proofs.Frames.SegmentSimWithFields.weaken
Compiler.Proofs.Frames.SegmentSimWithFields.frame
Compiler.Proofs.Frames.SegmentSimWithFields.frame_writeFootprint
Compiler.Proofs.Frames.SegmentSimWithFields.frame_owned_writeFootprint
Compiler.Proofs.Frames.SegmentSimWithFields.and_frame
Compiler.Proofs.Frames.SegmentSimWithFields.execForEachLoop_sim
Compiler.Proofs.Frames.SegmentSimWithFields.forEach
Expand Down Expand Up @@ -7497,4 +7499,4 @@ end Verity.AxiomAudit
Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
]

-- Total: 6938 theorems/lemmas (4948 public, 1990 private, 0 sorry'd)
-- Total: 6940 theorems/lemmas (4950 public, 1990 private, 0 sorry'd)
Loading