Skip to main content

🦥 Lazy_storage_kind.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.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.

Module TEMP_ID.
  Record signature {t : Set} : Set := {
    t := t;
    equal : t t bool;
    init_value : t;
    next : t t;
  }.
End TEMP_ID.
Definition TEMP_ID := @TEMP_ID.signature.
Arguments TEMP_ID {_}.

Module ID.
  Record signature {t : Set} : Set := {
    t := t;
    compare : t t int;
    encoding : Data_encoding.t t;
    rpc_arg : RPC_arg.arg t;
    init_value : t;
    
In the protocol, to be used in parse_data only
    parse_z : Z.t t;
    
In the protocol, to be used in unparse_data only
    unparse_to_z : t Z.t;
    next : t t;
    is_temp : t bool;
    of_legacy_USE_ONLY_IN_Legacy_big_map_diff : Z.t t;
    to_legacy_USE_ONLY_IN_Legacy_big_map_diff : t Z.t;
    to_path : t list string list string;
    of_path : list string M? (option t);
    path_length : M? int;
  }.
End ID.
Definition ID := @ID.signature.
Arguments ID {_}.

Module Title.
  Record signature : Set := {
    title : string;
  }.
End Title.
Definition Title := Title.signature.

Module TitleWithId.
  Record signature {Id_t IdSet_t : Set} : Set := {
    title : string;
    Id : ID (t := Id_t);
    Temp_id : TEMP_ID (t := Id.(ID.t));
    IdSet : _Set.S (elt := Id.(ID.t)) (t := IdSet_t);
  }.
End TitleWithId.
Definition TitleWithId := @TitleWithId.signature.
Arguments TitleWithId {_ _}.

Module MakeId.
  Class FArgs := {
    Title : Title;
  }.

  Definition title `{FArgs} : string := Title.(Title.title).

  Definition title_words `{FArgs} : string :=
    String.map
      (fun (function_parameter : ascii) ⇒
        match function_parameter with
        | "_" % char ⇒ " " % char
        | c_valuec_value
        end) title.

  Definition rpc_arg_error `{FArgs} : string :=
    Format.sprintf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Cannot parse "
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal " id"
              CamlinternalFormatBasics.End_of_format))) "Cannot parse %s id")
      title_words.

  Definition description `{FArgs} : string :=
    Format.sprintf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "A "
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal " identifier"
              CamlinternalFormatBasics.End_of_format))) "A %s identifier")
      title_words.

  Definition name `{FArgs} : string := Pervasives.op_caret title "_id".

  Definition encoding_title `{FArgs} : string :=
    Pervasives.op_caret (String.capitalize_ascii title_words) " identifier".

  Module Id.
    Definition t `{FArgs} : Set := Z.t.

    Definition compare `{FArgs} : Z.t Z.t int := Z.compare.

    Definition encoding `{FArgs} : Data_encoding.encoding Z.t :=
      Data_encoding.def name (Some encoding_title) (Some description)
        Data_encoding.z_value.

    Definition rpc_arg `{FArgs} : RPC_arg.arg Z.t :=
      let construct := Z.to_string in
      let destruct (hash_value : string) : Pervasives.result Z.t string :=
        Result.catch_f None
          (fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Z.of_string hash_value)
          (fun (function_parameter : extensible_type) ⇒
            let '_ := function_parameter in
            rpc_arg_error) in
      RPC_arg.make (Some description) name destruct construct tt.

    Definition init_value `{FArgs} : Z.t := Z.zero.

    Definition parse_z `{FArgs} (z_value : Z.t) : t := z_value.

    Definition unparse_to_z `{FArgs} (z_value : t) : Z.t := z_value.

    Definition next `{FArgs} : Z.t Z.t := Z.succ.

    Definition of_legacy_USE_ONLY_IN_Legacy_big_map_diff `{FArgs}
      (z_value : Z.t) : t := z_value.

    Definition to_legacy_USE_ONLY_IN_Legacy_big_map_diff `{FArgs} (z_value : t)
      : Z.t := z_value.

    Definition is_temp `{FArgs} (z_value : Z.t) : bool := z_value <Z Z.zero.

    Definition path_length `{FArgs} : M? int := return? 1.

    Definition to_path `{FArgs} (z_value : Z.t) (l_value : list string)
      : list string := cons (Z.to_string z_value) l_value.

    Definition of_path `{FArgs} (function_parameter : list string)
      : M? (option Z.t) :=
      match function_parameter with
      | ([] | cons _ (cons _ _)) ⇒ return? None
      | cons z_value []return? (Some (Z.of_string z_value))
      end.

    (* Id *)
    Definition module `{FArgs} :=
      {|
        ID.compare := compare;
        ID.encoding := encoding;
        ID.rpc_arg := rpc_arg;
        ID.init_value := init_value;
        ID.parse_z := parse_z;
        ID.unparse_to_z := unparse_to_z;
        ID.next := next;
        ID.of_legacy_USE_ONLY_IN_Legacy_big_map_diff :=
          of_legacy_USE_ONLY_IN_Legacy_big_map_diff;
        ID.to_legacy_USE_ONLY_IN_Legacy_big_map_diff :=
          to_legacy_USE_ONLY_IN_Legacy_big_map_diff;
        ID.is_temp := is_temp;
        ID.path_length := path_length;
        ID.to_path := to_path;
        ID.of_path := of_path
      |}.
  End Id.
  Definition Id `{FArgs} := Id.module.

  Module Temp_id.
    Definition t `{FArgs} : Set := Z.t.

    Definition equal `{FArgs} : Z.t Z.t bool := Z.equal.

    Definition init_value `{FArgs} : Z.t :=
      Z.of_int (Pervasives.op_tildeminus 1).

    Definition next `{FArgs} (z_value : Z.t) : Z.t := z_value -Z Z.one.

    (* Temp_id *)
    Definition module `{FArgs} :=
      {|
        TEMP_ID.equal := equal;
        TEMP_ID.init_value := init_value;
        TEMP_ID.next := next
      |}.
  End Temp_id.
  Definition Temp_id `{FArgs} := Temp_id.module.

  Definition IdSet `{FArgs} :=
    _Set.Make
      {|
        Compare.COMPARABLE.compare := Id.(ID.compare)
      |}.

  (* MakeId *)
  Definition functor `{FArgs} :=
    {|
      TitleWithId.title := title;
      TitleWithId.Id := Id;
      TitleWithId.Temp_id := Temp_id;
      TitleWithId.IdSet := IdSet
    |}.
