val gt (a b: t) : Tot bool
let gt (a:t) (b:t) : Tot bool = gt #n (v a) (v b)
val gt (a b: t) : Tot bool
let gt (a b: t) : Tot bool =
gt #n (v a) (v b)
FStar.UInt8.fsti.checked
prims.fst.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
FStar.UInt8.fsti
FStar.UInt8.t FStar.UInt.gt FStar.UInt8.n FStar.UInt8.v Prims.bool
(*
   Copyright 2008-2019 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.UInt8

(**** THIS MODULE IS GENERATED AUTOMATICALLY USING [mk_int.sh], DO NOT EDIT DIRECTLY ****)

unfold let n = 8

/// For FStar.UIntN.fstp: anything that you fix/update here should be
/// reflected in [FStar.IntN.fstp], which is mostly a copy-paste of
/// this module.
///
/// Except, as compared to [FStar.IntN.fstp], here:
///  - every occurrence of [int_t] has been replaced with [uint_t]
///  - every occurrence of [@%] has been replaced with [%].
///  - some functions (e.g., add_underspec, etc.) are only defined here, not on signed integers

/// This module provides an abstract type for machine integers of a
/// given signedness and width. The interface is designed to be safe
/// with respect to arithmetic underflow and overflow.

/// Note, we have attempted several times to re-design this module to
/// make it more amenable to normalization and to impose less overhead
/// on the SMT solver when reasoning about machine integer
/// arithmetic. The following github issue reports on the current
/// status of that work.
///
/// https://github.com/FStarLang/FStar/issues/1757

open FStar.UInt
open FStar.Mul

#set-options "--max_fuel 0 --max_ifuel 0"

(** Abstract type of machine integers, with an underlying
    representation using a bounded mathematical integer *)
new val t : eqtype

(** A coercion that projects a bounded mathematical integer from a
    machine integer *)
val v (x:t) : Tot (uint_t n)

(** A coercion that injects a bounded mathematical integers into a
    machine integer *)
val uint_to_t (x:uint_t n) : Pure t
  (requires True)
  (ensures (fun y -> v y = x))

(** Injection/projection inverse *)
val uv_inv (x : t) : Lemma
  (ensures (uint_to_t (v x) == x))
  [SMTPat (v x)]

(** Projection/injection inverse *)
val vu_inv (x : uint_t n) : Lemma
  (ensures (v (uint_to_t x) == x))
  [SMTPat (uint_to_t x)]

(** An alternate form of the injectivity of the [v] projection *)
val v_inj (x1 x2: t): Lemma
  (requires (v x1 == v x2))
  (ensures (x1 == x2))

(** Constants 0 and 1 *)
val zero : x:t{v x = 0}

val one : x:t{v x = 1}

(**** Addition primitives *)

(** Bounds-respecting addition

    The precondition enforces that the sum does not overflow,
    expressing the bound as an addition on mathematical integers *)
val add (a:t) (b:t) : Pure t
  (requires (size (v a + v b) n))
  (ensures (fun c -> v a + v b = v c))

(** Underspecified, possibly overflowing addition:

    The postcondition only enures that the result is the sum of the
    arguments in case there is no overflow *)
val add_underspec (a:t) (b:t) : Pure t
  (requires True)
  (ensures (fun c ->
    size (v a + v b) n ==> v a + v b = v c))

(** Addition modulo [2^n]

    Machine integers can always be added, but the postcondition is now
    in terms of addition modulo [2^n] on mathematical integers *)
val add_mod (a:t) (b:t) : Pure t
  (requires True)
  (ensures (fun c -> FStar.UInt.add_mod (v a) (v b) = v c))

(**** Subtraction primitives *)


(** Bounds-respecting subtraction

    The precondition enforces that the difference does not underflow,
    expressing the bound as a difference on mathematical integers *)
val sub (a:t) (b:t) : Pure t
  (requires (size (v a - v b) n))
  (ensures (fun c -> v a - v b = v c))

(** Underspecified, possibly overflowing subtraction:

    The postcondition only enures that the result is the difference of
    the arguments in case there is no underflow *)
val sub_underspec (a:t) (b:t) : Pure t
  (requires True)
  (ensures (fun c ->
    size (v a - v b) n ==> v a - v b = v c))

(** Subtraction modulo [2^n]

    Machine integers can always be subtractd, but the postcondition is
    now in terms of subtraction modulo [2^n] on mathematical integers *)
val sub_mod (a:t) (b:t) : Pure t
  (requires True)
  (ensures (fun c -> FStar.UInt.sub_mod (v a) (v b) = v c))

(**** Multiplication primitives *)


(** Bounds-respecting multiplication

    The precondition enforces that the product does not overflow,
    expressing the bound as a product on mathematical integers *)
val mul (a:t) (b:t) : Pure t
  (requires (size (v a * v b) n))
  (ensures (fun c -> v a * v b = v c))

(** Underspecified, possibly overflowing product

    The postcondition only enures that the result is the product of
    the arguments in case there is no overflow *)
val mul_underspec (a:t) (b:t) : Pure t
  (requires True)
  (ensures (fun c ->
    size (v a * v b) n ==> v a * v b = v c))

(** Multiplication modulo [2^n]

    Machine integers can always be multiplied, but the postcondition
    is now in terms of product modulo [2^n] on mathematical integers *)
val mul_mod (a:t) (b:t) : Pure t
  (requires True)
  (ensures (fun c -> FStar.UInt.mul_mod (v a) (v b) = v c))

(**** Division primitives *)

(** Euclidean division of [a] and [b], with [b] non-zero *)
val div (a:t) (b:t{v b <> 0}) : Pure t
  (requires (True))
  (ensures (fun c -> v a / v b = v c))

(**** Modulo primitives *)

(** Euclidean remainder

    The result is the modulus of [a] with respect to a non-zero [b] *)
val rem (a:t) (b:t{v b <> 0}) : Pure t
  (requires True)
  (ensures (fun c -> FStar.UInt.mod (v a) (v b) = v c))

(**** Bitwise operators *)

/// Also see FStar.BV

(** Bitwise logical conjunction *)
val logand (x:t) (y:t) : Pure t
  (requires True)
  (ensures (fun z -> v x `logand` v y = v z))

(** Bitwise logical exclusive-or *)
val logxor (x:t) (y:t) : Pure t
  (requires True)
  (ensures (fun z -> v x `logxor` v y == v z))

(** Bitwise logical disjunction *)
val logor (x:t) (y:t) : Pure t
  (requires True)
  (ensures (fun z -> v x `logor` v y == v z))

(** Bitwise logical negation *)
val lognot (x:t) : Pure t
  (requires True)
  (ensures (fun z -> lognot (v x) == v z))

(**** Shift operators *)

(** Shift right with zero fill, shifting at most the integer width *)
val shift_right (a:t) (s:UInt32.t) : Pure t
  (requires (UInt32.v s < n))
  (ensures (fun c -> FStar.UInt.shift_right (v a) (UInt32.v s) = v c))

(** Shift left with zero fill, shifting at most the integer width *)
val shift_left (a:t) (s:UInt32.t) : Pure t
  (requires (UInt32.v s < n))
  (ensures (fun c -> FStar.UInt.shift_left (v a) (UInt32.v s) = v c))

(**** Comparison operators *)

(** Equality

    Note, it is safe to also use the polymorphic decidable equality
    operator [=] *)
let eq (a:t) (b:t) : Tot bool = eq #n (v a) (v b)
val gt (a b: t) : Tot bool
a: FStar.UInt8.t -> b: FStar.UInt8.t -> Prims.bool