Skip to main content

🦏 Sc_rollup_commitment_repr.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.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.

Definition hash_prefix : string :=
  String.String "017" (String.String "144" (String.String "021" "d")).

Module Hash.
  Definition prefix : string := "scc1".

  Definition encoded_size : int := 54.

  Definition H :=
    Blake2B.Make
      {|
        Blake2B.Register.register_encoding _ := Base58.register_encoding
      |}
      (let name := "commitment_hash" in
      let title := "The hash of a commitment of a smart contract rollup" in
      let b58check_prefix := hash_prefix in
      let size_value {A : Set} : option A :=
        None in
      {|
        Blake2B.PrefixedName.name := name;
        Blake2B.PrefixedName.title := title;
        Blake2B.PrefixedName.size_value := size_value;
        Blake2B.PrefixedName.b58check_prefix := b58check_prefix
      |}).

Inclusion of the module [H]
  Definition t := H.(S.HASH.t).

  Definition name := H.(S.HASH.name).

  Definition title := H.(S.HASH.title).

  Definition pp := H.(S.HASH.pp).

  Definition pp_short := H.(S.HASH.pp_short).

  Definition op_eq := H.(S.HASH.op_eq).

  Definition op_ltgt := H.(S.HASH.op_ltgt).

  Definition op_lt := H.(S.HASH.op_lt).

  Definition op_lteq := H.(S.HASH.op_lteq).

  Definition op_gteq := H.(S.HASH.op_gteq).

  Definition op_gt := H.(S.HASH.op_gt).

  Definition compare := H.(S.HASH.compare).

  Definition equal := H.(S.HASH.equal).

  Definition max := H.(S.HASH.max).

  Definition min := H.(S.HASH.min).

  Definition hash_bytes := H.(S.HASH.hash_bytes).

  Definition hash_string := H.(S.HASH.hash_string).

  Definition zero := H.(S.HASH.zero).

  Definition size_value := H.(S.HASH.size_value).

  Definition to_bytes := H.(S.HASH.to_bytes).

  Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).

  Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).

  Definition to_b58check := H.(S.HASH.to_b58check).

  Definition to_short_b58check := H.(S.HASH.to_short_b58check).

  Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).

  Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).

  Definition b58check_encoding := H.(S.HASH.b58check_encoding).

  Definition encoding := H.(S.HASH.encoding).

  Definition rpc_arg := H.(S.HASH.rpc_arg).

Init function; without side-effects in Coq
Inclusion of the module [Path_encoding_Make_hex_include]
  Definition to_path :=
    Path_encoding_Make_hex_include.(Path_encoding.S.to_path).

  Definition of_path :=
    Path_encoding_Make_hex_include.(Path_encoding.S.of_path).

  Definition path_length :=
    Path_encoding_Make_hex_include.(Path_encoding.S.path_length).
End Hash.

