➗ Ratio_repr.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Ratio_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.

Validity predicate for [t].

Module Valid.
  Import Ratio_repr.t.

  Record t (x : Ratio_repr.t) : Prop := {
    numerator : Pervasives.UInt16.Valid.t x.(numerator);
    denominator :
      Pervasives.UInt16.Valid.t x.(denominator) ∧
      x.(denominator) ≠ 0;
  }.
End Valid.

The encoding [encoding] is valid.

Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Ratio_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  sauto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Module In_zero_one.
  Import Ratio_repr.t.

Condition for a ratio to be between 0 and 1.

  Definition t (x : Ratio_repr.t) : Prop :=
    x.(numerator) ≤ x.(denominator).
  #[global] Hint Unfold t : tezos_z.
End In_zero_one.