Heap semantics of IMP

AbbreviationHeap#✓fully proved

A heap is a finite partial map from addresses to values, where addresses and values are natural numbers: it stores a value \(v \in \mathbb{N}\) at each address of a finite set of addresses in \(\mathbb{N}\), called the addresses allocated in the heap.

abbrev Heap := Finmap (fun _ : Nat => Nat)

Used by 44

Used byAssignment rule with a store-irrelevant heap assertion · Empty-heap assertion · Entailment of heap assertions · Existential rule for separation-logic triples · Frame rule · Store-irrelevant frames satisfy the frame-rule side condition · Conjunction of heap assertions · Heap assertion · Existential heap assertion · Hoare validity embeds into separation validity · Framed embedding of Hoare validity · Points-to assertion · Pure assertion · Local rule for a heap read · Separation-logic triple validity · Separating conjunction · Pulling a store fact out of a separating conjunction · Rearranging a separating conjunction · Store-irrelevant heap assertions · Separation-logic while rule · Frame decomposition of heap executions · Frame decomposition of a single heap step · Disjoint heaps · The empty heap is disjoint from every heap · Every heap is disjoint from the empty heap · Erasing an address preserves disjointness · Inserting an address the other heap lacks preserves disjointness · Disjointness from a singleton heap · Erasing an address that the right heap of a union lacks · Every heap has a free address · Adding a frame heap preserves the ability to step · Heap configurations · Small-step semantics of heap commands · Reinserting an erased value restores the heap · Steps do not enlarge the modified variables · Executions of embedded commands are plain executions · Safe heap configurations · Embedded plain commands are safe · A heap step only changes assignable variables · Heap executions only change assignable variables · Symmetry of heap disjointness · Embedding preserves termination · Heap steps of embedded commands are plain steps · Plain executions lift to the heap language

DefinitionDisjoint heaps#✓fully proved

Two heaps \(h_1\) and \(h_2\) are disjoint when no address is allocated in both: every address allocated in \(h_1\) is not allocated in \(h_2\).

def Disjoint (h₁ h₂ : Heap) : Prop := ∀ a, a ∈ h₁ → a ∉ h₂

Uses 1 · Used by 13

Statement usesHeap

Used byFrame rule · Separating conjunction · Pulling a store fact out of a separating conjunction · Rearranging a separating conjunction · Frame decomposition of heap executions · Frame decomposition of a single heap step · The empty heap is disjoint from every heap · Every heap is disjoint from the empty heap · Erasing an address preserves disjointness · Inserting an address the other heap lacks preserves disjointness · Disjointness from a singleton heap · Adding a frame heap preserves the ability to step · Symmetry of heap disjointness

TheoremSymmetry of heap disjointness#✓fully proved

For heaps \(h_1\) and \(h_2\), if \(h_1\) and \(h_2\) are disjoint, then \(h_2\) and \(h_1\) are disjoint.

@[symm]
theorem Disjoint.symm {h₁ h₂ : Heap} (h : Disjoint h₁ h₂) : Disjoint h₂ h₁

Uses 2 · Used by 1

Statement usesHeap · Disjoint heaps

Used byRearranging a separating conjunction

TheoremThe empty heap is disjoint from every heap#✓fully proved

For every heap \(h\), the empty heap is disjoint from \(h\) (with the empty heap as the first heap).

theorem disjoint_empty_left (h : Heap) : Disjoint ∅ h

Uses 2

Statement usesHeap · Disjoint heaps

TheoremEvery heap is disjoint from the empty heap#✓fully proved

For every heap \(h\), \(h\) is disjoint from the empty heap (with the empty heap as the second heap).

theorem disjoint_empty_right (h : Heap) : Disjoint h ∅

Uses 2

Statement usesHeap · Disjoint heaps

TheoremErasing an address that the right heap of a union lacks#✓fully proved

