Skip to main content

🏋️ Fitness_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.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.

Module t.
  Record record : Set := Build {
    level : Raw_level_repr.t;
    locked_round : option Round_repr.t;
    predecessor_round : Round_repr.t;
    round : Round_repr.t;
  }.
  Definition with_level level (r : record) :=
    Build level r.(locked_round) r.(predecessor_round) r.(round).
  Definition with_locked_round locked_round (r : record) :=
    Build r.(level) locked_round r.(predecessor_round) r.(round).
  Definition with_predecessor_round predecessor_round (r : record) :=
    Build r.(level) r.(locked_round) predecessor_round r.(round).
  Definition with_round round (r : record) :=
    Build r.(level) r.(locked_round) r.(predecessor_round) round.
End t.
Definition t := t.record.

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.def "fitness" None None
    (Data_encoding.conv_with_guard
      (fun (function_parameter : t) ⇒
        let '{|
          t.level := level;
            t.locked_round := locked_round;
            t.predecessor_round := predecessor_round;
            t.round := round
            |} := function_parameter in
        (level, locked_round, predecessor_round, round))
      (fun (function_parameter :
        Raw_level_repr.t × option Round_repr.t × Round_repr.t × Round_repr.t) ⇒
        let '(level, locked_round, predecessor_round, round) :=
          function_parameter in
        match locked_round with
        | None
          return?
            {| t.level := level; t.locked_round := locked_round;
              t.predecessor_round := predecessor_round; t.round := round; |}
        | Some locked_round_val
          if Round_repr.op_lteq round locked_round_val then
            Pervasives.Error "Locked round must be smaller than round."
          else
            return?
              {| t.level := level; t.locked_round := locked_round;
                t.predecessor_round := predecessor_round; t.round := round; |}
        end) None
      (Data_encoding.obj4
        (Data_encoding.req None None "level" Raw_level_repr.encoding)
        (Data_encoding.req None None "locked_round"
          (Data_encoding.option_value Round_repr.encoding))
        (Data_encoding.req None None "predecessor_round" Round_repr.encoding)
        (Data_encoding.req None None "round" Round_repr.encoding))).

Definition pp (ppf : Format.formatter) (f_value : t) : unit :=
  let minus_sign :=
    if Round_repr.op_eq f_value.(t.predecessor_round) Round_repr.zero then
      ""
    else
      "-" in
  let locked_round (ppf : Format.formatter) (locked_round : option Round_repr.t)
    : unit :=
    match locked_round with
    | NoneFormat.pp_print_string ppf "unlocked"
    | Some round
      Format.fprintf ppf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "locked: "
            (CamlinternalFormatBasics.Alpha
              CamlinternalFormatBasics.End_of_format)) "locked: %a")
        Round_repr.pp round
    end in
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Char_literal "(" % char
        (CamlinternalFormatBasics.Alpha
          (CamlinternalFormatBasics.String_literal ", "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.String_literal ", "
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.Char_literal ")" % char
                          CamlinternalFormatBasics.End_of_format))))))))))
      "(%a, %a, %s%a, %a)") Raw_level_repr.pp f_value.(t.level) locked_round
    f_value.(t.locked_round) minus_sign Round_repr.pp
    f_value.(t.predecessor_round) Round_repr.pp f_value.(t.round).

Module Locked_round_not_less_than_round.
  Record record : Set := Build {
    round : Round_repr.t;
    locked_round : Round_repr.t;
  }.
  Definition with_round round (r : record) :=
    Build round r.(locked_round).
  Definition with_locked_round locked_round (r : record) :=
    Build r.(round) locked_round.
