verity/Compiler/CompilationModel/MappingWrites.lean at 04ecafccdf799d89fa4238ea47724426072bc8d2 · lfglabs-dev/verity · 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
134
135
136
137
138
139
140
141
142
143
import Compiler.CompilationModel.Types
import Compiler.CompilationModel.ValidationHelpers

namespace Compiler.CompilationModel

open Compiler
open Compiler.Yul

def compileMappingSlotWrite (fields : List Field) (field : String)
    (keyExpr valueExpr : YulExpr) (label : String) (wordOffset : Nat := 0)
    (allowTransient : Bool := false) : Except String (List YulStmt) :=
  if !isMapping fields field then
    throw s!"Compilation error: field '{field}' is not a mapping"
  else
    let storeBuiltin :=
      if allowTransient then
        match findFieldWithResolvedSlot fields field with
        | some (f, _) => if f.isTransient then "tstore" else "sstore"
        | none => "sstore"
      else
        "sstore"
    match findFieldWriteSlots fields field with
    | some slots =>
        match slots with
          | [] =>
              throw s!"Compilation error: internal invariant failure: no write slots for mapping field '{field}' in {label}"
          | [slot] =>
              let mappingBase := YulExpr.call "mappingSlot" [YulExpr.lit slot, keyExpr]
              let writeSlot := if wordOffset == 0 then mappingBase else YulExpr.call "add" [mappingBase, YulExpr.lit wordOffset]
              if allowTransient then
                match findFieldWithResolvedSlot fields field with
                | some (_, _) =>
                    pure [
                      YulStmt.expr (YulExpr.call storeBuiltin [
                        writeSlot,
                        valueExpr
                      ])
                    ]
                | none => throw s!"Compilation error: unknown mapping field '{field}' in {label}"
              else
                pure [
                  YulStmt.expr (YulExpr.call "sstore" [
                    writeSlot,
                    valueExpr
                  ])
                ]
          | _ =>
              let compatSlotExpr := fun (slot : Nat) =>
                let mappingBase := YulExpr.call "mappingSlot" [YulExpr.lit slot, YulExpr.ident "__compat_key"]
                if wordOffset == 0 then mappingBase else YulExpr.call "add" [mappingBase, YulExpr.lit wordOffset]
              pure [
                YulStmt.block (
                  [YulStmt.let_ "__compat_key" keyExpr, YulStmt.let_ "__compat_value" valueExpr] ++
                  slots.map (fun slot =>
                    YulStmt.expr (YulExpr.call storeBuiltin [
                      compatSlotExpr slot,
                      YulExpr.ident "__compat_value"
                    ]))
                )
              ]
    | none => throw s!"Compilation error: unknown mapping field '{field}' in {label}"

def compileMappingPackedSlotWrite (fields : List Field) (field : String)
    (keyExpr valueExpr : YulExpr) (wordOffset : Nat) (packed : PackedBits)
    (label : String) (allowTransient : Bool := false) : Except String (List YulStmt) :=
  if !isMapping fields field then
    throw s!"Compilation error: field '{field}' is not a mapping"
  else if !packedBitsValid packed then
    throw s!"Compilation error: {label} for field '{field}' has invalid packed range offset={packed.offset} width={packed.width}. Require 0 < width <= 256, offset < 256, and offset + width <= 256."
  else
    let loadBuiltin :=
      if allowTransient then
        match findFieldWithResolvedSlot fields field with
        | some (f, _) => if f.isTransient then "tload" else "sload"
        | none => "sload"
      else
        "sload"
    let storeBuiltin :=
      if allowTransient then
        match findFieldWithResolvedSlot fields field with
        | some (f, _) => if f.isTransient then "tstore" else "sstore"
        | none => "sstore"
      else
        "sstore"
    match findFieldWriteSlots fields field with
    | some slots =>
        match slots with
        | [] =>
            throw s!"Compilation error: internal invariant failure: no write slots for mapping field '{field}' in {label}"
        | [slot] =>
            let mappingBase := YulExpr.call "mappingSlot" [YulExpr.lit slot, keyExpr]
            let writeSlot := if wordOffset == 0 then mappingBase else YulExpr.call "add" [mappingBase, YulExpr.lit wordOffset]
            let maskNat := packedMaskNat packed
            let shiftedMaskNat := packedShiftedMaskNat packed
            pure [
              YulStmt.block [
                YulStmt.let_ "__compat_value" valueExpr,
                YulStmt.let_ "__compat_packed" (YulExpr.call "and" [YulExpr.ident "__compat_value", YulExpr.lit maskNat]),
                YulStmt.let_ "__compat_slot_word" (YulExpr.call loadBuiltin [writeSlot]),
                YulStmt.let_ "__compat_slot_cleared" (YulExpr.call "and" [
                  YulExpr.ident "__compat_slot_word",
                  YulExpr.call "not" [YulExpr.lit shiftedMaskNat]
                ]),
                YulStmt.expr (YulExpr.call storeBuiltin [
                  writeSlot,
                  YulExpr.call "or" [
                    YulExpr.ident "__compat_slot_cleared",
                    YulExpr.call "shl" [YulExpr.lit packed.offset, YulExpr.ident "__compat_packed"]
                  ]
                ])
              ]
            ]
        | _ =>
            let slotExpr := fun (slot : Nat) =>
              let mappingBase := YulExpr.call "mappingSlot" [YulExpr.lit slot, YulExpr.ident "__compat_key"]
              if wordOffset == 0 then mappingBase else YulExpr.call "add" [mappingBase, YulExpr.lit wordOffset]
            let maskNat := packedMaskNat packed
            let shiftedMaskNat := packedShiftedMaskNat packed
            pure [
              YulStmt.block (
                [YulStmt.let_ "__compat_key" keyExpr,
                 YulStmt.let_ "__compat_value" valueExpr,
                 YulStmt.let_ "__compat_packed" (YulExpr.call "and" [YulExpr.ident "__compat_value", YulExpr.lit maskNat])] ++
                slots.map (fun slot =>
                  YulStmt.block [
                    YulStmt.let_ "__compat_slot_word" (YulExpr.call loadBuiltin [slotExpr slot]),
                    YulStmt.let_ "__compat_slot_cleared" (YulExpr.call "and" [
                      YulExpr.ident "__compat_slot_word",
                      YulExpr.call "not" [YulExpr.lit shiftedMaskNat]
                    ]),
                    YulStmt.expr (YulExpr.call storeBuiltin [
                      slotExpr slot,
                      YulExpr.call "or" [
                        YulExpr.ident "__compat_slot_cleared",
                        YulExpr.call "shl" [YulExpr.lit packed.offset, YulExpr.ident "__compat_packed"]
                      ]
                    ])
                  ])
              )
            ]
    | none => throw s!"Compilation error: unknown mapping field '{field}' in {label}"

end Compiler.CompilationModel