For heaps \(h_1\) and \(h_2\), let \(h_1 \cup h_2\) be their left-biased union (at an address allocated in both it keeps the value from \(h_1\)). If the address \(a\) is not allocated in \(h_2\), then erasing \(a\) from \(h_1 \cup h_2\) gives the union of \(h_2\) with the heap obtained from \(h_1\) by erasing \(a\), taken with that heap on the left.

theorem erase_union_of_notMem {a : Nat} {h₁ h₂ : Heap} (ha : a ∉ h₂) :
    Finmap.erase a (h₁ ∪ h₂) = Finmap.erase a h₁ ∪ h₂

Uses 1 · Used by 1

Statement usesHeap

Used byFrame decomposition of a single heap step

TheoremInserting an address the other heap lacks preserves disjointness#✓fully proved

If heaps \(h_1\) and \(h_2\) are disjoint and the address \(a\) is not allocated in \(h_2\), then for every value \(v\), the heap obtained from \(h_1\) by inserting \(a\) with value \(v\) (overwriting any value \(h_1\) stores at \(a\)) is disjoint from \(h_2\).

theorem disjoint_insert_left {h₁ h₂ : Heap} {a v : Nat}
    (hd : Disjoint h₁ h₂) (ha : a ∉ h₂) : Disjoint (Finmap.insert a v h₁) h₂

Uses 2 · Used by 1

Statement usesHeap · Disjoint heaps

Used byFrame decomposition of a single heap step

TheoremErasing an address preserves disjointness#✓fully proved

If heaps \(h_1\) and \(h_2\) are disjoint, then for every address \(a\), the heap obtained from \(h_1\) by erasing \(a\) (removing the address \(a\) and its value) is disjoint from \(h_2\).

theorem disjoint_erase_left {h₁ h₂ : Heap} {a : Nat}
    (hd : Disjoint h₁ h₂) : Disjoint (Finmap.erase a h₁) h₂

Uses 2 · Used by 1

Statement usesHeap · Disjoint heaps

Used byFrame decomposition of a single heap step

TheoremDisjointness from a singleton heap#✓fully proved

For every address \(a\), value \(v\) and heap \(h\), the singleton heap that stores \(v\) at \(a\) and allocates no other address is disjoint from \(h\) if and only if \(a\) is not allocated in \(h\).

theorem disjoint_singleton_left {a v : Nat} {h : Heap} :
    Disjoint (Finmap.singleton a v) h ↔ a ∉ h

Uses 2

Statement usesHeap · Disjoint heaps

TheoremReinserting an erased value restores the heap#✓fully proved

If a heap \(h\) stores the value \(v\) at the address \(a\), then erasing \(a\) from \(h\) and then inserting \(a\) with value \(v\) gives back \(h\).

theorem insert_erase_eq_self {h : Heap} {a v : Nat} (hv : h.lookup a = some v) :
    Finmap.insert a v (Finmap.erase a h) = h

Uses 1

Statement usesHeap

TheoremEvery heap has a free address#✓fully proved

For every heap \(h\) there is an address that is not allocated in \(h\).

theorem exists_notMem (h : Heap) : ∃ a, a ∉ h

Uses 1 · Used by 1

Statement usesHeap

Used byAdding a frame heap preserves the ability to step

InductiveHeap commands#✓fully proved

Heap commands extend the commands of IMP with heap operations. A heap command is one of: \(\mathbf{skip}\); an assignment \(x := a\); a sequence \(c_1; c_2\); a conditional \(\mathbf{if}\ b\ \mathbf{then}\ c_1\ \mathbf{else}\ c_2\); a loop \(\mathbf{while}\ b\ \mathbf{do}\ c\); a heap read \(x := [a]\); a heap write \([a] := e\); an allocation \(x := \mathbf{alloc}(e)\); or a deallocation \(\mathbf{free}(a)\). Here \(x\) is a variable (a natural number), \(a\) and \(e\) are arithmetic expressions, \(b\) is a Boolean expression, and \(c\), \(c_1\), \(c_2\) are heap commands.