End Locked_round_not_less_than_round.
Definition Locked_round_not_less_than_round :=
  Locked_round_not_less_than_round.record.

Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent "invalid_fitness"
      "Invalid fitness"
      "Fitness representation should be exactly 4 times 4 bytes long."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Invalid fitness"
                  CamlinternalFormatBasics.End_of_format) "Invalid fitness")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_fitness" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_fitness" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent "wrong_fitness"
      "Wrong fitness" "Wrong fitness."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Wrong fitness."
                  CamlinternalFormatBasics.End_of_format) "Wrong fitness.")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_fitness" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Wrong_fitness" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent "outdated_fitness"
      "Outdated fitness" "Outdated fitness: referring to a previous version"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Outdated fitness: referring to a previous version."
                  CamlinternalFormatBasics.End_of_format)
                "Outdated fitness: referring to a previous version.")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Outdated_fitness" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Outdated_fitness" unit tt) in
  Error_monad.register_error_kind Error_monad.Permanent
    "locked_round_not_less_than_round" "Locked round not smaller than round"
    "The round is smaller than or equal to the locked round."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : Round_repr.t × Round_repr.t) ⇒
          let '(round, locked_round) := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Incorrect fitness: round "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal
                    " is less than or equal to locked round "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.Char_literal "." % char
                        CamlinternalFormatBasics.End_of_format)))))
              "Incorrect fitness: round %a is less than or equal to locked round %a.")
            Round_repr.pp round Round_repr.pp locked_round))
    (Data_encoding.obj2
      (Data_encoding.req None None "round" Round_repr.encoding)
      (Data_encoding.req None None "locked_round" Round_repr.encoding))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Locked_round_not_less_than_round" then
          let '{|
            Locked_round_not_less_than_round.round := round;
              Locked_round_not_less_than_round.locked_round := locked_round
              |} := cast Locked_round_not_less_than_round payload in
          Some (round, locked_round)
        else None
      end)
    (fun (function_parameter : Round_repr.t × Round_repr.t) ⇒
      let '(round, locked_round) := function_parameter in
      Build_extensible "Locked_round_not_less_than_round"
        Locked_round_not_less_than_round
        {| Locked_round_not_less_than_round.round := round;
          Locked_round_not_less_than_round.locked_round := locked_round; |}).

Definition create_without_locked_round
  (level : Raw_level_repr.t) (predecessor_round : Round_repr.t)
  (round : Round_repr.t) : t :=
  {| t.level := level; t.locked_round := None;
    t.predecessor_round := predecessor_round; t.round := round; |}.

Definition create
  (level : Raw_level_repr.t) (locked_round : option Round_repr.t)
  (predecessor_round : Round_repr.t) (round : Round_repr.t) : M? t :=
  match locked_round with
  | None
    return?
      {| t.level := level; t.locked_round := locked_round;
        t.predecessor_round := predecessor_round; t.round := round; |}
  | Some locked_round_val
    let? '_ :=
      Error_monad.error_when (Round_repr.op_lteq round locked_round_val)
        (Build_extensible "Locked_round_not_less_than_round"
          Locked_round_not_less_than_round
          {| Locked_round_not_less_than_round.round := round;
            Locked_round_not_less_than_round.locked_round := locked_round_val;
            |}) in
    return?
      {| t.level := level; t.locked_round := locked_round;
        t.predecessor_round := predecessor_round; t.round := round; |}
  end.

Definition int32_to_bytes (i_value : int32) : bytes :=
  let b_value := Bytes.make 4 "000" % char in
  let '_ := TzEndian.set_int32 b_value 0 i_value in
  b_value.

Definition int32_of_bytes (b_value : bytes) : M? int32 :=
  if (Bytes.length b_value) i 4 then
    Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt)
  else
    return? (TzEndian.get_int32 b_value 0).

Definition locked_round_to_bytes (function_parameter : option Round_repr.t)
  : bytes :=
  match function_parameter with
  | NoneBytes.empty
  | Some locked_roundint32_to_bytes (Round_repr.to_int32 locked_round)
  end.

Definition locked_round_of_bytes (b_value : bytes) : M? (option Round_repr.t) :=
  if (Bytes.length b_value) =i 0 then
    return? None
  else
    if (Bytes.length b_value) =i 4 then
      let? r_value := Round_repr.of_int32 (TzEndian.get_int32 b_value 0) in
      return? (Some r_value)
    else
      Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt).

Definition predecessor_round_of_bytes (neg_predecessor_round : bytes)
  : M? Round_repr.t :=
  let? neg_predecessor_round := int32_of_bytes neg_predecessor_round in
  Round_repr.of_int32 (Int32.pred (Int32.neg neg_predecessor_round)).

Definition round_of_bytes (round : bytes) : M? Round_repr.t :=
  Error_monad.op_gtgtquestion (int32_of_bytes round) Round_repr.of_int32.

Definition to_raw (function_parameter : t) : list bytes :=
  let '{|
    t.level := level;
      t.locked_round := locked_round;
      t.predecessor_round := predecessor_round;
      t.round := round
      |} := function_parameter in
  [
    Bytes.of_string Constants_repr.fitness_version_number;
    int32_to_bytes (Raw_level_repr.to_int32 level);
    locked_round_to_bytes locked_round;
    int32_to_bytes
      (Int32.pred (Int32.neg (Round_repr.to_int32 predecessor_round)));
    int32_to_bytes (Round_repr.to_int32 round)
  ].

