Verifying a trivial Native Token policy in UPLC using K

[ChristianoBraga]

Introduction

The scope of KPlutus project is to verify validation/minintg policies of Plutus' contracts in K.

For Milestone 2 we need to implement and verify an ERC20-equivalent contract in Cardano using KPlutus. It was agreed to use Plutus' native token contract as such. In what follows, first we briefly recall our methodology to verify the UPLC enconding of Plutus policies in KPlutus. Next, we explain how to extend that methodology to encompass the infrastructure that comes togeher with native tokens policies.

Verifying UPLC in K

Dealing with recursive functions

Fixed point operator

  syntax Term ::= "REC" [alias]
  rule REC => (lam f_0
                [ (lam s_0 [ s_0 s_0 ])
                  (lam s_0 (lam x_0 [ [ f_0 [ s_0 s_0 ] ] x_0 ])) ])

Function structure

Function name, function body and function loop.

  --LIST_FREE----------- (lam f_lstFree
  | --LIST_FREE_BODY------ (lam in_lst
  | | --LIST_FREE_LOOP------ (force [ (force (builtin ifThenElse))
  | | |                        [ (force (builtin nullList)) in_lst ]
  | | |                        ( delay in_lst )
  | | |                        ( delay [
  | | |                                  f_lstFree
  | | |                                  [ (force (builtin tailList)) in_lst ]
  | | |                                ] )
  | | ---------------------- ])
  | ---------------------- )
  ---------------------- )

Claim structure

syntax Term ::= "LIST_FREE_REC" [alias] 
  rule LIST_FREE_REC => [ REC LIST_FREE ] 

 claim
    <k>
      [ LIST_FREE_REC (con list(integer) [ _XS:ConstantList ]) ]
        =>
      < con list(integer) [ .ConstantList ] > ...
    </k>
    <env> _ => .Map </env>

Native Tokens in UPLC

Verifying Native Tokens contracts' policies in K

(This is a brief summary of Issue #269)

The UPLC code generated from Plutus policies has many datatypes which are encoded as follows:

data T
  = C_0 T_0_0 ... T_0_M0
  | ...
  | C_N T_N_0 ... T_N_MN

Its compilation to UPLC results in the following:

1. one identifier per constructor: these identifiers are used as some sort of selectors;
2. a matcher function, T_match,
3. a decoder function, fUnsafeFromDataT_cunsafeFromBuiltinData, which takes uplc data and decodes it, assuming it represents T.

Global environment

The first part of executing compiled code is loading all of the selectors, matchers, and decoders into the environment. This will create an environment of considerable size, which would then be duplicated and extended throughout the term. All of the identifiers used in the compilation of datatypes are static. This means that we could construct an auxiliary, global environment that holds all of the datatype-compilation-related identifiers and then adapt lookup to go to the global environment instead of the local one when appropriate.

Automatically generating the environment

The global environment can be automatically generated:

1. Define a top-level abstraction for the entire datatype.
2. Declare an injective function << T >>(Int, List), where << T >>(C, PARAMS) represents the inhabitant of T with constructor C and parameters described by PARAMS. We also declare a total function << T >>Def(Int, List), which captures the definability of << T >>. These two functions simply serve as collectors for the constructor functions and constructor definedness, and do not go into the structure of the passed parameters.
3. Define abstractions for each datatype constructor essentially instantiating the constructor selector with arguments carrying the appropriate values. For some T_I, (e.g., Integer or ByteString), these values are trivial (e.g., < con integer PARAM > or < con bytestring PARAM >), and the corresponding definability conditions equal true, but these can also involve other more complex types. The toFunctionParams meta-function transforms either a single paramerter or a list of parameters that is PARAM_X into a list of function parameters at the meta-logic level.

Automatically generating claims

Given the above abstractions, we can also automatically generate per-constructor correctness claims for each datatype, which are of the form:

  // Constructor I: << C_I >>
  claim
    <k>
      ( con data { << T >>Data(I, ListItem(PARAM_0) ... ListItem(PARAMS_MI)) } ) ~>
      [ gLookup(fUnsafeFromData<< T >>_cunsafeFromBuiltinData) _]
      =>
      << T >>(I, ListItem(PARAM_0) ... ListItem(PARAMS_MI))
      ... </k>
    <env> _ => .Map </env>
    requires << T >>Def(I, ListItem(PARAM_0) ... ListItem(PARAMS_MI))

as well as a general claim of the form:

  claim
    <k>
      ( con data { << T >>Data(C, PARAMS) } ) ~>
      [ gLookup(fUnsafeFromData<< T >>_cunsafeFromBuiltinData) _]
      =>
      << T >>(C, PARAMS)
      ... </k>
    <env> _ => .Map </env>
    requires << T >>Def(C, PARAMS)

where gLookup is the lookup function of the global environment.

Currently, the per-constructor claims can be proven assuming the general claims of all nested datatypes, and the general claims cannot be proven due to some (identified) limitations in the Haskell backend and are therefore marked as trusted.

These claims can, once proven, be converted to semantic rules that can then be used to shortcut the semantics and accelerate the verification process.

The trivial policy

The Plutus Pioneer Program is perhaps one the most consistent sources of Plutus code and information at this time. The subject of Its week 5 is on native tokens. The most trivial minting policies are thos which always return true or always return false.

Trivial policy: True

  // True trivial policy returns the delayed identity
  claim
    <k>
        [
          TRIVIAL_POLICY_TRUE
          (con data { Constr 0 [ _ ] } )
          (con data { Constr 0 [ TxInfoData(C1, PARAMS1), ScriptPurposeData(C2, PARAMS2) ] })
        ]
      =>  < delay ( lam case_Unit case_Unit ) .Map >
    ... </k>
    <env> _ => .Map </env>
    requires TxInfoDef(C1, PARAMS1)
     andBool ScriptPurposeDef(C2, PARAMS2)

Trivial policy: False

  // False trivial policy throws an error
  claim
    <k>
        [
          TRIVIAL_POLICY_FALSE
          (con data { Constr 0 [ _ ] } )
          (con data { Constr 0 [ TxInfoData(C1, PARAMS1), ScriptPurposeData(C2, PARAMS2) ] })
        ]
      => (error)
    ... </k>
    <env> _ => ?_ </env>
    <trace> TRACE => TRACE ListItem("PT5") </trace>
    requires TxInfoDef(C1, PARAMS1)
     andBool ScriptPurposeDef(C2, PARAMS2)