Skip to main content

🍬 Michelson_v1_primitives.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.

Inductive prim : Set :=
| K_parameter : prim
| K_storage : prim
| K_code : prim
| K_view : prim
| D_False : prim
| D_Elt : prim
| D_Left : prim
| D_None : prim
| D_Pair : prim
| D_Right : prim
| D_Some : prim
| D_True : prim
| D_Unit : prim
| D_Lambda_rec : prim
| I_PACK : prim
| I_UNPACK : prim
| I_BLAKE2B : prim
| I_SHA256 : prim
| I_SHA512 : prim
| I_ABS : prim
| I_ADD : prim
| I_AMOUNT : prim
| I_AND : prim
| I_BALANCE : prim
| I_CAR : prim
| I_CDR : prim
| I_CHAIN_ID : prim
| I_CHECK_SIGNATURE : prim
| I_COMPARE : prim
| I_CONCAT : prim
| I_CONS : prim
| I_CREATE_ACCOUNT : prim
| I_CREATE_CONTRACT : prim
| I_IMPLICIT_ACCOUNT : prim
| I_DIP : prim
| I_DROP : prim
| I_DUP : prim
| I_VIEW : prim
| I_EDIV : prim
| I_EMPTY_BIG_MAP : prim
| I_EMPTY_MAP : prim
| I_EMPTY_SET : prim
| I_EQ : prim
| I_EXEC : prim
| I_APPLY : prim
| I_FAILWITH : prim
| I_GE : prim
| I_GET : prim
| I_GET_AND_UPDATE : prim
| I_GT : prim
| I_HASH_KEY : prim
| I_IF : prim
| I_IF_CONS : prim
| I_IF_LEFT : prim
| I_IF_NONE : prim
| I_INT : prim
| I_LAMBDA : prim
| I_LAMBDA_REC : prim
| I_LE : prim
| I_LEFT : prim
| I_LEVEL : prim
| I_LOOP : prim
| I_LSL : prim
| I_LSR : prim
| I_LT : prim
| I_MAP : prim
| I_MEM : prim
| I_MUL : prim
| I_NEG : prim
| I_NEQ : prim
| I_NIL : prim
| I_NONE : prim
| I_NOT : prim
| I_NOW : prim
| I_MIN_BLOCK_TIME : prim
| I_OR : prim
| I_PAIR : prim
| I_UNPAIR : prim
| I_PUSH : prim
| I_RIGHT : prim
| I_SIZE : prim
| I_SOME : prim
| I_SOURCE : prim
| I_SENDER : prim
| I_SELF : prim
| I_SELF_ADDRESS : prim
| I_SLICE : prim
| I_STEPS_TO_QUOTA : prim
| I_SUB : prim
| I_SUB_MUTEZ : prim
| I_SWAP : prim
| I_TRANSFER_TOKENS : prim
| I_SET_DELEGATE : prim
| I_UNIT : prim
| I_UPDATE : prim
| I_XOR : prim
| I_ITER : prim
| I_LOOP_LEFT : prim
| I_ADDRESS : prim
| I_CONTRACT : prim
| I_ISNAT : prim
| I_CAST : prim
| I_RENAME : prim
| I_SAPLING_EMPTY_STATE : prim
| I_SAPLING_VERIFY_UPDATE : prim
| I_DIG : prim
| I_DUG : prim
| I_NEVER : prim
| I_VOTING_POWER : prim
| I_TOTAL_VOTING_POWER : prim
| I_KECCAK : prim
| I_SHA3 : prim
| I_PAIRING_CHECK : prim
| I_TICKET : prim
| I_TICKET_DEPRECATED : prim
| I_READ_TICKET : prim
| I_SPLIT_TICKET : prim
| I_JOIN_TICKETS : prim
| I_OPEN_CHEST : prim
| I_EMIT : prim
| T_bool : prim
| T_contract : prim
| T_int : prim
| T_key : prim
| T_key_hash : prim
| T_lambda : prim
| T_list : prim
| T_map : prim
| T_big_map : prim
| T_nat : prim
| T_option : prim
| T_or : prim
| T_pair : prim
| T_set : prim
| T_signature : prim
| T_string : prim
| T_bytes : prim
| T_mutez : prim
| T_timestamp : prim
| T_unit : prim
| T_operation : prim
| T_address : prim
| T_tx_rollup_l2_address : prim
| T_sapling_transaction : prim
| T_sapling_transaction_deprecated : prim
| T_sapling_state : prim
| T_chain_id : prim
| T_never : prim
| T_bls12_381_g1 : prim
| T_bls12_381_g2 : prim
| T_bls12_381_fr : prim
| T_ticket : prim
| T_chest_key : prim
| T_chest : prim
| H_constant : prim.

Inductive namespace : Set :=
| Type_namespace : namespace
| Constant_namespace : namespace
| Instr_namespace : namespace
| Keyword_namespace : namespace
| Constant_hash_namespace : namespace.

