Add version 0.1.

generated-src/lib/uint64gmp.h

+#include <stdlib.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <assert.h>
+#include <alloca.h>
+
+typedef unsigned __int128 uint128_t;
+
+struct __mul64_double_result
+{ uint64_t __field_0;
+  uint64_t __field_1;
+};
+
+static inline struct __mul64_double_result mul64_double(uint64_t x, uint64_t y)
+{
+  uint128_t z = (uint128_t)x * (uint128_t)y;
+  struct __mul64_double_result result = { z, z >> 64 };
+  return result;
+}
+
+static inline uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
+{
+  return (((uint128_t)uh << 64) | ul) / d;
+}
+
+
+struct __add64_with_carry_result
+{ uint64_t __field_0;
+  uint64_t __field_1;
+};
+
+static inline struct __add64_with_carry_result
+add64_with_carry(uint64_t x, uint64_t y, uint64_t c)
+{
+  struct __add64_with_carry_result result;
+  uint64_t r = x + y + c;
+  result.__field_0 = r;
+  if (r == x) result.__field_1 = c;
+  else result.__field_1 = (r < x);
+  return result;
+}
+
+struct __sub64_with_borrow_result
+{ uint64_t __field_0;
+  uint64_t __field_1;
+};
+
+static inline struct __sub64_with_borrow_result
+sub64_with_borrow(uint64_t x, uint64_t y, uint64_t b)
+{
+  struct __sub64_with_borrow_result result;
+  uint64_t r = x - y - b;
+  result.__field_0 = r;
+  if (r > x) result.__field_1 = 1;
+  else if (r == x) result.__field_1 = b;
+  else result.__field_1 = 0;
+  return result;
+}
+
+struct __add64_3_result
+{ uint64_t __field_0;
+  uint64_t __field_1;
+};
+
+static inline struct __add64_3_result add64_3(uint64_t x, uint64_t y, uint64_t z)
+{
+  struct __add64_3_result result;
+  uint64_t r, c1, c2;
+  r = x + y;
+  c1 = r < y;
+  r += z;
+  c2 = r < z;
+  result.__field_1 = c1 + c2;
+  result.__field_0 = r;
+  return result;
+}
+
+struct __lsld64_result
+{ uint64_t __field_0;
+  uint64_t __field_1;
+};
+
+static inline struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
+{
+  struct __lsld64_result result;
+  result.__field_1 = x >> (64 - cnt);
+  result.__field_0 = x << cnt;
+  return result;
+}
+
+

generated-src/lib/util.c

+#include <stdlib.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <assert.h>
+#include <alloca.h>
+#include "int.h"
+
+#include "int32.h"
+
+#include "uint64gmp.h"
+
+#include "power.h"
+
+#include "c.h"
+
+#include "map.h"
+
+#include "types.h"
+
+void wmpn_copyi(uint64_t * r, uint64_t * x, int32_t sz)
+{
+  int32_t i;
+  uint64_t * xp;
+  uint64_t * rp;
+  i = 0;
+  xp = x + 0;
+  rp = r + 0;
+  while (i < sz) {
+    *rp = *xp;
+    rp = rp + 1;
+    xp = xp + 1;
+    i = i + 1;
+  }
+}
+
+int32_t wmpn_zero_p(uint64_t * x, int32_t sz)
+{
+  int32_t i;
+  uint64_t uzero;
+  uint64_t lx;
+  i = sz;
+  uzero = UINT64_C(0);
+  lx = uzero;
+  while (i >= 1) {
+    i = i - 1;
+    lx = x[i];
+    if (!(lx == uzero)) {
+      return 0;
+    }
+  }
+  return 1;
+}
+
+void wmpn_zero(uint64_t * r, int32_t sz)
+{
+  int32_t i;
+  uint64_t lzero;
+  i = 0;
+  lzero = UINT64_C(0);
+  while (i < sz) {
+    r[i] = lzero;
+    i = i + 1;
+  }
+}
+

generated-src/lib/util.h

+#include <stdlib.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <assert.h>
+#include <alloca.h>
+void wmpn_copyi(uint64_t * r, uint64_t * x, int32_t sz);
+
+int32_t wmpn_zero_p(uint64_t * x, int32_t sz);
+
+void wmpn_zero(uint64_t * r, int32_t sz);
+

