Skip to content
Snippets Groups Projects
Script_bytes.v 996 B
Newer Older
Guillaume Claret's avatar
Guillaume Claret committed
(** 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.