leanexe/Verified/TreeAttach.lean at main · jsmorph/leanexe · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
import Verified.TreeDetach

namespace Verified

open Wasm LeanExe.Pipeline LeanExe.ProofKit LeanExe.Runtime

def TreeHeader.setMask (store : Store Unit) (p mask : UInt64) : Store Unit :=
  { store with mem := store.mem.write64 (p - 8).toUInt32 mask }

theorem TreeHeader.attach_spec {shape : TreeShape} {r : Fin shape.records} {heap : Heap}
    {store : Store Unit} {p : UInt64} {slots : List Slot}
    (hHeap : heap.At store) (hHeader : Owned shape r heap store p)
    (hLength : slots.length = shape.width r) (hSlots : SlotsOwned heap store p 0 slots)
    (hLengths : BufferLengths slots)
    (hApart : (Node.blocks store p (.record slots)).Pairwise regionsDisjoint) :
    let store' := setMask store p (maskOf slots)
    Memory.WritesRange store store' (p.toNat - 8) p.toNat ∧ heap.At store' ∧
      NodeOwned heap store' p (.record slots) ∧
      Node.blocks store' p (.record slots) = Node.blocks store p (.record slots) := by
  obtain ⟨words, hWords, hHead, _⟩ := hHeader
  have hBase := hHead.base
  have hAddress := hHead.address
  have hRoom := hHead.capacity
  have hLength' : slots.length = (words.map Slot.word).length := by
    simp only [List.length_map, hWords, hLength]
  let store' := setMask store p (maskOf slots)
  have hAddr : (p - 8).toUInt32.toNat = p.toNat - 8 :=
    headerAddress_toNat (by change 8 ≤ p.toNat; omega) (by omega)
  have hWrites : Memory.WritesRange store store' (p.toNat - 8) p.toNat :=
    Memory.WritesRange.write64 _ _ _ _ _ (by rw [hAddr]) (by rw [hAddr]; omega)
  have hRead (back : UInt64) (h16 : 16 ≤ back.toNat) (h48 : back.toNat ≤ 48) :
      store'.mem.read64 (p - back).toUInt32 = store.mem.read64 (p - back).toUInt32 := by
    apply hWrites.read64
    left
    rw [headerAddress_toNat (by omega) (by omega)]
    omega
  have hCapacity : capacityAt store' p = capacityAt store p := by
    unfold capacityAt
    rw [hRead 32 (by decide) (by decide)]
  have hHead' : RecordHeader heap store' p slots := by
    refine ⟨hBase, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, hLengths⟩
    · rw [hRead 48 (by decide) (by decide)]; exact hHead.magic
    · rw [hRead 40 (by decide) (by decide)]; exact hHead.count
    · rw [hRead 24 (by decide) (by decide)]; exact hHead.kind
    · rw [hRead 16 (by decide) (by decide), hLength']; exact hHead.width
    · exact Memory.read64_write64 ..
    · rw [hLength']; exact hHead.short
    · rw [hLength', hCapacity]; exact hHead.capacity
    · rw [hCapacity]; exact hHead.address
    · rw [hCapacity]; exact hHead.below
    · rw [hCapacity]; exact hHead.separate
  have hSeparate := (List.pairwise_cons.mp hApart).1
  have hHeap' : heap.At store' := hHeap.writesApart hWrites fun node hNode => by
    have := hHead.separate node hNode
    simp only [regionsDisjoint] at this ⊢
    omega
  obtain ⟨hSlots', hBlocks⟩ := SlotsOwned.frame hHeap' p 0 slots hSlots (by omega)
    (fun a hLow _ => hWrites.2.2 a (.inr (by omega)))
    (fun b hb => ⟨fun a hLow hHigh => hWrites.2.2 a (by
      have := hSeparate b hb
      simp only [regionsDisjoint, block] at this
      omega), SlotsOwned.regions p 0 slots hSlots b hb⟩)
  refine ⟨hWrites, hHeap', ⟨hHead', hSlots'⟩, ?_⟩
  change block store' p :: slotsBlocks store' p 0 slots = _
  rw [block_eq hCapacity, hBlocks]
  rfl

#print axioms TreeHeader.attach_spec

end Verified