Definition namespace_value (function_parameter : prim) : namespace :=
  match function_parameter with
  | (K_code | K_view | K_parameter | K_storage) ⇒ Keyword_namespace
  |
    (D_Elt | D_False | D_Left | D_None | D_Pair | D_Right | D_Some | D_True |
    D_Unit | D_Lambda_rec) ⇒ Constant_namespace
  |
    (I_ABS | I_ADD | I_ADDRESS | I_AMOUNT | I_AND | I_APPLY | I_BALANCE |
    I_BLAKE2B | I_CAR | I_CAST | I_CDR | I_CHAIN_ID | I_CHECK_SIGNATURE |
    I_COMPARE | I_CONCAT | I_CONS | I_CONTRACT | I_CREATE_ACCOUNT |
    I_CREATE_CONTRACT | I_DIG | I_DIP | I_DROP | I_DUG | I_DUP | I_VIEW | I_EDIV
    | I_EMPTY_BIG_MAP | I_EMPTY_MAP | I_EMPTY_SET | I_EQ | I_EXEC | I_FAILWITH |
    I_GE | I_GET | I_GET_AND_UPDATE | I_GT | I_HASH_KEY | I_IF | I_IF_CONS |
    I_IF_LEFT | I_IF_NONE | I_IMPLICIT_ACCOUNT | I_INT | I_ISNAT | I_ITER |
    I_JOIN_TICKETS | I_KECCAK | I_LAMBDA | I_LAMBDA_REC | I_LE | I_LEFT |
    I_LEVEL | I_LOOP | I_LOOP_LEFT | I_LSL | I_LSR | I_LT | I_MAP | I_MEM |
    I_MUL | I_NEG | I_NEQ | I_NEVER | I_NIL | I_NONE | I_NOT | I_NOW |
    I_MIN_BLOCK_TIME | I_OR | I_PACK | I_PAIR | I_PAIRING_CHECK | I_PUSH |
    I_READ_TICKET | I_RENAME | I_RIGHT | I_SAPLING_EMPTY_STATE |
    I_SAPLING_VERIFY_UPDATE | I_SELF | I_SELF_ADDRESS | I_SENDER |
    I_SET_DELEGATE | I_SHA256 | I_SHA512 | I_SHA3 | I_SIZE | I_SLICE | I_SOME |
    I_SOURCE | I_SPLIT_TICKET | I_STEPS_TO_QUOTA | I_SUB | I_SUB_MUTEZ | I_SWAP
    | I_TICKET | I_TICKET_DEPRECATED | I_TOTAL_VOTING_POWER | I_TRANSFER_TOKENS
    | I_UNIT | I_UNPACK | I_UNPAIR | I_UPDATE | I_VOTING_POWER | I_XOR |
    I_OPEN_CHEST | I_EMIT) ⇒ Instr_namespace
  |
    (T_address | T_tx_rollup_l2_address | T_big_map | T_bool | T_bytes |
    T_chain_id | T_contract | T_int | T_key | T_key_hash | T_lambda | T_list |
    T_map | T_mutez | T_nat | T_never | T_operation | T_option | T_or | T_pair |
    T_sapling_state | T_sapling_transaction | T_sapling_transaction_deprecated |
    T_set | T_signature | T_string | T_timestamp | T_unit | T_bls12_381_fr |
    T_bls12_381_g1 | T_bls12_381_g2 | T_ticket | T_chest_key | T_chest) ⇒
    Type_namespace
  | H_constantConstant_hash_namespace
  end.

#[bypass_check(guard)]
Definition valid_case (name : string) : bool :=
  let is_lower (function_parameter : ascii) : bool :=
    match function_parameter with
    |
      ("_" % char | "a" % char | "b" % char | "c" % char | "d" % char |
      "e" % char | "f" % char | "g" % char | "h" % char | "i" % char |
      "j" % char | "k" % char | "l" % char | "m" % char | "n" % char |
      "o" % char | "p" % char | "q" % char | "r" % char | "s" % char |
      "t" % char | "u" % char | "v" % char | "w" % char | "x" % char |
      "y" % char | "z" % char) ⇒ true
    | _false
    end in
  let is_upper (function_parameter : ascii) : bool :=
    match function_parameter with
    |
      ("_" % char | "A" % char | "B" % char | "C" % char | "D" % char |
      "E" % char | "F" % char | "G" % char | "H" % char | "I" % char |
      "J" % char | "K" % char | "L" % char | "M" % char | "N" % char |
      "O" % char | "P" % char | "Q" % char | "R" % char | "S" % char |
      "T" % char | "U" % char | "V" % char | "W" % char | "X" % char |
      "Y" % char | "Z" % char) ⇒ true
    | _false
    end in
  let fix for_all (a_value : int) (b_value : int) (f_value : int bool)
    {struct a_value} : bool :=
    (a_value >i b_value) ||
    ((f_value a_value) && (for_all (a_value +i 1) b_value f_value)) in
  let len := String.length name in
  (len i 0) &&
  ((Compare.Char.(Compare.S.op_ltgt) (String.get name 0) "_" % char) &&
  (((is_upper (String.get name 0)) &&
  (for_all 1 (len -i 1)
    (fun (i_value : int) ⇒ is_upper (String.get name i_value)))) ||
  (((is_upper (String.get name 0)) &&
  (for_all 1 (len -i 1)
    (fun (i_value : int) ⇒ is_lower (String.get name i_value)))) ||
  ((is_lower (String.get name 0)) &&
  (for_all 1 (len -i 1)
    (fun (i_value : int) ⇒ is_lower (String.get name i_value))))))).

