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 12 #ifndef __FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8_H 13 #define __FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8_H 14 15 16 #include <inttypes.h> 17 #include <stdbool.h> 18 #include "kremlin/internal/compat.h" 19 #include "kremlin/internal/types.h" 20 21 extern Prims_int FStar_UInt64_n; 22 23 extern Prims_int FStar_UInt64_v(uint64_t x0); 24 25 extern uint64_t FStar_UInt64_uint_to_t(Prims_int x0); 26 27 extern uint64_t FStar_UInt64_add(uint64_t x0, uint64_t x1); 28 29 extern uint64_t FStar_UInt64_add_underspec(uint64_t x0, uint64_t x1); 30 31 extern uint64_t FStar_UInt64_add_mod(uint64_t x0, uint64_t x1); 32 33 extern uint64_t FStar_UInt64_sub(uint64_t x0, uint64_t x1); 34 35 extern uint64_t FStar_UInt64_sub_underspec(uint64_t x0, uint64_t x1); 36 37 extern uint64_t FStar_UInt64_sub_mod(uint64_t x0, uint64_t x1); 38 39 extern uint64_t FStar_UInt64_mul(uint64_t x0, uint64_t x1); 40 41 extern uint64_t FStar_UInt64_mul_underspec(uint64_t x0, uint64_t x1); 42 43 extern uint64_t FStar_UInt64_mul_mod(uint64_t x0, uint64_t x1); 44 45 extern uint64_t FStar_UInt64_mul_div(uint64_t x0, uint64_t x1); 46 47 extern uint64_t FStar_UInt64_div(uint64_t x0, uint64_t x1); 48 49 extern uint64_t FStar_UInt64_rem(uint64_t x0, uint64_t x1); 50 51 extern uint64_t FStar_UInt64_logand(uint64_t x0, uint64_t x1); 52 53 extern uint64_t FStar_UInt64_logxor(uint64_t x0, uint64_t x1); 54 55 extern uint64_t FStar_UInt64_logor(uint64_t x0, uint64_t x1); 56 57 extern uint64_t FStar_UInt64_lognot(uint64_t x0); 58 59 extern uint64_t FStar_UInt64_shift_right(uint64_t x0, uint32_t x1); 60 61 extern uint64_t FStar_UInt64_shift_left(uint64_t x0, uint32_t x1); 62 63 extern bool FStar_UInt64_eq(uint64_t x0, uint64_t x1); 64 65 extern bool FStar_UInt64_gt(uint64_t x0, uint64_t x1); 66 67 extern bool FStar_UInt64_gte(uint64_t x0, uint64_t x1); 68 69 extern bool FStar_UInt64_lt(uint64_t x0, uint64_t x1); 70 71 extern bool FStar_UInt64_lte(uint64_t x0, uint64_t x1); 72 73 extern uint64_t FStar_UInt64_minus(uint64_t x0); 74 75 extern uint32_t FStar_UInt64_n_minus_one; 76 77 uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b); 78 79 uint64_t FStar_UInt64_gte_mask(uint64_t a, uint64_t b); 80 81 extern Prims_string FStar_UInt64_to_string(uint64_t x0); 82 83 extern uint64_t FStar_UInt64_of_string(Prims_string x0); 84 85 extern Prims_int FStar_UInt32_n; 86 87 extern Prims_int FStar_UInt32_v(uint32_t x0); 88 89 extern uint32_t FStar_UInt32_uint_to_t(Prims_int x0); 90 91 extern uint32_t FStar_UInt32_add(uint32_t x0, uint32_t x1); 92 93 extern uint32_t FStar_UInt32_add_underspec(uint32_t x0, uint32_t x1); 94 95 extern uint32_t FStar_UInt32_add_mod(uint32_t x0, uint32_t x1); 96 97 extern uint32_t FStar_UInt32_sub(uint32_t x0, uint32_t x1); 98 99 extern uint32_t FStar_UInt32_sub_underspec(uint32_t x0, uint32_t x1); 100 101 extern uint32_t FStar_UInt32_sub_mod(uint32_t x0, uint32_t x1); 102 103 extern uint32_t FStar_UInt32_mul(uint32_t x0, uint32_t x1); 104 105 extern uint32_t FStar_UInt32_mul_underspec(uint32_t x0, uint32_t x1); 106 107 extern uint32_t FStar_UInt32_mul_mod(uint32_t x0, uint32_t x1); 108 109 extern uint32_t FStar_UInt32_mul_div(uint32_t x0, uint32_t x1); 110 111 extern uint32_t FStar_UInt32_div(uint32_t x0, uint32_t x1); 112 113 extern uint32_t FStar_UInt32_rem(uint32_t x0, uint32_t x1); 114 115 extern uint32_t FStar_UInt32_logand(uint32_t x0, uint32_t x1); 116 117 extern uint32_t FStar_UInt32_logxor(uint32_t x0, uint32_t x1); 118 119 extern uint32_t FStar_UInt32_logor(uint32_t x0, uint32_t x1); 120 121 extern uint32_t FStar_UInt32_lognot(uint32_t x0); 122 123 extern uint32_t FStar_UInt32_shift_right(uint32_t x0, uint32_t x1); 124 125 extern uint32_t FStar_UInt32_shift_left(uint32_t x0, uint32_t x1); 126 127 extern bool FStar_UInt32_eq(uint32_t x0, uint32_t x1); 128 129 extern bool FStar_UInt32_gt(uint32_t x0, uint32_t x1); 130 131 extern bool FStar_UInt32_gte(uint32_t x0, uint32_t x1); 132 133 extern bool FStar_UInt32_lt(uint32_t x0, uint32_t x1); 134 135 extern bool FStar_UInt32_lte(uint32_t x0, uint32_t x1); 136 137 extern uint32_t FStar_UInt32_minus(uint32_t x0); 138 139 extern uint32_t FStar_UInt32_n_minus_one; 140 141 uint32_t FStar_UInt32_eq_mask(uint32_t a, uint32_t b); 142 143 uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b); 144 145 extern Prims_string FStar_UInt32_to_string(uint32_t x0); 146 147 extern uint32_t FStar_UInt32_of_string(Prims_string x0); 148 149 extern Prims_int FStar_UInt16_n; 150 151 extern Prims_int FStar_UInt16_v(uint16_t x0); 152 153 extern uint16_t FStar_UInt16_uint_to_t(Prims_int x0); 154 155 extern uint16_t FStar_UInt16_add(uint16_t x0, uint16_t x1); 156 157 extern uint16_t FStar_UInt16_add_underspec(uint16_t x0, uint16_t x1); 158 159 extern uint16_t FStar_UInt16_add_mod(uint16_t x0, uint16_t x1); 160 161 extern uint16_t FStar_UInt16_sub(uint16_t x0, uint16_t x1); 162 163 extern uint16_t FStar_UInt16_sub_underspec(uint16_t x0, uint16_t x1); 164 165 extern uint16_t FStar_UInt16_sub_mod(uint16_t x0, uint16_t x1); 166 167 extern uint16_t FStar_UInt16_mul(uint16_t x0, uint16_t x1); 168 169 extern uint16_t FStar_UInt16_mul_underspec(uint16_t x0, uint16_t x1); 170 171 extern uint16_t FStar_UInt16_mul_mod(uint16_t x0, uint16_t x1); 172 173 extern uint16_t FStar_UInt16_mul_div(uint16_t x0, uint16_t x1); 174 175 extern uint16_t FStar_UInt16_div(uint16_t x0, uint16_t x1); 176 177 extern uint16_t FStar_UInt16_rem(uint16_t x0, uint16_t x1); 178 179 extern uint16_t FStar_UInt16_logand(uint16_t x0, uint16_t x1); 180 181 extern uint16_t FStar_UInt16_logxor(uint16_t x0, uint16_t x1); 182 183 extern uint16_t FStar_UInt16_logor(uint16_t x0, uint16_t x1); 184 185 extern uint16_t FStar_UInt16_lognot(uint16_t x0); 186 187 extern uint16_t FStar_UInt16_shift_right(uint16_t x0, uint32_t x1); 188 189 extern uint16_t FStar_UInt16_shift_left(uint16_t x0, uint32_t x1); 190 191 extern bool FStar_UInt16_eq(uint16_t x0, uint16_t x1); 192 193 extern bool FStar_UInt16_gt(uint16_t x0, uint16_t x1); 194 195 extern bool FStar_UInt16_gte(uint16_t x0, uint16_t x1); 196 197 extern bool FStar_UInt16_lt(uint16_t x0, uint16_t x1); 198 199 extern bool FStar_UInt16_lte(uint16_t x0, uint16_t x1); 200 201 extern uint16_t FStar_UInt16_minus(uint16_t x0); 202 203 extern uint32_t FStar_UInt16_n_minus_one; 204 205 uint16_t FStar_UInt16_eq_mask(uint16_t a, uint16_t b); 206 207 uint16_t FStar_UInt16_gte_mask(uint16_t a, uint16_t b); 208 209 extern Prims_string FStar_UInt16_to_string(uint16_t x0); 210 211 extern uint16_t FStar_UInt16_of_string(Prims_string x0); 212 213 extern Prims_int FStar_UInt8_n; 214 215 extern Prims_int FStar_UInt8_v(uint8_t x0); 216 217 extern uint8_t FStar_UInt8_uint_to_t(Prims_int x0); 218 219 extern uint8_t FStar_UInt8_add(uint8_t x0, uint8_t x1); 220 221 extern uint8_t FStar_UInt8_add_underspec(uint8_t x0, uint8_t x1); 222 223 extern uint8_t FStar_UInt8_add_mod(uint8_t x0, uint8_t x1); 224 225 extern uint8_t FStar_UInt8_sub(uint8_t x0, uint8_t x1); 226 227 extern uint8_t FStar_UInt8_sub_underspec(uint8_t x0, uint8_t x1); 228 229 extern uint8_t FStar_UInt8_sub_mod(uint8_t x0, uint8_t x1); 230 231 extern uint8_t FStar_UInt8_mul(uint8_t x0, uint8_t x1); 232 233 extern uint8_t FStar_UInt8_mul_underspec(uint8_t x0, uint8_t x1); 234 235 extern uint8_t FStar_UInt8_mul_mod(uint8_t x0, uint8_t x1); 236 237 extern uint8_t FStar_UInt8_mul_div(uint8_t x0, uint8_t x1); 238 239 extern uint8_t FStar_UInt8_div(uint8_t x0, uint8_t x1); 240 241 extern uint8_t FStar_UInt8_rem(uint8_t x0, uint8_t x1); 242 243 extern uint8_t FStar_UInt8_logand(uint8_t x0, uint8_t x1); 244 245 extern uint8_t FStar_UInt8_logxor(uint8_t x0, uint8_t x1); 246 247 extern uint8_t FStar_UInt8_logor(uint8_t x0, uint8_t x1); 248 249 extern uint8_t FStar_UInt8_lognot(uint8_t x0); 250 251 extern uint8_t FStar_UInt8_shift_right(uint8_t x0, uint32_t x1); 252 253 extern uint8_t FStar_UInt8_shift_left(uint8_t x0, uint32_t x1); 254 255 extern bool FStar_UInt8_eq(uint8_t x0, uint8_t x1); 256 257 extern bool FStar_UInt8_gt(uint8_t x0, uint8_t x1); 258 259 extern bool FStar_UInt8_gte(uint8_t x0, uint8_t x1); 260 261 extern bool FStar_UInt8_lt(uint8_t x0, uint8_t x1); 262 263 extern bool FStar_UInt8_lte(uint8_t x0, uint8_t x1); 264 265 extern uint8_t FStar_UInt8_minus(uint8_t x0); 266 267 extern uint32_t FStar_UInt8_n_minus_one; 268 269 uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b); 270 271 uint8_t FStar_UInt8_gte_mask(uint8_t a, uint8_t b); 272 273 extern Prims_string FStar_UInt8_to_string(uint8_t x0); 274 275 extern uint8_t FStar_UInt8_of_string(Prims_string x0); 276 277 typedef uint8_t FStar_UInt8_byte; 278 279 #define __FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8_H_DEFINED 280 #endif 281
