vyper-semantics/vyper-lll/vyper-lll-utils.k at master · kframework/vyper-semantics · 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
module VYPER-LLL-UTILS
  imports STRING

//////////////////////////////////////////////////////////////////////////////
// Constants
//////////////////////////////////////////////////////////////////////////////


// Decimal Divisor
// ===============


    syntax Int  ::= "@decimalDivisor"
 // ---------------------------------
    rule @decimalDivisor => 10000000000  [macro]


// Memory Positions
// ================


    syntax Int  ::= "@reservedMemPos"
    syntax Int  ::= "@addrSizePos"
    syntax Int  ::= "@maxNumPos"
    syntax Int  ::= "@minNumPos"
    syntax Int  ::= "@maxDecimalPos"
    syntax Int  ::= "@minDecimalPos"
    syntax Int  ::= "@freeVarPos"
    syntax Int  ::= "@blankPos"
    syntax Int  ::= "@freeLoopIndexPos"
 // -----------------------------------
    rule @reservedMemPos => 320      [macro]
    rule @addrSizePos => 32          [macro]
    rule @maxNumPos => 64            [macro]
    rule @minNumPos => 96            [macro]
    rule @maxDecimalPos => 128       [macro]
    rule @minDecimalPos => 160       [macro]
    rule @freeVarPos => 192          [macro]
    rule @blankPos => 224            [macro]
    rule @freeLoopIndexPos => 256    [macro]


// Data Type Limits
// ================


    syntax Int  ::= "@addrSize"
    syntax Int  ::= "@maxNum"
    syntax Int  ::= "@minNum"
    syntax Int  ::= "@maxDecimal"
    syntax Int  ::= "@minDecimal"
 // ---------------------------------
    rule @addrSize   => 2 ^Int 160                                [macro]
    rule @maxNum     => 2 ^Int 127 -Int 1                         [macro]
    rule @minNum     => -2 ^Int 127                               [macro]
    rule @maxDecimal => (2 ^Int 127 -Int 1) *Int @decimalDivisor  [macro]
    rule @minDecimal => (-2 ^Int 127) *Int @decimalDivisor        [macro]


//////////////////////////////////////////////////////////////////////////////
// Functions
//////////////////////////////////////////////////////////////////////////////


    syntax Int  ::= "#ceil32" "(" Int ")"     [function]
 // ----------------------------------------------------
    rule #ceil32(NUM) => NUM
      requires (NUM modInt 32) ==Int 0

    rule #ceil32(NUM) => NUM +Int 32 -Int (NUM modInt 32)
      requires (NUM modInt 32) =/=Int 0

endmodule