Definition string_of_prim (function_parameter : prim) : string :=
  match function_parameter with
  | K_parameter ⇒ "parameter"
  | K_storage ⇒ "storage"
  | K_code ⇒ "code"
  | K_view ⇒ "view"
  | D_False ⇒ "False"
  | D_Elt ⇒ "Elt"
  | D_Left ⇒ "Left"
  | D_None ⇒ "None"
  | D_Pair ⇒ "Pair"
  | D_Right ⇒ "Right"
  | D_Some ⇒ "Some"
  | D_True ⇒ "True"
  | D_Unit ⇒ "Unit"
  | D_Lambda_rec ⇒ "Lambda_rec"
  | I_PACK ⇒ "PACK"
  | I_UNPACK ⇒ "UNPACK"
  | I_BLAKE2B ⇒ "BLAKE2B"
  | I_SHA256 ⇒ "SHA256"
  | I_SHA512 ⇒ "SHA512"
  | I_ABS ⇒ "ABS"
  | I_ADD ⇒ "ADD"
  | I_AMOUNT ⇒ "AMOUNT"
  | I_AND ⇒ "AND"
  | I_BALANCE ⇒ "BALANCE"
  | I_CAR ⇒ "CAR"
  | I_CDR ⇒ "CDR"
  | I_CHAIN_ID ⇒ "CHAIN_ID"
  | I_CHECK_SIGNATURE ⇒ "CHECK_SIGNATURE"
  | I_COMPARE ⇒ "COMPARE"
  | I_CONCAT ⇒ "CONCAT"
  | I_CONS ⇒ "CONS"
  | I_CREATE_ACCOUNT ⇒ "CREATE_ACCOUNT"
  | I_CREATE_CONTRACT ⇒ "CREATE_CONTRACT"
  | I_IMPLICIT_ACCOUNT ⇒ "IMPLICIT_ACCOUNT"
  | I_DIP ⇒ "DIP"
  | I_DROP ⇒ "DROP"
  | I_DUP ⇒ "DUP"
  | I_EDIV ⇒ "EDIV"
  | I_EMPTY_BIG_MAP ⇒ "EMPTY_BIG_MAP"
  | I_EMPTY_MAP ⇒ "EMPTY_MAP"
  | I_EMPTY_SET ⇒ "EMPTY_SET"
  | I_EQ ⇒ "EQ"
  | I_EXEC ⇒ "EXEC"
  | I_APPLY ⇒ "APPLY"
  | I_FAILWITH ⇒ "FAILWITH"
  | I_GE ⇒ "GE"
  | I_GET ⇒ "GET"
  | I_GET_AND_UPDATE ⇒ "GET_AND_UPDATE"
  | I_GT ⇒ "GT"
  | I_HASH_KEY ⇒ "HASH_KEY"
  | I_IF ⇒ "IF"
  | I_IF_CONS ⇒ "IF_CONS"
  | I_IF_LEFT ⇒ "IF_LEFT"
  | I_IF_NONE ⇒ "IF_NONE"
  | I_INT ⇒ "INT"
  | I_LAMBDA ⇒ "LAMBDA"
  | I_LAMBDA_REC ⇒ "LAMBDA_REC"
  | I_LE ⇒ "LE"
  | I_LEFT ⇒ "LEFT"
  | I_LEVEL ⇒ "LEVEL"
  | I_LOOP ⇒ "LOOP"
  | I_LSL ⇒ "LSL"
  | I_LSR ⇒ "LSR"
  | I_LT ⇒ "LT"
  | I_MAP ⇒ "MAP"
  | I_MEM ⇒ "MEM"
  | I_MUL ⇒ "MUL"
  | I_NEG ⇒ "NEG"
  | I_NEQ ⇒ "NEQ"
  | I_NIL ⇒ "NIL"
  | I_NONE ⇒ "NONE"
  | I_NOT ⇒ "NOT"
  | I_NOW ⇒ "NOW"
  | I_MIN_BLOCK_TIME ⇒ "MIN_BLOCK_TIME"
  | I_OR ⇒ "OR"
  | I_PAIR ⇒ "PAIR"
  | I_PUSH ⇒ "PUSH"
  | I_RIGHT ⇒ "RIGHT"
  | I_SIZE ⇒ "SIZE"
  | I_SOME ⇒ "SOME"
  | I_SOURCE ⇒ "SOURCE"
  | I_SENDER ⇒ "SENDER"
  | I_SELF ⇒ "SELF"
  | I_SELF_ADDRESS ⇒ "SELF_ADDRESS"
  | I_SLICE ⇒ "SLICE"
  | I_STEPS_TO_QUOTA ⇒ "STEPS_TO_QUOTA"
  | I_SUB ⇒ "SUB"
  | I_SUB_MUTEZ ⇒ "SUB_MUTEZ"
  | I_SWAP ⇒ "SWAP"
  | I_TRANSFER_TOKENS ⇒ "TRANSFER_TOKENS"
  | I_SET_DELEGATE ⇒ "SET_DELEGATE"
  | I_UNIT ⇒ "UNIT"
  | I_UNPAIR ⇒ "UNPAIR"
  | I_UPDATE ⇒ "UPDATE"
  | I_XOR ⇒ "XOR"
  | I_ITER ⇒ "ITER"
  | I_LOOP_LEFT ⇒ "LOOP_LEFT"
  | I_ADDRESS ⇒ "ADDRESS"
  | I_CONTRACT ⇒ "CONTRACT"
  | I_ISNAT ⇒ "ISNAT"
  | I_CAST ⇒ "CAST"
  | I_RENAME ⇒ "RENAME"
  | I_SAPLING_EMPTY_STATE ⇒ "SAPLING_EMPTY_STATE"
  | I_SAPLING_VERIFY_UPDATE ⇒ "SAPLING_VERIFY_UPDATE"
  | I_DIG ⇒ "DIG"
  | I_DUG ⇒ "DUG"
  | I_NEVER ⇒ "NEVER"
  | I_VOTING_POWER ⇒ "VOTING_POWER"
  | I_TOTAL_VOTING_POWER ⇒ "TOTAL_VOTING_POWER"
  | I_KECCAK ⇒ "KECCAK"
  | I_SHA3 ⇒ "SHA3"
  | I_PAIRING_CHECK ⇒ "PAIRING_CHECK"
  | I_TICKET ⇒ "TICKET"
  | I_TICKET_DEPRECATED ⇒ "TICKET_DEPRECATED"
  | I_READ_TICKET ⇒ "READ_TICKET"
  | I_SPLIT_TICKET ⇒ "SPLIT_TICKET"
  | I_JOIN_TICKETS ⇒ "JOIN_TICKETS"
  | I_OPEN_CHEST ⇒ "OPEN_CHEST"
  | I_EMIT ⇒ "EMIT"
  | I_VIEW ⇒ "VIEW"
  | T_bool ⇒ "bool"
  | T_contract ⇒ "contract"
  | T_int ⇒ "int"
  | T_key ⇒ "key"
  | T_key_hash ⇒ "key_hash"
  | T_lambda ⇒ "lambda"
  | T_list ⇒ "list"
  | T_map ⇒ "map"
  | T_big_map ⇒ "big_map"
  | T_nat ⇒ "nat"
  | T_option ⇒ "option"
  | T_or ⇒ "or"
  | T_pair ⇒ "pair"
  | T_set ⇒ "set"
  | T_signature ⇒ "signature"
  | T_string ⇒ "string"
  | T_bytes ⇒ "bytes"
  | T_mutez ⇒ "mutez"
  | T_timestamp ⇒ "timestamp"
  | T_unit ⇒ "unit"
  | T_operation ⇒ "operation"
  | T_address ⇒ "address"
  | T_tx_rollup_l2_address ⇒ "tx_rollup_l2_address"
  | T_sapling_state ⇒ "sapling_state"
  | T_sapling_transaction ⇒ "sapling_transaction"
  | T_sapling_transaction_deprecated ⇒ "sapling_transaction_deprecated"
  | T_chain_id ⇒ "chain_id"
  | T_never ⇒ "never"
  | T_bls12_381_g1 ⇒ "bls12_381_g1"
  | T_bls12_381_g2 ⇒ "bls12_381_g2"
  | T_bls12_381_fr ⇒ "bls12_381_fr"
  | T_ticket ⇒ "ticket"
  | T_chest_key ⇒ "chest_key"
  | T_chest ⇒ "chest"
  | H_constant ⇒ "constant"
  end.

