leanexe/Verified/Examples/TreeCore.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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
import Verified.TreeSource
import Verified.Compile
import Verified.Correct

namespace Verified.Examples.TreeCore

def cons (mode : Mode) : Func S :=
  { name := if mode = .owned then "consOwned" else "cons"
    params := [.word, .tree listShape], result := .tree listShape
    modes := [.borrowed, mode], body := listConsExpr, placeArgs := rfl }

def first (mode : Mode) : Func S :=
  { name := if mode = .owned then "firstOwned" else "first"
    params := [.tree listShape], result := .word
    modes := [mode], body := listFirstExpr, placeArgs := rfl }

def rest (mode : Mode) : Func S :=
  { name := if mode = .owned then "restOwned" else "rest"
    params := [.tree listShape], result := .tree listShape
    modes := [mode], body := listRestExpr, placeArgs := rfl }

def rebuild (mode : Mode) : Func S :=
  { name := if mode = .owned then "rebuildOwned" else "rebuild"
    params := [.tree listShape], result := .tree listShape
    modes := [mode], body := listRebuildExpr, placeArgs := rfl }

def duplicateExpr : Expr S [.tree listShape] (.pair (.tree listShape) (.tree listShape)) :=
  .treeCase .here (fun _ => .pair (.treeNil listShape rfl) (.v 0))
    (listBranch (.pair
      (.treeNode listCell (some .here) (fun _ => .v 1) (noFields rfl) (noFields rfl)
      (fun _ => .v 2)) (.v 3)))

def duplicate (mode : Mode) : Func S :=
  { name := if mode = .owned then "duplicateOwned" else "duplicate"
    params := [.tree listShape], result := .pair (.tree listShape) (.tree listShape)
    modes := [mode], body := duplicateExpr, placeArgs := rfl }

def changeExpr : Expr S [.word, .tree listShape] (.tree listShape) :=
  .treeCase (.there .here) (fun _ => .treeNil listShape rfl)
    (listBranch
      (.treeNode listCell (some .here) (fun _ => .bin .add (.v 1) (.v 3)) (noFields rfl)
        (noFields rfl) (fun _ => .v 2)))

def change (mode : Mode) : Func S :=
  { name := if mode = .owned then "changeOwned" else "change"
    params := [.word, .tree listShape], result := .tree listShape
    modes := [.borrowed, mode], body := changeExpr, placeArgs := rfl }

def foldWord (mode : Mode) : Func S :=
  { name := if mode = .owned then "foldWordOwned" else "foldWord"
    params := [.tree listShape, .word], result := .word
    modes := [mode, .borrowed]
    body := .listFold (e := .word) (captures := [])
      (Args.cons (.v 0) (.cons (.v 1) .nil)).get
      (.bin .add (.bin .mul (.v 4) (.word 3)) (.v 1))
    placeArgs := rfl }

def foldLookup (mode : Mode) : Func S :=
  { name := if mode = .owned then "foldLookupOwned" else "foldLookup"
    params := [.tree listShape, .word, .array .word], result := .word
    modes := [mode, .borrowed, mode]
    body := .listFold (e := .word) (captures := [.array .word])
      (Args.cons (.v 0) (.cons (.v 1) (.cons (.v 2) .nil))).get
      (.bin .add (.v 4) (.get (Var.ofIndex _ 5 rfl) (.v 1)))
    placeArgs := rfl }

def foldBuild (mode : Mode) : Func S :=
  { name := if mode = .owned then "foldBuildOwned" else "foldBuild"
    params := [.tree listShape, .word], result := .word
    modes := [mode, .borrowed]
    body := .listFold (e := .word) (captures := [])
      (Args.cons (.v 0) (.cons (.v 1) .nil)).get
      (.letE (.build (.word 2) (.bin .add (.v 0) (.v 2)))
        (.bin .add (.v 5) (.get .here (.word 1))))
    placeArgs := rfl }

def prog :=
  Prog.cons (foldBuild .owned) <| .cons (foldBuild .borrowed) <|
  .cons (foldLookup .owned) <| .cons (foldLookup .borrowed) <|
  .cons (foldWord .owned) <| .cons (foldWord .borrowed) <|
  .cons (change .owned) <| .cons (change .borrowed) <|
  .cons (duplicate .owned) <| .cons (duplicate .borrowed) <|
  .cons (rebuild .owned) <| .cons (rebuild .borrowed) <|
  .cons (rest .owned) <| .cons (rest .borrowed) <|
  .cons (first .owned) <| .cons (first .borrowed) <|
  .cons (cons .owned) <| .cons (cons .borrowed) .nil

def module : Wasm.Module := compile prog

theorem correct : Calls module prog.funs prog.flags
    (prog.boundsAt prog.funs) (prog.fitsAt prog.funs) Bytes.LiteralPool.empty :=
  prog.correct_funs rfl (by decide +kernel)

theorem duplicate_denote (xs : List UInt64) :
    duplicateExpr.denote .nil (.cons (.ofList xs) .nil) = (.ofList xs, .ofList xs) := by
  cases xs <;> rfl

theorem change_denote (x : UInt64) (xs : List UInt64) :
    changeExpr.denote .nil (.cons x (.cons (.ofList xs) .nil)) =
      .ofList (match xs with | [] => [] | y :: ys => (y + x) :: ys) := by
  cases xs <;> rfl

#print axioms duplicate_denote
#print axioms change_denote
#print axioms correct

end Verified.Examples.TreeCore