End MakeId.
Definition MakeId (Title : Title) : TitleWithId (Id_t := _) (IdSet_t := _) :=
  let '_ := MakeId.Build_FArgs Title in
  MakeId.functor.

Module Big_map.
  Definition MakeId_include :=
    MakeId
      (let title := "big_map" in
      {|
        Title.title := title
      |}).

Inclusion of the module [MakeId_include]
  Definition title := MakeId_include.(TitleWithId.title).

  Definition Id := MakeId_include.(TitleWithId.Id).

  Definition Temp_id := MakeId_include.(TitleWithId.Temp_id).

  Definition IdSet := MakeId_include.(TitleWithId.IdSet).

  Module alloc.
    Record record : Set := Build {
      key_type : Script_repr.expr;
      value_type : Script_repr.expr;
    }.
    Definition with_key_type key_type (r : record) :=
      Build key_type r.(value_type).
    Definition with_value_type value_type (r : record) :=
      Build r.(key_type) value_type.
  End alloc.
  Definition alloc := alloc.record.

  Module update.
    Record record : Set := Build {
      key : Script_repr.expr;
      key_hash : Script_expr_hash.t;
      value : option Script_repr.expr;
    }.
    Definition with_key key (r : record) :=
      Build key r.(key_hash) r.(value).
    Definition with_key_hash key_hash (r : record) :=
      Build r.(key) key_hash r.(value).
    Definition with_value value (r : record) :=
      Build r.(key) r.(key_hash) value.
  End update.
  Definition update := update.record.

  Definition updates : Set := list update.

  Definition alloc_encoding : Data_encoding.encoding alloc :=
    Data_encoding.conv
      (fun (function_parameter : alloc) ⇒
        let '{| alloc.key_type := key_type; alloc.value_type := value_type |} :=
          function_parameter in
        (key_type, value_type))
      (fun (function_parameter : Script_repr.expr × Script_repr.expr) ⇒
        let '(key_type, value_type) := function_parameter in
        {| alloc.key_type := key_type; alloc.value_type := value_type; |}) None
      (Data_encoding.obj2
        (Data_encoding.req None None "key_type" Script_repr.expr_encoding)
        (Data_encoding.req None None "value_type" Script_repr.expr_encoding)).

  Definition update_encoding : Data_encoding.encoding update :=
    Data_encoding.conv
      (fun (function_parameter : update) ⇒
        let '{|
          update.key := key_value;
            update.key_hash := key_hash;
            update.value := value_value
            |} := function_parameter in
        (key_hash, key_value, value_value))
      (fun (function_parameter :
        Script_expr_hash.t × Script_repr.expr × option Script_repr.expr) ⇒
        let '(key_hash, key_value, value_value) := function_parameter in
        {| update.key := key_value; update.key_hash := key_hash;
          update.value := value_value; |}) None
      (Data_encoding.obj3
        (Data_encoding.req None None "key_hash" Script_expr_hash.encoding)
        (Data_encoding.req None None "key" Script_repr.expr_encoding)
        (Data_encoding.opt None None "value" Script_repr.expr_encoding)).

  Definition updates_encoding : Data_encoding.encoding (list update) :=
    Data_encoding.list_value None update_encoding.