Definition prim_of_string (function_parameter : string) : M? prim :=
  match function_parameter with
  | "parameter" ⇒ return? K_parameter
  | "storage" ⇒ return? K_storage
  | "code" ⇒ return? K_code
  | "view" ⇒ return? K_view
  | "False" ⇒ return? D_False
  | "Elt" ⇒ return? D_Elt
  | "Left" ⇒ return? D_Left
  | "None" ⇒ return? D_None
  | "Pair" ⇒ return? D_Pair
  | "Right" ⇒ return? D_Right
  | "Some" ⇒ return? D_Some
  | "True" ⇒ return? D_True
  | "Unit" ⇒ return? D_Unit
  | "Lambda_rec" ⇒ return? D_Lambda_rec
  | "PACK" ⇒ return? I_PACK
  | "UNPACK" ⇒ return? I_UNPACK
  | "BLAKE2B" ⇒ return? I_BLAKE2B
  | "SHA256" ⇒ return? I_SHA256
  | "SHA512" ⇒ return? I_SHA512
  | "ABS" ⇒ return? I_ABS
  | "ADD" ⇒ return? I_ADD
  | "AMOUNT" ⇒ return? I_AMOUNT
  | "AND" ⇒ return? I_AND
  | "BALANCE" ⇒ return? I_BALANCE
  | "CAR" ⇒ return? I_CAR
  | "CDR" ⇒ return? I_CDR
  | "CHAIN_ID" ⇒ return? I_CHAIN_ID
  | "CHECK_SIGNATURE" ⇒ return? I_CHECK_SIGNATURE
  | "COMPARE" ⇒ return? I_COMPARE
  | "CONCAT" ⇒ return? I_CONCAT
  | "CONS" ⇒ return? I_CONS
  | "CREATE_ACCOUNT" ⇒ return? I_CREATE_ACCOUNT
  | "CREATE_CONTRACT" ⇒ return? I_CREATE_CONTRACT
  | "IMPLICIT_ACCOUNT" ⇒ return? I_IMPLICIT_ACCOUNT
  | "DIP" ⇒ return? I_DIP
  | "DROP" ⇒ return? I_DROP
  | "DUP" ⇒ return? I_DUP
  | "VIEW" ⇒ return? I_VIEW
  | "EDIV" ⇒ return? I_EDIV
  | "EMPTY_BIG_MAP" ⇒ return? I_EMPTY_BIG_MAP
  | "EMPTY_MAP" ⇒ return? I_EMPTY_MAP
  | "EMPTY_SET" ⇒ return? I_EMPTY_SET
  | "EQ" ⇒ return? I_EQ
  | "EXEC" ⇒ return? I_EXEC
  | "APPLY" ⇒ return? I_APPLY
  | "FAILWITH" ⇒ return? I_FAILWITH
  | "GE" ⇒ return? I_GE
  | "GET" ⇒ return? I_GET
  | "GET_AND_UPDATE" ⇒ return? I_GET_AND_UPDATE
  | "GT" ⇒ return? I_GT
  | "HASH_KEY" ⇒ return? I_HASH_KEY
  | "IF" ⇒ return? I_IF
  | "IF_CONS" ⇒ return? I_IF_CONS
  | "IF_LEFT" ⇒ return? I_IF_LEFT
  | "IF_NONE" ⇒ return? I_IF_NONE
  | "INT" ⇒ return? I_INT
  | "KECCAK" ⇒ return? I_KECCAK
  | "LAMBDA" ⇒ return? I_LAMBDA
  | "LAMBDA_REC" ⇒ return? I_LAMBDA_REC
  | "LE" ⇒ return? I_LE
  | "LEFT" ⇒ return? I_LEFT
  | "LEVEL" ⇒ return? I_LEVEL
  | "LOOP" ⇒ return? I_LOOP
  | "LSL" ⇒ return? I_LSL
  | "LSR" ⇒ return? I_LSR
  | "LT" ⇒ return? I_LT
  | "MAP" ⇒ return? I_MAP
  | "MEM" ⇒ return? I_MEM
  | "MUL" ⇒ return? I_MUL
  | "NEG" ⇒ return? I_NEG
  | "NEQ" ⇒ return? I_NEQ
  | "NIL" ⇒ return? I_NIL
  | "NONE" ⇒ return? I_NONE
  | "NOT" ⇒ return? I_NOT
  | "NOW" ⇒ return? I_NOW
  | "MIN_BLOCK_TIME" ⇒ return? I_MIN_BLOCK_TIME
  | "OR" ⇒ return? I_OR
  | "PAIR" ⇒ return? I_PAIR
  | "UNPAIR" ⇒ return? I_UNPAIR
  | "PAIRING_CHECK" ⇒ return? I_PAIRING_CHECK
  | "PUSH" ⇒ return? I_PUSH
  | "RIGHT" ⇒ return? I_RIGHT
  | "SHA3" ⇒ return? I_SHA3
  | "SIZE" ⇒ return? I_SIZE
  | "SOME" ⇒ return? I_SOME
  | "SOURCE" ⇒ return? I_SOURCE
  | "SENDER" ⇒ return? I_SENDER
  | "SELF" ⇒ return? I_SELF
  | "SELF_ADDRESS" ⇒ return? I_SELF_ADDRESS
  | "SLICE" ⇒ return? I_SLICE
  | "STEPS_TO_QUOTA" ⇒ return? I_STEPS_TO_QUOTA
  | "SUB" ⇒ return? I_SUB
  | "SUB_MUTEZ" ⇒ return? I_SUB_MUTEZ
  | "SWAP" ⇒ return? I_SWAP
  | "TRANSFER_TOKENS" ⇒ return? I_TRANSFER_TOKENS
  | "SET_DELEGATE" ⇒ return? I_SET_DELEGATE
  | "UNIT" ⇒ return? I_UNIT
  | "UPDATE" ⇒ return? I_UPDATE
  | "XOR" ⇒ return? I_XOR
  | "ITER" ⇒ return? I_ITER
  | "LOOP_LEFT" ⇒ return? I_LOOP_LEFT
  | "ADDRESS" ⇒ return? I_ADDRESS
  | "CONTRACT" ⇒ return? I_CONTRACT
  | "ISNAT" ⇒ return? I_ISNAT
  | "CAST" ⇒ return? I_CAST
  | "RENAME" ⇒ return? I_RENAME
  | "SAPLING_EMPTY_STATE" ⇒ return? I_SAPLING_EMPTY_STATE
  | "SAPLING_VERIFY_UPDATE" ⇒ return? I_SAPLING_VERIFY_UPDATE
  | "DIG" ⇒ return? I_DIG
  | "DUG" ⇒ return? I_DUG
  | "NEVER" ⇒ return? I_NEVER
  | "VOTING_POWER" ⇒ return? I_VOTING_POWER
  | "TOTAL_VOTING_POWER" ⇒ return? I_TOTAL_VOTING_POWER
  | "TICKET" ⇒ return? I_TICKET
  | "TICKET_DEPRECATED" ⇒ return? I_TICKET_DEPRECATED
  | "READ_TICKET" ⇒ return? I_READ_TICKET
  | "SPLIT_TICKET" ⇒ return? I_SPLIT_TICKET
  | "JOIN_TICKETS" ⇒ return? I_JOIN_TICKETS
  | "OPEN_CHEST" ⇒ return? I_OPEN_CHEST
  | "EMIT" ⇒ return? I_EMIT
  | "bool" ⇒ return? T_bool
  | "contract" ⇒ return? T_contract
  | "int" ⇒ return? T_int
  | "key" ⇒ return? T_key
  | "key_hash" ⇒ return? T_key_hash
  | "lambda" ⇒ return? T_lambda
  | "list" ⇒ return? T_list
  | "map" ⇒ return? T_map
  | "big_map" ⇒ return? T_big_map
  | "nat" ⇒ return? T_nat
  | "option" ⇒ return? T_option
  | "or" ⇒ return? T_or
  | "pair" ⇒ return? T_pair
  | "set" ⇒ return? T_set
  | "signature" ⇒ return? T_signature
  | "string" ⇒ return? T_string
  | "bytes" ⇒ return? T_bytes
  | "mutez" ⇒ return? T_mutez
  | "timestamp" ⇒ return? T_timestamp
  | "unit" ⇒ return? T_unit
  | "operation" ⇒ return? T_operation
  | "address" ⇒ return? T_address
  | "tx_rollup_l2_address" ⇒ return? T_tx_rollup_l2_address
  | "sapling_state" ⇒ return? T_sapling_state
  | "sapling_transaction" ⇒ return? T_sapling_transaction
  | "sapling_transaction_deprecated" ⇒ return? T_sapling_transaction_deprecated
  | "chain_id" ⇒ return? T_chain_id
  | "never" ⇒ return? T_never
  | "bls12_381_g1" ⇒ return? T_bls12_381_g1
  | "bls12_381_g2" ⇒ return? T_bls12_381_g2
  | "bls12_381_fr" ⇒ return? T_bls12_381_fr
  | "ticket" ⇒ return? T_ticket
  | "chest_key" ⇒ return? T_chest_key
  | "chest" ⇒ return? T_chest
  | "constant" ⇒ return? H_constant
  | n_value
    if valid_case n_value then
      Error_monad.error_value
        (Build_extensible "Unknown_primitive_name" string n_value)
    else
      Error_monad.error_value (Build_extensible "Invalid_case" string n_value)
  end.