inductive HeapCmd where
  | skip
  | assign (name : Nat) (value : AExp)
  | seq (first second : HeapCmd)
  | ite (guard : BExp) (thenBranch elseBranch : HeapCmd)
  | while (guard : BExp) (body : HeapCmd)
  | read (name : Nat) (addr : AExp)
  | write (addr value : AExp)
  | alloc (name : Nat) (value : AExp)
  | free (addr : AExp)
  deriving DecidableEq, Repr

Uses 2 · Used by 24

Statement usesArithmetic expressions of IMP · Boolean expressions of IMP

Used byAssignment rule with a store-irrelevant heap assertion · Existential rule for separation-logic triples · Frame rule · Store-irrelevant frames satisfy the frame-rule side condition · Hoare validity embeds into separation validity · Local rule for a heap read · Separation-logic triple validity · Separation-logic while rule · Frame decomposition of heap executions · Frame decomposition of a single heap step · Adding a frame heap preserves the ability to step · Heap configurations · Small-step semantics of heap commands · Modified variables of a heap command · Steps do not enlarge the modified variables · Executions of embedded commands are plain executions · Safe heap configurations · Embedded plain commands are safe · A heap step only changes assignable variables · Heap executions only change assignable variables · Embedding preserves termination · Embedding of IMP into the heap language · Heap steps of embedded commands are plain steps · Plain executions lift to the heap language

AbbreviationHeap configurations#✓fully proved

A heap configuration is a triple \((c, s, h)\) of a heap command \(c\), a store \(s\) and a heap \(h\).

abbrev HConfig := HeapCmd × State × Heap

Uses 3 · Used by 18

Statement usesHeap · Heap commands · IMP program states

Used byAssignment rule with a store-irrelevant heap assertion · Frame rule · Local rule for a heap read · Separation-logic while rule · Frame decomposition of heap executions · Frame decomposition of a single heap step · Adding a frame heap preserves the ability to step · Small-step semantics of heap commands · Multi-step heap execution · Steps do not enlarge the modified variables · Safety is preserved along executions · Executions of embedded commands are plain executions · Safe heap configurations · Embedded plain commands are safe · A heap step only changes assignable variables · Heap executions only change assignable variables · Heap steps of embedded commands are plain steps · Plain executions lift to the heap language

InductiveSmall-step semantics of heap commands#✓fully proved

