leanexe/LeanExe/Encoding/Values.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
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
import LeanExe.Encoding.Spec.Values
import Init.Omega
import Init.Data.UInt.Lemmas

namespace Wasm.Encoding

def unsignedFuel : Nat → Nat → Spec.Bytes
  | 0, _ => []
  | fuel + 1, value =>
      if value < 128 then [UInt8.ofNat value]
      else UInt8.ofNat (value % 128 + 128) :: unsignedFuel fuel (value / 128)

def unsigned (width value : Nat) : Spec.Bytes :=
  unsignedFuel ((width + 6) / 7) value

def signedFuel : Nat → Int → Spec.Bytes
  | 0, _ => []
  | fuel + 1, value =>
      if -64 ≤ value ∧ value < 64 then [UInt8.ofNat (value % 128).toNat]
      else UInt8.ofNat ((value % 128).toNat + 128) :: signedFuel fuel (value / 128)

def signed (width : Nat) (value : Int) : Spec.Bytes :=
  signedFuel ((width + 6) / 7) value

theorem unsignedFuel_correct (fuel width value : Nat)
    (positive : 0 < width) (room : width ≤ 7 * fuel)
    (fits : value < 2 ^ width) :
    Spec.Unsigned width (unsignedFuel fuel value) value := by
  induction fuel generalizing width value with
  | zero => omega
  | succ fuel ih =>
      simp only [unsignedFuel]
      by_cases small : value < 128
      · rw [ite_eq_left small]
        have byte : (UInt8.ofNat value).toNat = value := by
          simp only [UInt8.toNat_ofNat']
          omega
        simpa only [byte] using Spec.Unsigned.terminal width (UInt8.ofNat value)
          positive (by omega) (by omega)
      · rw [ite_eq_right small]
        have wide : 7 < width := by
          by_cases narrow : width ≤ 7
          · have power := Nat.pow_le_pow_right (by decide : 1 ≤ 2) narrow
            omega
          · omega
        have power : 2 ^ width = 128 * 2 ^ (width - 7) := by
          calc
            2 ^ width = 2 ^ (7 + (width - 7)) := by congr 1; omega
            _ = 128 * 2 ^ (width - 7) := by rw [Nat.pow_add]
        have divided : value / 128 < 2 ^ (width - 7) := by
          rw [power] at fits
          omega
        have byte : (UInt8.ofNat (value % 128 + 128)).toNat = value % 128 + 128 := by
          simp only [UInt8.toNat_ofNat']
          omega
        have tail := ih (width - 7) (value / 128) (by omega) (by omega) divided
        have result := Spec.Unsigned.next (width - 7)
          (UInt8.ofNat (value % 128 + 128)) _ _ (by omega) (by omega) tail
        have same : value % 128 + 128 - 128 + 128 * (value / 128) = value := by omega
        simpa only [byte, same, show width - 7 + 7 = width by omega] using result

theorem unsigned_correct (width value : Nat)
    (positive : 0 < width) (fits : value < 2 ^ width) :
    Spec.Unsigned width (unsigned width value) value :=
  unsignedFuel_correct _ _ _ positive (by omega) fits

theorem signedPayload (value : Int) (small : -64 ≤ value ∧ value < 64) :
    Spec.signedDigit (UInt8.ofNat (value % 128).toNat) = value := by
  have payload : (value % 128).toNat < 128 := by omega
  have byte : (UInt8.ofNat (value % 128).toNat).toNat = (value % 128).toNat := by
    simp only [UInt8.toNat_ofNat']
    omega
  simp only [Spec.signedDigit, byte]
  split <;> omega

theorem signedFuel_correct (fuel width : Nat) (value : Int)
    (positive : 0 < width) (room : width ≤ 7 * fuel)
    (lower : -(2 ^ (width - 1) : Int) ≤ value)
    (upper : value < (2 ^ (width - 1) : Int)) :
    Spec.Signed width (signedFuel fuel value) value := by
  induction fuel generalizing width value with
  | zero => omega
  | succ fuel ih =>
      simp only [signedFuel]
      by_cases small : -64 ≤ value ∧ value < 64
      · rw [ite_eq_left small]
        have byte : (UInt8.ofNat (value % 128).toNat).toNat = (value % 128).toNat := by
          simp only [UInt8.toNat_ofNat']
          omega
        simpa only [signedPayload value small] using
          Spec.Signed.terminal width (UInt8.ofNat (value % 128).toNat) positive
            (by rw [byte]; omega)
            (by rw [signedPayload value small]; exact lower)
            (by rw [signedPayload value small]; exact upper)
      · rw [ite_eq_right small]
        have wide : 7 < width := by
          by_cases narrow : width ≤ 7
          · have power := Nat.pow_le_pow_right (by decide : 1 ≤ 2)
              (by omega : width - 1 ≤ 6)
            have castPower : (2 ^ (width - 1) : Int) = (2 ^ (width - 1) : Nat) := by
              simp
            rw [castPower] at lower upper
            omega
          · omega
        have power : (2 ^ (width - 1) : Int) = 128 * 2 ^ (width - 7 - 1) := by
          rw [show width - 1 = 7 + (width - 7 - 1) by omega, Int.pow_add]
          rfl
        have dividedLower : -(2 ^ (width - 7 - 1) : Int) ≤ value / 128 := by
          rw [power] at lower
          omega
        have dividedUpper : value / 128 < (2 ^ (width - 7 - 1) : Int) := by
          rw [power] at upper
          omega
        have byte : (UInt8.ofNat ((value % 128).toNat + 128)).toNat =
            (value % 128).toNat + 128 := by
          simp only [UInt8.toNat_ofNat']
          omega
        have tail := ih (width - 7) (value / 128) (by omega) (by omega)
          dividedLower dividedUpper
        have result := Spec.Signed.next (width - 7)
          (UInt8.ofNat ((value % 128).toNat + 128)) _ _ (by omega) (by omega) tail
        have same : (((value % 128).toNat + 128 : Nat) : Int) - 128 +
            128 * (value / 128) = value := by omega
        simpa only [byte, same, show width - 7 + 7 = width by omega] using result

theorem signed_correct (width : Nat) (value : Int)
    (positive : 0 < width)
    (lower : -(2 ^ (width - 1) : Int) ≤ value)
    (upper : value < (2 ^ (width - 1) : Int)) :
    Spec.Signed width (signed width value) value :=
  signedFuel_correct _ _ _ positive (by omega) lower upper

end Wasm.Encoding