#[bypass_check(guard)]
Definition prims_of_strings (expr : Micheline.canonical string)
  : M? (Micheline.canonical prim) :=
  let fix convert
    (function_parameter : Micheline.node Micheline.canonical_location string)
    {struct function_parameter}
    : M? (Micheline.node Micheline.canonical_location prim) :=
    match function_parameter with
    | Micheline.Int l_value z_valuereturn? (Micheline.Int l_value z_value)
    | Micheline.String l_value s_value
      return? (Micheline.String l_value s_value)
    | Micheline.Bytes l_value b_value
      return? (Micheline.Bytes l_value b_value)
    | Micheline.Prim loc_value prim args annot
      let? prim :=
        Error_monad.record_trace
          (Build_extensible "Invalid_primitive_name"
            (Micheline.canonical string × Micheline.canonical_location)
            (expr, loc_value)) (prim_of_string prim) in
      let? args := List.map_e convert args in
      return? (Micheline.Prim loc_value prim args annot)
    | Micheline.Seq loc_value args
      let? args := List.map_e convert args in
      return? (Micheline.Seq loc_value args)
    end in
  let? expr := convert (Micheline.root_value expr) in
  return? (Micheline.strip_locations expr).

#[bypass_check(guard)]
Definition strings_of_prims (expr : Micheline.canonical prim)
  : Micheline.canonical string :=
  let fix convert {A : Set} (function_parameter : Micheline.node A prim)
    {struct function_parameter} : Micheline.node A string :=
    match function_parameter with
    | Micheline.Int l_value z_valueMicheline.Int l_value z_value
    | Micheline.String l_value s_valueMicheline.String l_value s_value
    | Micheline.Bytes l_value b_valueMicheline.Bytes l_value b_value
    | Micheline.Prim loc_value prim args annot
      let prim := string_of_prim prim in
      let args := List.map convert args in
      Micheline.Prim loc_value prim args annot
    | Micheline.Seq loc_value args
      let args := List.map convert args in
      Micheline.Seq loc_value args
    end in
  Micheline.strip_locations (convert (Micheline.root_value expr)).

