leanexe/Verified/Examples/CompositionPure.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.Examples.CompositionBase
import Verified.ModuleComposition
import Verified.ScalarAtoms

namespace Verified.Examples.CompositionBase

open Wasm LeanExe.Pipeline

theorem add_pure {m : Module} (hm : Runtime m)
    (hPrefix : compiled.program.functions Bytes.LiteralPool.empty <+: m.funcs.drop 2) :
    ImplementsPureA false m 2 (fun p : UInt64 × UInt64 => add p.1 p.2) := by
  have calls : Calls m compiled.funs compiled.program.flags
      (compiled.program.boundsAt compiled.funs) (compiled.program.fitsAt compiled.funs)
      Bytes.LiteralPool.empty :=
    compiled.program.calls_prefix compiled.funs compiled.meaning m hm hPrefix (by
      have noLiterals : compiled.program.literals = [] := by decide +kernel
      simp only [Prog.Covered, noLiterals, List.nil_subset])
  have hImpl : ImplementsA false m 2 (fun p : UInt64 × UInt64 => add p.1 p.2)
      (fun _ _ _ => True) (fun _ _ _ _ _ => True) :=
    ImplementsA.lean ((calls (.there .here) 0).implementsB_unpaid rfl rfl).implementsA
  have hLookup : m.funcs[2]? = some (compiled.add.func.function 2 Bytes.LiteralPool.empty) :=
    compiled.program.functions_prefix_lookup m hPrefix (k := 0) (by decide)
  have uniform : CodeUniform m (compiled.add.func.function 2 Bytes.LiteralPool.empty).body := by
    change CodeUniform m [.localGet 0, .localGet 1, .addI64]
    exact CodeUniform.cons (OneUniform.localGet m 0)
      (CodeUniform.cons (OneUniform.localGet m 1)
        (CodeUniform.cons (OneUniform.addI64 m) (CodeUniform.nil m)))
  have safe : CodeNoReturnCall m (compiled.add.func.function 2 Bytes.LiteralPool.empty).body := by
    change CodeNoReturnCall m [.localGet 0, .localGet 1, .addI64]
    exact CodeNoReturnCall.cons (OneNoReturnCall.localGet m 0)
      (CodeNoReturnCall.cons (OneNoReturnCall.localGet m 1)
        (CodeNoReturnCall.cons (OneNoReturnCall.addI64 m) (CodeNoReturnCall.nil m)))
  exact implementsPure_of_uniform hImpl (EntryUniform.of_code hm.imports hLookup uniform safe)

theorem scale_pure {m : Module} (hm : Runtime m)
    (hPrefix : compiled.program.functions Bytes.LiteralPool.empty <+: m.funcs.drop 2) :
    ImplementsPureA false m 3 scale := by
  have calls : Calls m compiled.funs compiled.program.flags
      (compiled.program.boundsAt compiled.funs) (compiled.program.fitsAt compiled.funs)
      Bytes.LiteralPool.empty :=
    compiled.program.calls_prefix compiled.funs compiled.meaning m hm hPrefix (by
      have noLiterals : compiled.program.literals = [] := by decide +kernel
      simp only [Prog.Covered, noLiterals, List.nil_subset])
  have hImpl : ImplementsA false m 3 scale
      (fun _ _ _ => True) (fun _ _ _ _ _ => True) :=
    ImplementsA.lean ((calls .here 0).implementsB_unpaid rfl rfl).implementsA
  have hLookup : m.funcs[3]? = some (compiled.scale.func.function 3 Bytes.LiteralPool.empty) :=
    compiled.program.functions_prefix_lookup m hPrefix (k := 1) (by decide)
  have uniform : CodeUniform m (compiled.scale.func.function 3 Bytes.LiteralPool.empty).body := by
    change CodeUniform m [.localGet 0, .localSet 1, .localGet 1,
      .f64Const 4609434218613702656, .f64Mul]
    exact CodeUniform.cons (OneUniform.localGet m 0)
      (CodeUniform.cons (OneUniform.localSet m 1)
        (CodeUniform.cons (OneUniform.localGet m 1)
          (CodeUniform.cons (OneUniform.f64Const m _)
            (CodeUniform.cons (OneUniform.f64Mul m) (CodeUniform.nil m)))))
  have safe : CodeNoReturnCall m (compiled.scale.func.function 3 Bytes.LiteralPool.empty).body := by
    change CodeNoReturnCall m [.localGet 0, .localSet 1, .localGet 1,
      .f64Const 4609434218613702656, .f64Mul]
    exact CodeNoReturnCall.cons (OneNoReturnCall.localGet m 0)
      (CodeNoReturnCall.cons (OneNoReturnCall.localSet m 1)
        (CodeNoReturnCall.cons (OneNoReturnCall.localGet m 1)
          (CodeNoReturnCall.cons (OneNoReturnCall.f64Const m _)
            (CodeNoReturnCall.cons (OneNoReturnCall.f64Mul m) (CodeNoReturnCall.nil m)))))
  exact implementsPure_of_uniform hImpl (EntryUniform.of_code hm.imports hLookup uniform safe)

#print axioms add_pure
#print axioms scale_pure

end Verified.Examples.CompositionBase