package tezos-protocol-007-PsDELPH1

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val manager_script_code : Script_repr.lazy_expr

This code mimics the now defunct scriptless KT1s.

The manager contract is from: https://gitlab.com/nomadic-labs/mi-cho-coq/blob/7b42f2e970e1541af54f8a9b6820b4f18e847575/src/contracts/manager.tz The formal proof is at: https://gitlab.com/nomadic-labs/mi-cho-coq/blob/a7603e12021166e15890f6d504feebec2f945502/src/contracts_coq/manager.v

val add_do : manager_pkh:Tezos_crypto.Signature.public_key_hash -> script_code:Script_repr.lazy_expr -> script_storage:Script_repr.lazy_expr -> (Script_repr.lazy_expr * Script_repr.lazy_expr, Tezos_protocol_environment_007_PsDELPH1__Environment.Error_monad.error list) result Lwt.t

This code mimics the now defunct "spendable" flags of KT1s by adding a do entrypoint, preserving the original script's at 'default' entrypoint.

The pseudo-code for the applied transformations is from: https://gitlab.com/nomadic-labs/mi-cho-coq/blob/7b42f2e970e1541af54f8a9b6820b4f18e847575/src/contracts/transform/add_do.tz

val add_set_delegate : manager_pkh:Tezos_crypto.Signature.public_key_hash -> script_code:Script_repr.lazy_expr -> script_storage:Script_repr.lazy_expr -> (Script_repr.lazy_expr * Script_repr.lazy_expr, Tezos_protocol_environment_007_PsDELPH1__Environment.Error_monad.error list) result Lwt.t

This code mimics the now defunct "spendable" flags of KT1s by adding a do entrypoint, preserving the original script's at 'default' entrypoint.

The pseudo-code for the applied transformations is from: https://gitlab.com/nomadic-labs/mi-cho-coq/blob/7b42f2e970e1541af54f8a9b6820b4f18e847575/src/contracts/transform/add_set_delegate.tz

val has_default_entrypoint : Script_repr.lazy_expr -> bool

Checks if a contract was declaring a default entrypoint somewhere else than at the root, in which case its type changes when entrypoints are activated.

val add_root_entrypoint : script_code:Script_repr.lazy_expr -> (Script_repr.lazy_expr, Tezos_protocol_environment_007_PsDELPH1__Environment.Error_monad.error list) result Lwt.t

Adds a %root annotation on the toplevel parameter construct.