owned this note
owned this note
Published
Linked with GitHub
---
title: Specification of dynamic views
tags: views
description: specification, test cases
---
[toc]
# 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
Unlike`VIEW`,`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`](https://hackmd.io/NCjj-E8VRPWnY_t8kcvIVA?view)
## Test cases
The details of tests can be found at this: [IV. Test suits for `VIEW_EXEC`](https://hackmd.io/O8kstVixTAeufAWEVLJJkA?view).
## Implementations
## Appendix
- [Proposal of on-chain view patch](https://hackmd.io/AOx08A15TluzdExgkNmbAg)
- [Agora discussions](https://forum.tezosagora.org/t/on-chain-view-patch/4717)