The single-step relation \((c, s, h) \to (c', s', h')\) on heap configurations is the least relation closed under the rules below. Here \(a(s)\) is the value of an expression \(a\) in the store \(s\), \(s[x \mapsto n]\) is \(s\) with variable \(x\) set to \(n\), \(h[\ell \mapsto n]\) is \(h\) with address \(\ell\) set to \(n\), and \(h \setminus \ell\) is \(h\) with address \(\ell\) removed.

• Assignment: \((x := a, s, h) \to (\mathbf{skip}, s[x \mapsto a(s)], h)\).
• Sequence: \((\mathbf{skip}; c_2, s, h) \to (c_2, s, h)\), and if \((c_1, s, h) \to (c_1', s', h')\) then \((c_1; c_2, s, h) \to (c_1'; c_2, s', h')\).
• Conditional: \((\mathbf{if}\ b\ \mathbf{then}\ c_1\ \mathbf{else}\ c_2, s, h)\) steps to \((c_1, s, h)\) if \(b(s)\) is true and to \((c_2, s, h)\) if \(b(s)\) is false.
• Loop: \((\mathbf{while}\ b\ \mathbf{do}\ c, s, h)\) steps to \((\mathbf{if}\ b\ \mathbf{then}\ d\ \mathbf{else}\ \mathbf{skip}, s, h)\), where \(d\) is the sequence \(c; \mathbf{while}\ b\ \mathbf{do}\ c\).
• Read: if \(h\) maps the address \(a(s)\) to \(v\), then \((x := [a], s, h) \to (\mathbf{skip}, s[x \mapsto v], h)\).
• Write: if \(a(s)\) is allocated in \(h\), then \(([a] := e, s, h) \to (\mathbf{skip}, s, h[a(s) \mapsto e(s)])\).
• Allocation: for every address \(\ell\) not allocated in \(h\), \((x := \mathbf{alloc}(e), s, h) \to (\mathbf{skip}, s[x \mapsto \ell], h[\ell \mapsto e(s)])\).
• Deallocation: if \(a(s)\) is allocated in \(h\), then \((\mathbf{free}(a), s, h) \to (\mathbf{skip}, s, h \setminus a(s))\).

Cslib.IMP.HStep · 35 lines

inductive HStep : HConfig → HConfig → Prop
  | assign (state) (name) (value) (heap) :
      HStep (.assign name value, state, heap)
        (.skip, Function.update state name (value.eval state), heap)
  | seqSkip (second) (state) (heap) :
      HStep (.seq .skip second, state, heap) (second, state, heap)
  | seqStep {first first' second initial final heap heap'}
      (step : HStep (first, initial, heap) (first', final, heap')) :
      HStep (.seq first second, initial, heap) (.seq first' second, final, heap')
  | iteTrue {guard thenBranch elseBranch state heap}
      (guardTrue : guard.eval state = true) :
      HStep (.ite guard thenBranch elseBranch, state, heap) (thenBranch, state, heap)
  | iteFalse {guard thenBranch elseBranch state heap}
      (guardFalse : guard.eval state = false) :
      HStep (.ite guard thenBranch elseBranch, state, heap) (elseBranch, state, heap)
  | whileStep (guard) (body) (state) (heap) :
      HStep (.while guard body, state, heap)
        (.ite guard (.seq body (.while guard body)) .skip, state, heap)
  | read {name addr state heap value}
      (lookup : heap.lookup (addr.eval state) = some value) :
      HStep (.read name addr, state, heap)
        (.skip, Function.update state name value, heap)
  | write {addr value state heap}
      (mem : addr.eval state ∈ heap) :
      HStep (.write addr value, state, heap)
        (.skip, state, Finmap.insert (addr.eval state) (value.eval state) heap)
  | alloc {name value state heap address}
      (notMem : address ∉ heap) :
      HStep (.alloc name value, state, heap)
        (.skip, Function.update state name address,
          Finmap.insert address (value.eval state) heap)
  | free {addr state heap}
      (mem : addr.eval state ∈ heap) :
      HStep (.free addr, state, heap)
        (.skip, state, Finmap.erase (addr.eval state) heap)

Uses 8 · Used by 17

Statement usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Heap configurations · Heap · Heap commands · IMP program states

Used byAssignment rule with a store-irrelevant heap assertion · Frame rule · Local rule for a heap read · Separation-logic while rule · Frame decomposition of heap executions · Frame decomposition of a single heap step · Adding a frame heap preserves the ability to step · Multi-step heap execution · Steps do not enlarge the modified variables · Safety is preserved along executions · Executions of embedded commands are plain executions · Safe heap configurations · Embedded plain commands are safe · A heap step only changes assignable variables · Heap executions only change assignable variables · Heap steps of embedded commands are plain steps · Plain executions lift to the heap language

AbbreviationMulti-step heap execution#✓fully proved

The relation \((c, s, h) \to^* (c', s', h')\) on heap configurations is the reflexive-transitive closure of the small-step relation: it holds when the first configuration reaches the second by a finite, possibly empty, sequence of small steps.

abbrev HSteps : HConfig → HConfig → Prop := Relation.ReflTransGen HStep

Uses 2 · Used by 15

Statement usesHeap configurations · Small-step semantics of heap commands

Used byAssignment rule with a store-irrelevant heap assertion · Existential rule for separation-logic triples · Frame rule · Hoare validity embeds into separation validity · Local rule for a heap read · Separation-logic triple validity · Separation-logic while rule · Frame decomposition of heap executions · Safety is preserved along executions · Executions of embedded commands are plain executions · Safe heap configurations · Embedded plain commands are safe · Heap executions only change assignable variables · Embedding preserves termination · Plain executions lift to the heap language

DefinitionSafe heap configurations#✓fully proved

A heap configuration, consisting of a heap command, a store and a heap, is safe when every heap configuration reachable from it in zero or more heap steps either has command \(\mathtt{skip}\) or can take a further heap step.

def Safe (cfg : HConfig) : Prop :=
  ∀ cfg', HSteps cfg cfg' → cfg'.1 = .skip ∨ ∃ cfg'', HStep cfg' cfg''

Uses 6 · Used by 10

Statement usesHeap configurations · Small-step semantics of heap commands · Multi-step heap execution · Heap · Heap commands · IMP program states

Used byAssignment rule with a store-irrelevant heap assertion · Existential rule for separation-logic triples · Frame rule · Hoare validity embeds into separation validity · Local rule for a heap read · Separation-logic triple validity · Separation-logic while rule · Frame decomposition of heap executions · Safety is preserved along executions · Embedded plain commands are safe

TheoremSafety is preserved along executions#✓fully proved

If a heap configuration is safe and reaches a second configuration by finitely many (possibly zero) small steps, then the second configuration is safe.

theorem Safe.of_steps {cfg cfg' : HConfig} (hsafe : Safe cfg)
    (hsteps : HSteps cfg cfg') : Safe cfg'

Uses 4 · Used by 1

Statement usesHeap configurations · Multi-step heap execution · Safe heap configurations

Proof usesSmall-step semantics of heap commands

Used byFrame decomposition of heap executions

TheoremAdding a frame heap preserves the ability to step#✓fully proved

Let \(h\) and \(h_f\) be disjoint heaps, \(c\) a heap command and \(s\) a store. If the configuration \((c, s, h)\) can take a small step, then so can \((c, s, h \cup h_f)\).

Allocation may choose a different fresh address on the larger heap.

theorem exists_step_frame {c : HeapCmd} {s : State} {h hf : Heap}
    (_hd : Heap.Disjoint h hf) (hex : ∃ cfg', HStep (c, s, h) cfg') :
    ∃ cfg', HStep (c, s, h ∪ hf) cfg'

Uses 11 · Used by 1

Statement usesHeap configurations · Small-step semantics of heap commands · Heap · Disjoint heaps · Heap commands · IMP program states

Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Every heap has a free address

Used byFrame rule

TheoremFrame decomposition of a single heap step#✓fully proved

Let \(h\) and \(h_f\) be disjoint heaps, \(c\) a heap command and \(s\) a store, and suppose that the configuration \((c, s, h)\) can take a small step. If \((c, s, h \cup h_f)\) takes a small step to \((c', s', h'')\), then there is a heap \(h_1\), disjoint from \(h_f\), such that \((c, s, h)\) takes a small step to \((c', s', h_1)\) and \(h'' = h_1 \cup h_f\).

The step-existence hypothesis forces any address the step touches to lie in \(h\).

theorem decompose_of_safe_step {c c' : HeapCmd} {s s' : State} {h hf h'' : Heap}
    (hd : Heap.Disjoint h hf) (hex : ∃ cfg', HStep (c, s, h) cfg')
    (hstep : HStep (c, s, h ∪ hf) (c', s', h'')) :
    ∃ h₁, HStep (c, s, h) (c', s', h₁) ∧ Heap.Disjoint h₁ hf ∧ h'' = h₁ ∪ hf

Uses 13 · Used by 1

Statement usesHeap configurations · Small-step semantics of heap commands · Heap · Disjoint heaps · Heap commands · IMP program states

Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Erasing an address preserves disjointness · Inserting an address the other heap lacks preserves disjointness · Erasing an address that the right heap of a union lacks

Used byFrame decomposition of heap executions

TheoremFrame decomposition of heap executions#✓fully proved

Let \(h\) and \(h_f\) be disjoint heaps, \(c\) a heap command and \(s\) a store, and suppose that the configuration \((c, s, h)\) is safe. If \((c, s, h \cup h_f)\) reaches \((c'', s'', h'')\) by finitely many (possibly zero) small steps, then there is a heap \(h_2\), disjoint from \(h_f\), such that \((c, s, h)\) reaches \((c'', s'', h_2)\) by finitely many small steps, \(h'' = h_2 \cup h_f\), and \((c'', s'', h_2)\) is safe.

Safety supplies the step-existence that single-step decomposition needs at each stage.

theorem decompose_of_safe {c c'' : HeapCmd} {s s'' : State} {h hf h'' : Heap}
    (hd : Heap.Disjoint h hf) (hsafe : Safe (c, s, h))
    (hsteps : HSteps (c, s, h ∪ hf) (c'', s'', h'')) :
    ∃ h₂, HSteps (c, s, h) (c'', s'', h₂) ∧ Heap.Disjoint h₂ hf ∧
      h'' = h₂ ∪ hf ∧ Safe (c'', s'', h₂)

Uses 14 · Used by 1

Statement usesMulti-step heap execution · Heap · Disjoint heaps · Heap commands · Safe heap configurations · IMP program states

Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Heap configurations · Small-step semantics of heap commands · Frame decomposition of a single heap step · Safety is preserved along executions

Used byFrame rule

DefinitionEmbedding of IMP into the heap language#✓fully proved

The embedding sends each plain IMP command to the heap command of the same shape: \(\mathtt{skip}\) goes to \(\mathtt{skip}\), an assignment of an arithmetic expression to a variable goes to the same assignment, a sequence goes to the sequence of the embeddings of its parts, and a conditional or while loop goes to the conditional or while loop with the same guard and with each subcommand replaced by its embedding.

def toHeap : Cmd → HeapCmd
  | .skip => .skip
  | .assign name value => .assign name value
  | .seq first second => .seq first.toHeap second.toHeap
  | .ite guard thenBranch elseBranch =>
      .ite guard thenBranch.toHeap elseBranch.toHeap
  | .while guard body => .while guard body.toHeap

Uses 4 · Used by 7

Statement usesArithmetic expressions of IMP · Boolean expressions of IMP · Commands of IMP · Heap commands

Used byHoare validity embeds into separation validity · Framed embedding of Hoare validity · Executions of embedded commands are plain executions · Embedded plain commands are safe · Embedding preserves termination · Heap steps of embedded commands are plain steps · Plain executions lift to the heap language

TheoremHeap steps of embedded commands are plain steps#✓fully proved

Let \(c\) be a plain IMP command, \(s\) a store and \(h\) a heap, and write \(\overline{d}\) for the embedding of a plain command \(d\) into the heap language. Then \((\overline{c}, s, h)\) takes a heap step to a heap configuration \(K\) if and only if there are a plain command \(c'\) and a store \(s'\) such that \((c, s)\) takes a plain small step to \((c', s')\) and \(K = (\overline{c'}, s', h)\).

theorem toHeap_iff {c : Cmd} {s : State} {h : Heap} {cfg : HConfig} :
    HStep (c.toHeap, s, h) cfg ↔
      ∃ c' s', Step (c, s) (c', s') ∧ cfg = (c'.toHeap, s', h)

Uses 13 · Used by 3

Statement usesCommands of IMP · Embedding of IMP into the heap language · Heap configurations · Small-step semantics of heap commands · Heap · Heap commands · IMP program states · IMP small-step relation

Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · IMP configuration

Used byExecutions of embedded commands are plain executions · Embedded plain commands are safe · Plain executions lift to the heap language

TheoremExecutions of embedded commands are plain executions#✓fully proved

Let \(c\) be a plain IMP command, \(s\) a store and \(h\) a heap, and write \(\overline{d}\) for the embedding of a plain command \(d\) into the heap language. If \((\overline{c}, s, h)\) reaches a heap configuration \((c_2, s_2, h_2)\) in zero or more heap steps, then \(h_2 = h\) and there is a plain command \(c_2'\) with \(c_2 = \overline{c_2'}\) such that \((c, s)\) reaches \((c_2', s_2)\) in zero or more plain small steps.

theorem of_toHeap {c : Cmd} {s : State} {h : Heap} {c₂ : HeapCmd} {s₂ : State}
    {h₂ : Heap} (hsteps : HSteps (c.toHeap, s, h) (c₂, s₂, h₂)) :
    ∃ c₂', c₂ = c₂'.toHeap ∧ Steps (c, s) (c₂', s₂) ∧ h₂ = h

Uses 12 · Used by 3

Statement usesCommands of IMP · Embedding of IMP into the heap language · Multi-step heap execution · Heap · Heap commands · IMP program states · IMP multi-step relation

Proof usesIMP configuration · Heap configurations · Small-step semantics of heap commands · Heap steps of embedded commands are plain steps · IMP small-step relation

Used byHoare validity embeds into separation validity · Embedded plain commands are safe · Embedding preserves termination

TheoremPlain executions lift to the heap language#✓fully proved

Let \(c, c_2\) be plain IMP commands, \(s, s_2\) stores and \(h\) a heap, and write \(\overline{d}\) for the embedding of a plain command \(d\) into the heap language. If \((c, s)\) reaches \((c_2, s_2)\) in zero or more plain small steps, then \((\overline{c}, s, h)\) reaches \((\overline{c_2}, s_2, h)\) in zero or more heap steps.

theorem toHeap_of_steps {c c₂ : Cmd} {s s₂ : State} {h : Heap}
    (hsteps : Steps (c, s) (c₂, s₂)) :
    HSteps (c.toHeap, s, h) (c₂.toHeap, s₂, h)

Uses 12 · Used by 1

Statement usesCommands of IMP · Embedding of IMP into the heap language · Multi-step heap execution · Heap · Heap commands · IMP program states · IMP multi-step relation

Proof usesIMP configuration · Heap configurations · Small-step semantics of heap commands · Heap steps of embedded commands are plain steps · IMP small-step relation

Used byEmbedding preserves termination

TheoremEmbedded plain commands are safe#✓fully proved

For every plain IMP command \(c\) with embedding \(\overline{c}\) into the heap language, every store \(s\) and every heap \(h\), the heap configuration \((\overline{c}, s, h)\) is safe.

This holds because plain IMP never gets stuck except at \(\mathtt{skip}\).

theorem safe_toHeap (c : Cmd) (s : State) (h : Heap) : Safe (c.toHeap, s, h)

Uses 18 · Used by 1

Statement usesCommands of IMP · Embedding of IMP into the heap language · Heap · Heap commands · Safe heap configurations · IMP program states

Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · IMP configuration · Heap configurations · Small-step semantics of heap commands · Heap steps of embedded commands are plain steps · Multi-step heap execution · Executions of embedded commands are plain executions · IMP small-step relation · IMP multi-step relation

Used byHoare validity embeds into separation validity

TheoremEmbedding preserves termination#✓fully proved

Let \(c\) be a plain IMP command with embedding \(\overline{c}\) into the heap language, let \(s, s'\) be stores and let \(h\) be a heap. Then \(c\) terminates from \(s\) with final store \(s'\) if and only if \((\overline{c}, s, h)\) reaches \((\mathtt{skip}, s', h)\) in zero or more heap steps.

theorem terminates_toHeap {c : Cmd} {s s' : State} {h : Heap} :
    Terminates c s s' ↔ HSteps (c.toHeap, s, h) (.skip, s', h)

Uses 12

Statement usesCommands of IMP · Embedding of IMP into the heap language · Multi-step heap execution · Heap · Heap commands · IMP program states · Termination of an IMP command

Proof usesArithmetic expressions of IMP · Boolean expressions of IMP · Executions of embedded commands are plain executions · Plain executions lift to the heap language · IMP multi-step relation

DefinitionModified variables of a heap command#✓fully proved

The set \(\mathrm{mod}(c)\) of variables a heap command \(c\) may assign to is defined by recursion on \(c\). It is empty for \(\mathbf{skip}\), a heap write \([a] := e\) and a deallocation \(\mathbf{free}(a)\); it is \(\{x\}\) for an assignment \(x := a\), a heap read \(x := [a]\) and an allocation \(x := \mathbf{alloc}(e)\); it is \(\mathrm{mod}(c_1) \cup \mathrm{mod}(c_2)\) for a sequence \(c_1; c_2\) and for a conditional \(\mathbf{if}\ b\ \mathbf{then}\ c_1\ \mathbf{else}\ c_2\); and it is \(\mathrm{mod}(c_0)\) for a loop \(\mathbf{while}\ b\ \mathbf{do}\ c_0\).

def modVars : HeapCmd → Finset Nat
  | .skip => ∅
  | .assign name _ => {name}
  | .seq first second => first.modVars ∪ second.modVars
  | .ite _ thenBranch elseBranch => thenBranch.modVars ∪ elseBranch.modVars
  | .while _ body => body.modVars
  | .read name _ => {name}
  | .write _ _ => ∅
  | .alloc name _ => {name}
  | .free _ => ∅

Uses 3 · Used by 6

Statement usesArithmetic expressions of IMP · Boolean expressions of IMP · Heap commands

Used byFrame rule · Store-irrelevant frames satisfy the frame-rule side condition · Framed embedding of Hoare validity · Steps do not enlarge the modified variables · A heap step only changes assignable variables · Heap executions only change assignable variables

TheoremSteps do not enlarge the modified variables#✓fully proved

Write \(\mathrm{mod}(c)\) for the set of variables a heap command \(c\) may assign to. If the configuration \((c, s, h)\) takes a small step to \((c', s', h')\), then \(\mathrm{mod}(c') \subseteq \mathrm{mod}(c)\).

theorem modVars_subset {c c' : HeapCmd} {s s' : State} {h h' : Heap}
    (hstep : HStep (c, s, h) (c', s', h')) : c'.modVars ⊆ c.modVars

Uses 10 · Used by 1

Statement usesSmall-step semantics of heap commands · Heap · Heap commands · Modified variables of a heap command · IMP program states

Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Heap configurations

Used byHeap executions only change assignable variables

TheoremA heap step only changes assignable variables#✓fully proved

If a heap configuration \((c, s, h)\) takes one heap step to \((c', s', h')\), then \(s'(x) = s(x)\) for every variable \(x\) outside the set of variables that \(c\) may assign to.

theorem store_agree {c c' : HeapCmd} {s s' : State} {h h' : Heap}
    (hstep : HStep (c, s, h) (c', s', h')) :
    ∀ x, x ∉ c.modVars → s' x = s x

Uses 10 · Used by 1

Statement usesSmall-step semantics of heap commands · Heap · Heap commands · Modified variables of a heap command · IMP program states

Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Heap configurations

Used byHeap executions only change assignable variables

TheoremHeap executions only change assignable variables#✓fully proved

If a heap configuration \((c, s, h)\) reaches a heap configuration \((c', s', h')\) in zero or more heap steps, then \(s'(x) = s(x)\) for every variable \(x\) outside the set of variables that \(c\) may assign to.

theorem store_agree {c c' : HeapCmd} {s s' : State} {h h' : Heap}
    (hsteps : HSteps (c, s, h) (c', s', h')) :
    ∀ x, x ∉ c.modVars → s' x = s x

Uses 9 · Used by 1

Statement usesMulti-step heap execution · Heap · Heap commands · Modified variables of a heap command · IMP program states

Proof usesHeap configurations · Small-step semantics of heap commands · Steps do not enlarge the modified variables · A heap step only changes assignable variables

Used byFrame rule

30 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.