SepLogic.lean🔗

Declarations on this page (32)

Byte-Granular Separation Logic Primitives

Defines byte-granular partial heaps (Heap, GhostName), nominal separation-logic propositions and connectives (SepProp, m ⊨ P, P ∗ Q, P -∗ Q, ∃∗ x, P x, P ⊢ Q, |==> P, ⌜φ⌝), multi-width points-to assertions (↦₈, ↦₁₆, ↦₃₂, ↦₆₄, ↦₁₂₈, ↦ₛ, ↦₆₄*, ↦₈ₙ, ↦ₙ, and their read-only and lazy-free counterparts), byte regions (InRegion, DisjointRegions, regionBlock, memRegion, regionBlockProtNone, memRegionProtNone), downward stack frames (stackFrame, stackFrame16, stackFrame32, stackFrameAt), and abstract allocator interfaces (Allocator, AllocatorOom).

SepProp is a nominal structure whose projection (SepProp.holds) and core connective/points-to definitions live inside a plain public section (without @[expose]), keeping connective bodies module-opaque to client proofs unless Arm64/Trusted/Spec/SepLogicModel.lean is imported explicitly. The partial commutative monoid laws for Heap and BI laws for SepProp are verified in Arm64/Testing/Tours/SepLogicLawsTour.lean.

namespace Arm64

@[expose] public section

Memory Regions

def InRegionL41–43 ↗#

a lies in the len-byte region [base, base + len) (wrapping modulo 2^64).

def InRegion (base : BitVec 64) (len : Nat) (a : BitVec 64) : Prop :=
  (a - base).toNat < len

instance instDecidableInRegionL45–47 ↗#

instance instDecidableInRegion (base : BitVec 64) (len : Nat) (a : BitVec 64) :
    Decidable (InRegion base len a) :=
  inferInstanceAs (Decidable ((a - base).toNat < len))

22 declarations not shown (lines 49–220): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.OutsideRegion, Arm64.DisjointRegions, Arm64.Memory.Readable, Arm64.Memory.RO, Arm64.memRO, Arm64.GhostName, Arm64.HeapCell.protNoneLazy, Arm64.HeapCell.rw, Arm64.HeapCell.ro, Arm64.HeapCell.protNone, Arm64.HeapCell, Arm64.HeapCell.lazy, Arm64.Heap.frag, Arm64.Heap, Arm64.Heap.phys, Arm64.Heap.mapped, Arm64.Heap.auth, Arm64.Heap.empty, Arm64.Heap.singleton, Arm64.Heap.singletonRO, Arm64.Heap.singletonProtNone, Arm64.Heap.singletonLazy, Arm64.Heap.Disjoint, Arm64.Heap.union, Arm64.Heap.GhostValid, Arm64.Heap.Matches, Arm64.regionHeap, Arm64.regionHeapRO, Arm64.regionHeapProtNone, Arm64.regionHeapLazy, Arm64.SepProp.holds, Arm64.SepProp

end -- @[expose] public section

10 declarations not shown (lines 226–274): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.SepProp.Holds, Arm64.SepProp.Satisfies, Arm64.SepProp.Entails, Arm64.SepProp.bupd, Arm64.SepProp.emp, Arm64.SepProp.anyHeap, Arm64.SepProp.pure, Arm64.SepProp.sepConj, Arm64.SepProp.sepImp, Arm64.SepProp.sepExists

notation " ⊨ "L280 ↗#

notation:50 m:50 " ⊨ " P:51 => SepProp.Satisfies P m

infixL281 ↗#

infix:50 " ⊢ " => SepProp.Entails

prefixL282 ↗#

prefix:58 "|==> " => SepProp.bupd

notation "⌜"L283 ↗#

notation "⌜" φ "⌝" => SepProp.pure φ

infixrL284 ↗#

infixr:60 " ∗ " => SepProp.sepConj

infixrL285 ↗#

infixr:55 " -∗ " => SepProp.sepImp

notation "∃∗ "L286 ↗#

notation:65 "∃∗ " x ", " P => SepProp.sepExists (fun x => P)

