🍃 Wasm_2_0_0.v

Environment

Gitlab

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

Require TezosOfOCaml.Environment.Structs.V7.Bounded.
Require TezosOfOCaml.Environment.Structs.V0.Context.

Module input.
  Record record : Set := Build {
    inbox_level : Bounded.Non_negative_int32.(Bounded.S.t);
    message_counter : Z.t;
  }.
  Definition with_inbox_level inbox_level (r : record) :=
    Build inbox_level r.(message_counter).
  Definition with_message_counter message_counter (r : record) :=
    Build r.(inbox_level) message_counter.
End input.
Definition input := input.record.

Module output.
  Record record : Set := Build {
    outbox_level : Bounded.Non_negative_int32.(Bounded.S.t);
    message_index : Z.t;
  }.
  Definition with_outbox_level outbox_level (r : record) :=
    Build outbox_level r.(message_index).
  Definition with_message_index message_index (r : record) :=
    Build r.(outbox_level) message_index.
End output.
Definition output := output.record.

Parameter reveal_hash : Set.

Parameter reveal_hash_to_string : reveal_hash → string.

Inductive reveal : Set :=
| Reveal_raw_data : reveal_hash → reveal
| Reveal_metadata : reveal.

Inductive input_request : Set :=
| No_input_required : input_request
| Input_required : input_request
| Reveal_required : reveal → input_request.

Module info.
  Record record : Set := Build {
    current_tick : Z.t;
    last_input_read : option input;
    input_request : input_request;
  }.
  Definition with_current_tick current_tick (r : record) :=
    Build current_tick r.(last_input_read) r.(input_request).
  Definition with_last_input_read last_input_read (r : record) :=
    Build r.(current_tick) last_input_read r.(input_request).
  Definition with_input_request input_request (r : record) :=
    Build r.(current_tick) r.(last_input_read) input_request.
End info.
Definition info := info.record.

Module S.
  Record signature {tree : Set} : Set := {
    tree := tree;
    install_boot_sector : string → tree → tree;
    compute_step : tree → tree;
    set_input_step : input → string → tree → tree;
    reveal_step : bytes → tree → tree;
    get_output : output → tree → option string;
    get_info : tree → info;
  }.
End S.
Definition S := @S.signature.
Arguments S {_}.

Parameter Make :
  ∀ {Tree_t Tree_tree : Set},
  ∀ (Tree :
    Context.TREE (t := Tree_t) (tree := Tree_tree) (key := list string)
      (value := bytes)), S (tree := Tree.(Context.TREE.tree)).