Module V1.
  Module t.
    Record record : Set := Build {
      compressed_state : Sc_rollup_repr.State_hash.t;
      inbox_level : Raw_level_repr.t;
      predecessor : Hash.t;
      number_of_ticks : Sc_rollup_repr.Number_of_ticks.t;
    }.
    Definition with_compressed_state compressed_state (r : record) :=
      Build compressed_state r.(inbox_level) r.(predecessor)
        r.(number_of_ticks).
    Definition with_inbox_level inbox_level (r : record) :=
      Build r.(compressed_state) inbox_level r.(predecessor)
        r.(number_of_ticks).
    Definition with_predecessor predecessor (r : record) :=
      Build r.(compressed_state) r.(inbox_level) predecessor
        r.(number_of_ticks).
    Definition with_number_of_ticks number_of_ticks (r : record) :=
      Build r.(compressed_state) r.(inbox_level) r.(predecessor)
        number_of_ticks.
  End t.
  Definition t := t.record.

  Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
    let '{|
      t.compressed_state := compressed_state;
        t.inbox_level := inbox_level;
        t.predecessor := predecessor;
        t.number_of_ticks := number_of_ticks
        |} := function_parameter in
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "compressed_state: "
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.Formatting_lit
              (CamlinternalFormatBasics.Break "@," 0 0)
              (CamlinternalFormatBasics.String_literal "inbox_level: "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.Formatting_lit
                    (CamlinternalFormatBasics.Break "@," 0 0)
                    (CamlinternalFormatBasics.String_literal "predecessor: "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.Formatting_lit
                          (CamlinternalFormatBasics.Break "@," 0 0)
                          (CamlinternalFormatBasics.String_literal
                            "number_of_ticks: "
                            (CamlinternalFormatBasics.Int64
                              CamlinternalFormatBasics.Int_d
                              CamlinternalFormatBasics.No_padding
                              CamlinternalFormatBasics.No_precision
                              CamlinternalFormatBasics.End_of_format)))))))))))
        "compressed_state: %a@,inbox_level: %a@,predecessor: %a@,number_of_ticks: %Ld")
      Sc_rollup_repr.State_hash.pp compressed_state Raw_level_repr.pp
      inbox_level Hash.pp predecessor
      (Sc_rollup_repr.Number_of_ticks.to_value number_of_ticks).

  Definition encoding : Data_encoding.encoding t :=
    Data_encoding.conv
      (fun (function_parameter : t) ⇒
        let '{|
          t.compressed_state := compressed_state;
            t.inbox_level := inbox_level;
            t.predecessor := predecessor;
            t.number_of_ticks := number_of_ticks
            |} := function_parameter in
        (compressed_state, inbox_level, predecessor, number_of_ticks))
      (fun (function_parameter :
        Sc_rollup_repr.State_hash.t × Raw_level_repr.t × Hash.t ×
          Sc_rollup_repr.Number_of_ticks.t) ⇒
        let '(compressed_state, inbox_level, predecessor, number_of_ticks) :=
          function_parameter in
        {| t.compressed_state := compressed_state; t.inbox_level := inbox_level;
          t.predecessor := predecessor; t.number_of_ticks := number_of_ticks; |})
      None
      (Data_encoding.obj4
        (Data_encoding.req None None "compressed_state"
          Sc_rollup_repr.State_hash.encoding)
        (Data_encoding.req None None "inbox_level" Raw_level_repr.encoding)
        (Data_encoding.req None None "predecessor" Hash.encoding)
        (Data_encoding.req None None "number_of_ticks"
          Sc_rollup_repr.Number_of_ticks.encoding)).

  Definition hash_uncarbonated (commitment : t) : Hash.t :=
    let commitment_bytes :=
      Data_encoding.Binary.to_bytes_exn None encoding commitment in
    Hash.hash_bytes None [ commitment_bytes ].

  Definition genesis_commitment
    (origination_level : Raw_level_repr.t)
    (genesis_state_hash : Sc_rollup_repr.State_hash.t) : M? t :=
    let? number_of_ticks := Sc_rollup_repr.Number_of_ticks.zero in
    return?
      {| t.compressed_state := genesis_state_hash;
        t.inbox_level := origination_level; t.predecessor := Hash.zero;
        t.number_of_ticks := number_of_ticks; |}.

  Module genesis_info.
    Record record : Set := Build {
      level : Raw_level_repr.t;
      commitment_hash : Hash.t;
    }.
    Definition with_level level (r : record) :=
      Build level r.(commitment_hash).
    Definition with_commitment_hash commitment_hash (r : record) :=
      Build r.(level) commitment_hash.
  End genesis_info.
  Definition genesis_info := genesis_info.record.

  Definition genesis_info_encoding : Data_encoding.encoding genesis_info :=
    Data_encoding.conv
      (fun (function_parameter : genesis_info) ⇒
        let '{|
          genesis_info.level := level;
            genesis_info.commitment_hash := commitment_hash
            |} := function_parameter in
        (level, commitment_hash))
      (fun (function_parameter : Raw_level_repr.t × Hash.t) ⇒
        let '(level, commitment_hash) := function_parameter in
        {| genesis_info.level := level;
          genesis_info.commitment_hash := commitment_hash; |}) None
      (Data_encoding.obj2
        (Data_encoding.req None None "level" Raw_level_repr.encoding)
        (Data_encoding.req None None "commitment_hash" Hash.encoding)).
End V1.

Inductive versioned : Set :=
| V1 : V1.t versioned.

Definition versioned_encoding : Data_encoding.encoding versioned :=
  Data_encoding.union None
    [
      Data_encoding.case_value "V1" None (Data_encoding.Tag 0) V1.encoding
        (fun (function_parameter : versioned) ⇒
          let 'V1 commitment := function_parameter in
          Some commitment) (fun (commitment : V1.t) ⇒ V1 commitment)
    ].

Include V1.

Definition of_versioned (function_parameter : versioned) : V1.t :=
  let 'V1 commitment := function_parameter in
  commitment.

Definition to_versioned (commitment : V1.t) : versioned := V1 commitment.