End Big_map.

Module Sapling_state.
  Definition MakeId_include :=
    MakeId
      (let title := "sapling_state" in
      {|
        Title.title := title
      |}).

Inclusion of the module [MakeId_include]
  Definition title := MakeId_include.(TitleWithId.title).

  Definition Id := MakeId_include.(TitleWithId.Id).

  Definition Temp_id := MakeId_include.(TitleWithId.Temp_id).

  Definition IdSet := MakeId_include.(TitleWithId.IdSet).

  Module alloc.
    Record record : Set := Build {
      memo_size : Sapling_repr.Memo_size.t;
    }.
    Definition with_memo_size memo_size (r : record) :=
      Build memo_size.
  End alloc.
  Definition alloc := alloc.record.

  Definition updates : Set := Sapling_repr.diff.

  Definition alloc_encoding : Data_encoding.encoding alloc :=
    Data_encoding.conv
      (fun (function_parameter : alloc) ⇒
        let '{| alloc.memo_size := memo_size |} := function_parameter in
        memo_size)
      (fun (memo_size : Sapling_repr.Memo_size.t) ⇒
        {| alloc.memo_size := memo_size; |}) None
      (Data_encoding.obj1
        (Data_encoding.req None None "memo_size" Sapling_repr.Memo_size.encoding)).

  Definition updates_encoding : Data_encoding.encoding Sapling_repr.diff :=
    Sapling_repr.diff_encoding.
End Sapling_state.

Inductive t : Set :=
| Big_map : t
| Sapling_state : t.

Inductive ex : Set :=
| Ex_Kind : t ex.

Definition all : list (int × ex) :=
  [ (0, (Ex_Kind Big_map)); (1, (Ex_Kind Sapling_state)) ].

Inductive cmp : Set :=
| Eq : cmp
| Neq : cmp.

Definition equal (k1 : t) (k2 : t) : cmp :=
  match (k1, k2) with
  | (Big_map, Big_map)Eq
  | (Sapling_state, Sapling_state)Eq
  | (Big_map, _)Neq
  | (_, Big_map)Neq
  end.

Definition kind : Set := t.

Module Temp_ids.
  Module t.
    Record record : Set := Build {
      big_map : Big_map.Id.(ID.t);
      sapling_state : Sapling_state.Id.(ID.t);
    }.
    Definition with_big_map big_map (r : record) :=
      Build big_map r.(sapling_state).
    Definition with_sapling_state sapling_state (r : record) :=
      Build r.(big_map) sapling_state.
  End t.
  Definition t := t.record.

  Definition init_value : t :=
    {| t.big_map := Big_map.Temp_id.(TEMP_ID.init_value);
      t.sapling_state := Sapling_state.Temp_id.(TEMP_ID.init_value); |}.

  Definition fresh {i : Set} (kind_value : kind) (temp_ids : t) : t × i :=
    match kind_value with
    | Big_map
      cast (t × i)
      (let big_map := Big_map.Temp_id.(TEMP_ID.next) temp_ids.(t.big_map) in
      ((t.with_big_map big_map temp_ids), temp_ids.(t.big_map)))
    | Sapling_state
      cast (t × i)
      (let sapling_state :=
        Sapling_state.Temp_id.(TEMP_ID.next) temp_ids.(t.sapling_state) in
      ((t.with_sapling_state sapling_state temp_ids), temp_ids.(t.sapling_state)))
    end.

  #[bypass_check(guard)]
  Definition fold_s {acc i : Set}
    (kind_value : kind) (f_value : acc i acc) (temp_ids : t)
    (acc_value : acc) : acc :=
    let helper {j : Set} (Temp_id : {_ : unit @ TEMP_ID (t := j)})
      : j (acc j acc) acc :=
      let 'existS _ _ Temp_id := Temp_id in
      fun (last : j) ⇒
        fun (f_value : acc j acc) ⇒
          let fix aux (acc_value : acc) (id : j) {struct id} : acc :=
            if Temp_id.(TEMP_ID.equal) id last then
              acc_value
            else
              let acc_value := f_value acc_value id in
              aux acc_value (Temp_id.(TEMP_ID.next) id) in
          aux acc_value Temp_id.(TEMP_ID.init_value) in
    match (kind_value, f_value) with
    | (Big_map, f_value)
      let f_value := cast (acc Big_map.Id.(ID.t) acc) f_value in
      helper (existS (A := unit) (fun __) tt Big_map.Temp_id)
        temp_ids.(t.big_map)
        (fun (acc_value : acc) ⇒
          fun (temp_id : Big_map.Id.(ID.t)) ⇒ f_value acc_value temp_id)
    | (Sapling_state, f_value)
      let f_value := cast (acc Sapling_state.Id.(ID.t) acc) f_value in
      helper (existS (A := unit) (fun __) tt Sapling_state.Temp_id)
        temp_ids.(t.sapling_state)
        (fun (acc_value : acc) ⇒
          fun (temp_id : Sapling_state.Id.(ID.t)) ⇒ f_value acc_value temp_id)
    end.
