🍬 Script_bytes.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_int.

Definition bytes_and : bytes → bytes → bytes := Bytes.logand.

Definition bytes_or : bytes → bytes → bytes := Bytes.logor.

Definition bytes_xor : bytes → bytes → bytes := Bytes.logxor.

Definition bytes_not : bytes → bytes := Bytes.lognot.

Definition bytes_lsl (a_value : bytes) (n_value : Script_int.num)
  : option bytes :=
  match
    ((Script_int.to_int n_value),
      match Script_int.to_int n_value with
      | Some n_value ⇒ n_value ≤i 64000
      | _ ⇒ false
      end) with
  | (Some n_value, true) ⇒ Some (Bytes.shift_left a_value n_value)
  | (_, _) ⇒ None
  end.

Definition bytes_lsr (a_value : bytes) (n_value : Script_int.num) : bytes :=
  match Script_int.to_int n_value with
  | None ⇒ Bytes.empty
  | Some n_value ⇒ Bytes.shift_right a_value n_value
  end.