leanexe/Verified/TailCode.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
import Verified.TailBranch
import Verified.TailLetPair
import Verified.TailTreeCase
import Verified.ExprCorrect

namespace Verified

open Wasm

theorem TailBody.code_spec {S : List Sig} (m : Module) (funs : Funs S) (flags : Flags S)
    (bounds : Bounds S) (fits : Fits S) (host : HostEnv Unit) (hm : Runtime m) {pv : List Value}
    {d0 : UInt64} {pool : Bytes.LiteralPool}
    (hCalls : CallsAt m funs flags bounds fits d0 pool) {Γ params : List Ty}
    {result : Ty} (targetModes : List Mode) (body : TailBody S params result Γ) :
    body.Covered pool →
    (body.depthCalls = true → pv.head? = some (.i64 d0)) →
    TailCodeSpec m funs flags bounds fits host pv targetModes body pool := by
  induction body with
  | ret value =>
    intro hCovered hDepth
    exact tail_ret_spec hm targetModes value
      (Expr.code_spec m funs flags bounds fits host hm hCalls value hCovered hDepth)
  | next args =>
    intro hCovered hDepth
    have hArgs : ∀ i, (args i).Covered pool :=
      (literals_args_subset.mp hCovered)
    exact tail_next_spec hm targetModes args fun i =>
      Expr.code_spec m funs flags bounds fits host hm hCalls (args i) (hArgs i) fun hd =>
        hDepth (le_argsAny _ i hd)
  | ite cond yes no yesSpec noSpec =>
    intro hCovered hDepth
    have hParts : (cond.Covered pool ∧ yes.Covered pool) ∧ no.Covered pool := by
      simpa only [TailBody.Covered, TailBody.literals_ite, TailBody.literals_letE,
        TailBody.literals_letPair, Expr.Covered, List.append_subset,
        and_assoc] using hCovered
    exact tail_ite_spec hm targetModes cond yes no
      (Expr.code_spec m funs flags bounds fits host hm hCalls cond hParts.1.1 fun hd =>
        hDepth (by simp [TailBody.depthCalls, hd]))
      (yesSpec hParts.1.2 fun hd => hDepth (by simp [TailBody.depthCalls, hd]))
      (noSpec hParts.2 fun hd => hDepth (by simp [TailBody.depthCalls, hd]))
  | letE value body bodySpec =>
    intro hCovered hDepth
    have hParts : value.Covered pool ∧ body.Covered pool := by
      simpa only [TailBody.Covered, TailBody.literals_ite, TailBody.literals_letE,
        TailBody.literals_letPair, Expr.Covered, List.append_subset] using hCovered
    exact tail_let_spec hm targetModes value body
      (Expr.code_spec m funs flags bounds fits host hm hCalls value hParts.1 fun hd =>
        hDepth (by simp [TailBody.depthCalls, hd]))
      (bodySpec hParts.2 fun hd => hDepth (by simp [TailBody.depthCalls, hd]))
  | letPair value body bodySpec =>
    intro hCovered hDepth
    have hParts : value.Covered pool ∧ body.Covered pool := by
      simpa only [TailBody.Covered, TailBody.literals_ite, TailBody.literals_letE,
        TailBody.literals_letPair, Expr.Covered, List.append_subset] using hCovered
    exact tail_letPair_spec hm targetModes value body
      (Expr.code_spec m funs flags bounds fits host hm hCalls value hParts.1 fun hd =>
        hDepth (by simp [TailBody.depthCalls, hd]))
      (bodySpec hParts.2 fun hd => hDepth (by simp [TailBody.depthCalls, hd]))
  | treeCase x empty nodes emptySpec nodesSpec =>
    intro hCovered hDepth
    have hParts := List.append_subset.mp hCovered
    exact tail_treeCase_spec hm targetModes x empty nodes
      (fun hn => emptySpec hn (by
          have hEmpty := hParts.1
          rw [dif_pos hn] at hEmpty
          exact hEmpty)
        fun hd => hDepth (by simp [TailBody.depthCalls, hn, hd]))
      (fun r => nodesSpec r (literals_args_subset.mp hParts.2 r) fun hd => hDepth (by
        simp [TailBody.depthCalls, le_argsAny (fun r => (nodes r).depthCalls) r hd]))

#print axioms TailBody.code_spec

end Verified