summaryrefslogtreecommitdiffstats
path: root/security/nss/lib/freebl/verified/FStar.h
diff options
context:
space:
mode:
authorwolfbeast <mcwerewolf@gmail.com>2018-02-23 11:04:39 +0100
committerwolfbeast <mcwerewolf@gmail.com>2018-02-23 11:04:39 +0100
commitf1a0f0a56fdd0fc39f255174ce08c06b91c66c94 (patch)
tree99ccc8e212257e1da1902036ae261e8e55d55c1c /security/nss/lib/freebl/verified/FStar.h
parent8781f745556be5d7402d0f3adc67ecfe32fe04a0 (diff)
downloadUXP-f1a0f0a56fdd0fc39f255174ce08c06b91c66c94.tar
UXP-f1a0f0a56fdd0fc39f255174ce08c06b91c66c94.tar.gz
UXP-f1a0f0a56fdd0fc39f255174ce08c06b91c66c94.tar.lz
UXP-f1a0f0a56fdd0fc39f255174ce08c06b91c66c94.tar.xz
UXP-f1a0f0a56fdd0fc39f255174ce08c06b91c66c94.zip
Update NSS to 3.35-RTM
Diffstat (limited to 'security/nss/lib/freebl/verified/FStar.h')
-rw-r--r--security/nss/lib/freebl/verified/FStar.h69
1 files changed, 69 insertions, 0 deletions
diff --git a/security/nss/lib/freebl/verified/FStar.h b/security/nss/lib/freebl/verified/FStar.h
new file mode 100644
index 000000000..7b105b8f2
--- /dev/null
+++ b/security/nss/lib/freebl/verified/FStar.h
@@ -0,0 +1,69 @@
+/* Copyright 2016-2017 INRIA and Microsoft Corporation
+ *
+ * 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.
+ */
+
+/* This file was auto-generated by KreMLin! */
+#ifndef __FStar_H
+#define __FStar_H
+
+#include "kremlib_base.h"
+
+typedef struct
+{
+ uint64_t low;
+ uint64_t high;
+} FStar_UInt128_uint128;
+
+typedef FStar_UInt128_uint128 FStar_UInt128_t;
+
+extern void FStar_UInt128_constant_time_carry_ok(uint64_t x0, uint64_t x1);
+
+FStar_UInt128_uint128 FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_add_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_sub_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_logand(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_logxor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_logor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_lognot(FStar_UInt128_uint128 a);
+
+FStar_UInt128_uint128 FStar_UInt128_shift_left(FStar_UInt128_uint128 a, uint32_t s);
+
+FStar_UInt128_uint128 FStar_UInt128_shift_right(FStar_UInt128_uint128 a, uint32_t s);
+
+FStar_UInt128_uint128 FStar_UInt128_eq_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_gte_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t a);
+
+uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a);
+
+typedef struct
+{
+ uint64_t fst;
+ uint64_t snd;
+ uint64_t thd;
+ uint64_t f3;
+} K___uint64_t_uint64_t_uint64_t_uint64_t;
+
+FStar_UInt128_uint128 FStar_UInt128_mul_wide(uint64_t x, uint64_t y);
+#endif