Skip to main content

🧮 Saturation_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.

Definition t : Set := int.

Parameter mul_safe : Set.

Parameter may_saturate : Set.

Definition may_saturate_value (x_value : t) : t := x_value.

Definition to_int {A : Set} (x_value : A) : A := x_value.

Definition op_lt : t t bool := Compare.Int.op_lt.

Definition op_lteq : t t bool := Compare.Int.op_lteq.

Definition op_gt : t t bool := Compare.Int.op_gt.

Definition op_gteq : t t bool := Compare.Int.op_gteq.

Definition op_eq : t t bool := Compare.Int.op_eq.

Definition equal : t t bool := op_eq.

Definition op_ltgt : t t bool := Compare.Int.op_ltgt.

Definition max (x_value : t) (y_value : t) : t :=
  if op_gteq x_value y_value then
    x_value
  else
    y_value.

Definition min (x_value : t) (y_value : t) : t :=
  if op_gteq x_value y_value then
    y_value
  else
    x_value.

Definition compare : t t t := Compare.Int.compare.

Definition saturated : int := Pervasives.max_int.

Definition of_int_opt (t_value : int) : option int :=
  if (op_gteq t_value 0) && (op_lt t_value saturated) then
    Some t_value
  else
    None.

Definition of_z_opt (z_value : Z.t) : option int :=
  let 'int_value := Z.to_int z_value in
  of_int_opt int_value.

Definition to_z (x_value : int) : Z.t := Z.of_int x_value.

Definition saturate_if_undef (function_parameter : option int) : int :=
  match function_parameter with
  | Nonesaturated
  | Some x_valuex_value
  end.

Definition safe_int (x_value : int) : int :=
  saturate_if_undef (of_int_opt x_value).

Definition numbits (x_value : int) : int :=
  let x_value : Pervasives.ref int :=
    Pervasives.ref_value x_value
  in let n_value : Pervasives.ref int :=
    Pervasives.ref_value 0 in
  let '_ :=
    let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 32 in
    if op_ltgt y_value 0 then
      let '_ :=
        Pervasives.op_coloneq n_value
          ((Pervasives.op_exclamation n_value) +i 32) in
      Pervasives.op_coloneq x_value y_value
    else
      tt in
  let '_ :=
    let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 16 in
    if op_ltgt y_value 0 then
      let '_ :=
        Pervasives.op_coloneq n_value
          ((Pervasives.op_exclamation n_value) +i 16) in
      Pervasives.op_coloneq x_value y_value
    else
      tt in
  let '_ :=
    let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 8 in
    if op_ltgt y_value 0 then
      let '_ :=
        Pervasives.op_coloneq n_value ((Pervasives.op_exclamation n_value) +i 8)
        in
      Pervasives.op_coloneq x_value y_value
    else
      tt in
  let '_ :=
    let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 4 in
    if op_ltgt y_value 0 then
      let '_ :=
        Pervasives.op_coloneq n_value ((Pervasives.op_exclamation n_value) +i 4)
        in
      Pervasives.op_coloneq x_value y_value
    else
      tt in
  let '_ :=
    let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 2 in
    if op_ltgt y_value 0 then
      let '_ :=
        Pervasives.op_coloneq n_value ((Pervasives.op_exclamation n_value) +i 2)
        in
      Pervasives.op_coloneq x_value y_value
    else
      tt in
  if op_ltgt (Pervasives.lsr (Pervasives.op_exclamation x_value) 1) 0 then
    (Pervasives.op_exclamation n_value) +i 2
  else
    (Pervasives.op_exclamation n_value) +i (Pervasives.op_exclamation x_value).

Definition zero : int := 0.

Definition one : int := 1.

Definition small_enough (z_value : int) : bool :=
  op_eq (Pervasives.land z_value (-2147483648)) 0.

Definition mul_safe_value (x_value : int) : option int :=
  if small_enough x_value then
    Some x_value
  else
    None.

Definition mul_safe_exn (x_value : int) : int :=
  if small_enough x_value then
    x_value
  else
    Pervasives.failwith
      (Format.sprintf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "mul_safe_exn: "
            (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
              CamlinternalFormatBasics.No_padding
              CamlinternalFormatBasics.No_precision
              (CamlinternalFormatBasics.String_literal
                " must be below 2147483648"
                CamlinternalFormatBasics.End_of_format)))
          "mul_safe_exn: %d must be below 2147483648") x_value).

Definition mul_safe_of_int_exn (x_value : int) : int :=
  (fun (function_parameter : option int) ⇒
    match function_parameter with
    | None
      Pervasives.failwith
        (Format.sprintf
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.String_literal "mul_safe_of_int_exn: "
              (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                CamlinternalFormatBasics.No_padding
                CamlinternalFormatBasics.No_precision
                (CamlinternalFormatBasics.String_literal
                  " must be below 2147483648"
                  CamlinternalFormatBasics.End_of_format)))
            "mul_safe_of_int_exn: %d must be below 2147483648") x_value)
    | Some x_valuex_value
    end) (Option.bind (of_int_opt x_value) mul_safe_value).

Definition shift_right (x_value : int) (y_value : int) : int :=
  Pervasives.lsr x_value y_value.

Definition shift_left (x_value : int) (y_value : int) : int :=
  if op_lt (shift_right saturated y_value) x_value then
    saturated
  else
    Pervasives.lsl x_value y_value.

Definition mul (x_value : int) (y_value : int) : int :=
  match x_value with
  | 0 ⇒ 0
  | x_value
    if (small_enough x_value) && (small_enough y_value) then
      x_value ×i y_value
    else
      if y_value >i (saturated /i x_value) then
        saturated
      else
        x_value ×i y_value
  end.

Definition mul_fast (x_value : int) (y_value : int) : int := x_value ×i y_value.

Definition scale_fast (x_value : int) (y_value : int) : int :=
  if op_eq x_value 0 then
    0
  else
    if small_enough y_value then
      x_value ×i y_value
    else
      if y_value >i (saturated /i x_value) then
        saturated
      else
        x_value ×i y_value.

Definition add (x_value : int) (y_value : int) : int :=
  let z_value := x_value +i y_value in
  if z_value i 0 then
    z_value
  else
    saturated.

Definition succ (x_value : int) : int := add one x_value.

Definition sub (x_value : int) (y_value : int) : int :=
  Compare.Int.max (x_value -i y_value) 0.

Definition sub_opt (x_value : int) (y_value : int) : option int :=
  let s_value := x_value -i y_value in
  if s_value i 0 then
    Some s_value
  else
    None.

Definition erem (x_value : int) (y_value : int) : int :=
  Pervasives._mod x_value y_value.

Definition ediv (x_value : int) (y_value : int) : int := x_value /i y_value.

Definition sqrt (x_value : int) : int :=
  saturate_if_undef
    (Option.map (fun (x_value : int) ⇒ Z.to_int (Z.sqrt (Z.of_int x_value)))
      (of_int_opt x_value)).

Definition t_to_z_exn (z_value : Z.t) : int :=
  match of_z_opt z_value with
  | None
    (* ❌ Assert instruction is not handled. *)
    assert int false
  | Some x_valuex_value
  end.

Definition z_encoding : Data_encoding.encoding int :=
  Data_encoding.check_size 9
    (Data_encoding.conv to_z t_to_z_exn None Data_encoding.z_value).

Definition n_encoding : Data_encoding.encoding int :=
  Data_encoding.check_size 9
    (Data_encoding.conv to_z t_to_z_exn None Data_encoding.n_value).

Definition pp (fmt : Format.formatter) (x_value : int) : unit :=
  Format.pp_print_int fmt x_value.