Skip to main content

📜 Bounded_history_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.

Module NAME.
  Record signature : Set := {
    name : string;
    _sig_NAME : unit;
  }.
End NAME.
Definition NAME := NAME.signature.

Module KEY.
  Record signature {t : Set} : Set := {
    t := t;
    compare : t t int;
    pp : Format.formatter t unit;
    encoding : Data_encoding.t t;
    _sig_KEY : unit;
  }.
End KEY.
Definition KEY := @KEY.signature.
Arguments KEY {_}.

Module VALUE.
  Record signature {t : Set} : Set := {
    t := t;
    equal : t t bool;
    pp : Format.formatter t unit;
    encoding : Data_encoding.t t;
  }.
End VALUE.
Definition VALUE := @VALUE.signature.
Arguments VALUE {_}.

Module S.
  Record signature {t key value : Set} : Set := {
    t := t;
    key := key;
    value := value;
    empty : int64 t;
    encoding : Data_encoding.t t;
    pp : Format.formatter t unit;
    find : key t option value;
    remember : key value t M? t;
  }.
End S.
Definition S := @S.signature.
Arguments S {_ _ _}.

Module Make.
  Class FArgs {Key_t Value_t : Set} := {
    Name : NAME;
    Key : KEY (t := Key_t);
    Value : VALUE (t := Value_t);
  }.
  Arguments Build_FArgs {_ _}.

  Definition key `{FArgs} : Set := Key.(KEY.t).

  Definition value `{FArgs} : Set := Value.(VALUE.t).

  Definition Int64_map `{FArgs} :=
    Map.Make
      {|
        Compare.COMPARABLE.compare := Int64.compare
      |}.

  Definition Map `{FArgs} :=
    Map.Make
      {|
        Compare.COMPARABLE.compare := Key.(KEY.compare)
      |}.

  Module t.
    Record record `{FArgs} : Set := Build {
      events : Map.(Map.S.t) value;
      sequence : Int64_map.(Map.S.t) key;
      capacity : int64;
      next_index : int64;
      oldest_index : int64;
      size : int64;
    }.
    Definition with_events `{FArgs} events (r : record) :=
      Build _ _ _ events r.(sequence) r.(capacity) r.(next_index)
        r.(oldest_index) r.(size).
    Definition with_sequence `{FArgs} sequence (r : record) :=
      Build _ _ _ r.(events) sequence r.(capacity) r.(next_index)
        r.(oldest_index) r.(size).
    Definition with_capacity `{FArgs} capacity (r : record) :=
      Build _ _ _ r.(events) r.(sequence) capacity r.(next_index)
        r.(oldest_index) r.(size).
    Definition with_next_index `{FArgs} next_index (r : record) :=
      Build _ _ _ r.(events) r.(sequence) r.(capacity) next_index
        r.(oldest_index) r.(size).
    Definition with_oldest_index `{FArgs} oldest_index (r : record) :=
      Build _ _ _ r.(events) r.(sequence) r.(capacity) r.(next_index)
        oldest_index r.(size).
    Definition with_size `{FArgs} size (r : record) :=
      Build _ _ _ r.(events) r.(sequence) r.(capacity) r.(next_index)
        r.(oldest_index) size.
  End t.
  Definition t `{FArgs} := t.record.

  Definition encoding `{FArgs} : Data_encoding.t t :=
    let events_encoding :=
      Data_encoding.conv Map.(Map.S.bindings)
        (fun (l_value : list (Key.(KEY.t) × Value.(VALUE.t))) ⇒
          Map.(Map.S.add_seq) (List.to_seq l_value) Map.(Map.S.empty)) None
        (Data_encoding.list_value None
          (Data_encoding.tup2 Key.(KEY.encoding) Value.(VALUE.encoding))) in
    let sequence_encoding :=
      Data_encoding.conv Int64_map.(Map.S.bindings)
        (List.fold_left
          (fun (m_value : Int64_map.(Map.S.t) Key.(KEY.t)) ⇒
            fun (function_parameter : Int64.t × Key.(KEY.t)) ⇒
              let '(k_value, v_value) := function_parameter in
              Int64_map.(Map.S.add) k_value v_value m_value)
          Int64_map.(Map.S.empty)) None
        (Data_encoding.list_value None
          (Data_encoding.tup2 Data_encoding.int64_value Key.(KEY.encoding))) in
    Data_encoding.conv
      (fun (function_parameter : t) ⇒
        let '{|
          t.events := events;
            t.sequence := sequence_value;
            t.capacity := capacity;
            t.next_index := next_index;
            t.oldest_index := oldest_index;
            t.size := size_value
            |} := function_parameter in
        (events, sequence_value, capacity, next_index, oldest_index, size_value))
      (fun (function_parameter :
        Map.(Map.S.t) value × Int64_map.(Map.S.t) key × int64 × int64 × int64 ×
          int64) ⇒
        let
          '(events, sequence_value, capacity, next_index, oldest_index,
            size_value) := function_parameter in
        {| t.events := events; t.sequence := sequence_value;
          t.capacity := capacity; t.next_index := next_index;
          t.oldest_index := oldest_index; t.size := size_value; |}) None
      (Data_encoding.obj6 (Data_encoding.req None None "events" events_encoding)
        (Data_encoding.req None None "sequence" sequence_encoding)
        (Data_encoding.req None None "capacity" Data_encoding.int64_value)
        (Data_encoding.req None None "next_index" Data_encoding.int64_value)
        (Data_encoding.req None None "oldest_index" Data_encoding.int64_value)
        (Data_encoding.req None None "size" Data_encoding.int64_value)).

  Definition pp `{FArgs} (fmt : Format.formatter) (function_parameter : t)
    : unit :=
    let '{|
      t.events := events;
        t.sequence := sequence_value;
        t.capacity := capacity;
        t.next_index := next_index;
        t.oldest_index := oldest_index;
        t.size := size_value
        |} := function_parameter in
    (fun (bindings : list (Key.(KEY.t) × value)) ⇒
      (fun (sequence_bindings : list (Int64.t × key)) ⇒
        let pp_binding
          (fmt : Format.formatter)
          (function_parameter : Key.(KEY.t) × Value.(VALUE.t)) : unit :=
          let '(hash_value, history_proof) := function_parameter in
          Format.fprintf fmt
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.Formatting_gen
                (CamlinternalFormatBasics.Open_box
                  (CamlinternalFormatBasics.Format
                    CamlinternalFormatBasics.End_of_format ""))
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal " -> "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.Formatting_lit
                        (CamlinternalFormatBasics.Break "@;" 1 0)
                        (CamlinternalFormatBasics.Formatting_lit
                          CamlinternalFormatBasics.Close_box
                          CamlinternalFormatBasics.End_of_format))))))
              "@[%a -> %a@;@]") Key.(KEY.pp) hash_value Value.(VALUE.pp)
            history_proof in
        let pp_sequence_binding
          (fmt : Format.formatter) (function_parameter : int64 × Key.(KEY.t))
          : unit :=
          let '(counter, hash_value) := function_parameter in
          Format.fprintf fmt
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.Formatting_gen
                (CamlinternalFormatBasics.Open_box
                  (CamlinternalFormatBasics.Format
                    CamlinternalFormatBasics.End_of_format ""))
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.String_literal " -> "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.Formatting_lit
                        (CamlinternalFormatBasics.Break "@;" 1 0)
                        (CamlinternalFormatBasics.Formatting_lit
                          CamlinternalFormatBasics.Close_box
                          CamlinternalFormatBasics.End_of_format))))))
              "@[%s -> %a@;@]") (Int64.to_string counter) Key.(KEY.pp)
            hash_value in
        Format.fprintf fmt
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.Formatting_gen
              (CamlinternalFormatBasics.Open_box
                (CamlinternalFormatBasics.Format
                  (CamlinternalFormatBasics.String_literal "<hov 2>"
                    CamlinternalFormatBasics.End_of_format) "<hov 2>"))
              (CamlinternalFormatBasics.String_literal "History:"
                (CamlinternalFormatBasics.Formatting_lit
                  (CamlinternalFormatBasics.Break "@;" 1 0)
                  (CamlinternalFormatBasics.String_literal " { capacity: "
                    (CamlinternalFormatBasics.Int64
                      CamlinternalFormatBasics.Int_d
                      CamlinternalFormatBasics.No_padding
                      CamlinternalFormatBasics.No_precision
                      (CamlinternalFormatBasics.Char_literal ";" % char
                        (CamlinternalFormatBasics.Formatting_lit
                          (CamlinternalFormatBasics.Break "@;" 1 0)
                          (CamlinternalFormatBasics.String_literal
                            " current size: "
                            (CamlinternalFormatBasics.Int64
                              CamlinternalFormatBasics.Int_d
                              CamlinternalFormatBasics.No_padding
                              CamlinternalFormatBasics.No_precision
                              (CamlinternalFormatBasics.Char_literal ";" % char
                                (CamlinternalFormatBasics.Formatting_lit
                                  (CamlinternalFormatBasics.Break "@;" 1 0)
                                  (CamlinternalFormatBasics.String_literal
                                    " oldest index: "
                                    (CamlinternalFormatBasics.Int64
                                      CamlinternalFormatBasics.Int_d
                                      CamlinternalFormatBasics.No_padding
                                      CamlinternalFormatBasics.No_precision
                                      (CamlinternalFormatBasics.Char_literal
                                        ";" % char
                                        (CamlinternalFormatBasics.Formatting_lit
                                          (CamlinternalFormatBasics.Break "@;" 1
                                            0)
                                          (CamlinternalFormatBasics.String_literal
                                            " next_index : "
                                            (CamlinternalFormatBasics.Int64
                                              CamlinternalFormatBasics.Int_d
                                              CamlinternalFormatBasics.No_padding
                                              CamlinternalFormatBasics.No_precision
                                              (CamlinternalFormatBasics.Char_literal
                                                ";" % char
                                                (CamlinternalFormatBasics.Formatting_lit
                                                  (CamlinternalFormatBasics.Break
                                                    "@;" 1 0)
                                                  (CamlinternalFormatBasics.String_literal
                                                    " bindings: "
                                                    (CamlinternalFormatBasics.Alpha
                                                      (CamlinternalFormatBasics.Char_literal
                                                        ";" % char
                                                        (CamlinternalFormatBasics.Formatting_lit
                                                          (CamlinternalFormatBasics.Break
                                                            "@;" 1 0)
                                                          (CamlinternalFormatBasics.String_literal
                                                            " sequence: "
                                                            (CamlinternalFormatBasics.Alpha
                                                              (CamlinternalFormatBasics.String_literal
                                                                "; }"
                                                                (CamlinternalFormatBasics.Formatting_lit
                                                                  CamlinternalFormatBasics.Close_box
                                                                  CamlinternalFormatBasics.End_of_format)))))))))))))))))))))))))))
            "@[<hov 2>History:@; { capacity: %Ld;@; current size: %Ld;@; oldest index: %Ld;@; next_index : %Ld;@; bindings: %a;@; sequence: %a; }@]")
          capacity size_value oldest_index next_index
          (Format.pp_print_list None pp_binding) bindings
          (Format.pp_print_list None pp_sequence_binding) sequence_bindings)
        (Int64_map.(Map.S.bindings) sequence_value))
      (Map.(Map.S.bindings) events).

  Definition empty `{FArgs} (capacity : int64) : t :=
    let next_index := 0 in
    {| t.events := Map.(Map.S.empty); t.sequence := Int64_map.(Map.S.empty);
      t.capacity := capacity; t.next_index := next_index;
      t.oldest_index := next_index; t.size := 0; |}.

  Module Key_bound_to_different_value.
    Record record `{FArgs} : Set := Build {
      key : key;
      existing_value : value;
      given_value : value;
    }.
    Definition with_key `{FArgs} key (r : record) :=
      Build _ _ _ key r.(existing_value) r.(given_value).
    Definition with_existing_value `{FArgs} existing_value (r : record) :=
      Build _ _ _ r.(key) existing_value r.(given_value).
    Definition with_given_value `{FArgs} given_value (r : record) :=
      Build _ _ _ r.(key) r.(existing_value) given_value.
  End Key_bound_to_different_value.
  Definition Key_bound_to_different_value `{FArgs} :=
    Key_bound_to_different_value.record.

