• Specification of Dynamic views
  • Summary
  • Abstract
  • Specification
    • Example
    • Properties
    • Alternative approach
  • Test cases
  • Implementations
  • Appendix

Specification of Dynamic views

Summary

We propose read-only access from a contract to another. A Michelson instruction VIEW_EXEC is added.

Abstract

Currently, we can fetch data from another contract synchronously thanks to the onchain views feature provides since the update of the Hangzhou's protocol. This, however, benefits to no contract who was originated before it.

In this proposal, we propose to add a new view instruction, this view takes a lambda term of type s -> a as input, where s is the storage type of the target contract, and a is a value type derivable from s. By providing a proper lambda function, a contract could read anything from the target contract storage at will.

Specification

To this aim, an extend Michelson primitive is introduced: the VIEW_EXEC instruction.

The type of VIEW_EXEC is:

:: lambda 'storage_ty 'return : address : 'S -> option 'return : 'S

• lambda 'storage_ty 'return: The lambda that we apply to the target contract's storage 'storage_ty to retreive a value 'return.
• address: The target contract address. If a contract address containing an entrypoint address%entrypoint, only the address part will be taken.
• option 'return: The value retrieved from the target contract. Returns None if failed.

The semantics of VIEW_EXEC is:

> VIEW_EXEC / code: addr : S => Some v : S
    iff 
        code / s : []  =>  v : [] 
    where
        addr is the address of the target contract with storage s  
       
> VIEW_EXEC / _ : _ : S => None : S 
       otherwise

VIEW_EXEC will return None if:

• Contract with address addr:
  • is nonexistent.
  • the storage type does not match the argument type of the lambda ('storage_ty).
• Lambda function:
  • code results in runtime failure

Example

Suppose we have a contract that looks like below:

# contract_a
parameter unit ;
storage int ; # int 2
code { CDR;
       NIL operation;
       PAIR
}

Suppose we want to write contract_b that fetches the int in the storage of contract_a and increment it.

Using the new VIEW_EXEC instruction, we can write:

# contract_b
parameter address ;
storage int ;
code { 
      CAR; # address
      LAMBDA int int { PUSH int 1; ADD } ;
      VIEW_EXEC ; # result: Some (int 3)
      ASSERT_SOME ;
      NIL operation ;
      PAIR ;
     }

Properties

VIEW_EXEC has the same properties as VIEW, namely they are:

• read-only: they may depend on the storage of the contract but cannot modify it nor emit operations,
• synchronous: the result is immediately available on the stack of the contract

UnlikeVIEW,VIEW_EXEC has:

• no name,
• no input and output arguments,
• lambda function in a stack. In lambda output (type 'return), the following types are forbidden: ticket, operation, big_map and sapling_state.
  - current proposal does not accept recursively calling a lambda (for simplicity, light computation for node via RPC, gas cost, etc.).

Alternative approach

The specification and test suits of this approach can be found at: specification of VIEW_APPLY

Test cases

The details of tests can be found at this: IV. Test suits for VIEW_EXEC.

Implementations

Appendix

• Proposal of on-chain view patch
• Agora discussions