End Temp_ids.

Module IdSet.
  Module t.
    Record record : Set := Build {
      big_map : Big_map.IdSet.(_Set.S.t);
      sapling_state : Sapling_state.IdSet.(_Set.S.t);
    }.
    Definition with_big_map big_map (r : record) :=
      Build big_map r.(sapling_state).
    Definition with_sapling_state sapling_state (r : record) :=
      Build r.(big_map) sapling_state.
  End t.
  Definition t := t.record.

  Module fold_f.
    Record record {acc : Set} : Set := Build {
      f : {i : Set}, kind i acc acc;
    }.
    Arguments record : clear implicits.
    Definition with_f {t_acc} f (r : record t_acc) :=
      Build t_acc f.
  End fold_f.
  Definition fold_f := fold_f.record.

  Definition empty : t :=
    {| t.big_map := Big_map.IdSet.(_Set.S.empty);
      t.sapling_state := Sapling_state.IdSet.(_Set.S.empty); |}.

  Definition mem {i : Set} (kind_value : kind) (id : i) (set : t) : bool :=
    match (kind_value, id, set) with
    | (Big_map, id, {| t.big_map := big_map |})
      let '[big_map, id] :=
        cast [Big_map.IdSet.(_Set.S.t) ** Big_map.Id.(ID.t)] [big_map, id] in
      Big_map.IdSet.(_Set.S.mem) id big_map
    | (Sapling_state, id, {| t.sapling_state := sapling_state |})
      let '[sapling_state, id] :=
        cast [Sapling_state.IdSet.(_Set.S.t) ** Sapling_state.Id.(ID.t)]
          [sapling_state, id] in
      Sapling_state.IdSet.(_Set.S.mem) id sapling_state
    end.

  Definition add {i : Set} (kind_value : kind) (id : i) (set : t) : t :=
    match (kind_value, id, set) with
    | (Big_map, id, {| t.big_map := big_map |})
      let '[big_map, id] :=
        cast [Big_map.IdSet.(_Set.S.t) ** Big_map.Id.(ID.t)] [big_map, id] in
      let big_map := Big_map.IdSet.(_Set.S.add) id big_map in
      t.with_big_map big_map set
    | (Sapling_state, id, {| t.sapling_state := sapling_state |})
      let '[sapling_state, id] :=
        cast [Sapling_state.IdSet.(_Set.S.t) ** Sapling_state.Id.(ID.t)]
          [sapling_state, id] in
      let sapling_state := Sapling_state.IdSet.(_Set.S.add) id sapling_state in
      t.with_sapling_state sapling_state set
    end.

  Definition diff_value (set1 : t) (set2 : t) : t :=
    let big_map :=
      Big_map.IdSet.(_Set.S.diff_value) set1.(t.big_map) set2.(t.big_map) in
    let sapling_state :=
      Sapling_state.IdSet.(_Set.S.diff_value) set1.(t.sapling_state)
        set2.(t.sapling_state) in
    {| t.big_map := big_map; t.sapling_state := sapling_state; |}.

  Definition fold {i acc : Set}
    (kind_value : kind) (f_value : i acc acc) (set : t) (acc_value : acc)
    : acc :=
    match (kind_value, f_value, set) with
    | (Big_map, f_value, {| t.big_map := big_map |})
      let '[big_map, f_value] :=
        cast [Big_map.IdSet.(_Set.S.t) ** Big_map.Id.(ID.t) acc acc]
          [big_map, f_value] in
      Big_map.IdSet.(_Set.S.fold) f_value big_map acc_value
    | (Sapling_state, f_value, {| t.sapling_state := sapling_state |})
      let '[sapling_state, f_value] :=
        cast
          [Sapling_state.IdSet.(_Set.S.t) **
            Sapling_state.Id.(ID.t) acc acc] [sapling_state, f_value] in
      Sapling_state.IdSet.(_Set.S.fold) f_value sapling_state acc_value
    end.

  Definition fold_all {A : Set} (f_value : fold_f A) (set : t) (acc_value : A)
    : A :=
    List.fold_left
      (fun (acc_value : A) ⇒
        fun (function_parameter : int × ex) ⇒
          let '(_, Ex_Kind kind_value) := function_parameter in
          let 'existT _ __Ex_Kind kind_value :=
            cast_exists (Es := Set) (fun __Ex_Kindkind) kind_value in
          (fold (i := __Ex_Kind)) kind_value (f_value.(fold_f.f) kind_value) set
            acc_value) acc_value all.
End IdSet.