[KIP] - Configuration Macros

Start by reading issue #2075, which this proposal identifies as a likely prerequisite, then trace the frontend macro-expansion behavior described in the issue. Done means configuration macros can expand the high-level configuration into the low-level configuration on both sides of a claim, supporting the VAT-SPEC example.

Motivation

This would likely be blocked on #2075.

In Tezos we are now doing "constructive refinement" proofs. To do this, we declare a new configuration which is the abstract state of the high-level program/contract/system we're trying to represent (eg. Dexter), and then define a mapping from that configuration to the low-level configuration (eg. Tezos). Then we state the proof over the high-level configuration, basically saying "if we serialize this high-level state to the low-level VM, run the low-level semantics, then deserialize the low-level semantics to the high-level state, we will see the specified state-update over the high-level configuration". This allows us to write proofs about the code at a higher-level, without messing with the details of the low-level VM.

The proof ends up having the form:

rule <k> #runProof => #serializeHighToLow ~> #executeLow ~> #deserializeLowToHigh ... </k>


claim <k> #runProof => . ... </k>
       <high-level-state> SOME_PRE_STATE => SOME_POST_STATE </high-level-state>

So that we don't have to mention the actual state that happens over the low-level. The problem is that these proofs are not composable anymore, because the executions are book-ended by the #serializeHighToLow and #deserializeLowToHigh. Instead, if we could declare a new configuration as a macro which immediately simplifies to the low-level configuration, we could write our proof over the high-level configuration and have the frontend expand the RHS and LHS of the proof according to the macro supplied.

Example K Code

In the following code, similar to #2075, we declare a new storage layout called <vat> which we expect to be able to use directly instead of the <storage> cell in our proofs.

requires "domains.md"

module EVM
    imports BOOL
    imports INT
    imports LIST
    imports MAP

    configuration
      <kevm>
        <k> 0 </k>
        <storage> .Map </storage>
        <reads> .List </reads>
      </kevm>

    rule <k> 0 => 1 ... </k> <storage> STORAGE => #write(STORAGE, 3, 4) </storage>
    rule <k> 1 => 2 ... </k> <storage> STORAGE => #write(STORAGE, 5, 6) </storage>

    rule <k> 2 => #lookup(STORAGE, 3) ... </k> <storage> STORAGE </storage>
    rule <k> 4 => #lookup(STORAGE, 5) ... </k> <storage> STORAGE </storage>
    rule <k> 6 => #lookup(STORAGE, 9) ... </k> <storage> STORAGE </storage>

    rule <k> B:Bool => . ... </k> <reads> ... .List => ListItem(B) </reads>

    syntax Int ::= #lookup ( Map , Int ) [function, functional]
 // -----------------------------------------------------------------------
    rule #lookup( (KEY |-> VAL:Int) _M:Map, KEY ) => VAL modInt (2 ^Int 256)
    rule #lookup(                    M:Map, KEY ) => 0                       requires notBool KEY in_keys(M)
    rule #lookup( (KEY |-> VAL    ) _M:Map, KEY ) => 0                       requires notBool isInt(VAL)

    syntax Map ::= #write ( Map , Int , Int ) [function, functional]
 // ----------------------------------------------------------------------------------------
    rule #write(M, K, V) => M [ K <- V ]

    syntax Bool ::= Word2Bool ( Int ) [function, functional]
 // --------------------------------------------------------
    rule Word2Bool(I) => true  requires I ==Int 1
    rule Word2Bool(I) => false [owise]

    syntax Int ::= Bool2Word ( Bool ) [function, functional]
 // --------------------------------------------------------
    rule Bool2Word(true)  => 1
    rule Bool2Word(false) => 0

endmodule
    
module VAT
    imports EVM

    configuration
      <vat>
        <vat-wards> .Set </vat-wards>
      </vat>

    syntax StorageCell ::= VatCell

    rule <vat> <vat-wards> S </vat-wards> </vat> => <storage> VatWards2Storage(S) </storage> [macro]

    syntax Map ::= VatWards2Storage(Set)
                 | VatWards2Storage(Set, Map)
 // -----------------------------------------
    rule VatWards2Storage(S) => VatWards2Storage(S, .Map) [macro]

    rule VatWards2Storage(.Set, M)            => M                                    [macro]
    rule VatWards2Storage(SetItem(I) REST, M) => VatWards2Storage(REST, M [ I <- 1 ]) [macro]
endmodule

Notice how we've subsorted VatCell into StorageCell, which allows us to have a macro which expands the <vat> cell directly into a <storage> cell.

This allows us to write the following spec, without ever having to mention the <storage> cell:

module VAT-SPEC
    imports VAT

    claim <k> 0 => 6 ... </k>
          <vat> <vat-wards> .Set => SetItem(3) SetItem(4) </vat-wards> </vat>
          <reads> .List => ListItem(true) ListItem(true) ListItem(false) </reads>

endmodule

Presumably the frontend would expand the LHS and RHS of the claim separately with the macro expander, which would result in the correct <storage> being put in place.

Ideas

• This might be made trivial by supporting #2075.