Definition prim_encoding : Data_encoding.encoding prim :=
  Data_encoding.def "michelson.v1.primitives" None None
    (Data_encoding.string_enum
      [
        ("parameter", K_parameter);
        ("storage", K_storage);
        ("code", K_code);
        ("False", D_False);
        ("Elt", D_Elt);
        ("Left", D_Left);
        ("None", D_None);
        ("Pair", D_Pair);
        ("Right", D_Right);
        ("Some", D_Some);
        ("True", D_True);
        ("Unit", D_Unit);
        ("PACK", I_PACK);
        ("UNPACK", I_UNPACK);
        ("BLAKE2B", I_BLAKE2B);
        ("SHA256", I_SHA256);
        ("SHA512", I_SHA512);
        ("ABS", I_ABS);
        ("ADD", I_ADD);
        ("AMOUNT", I_AMOUNT);
        ("AND", I_AND);
        ("BALANCE", I_BALANCE);
        ("CAR", I_CAR);
        ("CDR", I_CDR);
        ("CHECK_SIGNATURE", I_CHECK_SIGNATURE);
        ("COMPARE", I_COMPARE);
        ("CONCAT", I_CONCAT);
        ("CONS", I_CONS);
        ("CREATE_ACCOUNT", I_CREATE_ACCOUNT);
        ("CREATE_CONTRACT", I_CREATE_CONTRACT);
        ("IMPLICIT_ACCOUNT", I_IMPLICIT_ACCOUNT);
        ("DIP", I_DIP);
        ("DROP", I_DROP);
        ("DUP", I_DUP);
        ("EDIV", I_EDIV);
        ("EMPTY_MAP", I_EMPTY_MAP);
        ("EMPTY_SET", I_EMPTY_SET);
        ("EQ", I_EQ);
        ("EXEC", I_EXEC);
        ("FAILWITH", I_FAILWITH);
        ("GE", I_GE);
        ("GET", I_GET);
        ("GT", I_GT);
        ("HASH_KEY", I_HASH_KEY);
        ("IF", I_IF);
        ("IF_CONS", I_IF_CONS);
        ("IF_LEFT", I_IF_LEFT);
        ("IF_NONE", I_IF_NONE);
        ("INT", I_INT);
        ("LAMBDA", I_LAMBDA);
        ("LE", I_LE);
        ("LEFT", I_LEFT);
        ("LOOP", I_LOOP);
        ("LSL", I_LSL);
        ("LSR", I_LSR);
        ("LT", I_LT);
        ("MAP", I_MAP);
        ("MEM", I_MEM);
        ("MUL", I_MUL);
        ("NEG", I_NEG);
        ("NEQ", I_NEQ);
        ("NIL", I_NIL);
        ("NONE", I_NONE);
        ("NOT", I_NOT);
        ("NOW", I_NOW);
        ("OR", I_OR);
        ("PAIR", I_PAIR);
        ("PUSH", I_PUSH);
        ("RIGHT", I_RIGHT);
        ("SIZE", I_SIZE);
        ("SOME", I_SOME);
        ("SOURCE", I_SOURCE);
        ("SENDER", I_SENDER);
        ("SELF", I_SELF);
        ("STEPS_TO_QUOTA", I_STEPS_TO_QUOTA);
        ("SUB", I_SUB);
        ("SWAP", I_SWAP);
        ("TRANSFER_TOKENS", I_TRANSFER_TOKENS);
        ("SET_DELEGATE", I_SET_DELEGATE);
        ("UNIT", I_UNIT);
        ("UPDATE", I_UPDATE);
        ("XOR", I_XOR);
        ("ITER", I_ITER);
        ("LOOP_LEFT", I_LOOP_LEFT);
        ("ADDRESS", I_ADDRESS);
        ("CONTRACT", I_CONTRACT);
        ("ISNAT", I_ISNAT);
        ("CAST", I_CAST);
        ("RENAME", I_RENAME);
        ("bool", T_bool);
        ("contract", T_contract);
        ("int", T_int);
        ("key", T_key);
        ("key_hash", T_key_hash);
        ("lambda", T_lambda);
        ("list", T_list);
        ("map", T_map);
        ("big_map", T_big_map);
        ("nat", T_nat);
        ("option", T_option);
        ("or", T_or);
        ("pair", T_pair);
        ("set", T_set);
        ("signature", T_signature);
        ("string", T_string);
        ("bytes", T_bytes);
        ("mutez", T_mutez);
        ("timestamp", T_timestamp);
        ("unit", T_unit);
        ("operation", T_operation);
        ("address", T_address);
        ("SLICE", I_SLICE);
        ("DIG", I_DIG);
        ("DUG", I_DUG);
        ("EMPTY_BIG_MAP", I_EMPTY_BIG_MAP);
        ("APPLY", I_APPLY);
        ("chain_id", T_chain_id);
        ("CHAIN_ID", I_CHAIN_ID);
        ("LEVEL", I_LEVEL);
        ("SELF_ADDRESS", I_SELF_ADDRESS);
        ("never", T_never);
        ("NEVER", I_NEVER);
        ("UNPAIR", I_UNPAIR);
        ("VOTING_POWER", I_VOTING_POWER);
        ("TOTAL_VOTING_POWER", I_TOTAL_VOTING_POWER);
        ("KECCAK", I_KECCAK);
        ("SHA3", I_SHA3);
        ("PAIRING_CHECK", I_PAIRING_CHECK);
        ("bls12_381_g1", T_bls12_381_g1);
        ("bls12_381_g2", T_bls12_381_g2);
        ("bls12_381_fr", T_bls12_381_fr);
        ("sapling_state", T_sapling_state);
        ("sapling_transaction_deprecated", T_sapling_transaction_deprecated);
        ("SAPLING_EMPTY_STATE", I_SAPLING_EMPTY_STATE);
        ("SAPLING_VERIFY_UPDATE", I_SAPLING_VERIFY_UPDATE);
        ("ticket", T_ticket);
        ("TICKET_DEPRECATED", I_TICKET_DEPRECATED);
        ("READ_TICKET", I_READ_TICKET);
        ("SPLIT_TICKET", I_SPLIT_TICKET);
        ("JOIN_TICKETS", I_JOIN_TICKETS);
        ("GET_AND_UPDATE", I_GET_AND_UPDATE);
        ("chest", T_chest);
        ("chest_key", T_chest_key);
        ("OPEN_CHEST", I_OPEN_CHEST);
        ("VIEW", I_VIEW);
        ("view", K_view);
        ("constant", H_constant);
        ("SUB_MUTEZ", I_SUB_MUTEZ);
        ("tx_rollup_l2_address", T_tx_rollup_l2_address);
        ("MIN_BLOCK_TIME", I_MIN_BLOCK_TIME);
        ("sapling_transaction", T_sapling_transaction);
        ("EMIT", I_EMIT);
        ("Lambda_rec", D_Lambda_rec);
        ("LAMBDA_REC", I_LAMBDA_REC);
        ("TICKET", I_TICKET)
      ]).

