1 /*
2 Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
3 Licensed under the Apache 2.0 License.
4 */
5
6
7 #ifndef __FStar_UInt_8_16_32_64_H
8 #define __FStar_UInt_8_16_32_64_H
9
10 #include <inttypes.h>
11 #include <stdbool.h>
12
13 #include "krml/lowstar_endianness.h"
14 #include "krml/types.h"
15 #include "krml/internal/target.h"
16
FStar_UInt64_eq_mask(uint64_t a,uint64_t b)17 static KRML_NOINLINE uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b)
18 {
19 uint64_t x = a ^ b;
20 uint64_t minus_x = ~x + 1ULL;
21 uint64_t x_or_minus_x = x | minus_x;
22 uint64_t xnx = x_or_minus_x >> 63U;
23 return xnx - 1ULL;
24 }
25
FStar_UInt64_gte_mask(uint64_t a,uint64_t b)26 static KRML_NOINLINE uint64_t FStar_UInt64_gte_mask(uint64_t a, uint64_t b)
27 {
28 uint64_t x = a;
29 uint64_t y = b;
30 uint64_t x_xor_y = x ^ y;
31 uint64_t x_sub_y = x - y;
32 uint64_t x_sub_y_xor_y = x_sub_y ^ y;
33 uint64_t q = x_xor_y | x_sub_y_xor_y;
34 uint64_t x_xor_q = x ^ q;
35 uint64_t x_xor_q_ = x_xor_q >> 63U;
36 return x_xor_q_ - 1ULL;
37 }
38
FStar_UInt32_eq_mask(uint32_t a,uint32_t b)39 static KRML_NOINLINE uint32_t FStar_UInt32_eq_mask(uint32_t a, uint32_t b)
40 {
41 uint32_t x = a ^ b;
42 uint32_t minus_x = ~x + 1U;
43 uint32_t x_or_minus_x = x | minus_x;
44 uint32_t xnx = x_or_minus_x >> 31U;
45 return xnx - 1U;
46 }
47
FStar_UInt32_gte_mask(uint32_t a,uint32_t b)48 static KRML_NOINLINE uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b)
49 {
50 uint32_t x = a;
51 uint32_t y = b;
52 uint32_t x_xor_y = x ^ y;
53 uint32_t x_sub_y = x - y;
54 uint32_t x_sub_y_xor_y = x_sub_y ^ y;
55 uint32_t q = x_xor_y | x_sub_y_xor_y;
56 uint32_t x_xor_q = x ^ q;
57 uint32_t x_xor_q_ = x_xor_q >> 31U;
58 return x_xor_q_ - 1U;
59 }
60
FStar_UInt16_eq_mask(uint16_t a,uint16_t b)61 static KRML_NOINLINE uint16_t FStar_UInt16_eq_mask(uint16_t a, uint16_t b)
62 {
63 uint16_t x = (uint32_t)a ^ (uint32_t)b;
64 uint16_t minus_x = (uint32_t)~x + 1U;
65 uint16_t x_or_minus_x = (uint32_t)x | (uint32_t)minus_x;
66 uint16_t xnx = (uint32_t)x_or_minus_x >> 15U;
67 return (uint32_t)xnx - 1U;
68 }
69
FStar_UInt16_gte_mask(uint16_t a,uint16_t b)70 static KRML_NOINLINE uint16_t FStar_UInt16_gte_mask(uint16_t a, uint16_t b)
71 {
72 uint16_t x = a;
73 uint16_t y = b;
74 uint16_t x_xor_y = (uint32_t)x ^ (uint32_t)y;
75 uint16_t x_sub_y = (uint32_t)x - (uint32_t)y;
76 uint16_t x_sub_y_xor_y = (uint32_t)x_sub_y ^ (uint32_t)y;
77 uint16_t q = (uint32_t)x_xor_y | (uint32_t)x_sub_y_xor_y;
78 uint16_t x_xor_q = (uint32_t)x ^ (uint32_t)q;
79 uint16_t x_xor_q_ = (uint32_t)x_xor_q >> 15U;
80 return (uint32_t)x_xor_q_ - 1U;
81 }
82
FStar_UInt8_eq_mask(uint8_t a,uint8_t b)83 static KRML_NOINLINE uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b)
84 {
85 uint8_t x = (uint32_t)a ^ (uint32_t)b;
86 uint8_t minus_x = (uint32_t)~x + 1U;
87 uint8_t x_or_minus_x = (uint32_t)x | (uint32_t)minus_x;
88 uint8_t xnx = (uint32_t)x_or_minus_x >> 7U;
89 return (uint32_t)xnx - 1U;
90 }
91
FStar_UInt8_gte_mask(uint8_t a,uint8_t b)92 static KRML_NOINLINE uint8_t FStar_UInt8_gte_mask(uint8_t a, uint8_t b)
93 {
94 uint8_t x = a;
95 uint8_t y = b;
96 uint8_t x_xor_y = (uint32_t)x ^ (uint32_t)y;
97 uint8_t x_sub_y = (uint32_t)x - (uint32_t)y;
98 uint8_t x_sub_y_xor_y = (uint32_t)x_sub_y ^ (uint32_t)y;
99 uint8_t q = (uint32_t)x_xor_y | (uint32_t)x_sub_y_xor_y;
100 uint8_t x_xor_q = (uint32_t)x ^ (uint32_t)q;
101 uint8_t x_xor_q_ = (uint32_t)x_xor_q >> 7U;
102 return (uint32_t)x_xor_q_ - 1U;
103 }
104
105
106 #define __FStar_UInt_8_16_32_64_H_DEFINED
107 #endif
108