generated-src/lib/valuation.h

+#include <stdlib.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <assert.h>
+#include <alloca.h>
+

generated-src/wmp.h

+#ifndef __WMP_H__
+#define __WMP_H__
+
+#include <stdint.h>
+
+typedef int32_t wmp_size_t;
+typedef uint64_t wmp_limb_t;
+typedef wmp_limb_t *wmp_ptr;
+typedef wmp_limb_t const *wmp_srcptr;
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+int32_t wmpn_cmp (wmp_srcptr, wmp_srcptr, wmp_size_t);
+
+void wmpn_copyi (wmp_ptr, wmp_srcptr, wmp_size_t);
+
+int32_t wmpn_zero_p (wmp_srcptr, wmp_size_t);
+
+void wmpn_zero (wmp_ptr, wmp_size_t);
+
+wmp_limb_t wmpn_add (wmp_ptr, wmp_srcptr, wmp_size_t, wmp_srcptr, wmp_size_t);
+wmp_limb_t wmpn_add_1 (wmp_ptr, wmp_srcptr, wmp_size_t, wmp_limb_t);
+wmp_limb_t wmpn_add_n (wmp_ptr, wmp_srcptr, wmp_srcptr, wmp_size_t);
+wmp_limb_t wmpn_add_in_place (wmp_ptr, wmp_size_t, wmp_srcptr, wmp_size_t);
+wmp_limb_t wmpn_add_1_in_place (wmp_ptr, wmp_size_t, wmp_limb_t);
+
+wmp_limb_t wmpn_sub (wmp_ptr, wmp_srcptr, wmp_size_t, wmp_srcptr, wmp_size_t);
+wmp_limb_t wmpn_sub_1 (wmp_ptr, wmp_srcptr, wmp_size_t, wmp_limb_t);
+wmp_limb_t wmpn_sub_n (wmp_ptr, wmp_srcptr, wmp_srcptr, wmp_size_t);
+wmp_limb_t wmpn_sub_in_place (wmp_ptr, wmp_size_t, wmp_srcptr, wmp_size_t);
+wmp_limb_t wmpn_sub_1_in_place (wmp_ptr, wmp_size_t, wmp_limb_t);
+
+void wmpn_mul (wmp_ptr, wmp_srcptr, wmp_size_t, wmp_srcptr, wmp_size_t);
+wmp_limb_t wmpn_mul_1 (wmp_ptr, wmp_srcptr, wmp_size_t, wmp_limb_t);
+void wmpn_mul_n (wmp_ptr, wmp_srcptr, wmp_srcptr, wmp_size_t);
+
+wmp_limb_t wmpn_addmul_1 (wmp_ptr, wmp_srcptr, wmp_size_t, wmp_limb_t);
+wmp_limb_t wmpn_submul_1 (wmp_ptr, wmp_srcptr, wmp_size_t, wmp_limb_t);
+
+wmp_limb_t wmpn_lshift (wmp_ptr, wmp_srcptr, wmp_size_t, uint64_t);
+wmp_limb_t wmpn_rshift (wmp_ptr, wmp_srcptr, wmp_size_t, uint64_t);
+wmp_limb_t wmpn_lshift_in_place (wmp_ptr, wmp_size_t, uint64_t);
+wmp_limb_t wmpn_rshift_in_place (wmp_ptr, wmp_size_t, uint64_t);
+
+wmp_limb_t wmpn_divrem_1 (wmp_ptr, wmp_srcptr, wmp_size_t, wmp_limb_t);
+void wmpn_tdiv_qr (wmp_ptr, wmp_ptr, wmp_srcptr, wmp_size_t, wmp_srcptr, wmp_size_t);
+void wmpn_tdiv_qr_in_place (wmp_ptr, wmp_srcptr, wmp_size_t, wmp_srcptr, wmp_size_t);
+
+wmp_size_t wmpn_sqrtrem (wmp_ptr, wmp_ptr, wmp_srcptr, wmp_size_t);
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif

why3 @ 83bee6fa

+Subproject commit 83bee6fa62b20de592920e1b163df0e5e52d6955