1 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
2 Licensed under the Apache 2.0 License. */
3
4 /* This file was generated by KreMLin <https://github.com/FStarLang/kremlin>
5 * KreMLin invocation: ../krml -fc89 -fparentheses -fno-shadow -header /mnt/e/everest/verify/hdrB9w -minimal -fparentheses -fcurly-braces -fno-shadow -header copyright-header.txt -minimal -tmpdir dist/minimal -skip-compilation -extract-uints -add-include <inttypes.h> -add-include <stdbool.h> -add-include "kremlin/internal/compat.h" -add-include "kremlin/internal/types.h" -bundle FStar.UInt64+FStar.UInt32+FStar.UInt16+FStar.UInt8=* extracted/prims.krml extracted/FStar_Pervasives_Native.krml extracted/FStar_Pervasives.krml extracted/FStar_Mul.krml extracted/FStar_Squash.krml extracted/FStar_Classical.krml extracted/FStar_StrongExcludedMiddle.krml extracted/FStar_FunctionalExtensionality.krml extracted/FStar_List_Tot_Base.krml extracted/FStar_List_Tot_Properties.krml extracted/FStar_List_Tot.krml extracted/FStar_Seq_Base.krml extracted/FStar_Seq_Properties.krml extracted/FStar_Seq.krml extracted/FStar_Math_Lib.krml extracted/FStar_Math_Lemmas.krml extracted/FStar_BitVector.krml extracted/FStar_UInt.krml extracted/FStar_UInt32.krml extracted/FStar_Int.krml extracted/FStar_Int16.krml extracted/FStar_Preorder.krml extracted/FStar_Ghost.krml extracted/FStar_ErasedLogic.krml extracted/FStar_UInt64.krml extracted/FStar_Set.krml extracted/FStar_PropositionalExtensionality.krml extracted/FStar_PredicateExtensionality.krml extracted/FStar_TSet.krml extracted/FStar_Monotonic_Heap.krml extracted/FStar_Heap.krml extracted/FStar_Map.krml extracted/FStar_Monotonic_HyperHeap.krml extracted/FStar_Monotonic_HyperStack.krml extracted/FStar_HyperStack.krml extracted/FStar_Monotonic_Witnessed.krml extracted/FStar_HyperStack_ST.krml extracted/FStar_HyperStack_All.krml extracted/FStar_Date.krml extracted/FStar_Universe.krml extracted/FStar_GSet.krml extracted/FStar_ModifiesGen.krml extracted/LowStar_Monotonic_Buffer.krml extracted/LowStar_Buffer.krml extracted/Spec_Loops.krml extracted/LowStar_BufferOps.krml extracted/C_Loops.krml extracted/FStar_UInt8.krml extracted/FStar_Kremlin_Endianness.krml extracted/FStar_UInt63.krml extracted/FStar_Exn.krml extracted/FStar_ST.krml extracted/FStar_All.krml extracted/FStar_Dyn.krml extracted/FStar_Int63.krml extracted/FStar_Int64.krml extracted/FStar_Int32.krml extracted/FStar_Int8.krml extracted/FStar_UInt16.krml extracted/FStar_Int_Cast.krml extracted/FStar_UInt128.krml extracted/C_Endianness.krml extracted/FStar_List.krml extracted/FStar_Float.krml extracted/FStar_IO.krml extracted/C.krml extracted/FStar_Char.krml extracted/FStar_String.krml extracted/LowStar_Modifies.krml extracted/C_String.krml extracted/FStar_Bytes.krml extracted/FStar_HyperStack_IO.krml extracted/C_Failure.krml extracted/TestLib.krml extracted/FStar_Int_Cast_Full.krml
6 * F* version: 059db0c8
7 * KreMLin version: 916c37ac
8 */
9
10
11 #include "FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8.h"
12
FStar_UInt64_eq_mask(uint64_t a,uint64_t b)13 uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b)
14 {
15 uint64_t x = a ^ b;
16 uint64_t minus_x = ~x + (uint64_t)1U;
17 uint64_t x_or_minus_x = x | minus_x;
18 uint64_t xnx = x_or_minus_x >> (uint32_t)63U;
19 return xnx - (uint64_t)1U;
20 }
21
FStar_UInt64_gte_mask(uint64_t a,uint64_t b)22 uint64_t FStar_UInt64_gte_mask(uint64_t a, uint64_t b)
23 {
24 uint64_t x = a;
25 uint64_t y = b;
26 uint64_t x_xor_y = x ^ y;
27 uint64_t x_sub_y = x - y;
28 uint64_t x_sub_y_xor_y = x_sub_y ^ y;
29 uint64_t q = x_xor_y | x_sub_y_xor_y;
30 uint64_t x_xor_q = x ^ q;
31 uint64_t x_xor_q_ = x_xor_q >> (uint32_t)63U;
32 return x_xor_q_ - (uint64_t)1U;
33 }
34
FStar_UInt32_eq_mask(uint32_t a,uint32_t b)35 uint32_t FStar_UInt32_eq_mask(uint32_t a, uint32_t b)
36 {
37 uint32_t x = a ^ b;
38 uint32_t minus_x = ~x + (uint32_t)1U;
39 uint32_t x_or_minus_x = x | minus_x;
40 uint32_t xnx = x_or_minus_x >> (uint32_t)31U;
41 return xnx - (uint32_t)1U;
42 }
43
FStar_UInt32_gte_mask(uint32_t a,uint32_t b)44 uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b)
45 {
46 uint32_t x = a;
47 uint32_t y = b;
48 uint32_t x_xor_y = x ^ y;
49 uint32_t x_sub_y = x - y;
50 uint32_t x_sub_y_xor_y = x_sub_y ^ y;
51 uint32_t q = x_xor_y | x_sub_y_xor_y;
52 uint32_t x_xor_q = x ^ q;
53 uint32_t x_xor_q_ = x_xor_q >> (uint32_t)31U;
54 return x_xor_q_ - (uint32_t)1U;
55 }
56
FStar_UInt16_eq_mask(uint16_t a,uint16_t b)57 uint16_t FStar_UInt16_eq_mask(uint16_t a, uint16_t b)
58 {
59 uint16_t x = a ^ b;
60 uint16_t minus_x = ~x + (uint16_t)1U;
61 uint16_t x_or_minus_x = x | minus_x;
62 uint16_t xnx = x_or_minus_x >> (uint32_t)15U;
63 return xnx - (uint16_t)1U;
64 }
65
FStar_UInt16_gte_mask(uint16_t a,uint16_t b)66 uint16_t FStar_UInt16_gte_mask(uint16_t a, uint16_t b)
67 {
68 uint16_t x = a;
69 uint16_t y = b;
70 uint16_t x_xor_y = x ^ y;
71 uint16_t x_sub_y = x - y;
72 uint16_t x_sub_y_xor_y = x_sub_y ^ y;
73 uint16_t q = x_xor_y | x_sub_y_xor_y;
74 uint16_t x_xor_q = x ^ q;
75 uint16_t x_xor_q_ = x_xor_q >> (uint32_t)15U;
76 return x_xor_q_ - (uint16_t)1U;
77 }
78
FStar_UInt8_eq_mask(uint8_t a,uint8_t b)79 uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b)
80 {
81 uint8_t x = a ^ b;
82 uint8_t minus_x = ~x + (uint8_t)1U;
83 uint8_t x_or_minus_x = x | minus_x;
84 uint8_t xnx = x_or_minus_x >> (uint32_t)7U;
85 return xnx - (uint8_t)1U;
86 }
87
FStar_UInt8_gte_mask(uint8_t a,uint8_t b)88 uint8_t FStar_UInt8_gte_mask(uint8_t a, uint8_t b)
89 {
90 uint8_t x = a;
91 uint8_t y = b;
92 uint8_t x_xor_y = x ^ y;
93 uint8_t x_sub_y = x - y;
94 uint8_t x_sub_y_xor_y = x_sub_y ^ y;
95 uint8_t q = x_xor_y | x_sub_y_xor_y;
96 uint8_t x_xor_q = x ^ q;
97 uint8_t x_xor_q_ = x_xor_q >> (uint32_t)7U;
98 return x_xor_q_ - (uint8_t)1U;
99 }
100
101