Init function; without side-effects in Coq
Definition init_module : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.unknown_primitive_name" "Unknown primitive name"
      "In a script or data expression, a primitive was unknown."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (n_value : string) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Unknown primitive "
                  (CamlinternalFormatBasics.String
                    CamlinternalFormatBasics.No_padding
                    (CamlinternalFormatBasics.Char_literal "." % char
                      CamlinternalFormatBasics.End_of_format)))
                "Unknown primitive %s.") n_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "wrong_primitive_name"
          Data_encoding.string_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Unknown_primitive_name" then
            let got := cast string payload in
            Some got
          else None
        end)
      (fun (got : string) ⇒
        Build_extensible "Unknown_primitive_name" string got) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "michelson_v1.invalid_primitive_name_case" "Invalid primitive name case"
      "In a script or data expression, a primitive name is neither uppercase, lowercase or capitalized."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (n_value : string) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Primitive "
                  (CamlinternalFormatBasics.String
                    CamlinternalFormatBasics.No_padding
                    (CamlinternalFormatBasics.String_literal
                      " has invalid case."
                      CamlinternalFormatBasics.End_of_format)))
                "Primitive %s has invalid case.") n_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "wrong_primitive_name"
          Data_encoding.string_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_case" then
            let name := cast string payload in
            Some name
          else None
        end)
      (fun (name : string) ⇒ Build_extensible "Invalid_case" string name) in
  Error_monad.register_error_kind Error_monad.Permanent
    "michelson_v1.invalid_primitive_name" "Invalid primitive name"
    "In a script or data expression, a primitive name is unknown or has a wrong case."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter :
          Micheline.canonical string × Micheline.canonical_location) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "Invalid primitive."
                CamlinternalFormatBasics.End_of_format) "Invalid primitive.")))
    (Data_encoding.obj2
      (Data_encoding.req None None "expression"
        (Micheline.canonical_encoding "generic" Data_encoding.string_value))
      (Data_encoding.req None None "location"
        Micheline.canonical_location_encoding))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Invalid_primitive_name" then
          let '(expr, loc_value) :=
            cast (Micheline.canonical string × Micheline.canonical_location)
              payload in
          Some (expr, loc_value)
        else None
      end)
    (fun (function_parameter :
      Micheline.canonical string × Micheline.canonical_location) ⇒
      let '(expr, loc_value) := function_parameter in
      Build_extensible "Invalid_primitive_name"
        (Micheline.canonical string × Micheline.canonical_location)
        (expr, loc_value)).

Definition string_of_namespace (function_parameter : namespace) : string :=
  match function_parameter with
  | Type_namespace ⇒ "T"
  | Constant_namespace ⇒ "D"
  | Instr_namespace ⇒ "I"
  | Keyword_namespace ⇒ "K"
  | Constant_hash_namespace ⇒ "H"
  end.