Skip to main content

✒️ Contract_delegate_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Contract_delegate_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.

The function [find] is valid.
The function [init_value] is valid.
The function [unlink] is valid.
The function [delete] is valid.
The function [set] is valid.
The function [delegated_contracts] is valid.