Definition from_raw (function_parameter : list bytes) : M? t :=
  match
    (function_parameter,
      match function_parameter with
      |
        cons version
          (cons level
            (cons locked_round (cons neg_predecessor_round (cons round [])))) ⇒
        Compare.String.(Compare.S.op_eq) (Bytes.to_string version)
          Constants_repr.fitness_version_number
      | _false
      end,
      match function_parameter with
      | cons version (cons _ []) ⇒
        Compare.String.(Compare.S.op_lt) (Bytes.to_string version)
          Constants_repr.fitness_version_number
      | _false
      end) with
  |
    (cons version
      (cons level
        (cons locked_round (cons neg_predecessor_round (cons round [])))), true,
      _)
    let? level :=
      Error_monad.op_gtgtquestion (int32_of_bytes level) Raw_level_repr.of_int32
      in
    let? locked_round := locked_round_of_bytes locked_round in
    let? predecessor_round := predecessor_round_of_bytes neg_predecessor_round
      in
    let? round := round_of_bytes round in
    create level locked_round predecessor_round round
  | (cons version (cons _ []), _, true)
    Error_monad.error_value (Build_extensible "Outdated_fitness" unit tt)
  | ([], _, _)
    Error_monad.error_value (Build_extensible "Outdated_fitness" unit tt)
  | (_, _, _)
    Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt)
  end.

Definition round_from_raw (function_parameter : list bytes) : M? Round_repr.t :=
  match
    (function_parameter,
      match function_parameter with
      |
        cons version
          (cons _level
            (cons _locked_round (cons _neg_predecessor_round (cons round []))))
        ⇒
        Compare.String.(Compare.S.op_eq) (Bytes.to_string version)
          Constants_repr.fitness_version_number
      | _false
      end,
      match function_parameter with
      | cons version (cons _ []) ⇒
        Compare.String.(Compare.S.op_lt) (Bytes.to_string version)
          Constants_repr.fitness_version_number
      | _false
      end) with
  |
    (cons version
      (cons _level
        (cons _locked_round (cons _neg_predecessor_round (cons round [])))),
      true, _)round_of_bytes round
  | (cons version (cons _ []), _, true)return? Round_repr.zero
  | ([], _, _)return? Round_repr.zero
  | (_, _, _)
    Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt)
  end.

Definition predecessor_round_from_raw (function_parameter : list bytes)
  : M? Round_repr.t :=
  match
    (function_parameter,
      match function_parameter with
      |
        cons version
          (cons _level
            (cons _locked_round (cons neg_predecessor_round (cons _round []))))
        ⇒
        Compare.String.(Compare.S.op_eq) (Bytes.to_string version)
          Constants_repr.fitness_version_number
      | _false
      end,
      match function_parameter with
      | cons version (cons _ []) ⇒
        Compare.String.(Compare.S.op_lt) (Bytes.to_string version)
          Constants_repr.fitness_version_number
      | _false
      end) with
  |
    (cons version
      (cons _level
        (cons _locked_round (cons neg_predecessor_round (cons _round [])))),
      true, _)predecessor_round_of_bytes neg_predecessor_round
  | (cons version (cons _ []), _, true)return? Round_repr.zero
  | ([], _, _)return? Round_repr.zero
  | (_, _, _)
    Error_monad.error_value (Build_extensible "Invalid_fitness" unit tt)
  end.

Definition check_except_locked_round
  (fitness : t) (level : Raw_level_repr.raw_level)
  (predecessor_round : Round_repr.t) : M? unit :=
  let '{|
    t.level := expected_level;
      t.locked_round := _;
      t.predecessor_round := expected_predecessor_round;
      t.round := _
      |} := fitness in
  let correct :=
    (Raw_level_repr.op_eq level expected_level) &&
    (Round_repr.op_eq predecessor_round expected_predecessor_round) in
  Error_monad.error_unless correct (Build_extensible "Wrong_fitness" unit tt).

Definition check_locked_round (fitness : t) (locked_round : option Round_repr.t)
  : M? unit :=
  let '{|
    t.level := _;
      t.locked_round := expected_locked_round;
      t.predecessor_round := _;
      t.round := _
      |} := fitness in
  let correct :=
    match (locked_round, expected_locked_round) with
    | (None, None)true
    | ((Some _, None) | (None, Some _)) ⇒ false
    | (Some v_value, Some v')Round_repr.op_eq v_value v'
    end in
  Error_monad.error_unless correct (Build_extensible "Wrong_fitness" unit tt).

Definition level (fitness : t) : Raw_level_repr.t := fitness.(t.level).

Definition round (fitness : t) : Round_repr.t := fitness.(t.round).

Definition locked_round (fitness : t) : option Round_repr.t :=
  fitness.(t.locked_round).

Definition predecessor_round (fitness : t) : Round_repr.t :=
  fitness.(t.predecessor_round).