notation "∃∗ "L287 ↗#

notation:65 "∃∗ " x " : " α ", " P => SepProp.sepExists (fun (x : α) => P)

19 declarations not shown (lines 289–398): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.SepProp.pure_dup, Arm64.pointsTo8, Arm64.pointsToBytes, Arm64.pointsTo8RO, Arm64.pointsToBytesRO, Arm64.pointsTo8ProtNone, Arm64.pointsToBytesProtNone, Arm64.pointsTo8Lazy, Arm64.regionBlock, Arm64.regionBlockRO, Arm64.regionBlockProtNone, Arm64.memRegion, Arm64.memRegionProtNone, Arm64.memRegionLazy, Arm64.pointsTo16, Arm64.pointsTo32, Arm64.pointsTo64, Arm64.pointsTo128, Arm64.pointsToWords64

infixL400 ↗#

infix:70 " ↦₈ " => pointsTo8

infixL401 ↗#

infix:70 " ↦ₛ " => pointsToBytes

infixL402 ↗#

infix:70 " ↦₁₆ " => pointsTo16

infixL403 ↗#

infix:70 " ↦₃₂ " => pointsTo32

infixL404 ↗#

infix:70 " ↦₆₄ " => pointsTo64

infixL405 ↗#

infix:70 " ↦₁₂₈ " => pointsTo128

infixL406 ↗#

infix:70 " ↦₆₄* " => pointsToWords64

5 declarations not shown (lines 408–438): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.pointsTo16RO, Arm64.pointsTo32RO, Arm64.pointsTo64RO, Arm64.pointsTo128RO, Arm64.pointsToWords64RO

infixL440 ↗#

infix:70 " ↦₈ᵣ " => pointsTo8RO

infixL441 ↗#

infix:70 " ↦ᵣ " => pointsToBytesRO

infixL442 ↗#

infix:70 " ↦₁₆ᵣ " => pointsTo16RO

infixL443 ↗#

infix:70 " ↦₃₂ᵣ " => pointsTo32RO

infixL444 ↗#

infix:70 " ↦₆₄ᵣ " => pointsTo64RO

infixL445 ↗#

infix:70 " ↦₁₂₈ᵣ " => pointsTo128RO

infixL446 ↗#

infix:70 " ↦₆₄ᵣ* " => pointsToWords64RO

infixL448 ↗#

infix:70 " ↦₈ₙ " => pointsTo8ProtNone

infixL449 ↗#

infix:70 " ↦ₙ " => pointsToBytesProtNone

5 declarations not shown (lines 451–480): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.pointsTo16Lazy, Arm64.pointsTo32Lazy, Arm64.pointsTo64Lazy, Arm64.pointsTo128Lazy, Arm64.memLazy

postfixL482 ↗#

postfix:70 " ↦₈ₗ" => pointsTo8Lazy

postfixL483 ↗#

postfix:70 " ↦₁₆ₗ" => pointsTo16Lazy

postfixL484 ↗#

postfix:70 " ↦₃₂ₗ" => pointsTo32Lazy

postfixL485 ↗#

postfix:70 " ↦₆₄ₗ" => pointsTo64Lazy

postfixL486 ↗#

postfix:70 " ↦₁₂₈ₗ" => pointsTo128Lazy

postfixL487 ↗#

postfix:70 " ↦ₗ" => pointsTo8Lazy

12 declarations not shown (lines 489–577): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.stackFrame, Arm64.stackFrame16At, Arm64.stackFrame16, Arm64.stackFrame32At, Arm64.stackFrame32, Arm64.stackFrameSlotsCont, Arm64.stackFrameSlotsFrom, Arm64.stackFrameAt, Arm64.Allocator, Arm64.Allocator.noWrap, Arm64.Allocator.live, Arm64.Allocator.pool, Arm64.AllocatorOom, Arm64.AllocatorOom.noWrap, Arm64.AllocatorOom.pool, Arm64.AllocatorOom.live, Arm64.AllocatorOom.toAllocator, Arm64.Allocator.toAllocatorOom

end Arm64