Init function; without side-effects in Coq
  Definition init_module_repr `{FArgs} : unit :=
    let '_ :=
      (* ❌ Assert instruction is not handled. *)
      assert unit (Pervasives.not (String.equal Name.(NAME.name) "")) in
    Error_monad.register_error_kind Error_monad.Temporary
      (Format.sprintf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "Bounded_history_repr."
            (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
              (CamlinternalFormatBasics.String_literal
                ".key_bound_to_different_value"
                CamlinternalFormatBasics.End_of_format)))
          "Bounded_history_repr.%s.key_bound_to_different_value")
        Name.(NAME.name))
      (Pervasives.op_caret Name.(NAME.name)
        ": Key already bound to a different value.")
      (Pervasives.op_caret Name.(NAME.name)
        (": Remember called with a key that is already bound to a different" ++
          String.String "010" " value.")) None
      (Data_encoding.obj3 (Data_encoding.req None None "key" Key.(KEY.encoding))
        (Data_encoding.req None None "existing_value" Value.(VALUE.encoding))
        (Data_encoding.req None None "given_value" Value.(VALUE.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Key_bound_to_different_value" then
            let '{|
              Key_bound_to_different_value.key := key_value;
                Key_bound_to_different_value.existing_value := existing_value;
                Key_bound_to_different_value.given_value := given_value
                |} := cast Key_bound_to_different_value payload in
            Some (key_value, existing_value, given_value)
          else None
        end)
      (fun (function_parameter : key × value × value) ⇒
        let '(key_value, existing_value, given_value) := function_parameter in
        Build_extensible "Key_bound_to_different_value"
          Key_bound_to_different_value
          {| Key_bound_to_different_value.key := key_value;
            Key_bound_to_different_value.existing_value := existing_value;
            Key_bound_to_different_value.given_value := given_value; |}).

  Definition remember `{FArgs}
    (key_value : Key.(KEY.t)) (value_value : value) (t_value : t) : M? t :=
    if t_value.(t.capacity) i64 0 then
      return? t_value
    else
      match
        ((Map.(Map.S.find) key_value t_value.(t.events)),
          match Map.(Map.S.find) key_value t_value.(t.events) with
          | Some value'
            Pervasives.not (Value.(VALUE.equal) value_value value')
          | _false
          end) with
      | (Some value', true)
        Error_monad.error_value
          (Build_extensible "Key_bound_to_different_value"
            Key_bound_to_different_value
            {| Key_bound_to_different_value.key := key_value;
              Key_bound_to_different_value.existing_value := value';
              Key_bound_to_different_value.given_value := value_value; |})
      | (_, _)
        let events := Map.(Map.S.add) key_value value_value t_value.(t.events)
          in
        let current_index := t_value.(t.next_index) in
        let next_index := Int64.succ current_index in
        let t_value :=
          {| t.events := events;
            t.sequence :=
              Int64_map.(Map.S.add) current_index key_value t_value.(t.sequence);
            t.capacity := t_value.(t.capacity); t.next_index := next_index;
            t.oldest_index := t_value.(t.oldest_index);
            t.size := Int64.succ t_value.(t.size); |} in
        if
          (t_value.(t.size) >i64 0) &&
          (t_value.(t.size) i64 t_value.(t.capacity))
        then
          return? t_value
        else
          let l_value := t_value.(t.oldest_index) in
          match Int64_map.(Map.S.find) l_value t_value.(t.sequence) with
          | None
            Error_monad.error_value (Build_extensible "Asserted" unit tt)
          | Some h_value
            let sequence_value :=
              Int64_map.(Map.S.remove) l_value t_value.(t.sequence) in
            let events := Map.(Map.S.remove) h_value events in
            return?
              {| t.events := events; t.sequence := sequence_value;
                t.capacity := t_value.(t.capacity);
                t.next_index := t_value.(t.next_index);
                t.oldest_index := Int64.succ t_value.(t.oldest_index);
                t.size := t_value.(t.capacity); |}
          end
      end.

  Definition find `{FArgs} (key_value : Key.(KEY.t)) (t_value : t)
    : option value := Map.(Map.S.find_opt) key_value t_value.(t.events).

  (* Make *)
  Definition functor `{FArgs} :=
    {|
      S.empty := empty;
      S.encoding := encoding;
      S.pp := pp;
      S.find := find;
      S.remember := remember
    |}.
End Make.
Definition Make {Key_t Value_t : Set}
  (Name : NAME) (Key : KEY (t := Key_t)) (Value : VALUE (t := Value_t))
  : S (t := _) (key := Key.(KEY.t)) (value := Value.(VALUE.t)) :=
  let '_ := Make.Build_FArgs Name Key Value in
  Make.functor.