doc/computation-model/speculation.rst

@@ -1,6 +1,8 @@
 .. SPDX-License-Identifier: GPL-2.0 or GPL-3.0
 .. Copyright © 2019 Ariadne Devos
 
+.. _speculation:
+
 Controlling speculation
 =======================
 

doc/program-proofs/index.rst

@@ -14,14 +14,13 @@ A few guidelines are given.
 Contracts
 ---------
 The contract of a function is given where it is declared:
-the header file for exported functions.
+the header file for exported functions. If a proposition
+is conditional on presence or absence of :ref:`speculation <speculation>`,
+this is modelled as being conditional on `S` or `NS` respectively,
+defined in `<sHT/nospec.h> `.
 
 Lemmas
 ------
-The name of lemmas (preconditions, postconditions and invariants)
-are postfixed by `S` or `NS` if they only need to hold speculatively
-or non-speculatively respectively.
-
 Invariants' names are suffixed by `I`, before any speculation suffix.
 
 Loops

lex/nat-generic.c

@@ -0,0 +1,144 @@
+// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
+// Copyright © 2019 Ariadne Devos
+
+// Integer model: wrap-around
+// Proof status: auto
+
+#include <stdint.h>
+#include <sHT/index.h>
+#include <sHT/lex/digit.h>
+#include <sHT/lex/nat.h>
+#include <sHT/logic/arithmetic.h>
+#include <sHT/test.h>
+
+#ifdef __FRAMAC__
+#  include <sHT/math/vector-memory.h>
+#  include <sHT/math/expnat/lt.h>
+#endif
+
+/*@ requires S ==> \valid_read(&c[0 .. e - 1]);
+    requires S ==> \valid_read(&c[0]);
+    requires \valid_read(&c[b .. e - 1]);
+    requires NS ==> b <= i < e;
+    requires i < e || i == 0;
+    requires NS ==> X_num_p(vector_load_u8(c + b, e - b));
+    terminates \true;
+    assigns \result;
+    ensures NS ==> \result == X_val(c[i]); */
+static inline uint32_t
+sHT_X_given_X_num_p(uint8_t *c, size_t b, size_t e, size_t i)
+{
+	/*@ assert NS ==> X_p(\nth(vector_load_u8(c + b, e - b), i - b)); */
+	/*@ assert NS ==> X_p((c + b)[i - b]); */
+	return sHT_X_val(c[i]);
+}
+
+/** Reduce scope of X_num_p
+
+    (Doing i + 1 here avoids overflow later.) */
+/*@ requires NS ==> i < n;
+    requires NS ==> X_num_p(vector_load_u8(c, n));
+    terminates \true;
+    assigns \nothing;
+    ensures NS ==> X_num_p(vector_load_u8(c, i + 1)); */
+static inline void
+sHT_X_num_p_less(uint8_t *c, size_t n, size_t i)
+{
+	/* Limit range to 0 .. i: elements */
+	/*@ assert \length(vector_load_u8(c, n)) == n; */
+	/*@ assert \length(vector_load_u8(c, i + 1)) == i + 1; */
+	/*@ assert NS ==> ∀ ℤ j; 0 <= j < n
+	      ==> \nth(vector_load_u8(c, n), j) == c[j]; */
+	/*@ assert NS ==> ∀ ℤ j; 0 <= j < i + 1
+	      ==> \nth(vector_load_u8(c, n), j) == c[j]; */
+	/*@ assert NS ==> ∀ ℤ j; 0 <= j < i + 1
+	      ==> \nth(vector_load_u8(c, i + 1), j) == c[j]; */
+	/*@ assert NS ==> ∀ ℤ j; 0 <= j < i + 1
+	      ==> \nth(vector_load_u8(c, n), j) == \nth(vector_load_u8(c, i + 1), j); */
+
+	/* Limit range to 0 .. i: predicate*/
+	/*@ assert NS ==> ∀ ℤ j; 0 <= j < \length(vector_load_u8(c, n))
+	      ==> X_p(\nth(vector_load_u8(c, n), j)); */
+	/*@ assert NS ==> ∀ ℤ j; 0 <= j < n
+	      ==> X_p(\nth(vector_load_u8(c, n), j)); */
+	/*@ assert NS ==> ∀ ℤ j; 0 <= j < i + 1
+	      ==> X_p(\nth(vector_load_u8(c, n), j)); */
+	/*@ assert NS ==> ∀ ℤ j; 0 <= j < i + 1
+	      ==> X_p(\nth(vector_load_u8(c, i + 1), j)); */
+}
+
+/*@ requires NS ==> X_num_p(vector_load_u8(c, n));
+    requires NS ==> k <= n;
+    terminates \true;
+    assigns \nothing;
+    ensures NS ==> X_num_val(vector_load_u8(c, k))
+      ≤ X_num_val(vector_load_u8(c, n)); */
+static inline void
+sHT_X_num_val_less_lt(uint8_t *c, size_t n, size_t k)
+{
+	/*@ assert NS ==> ∀ integer j; 0 <= j < \length(vector_load_u8(c, n))
+	      ==> X_p(\nth(vector_load_u8(c, n), j)); */
+	/*@ assert NS ==> ∀ integer j; 0 <= j < n
+	      ==> X_p(\nth(vector_load_u8(c, n), j)); */
+	/*@ assert NS ==> ∀ integer j; 0 <= j < n
+	      ==> \nth(vector_load_u8(c, n), j) == c[j]; */
+	/*@ assert NS ==> ∀ integer j; 0 <= j < n
+	      ==> X_p(c[j]); */
+	/*@ assert NS ==> ∀ integer j; 0 <= j < n
+	      ==> 0 <= X_val(c[j]) < X_base; */
+
+	/*@ loop invariant NS ==> k <= i <= n;
+	    loop invariant NS ==> X_num_val(vector_load_u8(c, k))
+	      ≤ X_num_val(vector_load_u8(c, i));
+	    loop assigns i;
+	    loop variant n - i; */
+	for (size_t i = k; i < n; i++) {
+		/* Step X_num_val */
+		sHT_X_num_p_less(c, n, i);
+		/*@ assert vector_load_u8(c, i + 1) == (vector_load_u8(c, i) ^ [| c[i] |]); */
+		/*@ assert NS ==> X_num_p(vector_load_u8(c, i) ^ [| c[i] |]); */
+		/*@ assert NS ==> X_num_val(vector_load_u8(c, i) ^ [| c[i] |])
+		      == X_base * X_num_val(vector_load_u8(c, i))
+		         + X_val(c[i]); */
+		/*@ assert NS ==> X_num_val(vector_load_u8(c, i + 1))
+		      == X_base * X_num_val(vector_load_u8(c, i))
+		         + X_val(c[i]); */
+
+		/* Bounds on the extra digit */
+		/*@ assert NS ==> X_p(\nth(vector_load_u8(c, n), i)); */
+		/*@ assert NS ==> X_p(c[i]); */
+		/*@ assert NS ==> 0 <= X_val(c[i]) < X_base; */
+	}
+}
+
+uint32_t
+sHT_X_to_u32(uint8_t *c, size_t b, size_t e)
+{
+	size_t i = b;
+	uint32_t x = 0;
+	if (sHT_ge(b, e))
+		return x;
+	/*@ loop invariant NS ==> b <= i < e;
+	    loop invariant NS ==> x == X_num_val(vector_load_u8(c + b, i - b));
+	    loop assigns i, x;
+	    loop variant e - i; */
+	do {	loop: i = sHT_index_nospec(i, e);
+		sHT_X_num_p_less(c + b, e - b, i - b);
+		uint32_t y = sHT_X_given_X_num_p(c, b, e, i);
+		/* Value */
+		/*@ assert NS ==> vector_load_u8(c + b, i - b + 1)
+		      == (vector_load_u8(c + b, i - b) ^ [| c[i] |]); */
+		/*@ assert NS ==> X_num_val(vector_load_u8(c + b, i - b + 1))
+		      == X_base * X_num_val(vector_load_u8(c + b, i - b))
+		         + X_val(c[i]); */
+		/*@ assert NS ==> X_num_val(vector_load_u8(c + b, i - b + 1))
+		      == X_base * X_num_val(vector_load_u8(c + b, i - b))
+		         + y; */
+		/* Bounds */
+		sHT_X_num_val_less_lt(c + b, e - b, (i - b) + 1);
+		/*@ assert NS ==> X_num_val(vector_load_u8(c + b, (i - b) + 1)) <= UINT32_MAX; */
+		x = sHT_muladd_nooverflowNS_u32(sHT_X_base, x, y);
+		i++;
+	} while (sHT_lt(i, e));
+	return x;
+}

lex/nat-uphex.c

@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
+// Copyright © 2019 Ariadne Devos
+
+// Integer model: wrap-around
+// Proof status: auto
+
+#define X_p uphex_p
+#define X_num_p uphex_num_p
+#define X_val uphex_val
+#define X_num_val uphex_num_val
+#define X_base 16
+#define sHT_X_val sHT_uphex_val
+#define sHT_X_base 16
+#define sHT_X_given_X_num_p sHT_uphex_given_uphex_num_p
+#define sHT_X_num_p_less sHT_uphex_num_p_less
+#define sHT_X_num_val_less_lt sHT_uphex_num_val_less_lt
+#define sHT_X_to_u32 sHT_uphex_to_u32
+#include "nat-generic.c"

sHT/lex/digit.h

@@ -6,6 +6,10 @@
 
 #include <stdint.h>
 
+#ifdef __FRAMAC__
+#  include <sHT/nospec.h>
+#endif
+
 /*@ axiomatic Digit {
       logic 𝔹 decimal_p(ℤ c) = '0' <= c <= '9';
       logic 𝔹 downaf_p(ℤ c) = 'a' <= c <= 'f';
@@ -31,6 +35,8 @@
         : downaf_p(c) ? downaf_val(c) : digitval_undef;
       logic ℤ uphex_val(ℤ c) = decimal_p(c) ? decimal_val(c)
         : upaf_p(c) ? upaf_val(c) : digitval_undef;
+      logic ℤ hex_val(ℤ c) = downhex_p(c) ? downhex_val(c)
+        : uphex_p(c) ? uphex_val(c) : digitval_undef;
     } */
 
 /* TODO which types are the most interesting?
@@ -43,25 +49,25 @@
    In any case, unsigned is useful for SMT solvers are being confused
    by the implicit casts. */
 
-/*@ requires cNS: decimal_p(c);
-    requires crange: 0 <= c < 256;
+/*@ requires c: NS ==> decimal_p(c);
+    requires range: 0 <= c < 256;
     terminates \true;
     assigns \result \from c;
-    ensures rNS: \result == decimal_val(c);
-    ensures rangeNS: 0 <= \result < 10; */
-sHT_digit_val_t
+    ensures result: NS ==> \result == decimal_val(c);
+    ensures range: NS ==> 0 <= \result < 10; */
+static sHT_digit_val_t
 sHT_decimal_val(sHT_digit_char_t c)
 {
 	return c - 0x30u;
 }
 
-/*@ requires cNS: uphex_p(c);
-    requires crange: 0 <= c < 256;
+/*@ requires c: NS ==> uphex_p(c);
+    requires range: 0 <= c < 256;
     terminates \true;
     assigns \result \from c;
-    ensures resultNS: \result == uphex_val(c);
-    ensures rangeNS: 0 <= \result < 16; */
-sHT_digit_val_t
+    ensures result: NS ==> \result == uphex_val(c);
+    ensures range: NS ==> 0 <= \result < 16; */
+static sHT_digit_val_t
 sHT_uphex_val(sHT_digit_char_t c)
 {
 	c -= 0x30u;
@@ -72,13 +78,13 @@ sHT_uphex_val(sHT_digit_char_t c)
 	return c;
 }
 
-/*@ requires cNS: downhex_p(c);
-    requires crange: 0 <= c < 256;
+/*@ requires c: NS ==> downhex_p(c);
+    requires range: 0 <= c < 256;
     terminates \true;
     assigns \result \from c;
-    ensures resultNS: \result == downhex_val(c);
-    ensures rangeNS: 0 <= \result < 16; */
-sHT_digit_val_t
+    ensures result: NS ==> \result == downhex_val(c);
+    ensures range: NS ==> 0 <= \result < 16; */
+static sHT_digit_val_t
 sHT_downhex_val(sHT_digit_char_t c)
 {
 	c -= 0x30u;

sHT/lex/nat.h

@@ -5,11 +5,196 @@
 #define _sHT_LEX_NAT_H
 
 #include <limits.h>
+#include <stddef.h>
 #include <stdint.h>
 
 #include <sHT/logic/failbit.h>
 #include <sHT/logic/arithmetic.h>
 
+#ifdef __FRAMAC__
+#  include <sHT/lex/digit.h>
+#  include <sHT/math/expnat.h>
+#  include <sHT/math/expnat/power16.h>
+#  include <sHT/math/positional.h>
+#  include <sHT/math/vector-memory.h>
+#endif
+
+/*@ axiomatic DigitStar {
+      predicate decimal_num_p(\list<ℤ> c) =
+        ∀ ℤ i; 0 <= i < \length(c) ==> decimal_p(\nth(c, i));
+      predicate downhex_num_p(\list<ℤ> c) =
+        ∀ ℤ i; 0 <= i < \length(c) ==> downhex_p(\nth(c, i));
+      predicate uphex_num_p(\list<ℤ> c) =
+        ∀ ℤ i; 0 <= i < \length(c) ==> uphex_p(\nth(c, i));
+      predicate hex_num_p(\list<ℤ> c) =
+        ∀ ℤ i; 0 <= i < \length(c) ==> hex_p(\nth(c, i));
+
+      lemma uphex_hex_num:
+        ∀ \list<ℤ> c; uphex_num_p(c) ==> hex_num_p(c);
+      lemma downhex_hex_num:
+        ∀ \list<ℤ> c; downhex_num_p(c) ==> hex_num_p(c);
+      lemma decimal_uphex_num:
+        ∀ \list<ℤ> c; decimal_num_p(c) ==> uphex_num_p(c);
+      lemma decimal_downhex_num:
+        ∀ \list<ℤ> c; decimal_num_p(c) ==> downhex_num_p(c);
+      lemma decimal_hex_num:
+        ∀ \list<ℤ> c; decimal_num_p(c) ==> hex_num_p(c);
+    } */
+
+/*@ axiomatic DigitSequence {
+      // TODO: non-axiomatic delete once lambda's are supported
+      // (= map decimal_val c)
+      logic \list<ℤ> decimal_val_plural(\list<ℤ> c);
+      axiom decimal_val_plural_length: ∀ \list<ℤ> c;
+        \length(decimal_val_plural(c)) == \length(c);
+      axiom decimal_val_plural_at: ∀ \list<ℤ> c, ℤ i;
+        0 <= i < \length(c) ==> \nth(decimal_val_plural(c), i) == decimal_val(\nth(c, i));
+      lemma decimal_val_plural_split: ∀ \list<ℤ> c, d;
+        decimal_val_plural(c ^ d)
+        == (decimal_val_plural(c) ^ decimal_val_plural(d));
+      lemma decimal_val_plural_peelr: ∀ \list<ℤ> c, ℤ d;
+        decimal_val_plural(c ^ [| d |])
+        == (decimal_val_plural(c) ^ [| decimal_val(d) |]);
+
+      logic \list<ℤ> uphex_val_plural(\list<ℤ> c);
+      axiom uphex_val_plural_length: ∀ \list<ℤ> c;
+        \length(uphex_val_plural(c)) == \length(c);
+      axiom uphex_val_plural_at: ∀ \list<ℤ> c, ℤ i;
+        0 <= i < \length(c) ==> \nth(uphex_val_plural(c), i) == uphex_val(\nth(c, i));
+      lemma uphex_val_plural_split: ∀ \list<ℤ> c, d;
+        uphex_val_plural(c ^ d)
+        == (uphex_val_plural(c) ^ uphex_val_plural(d));
+      lemma uphex_val_plural_peelr: ∀ \list<ℤ> c, ℤ d;
+        uphex_val_plural(c ^ [| d |])
+        == (uphex_val_plural(c) ^ [| uphex_val(d) |]);
+
+      logic \list<ℤ> downhex_val_plural(\list<ℤ> c);
+      axiom downhex_val_plural_length: ∀ \list<ℤ> c;
+        \length(downhex_val_plural(c)) == \length(c);
+      axiom downhex_val_plural_at: ∀ \list<ℤ> c, ℤ i;
+        0 <= i < \length(c) ==> \nth(downhex_val_plural(c), i) == downhex_val(\nth(c, i));
+      lemma downhex_val_plural_split: ∀ \list<ℤ> c, d;
+        downhex_val_plural(c ^ d)
+        == (downhex_val_plural(c) ^ downhex_val_plural(d));
+      lemma downhex_val_plural_peelr: ∀ \list<ℤ> c, ℤ d;
+        downhex_val_plural(c ^ [| d |])
+        == (downhex_val_plural(c) ^ [| downhex_val(d) |]);
+
+      logic \list<ℤ> hex_val_plural(\list<ℤ> c);
+      axiom hex_val_plural_length: ∀ \list<ℤ> c;
+        \length(hex_val_plural(c)) == \length(c);
+      axiom hex_val_plural_at: ∀ \list<ℤ> c, ℤ i;
+        0 <= i < \length(c) ==> \nth(hex_val_plural(c), i) == hex_val(\nth(c, i));
+      lemma hex_val_plural_split: ∀ \list<ℤ> c, d;
+        hex_val_plural(c ^ d)
+        == (hex_val_plural(c) ^ hex_val_plural(d));
+      lemma hex_val_plural_peelr: ∀ \list<ℤ> c, ℤ d;
+        hex_val_plural(c ^ [| d |])
+        == (hex_val_plural(c) ^ [| hex_val(d) |]);
+    } */
+
+/*@ // Desc: upper bounds for vectorised digit lexing
+    // Status: automatic
+    axiomatic DigitSequenceLt {
+      lemma decimal_val_plural_lt_at0: ∀ \list<ℤ> c, ℤ j;
+        decimal_num_p(c) ==> 0 <= j < \length(decimal_val_plural(c))
+        ==> \nth(decimal_val_plural(c), j) < 10;
+      lemma decimal_val_plural_lt_at1: ∀ \list<ℤ> c, ℤ j;
+        decimal_num_p(c) ==> 0 <= j < \length(c)
+        ==> \nth(decimal_val_plural(c), j) < 10;
+      lemma decimal_val_plural_lt: ∀ \list<ℤ> c;
+        decimal_num_p(c) ==> vector_lt_constant(decimal_val_plural(c), 10);
+
+      lemma uphex_val_plural_lt_at0: ∀ \list<ℤ> c, ℤ j;
+        uphex_num_p(c) ==> 0 <= j < \length(uphex_val_plural(c))
+        ==> \nth(uphex_val_plural(c), j) < 16;
+      lemma uphex_val_plural_lt_at1: ∀ \list<ℤ> c, ℤ j;
+        uphex_num_p(c) ==> 0 <= j < \length(c)
+        ==> \nth(uphex_val_plural(c), j) < 16;
+      lemma uphex_val_plural_lt: ∀ \list<ℤ> c;
+        uphex_num_p(c) ==> vector_lt_constant(uphex_val_plural(c), 16);
+
+      lemma downhex_val_plural_lt_at0: ∀ \list<ℤ> c, ℤ j;
+        downhex_num_p(c) ==> 0 <= j < \length(downhex_val_plural(c))
+        ==> \nth(downhex_val_plural(c), j) < 16;
+      lemma downhex_val_plural_lt_at1: ∀ \list<ℤ> c, ℤ j;
+        downhex_num_p(c) ==> 0 <= j < \length(c)
+        ==> \nth(downhex_val_plural(c), j) < 16;
+      lemma downhex_val_plural_lt: ∀ \list<ℤ> c;
+        downhex_num_p(c) ==> vector_lt_constant(downhex_val_plural(c), 16);
+
+      lemma hex_val_plural_lt_at0: ∀ \list<ℤ> c, ℤ j;
+        hex_num_p(c) ==> 0 <= j < \length(hex_val_plural(c))
+        ==> \nth(hex_val_plural(c), j) < 16;
+      lemma hex_val_plural_lt_at1: ∀ \list<ℤ> c, ℤ j;
+        hex_num_p(c) ==> 0 <= j < \length(c)
+        ==> \nth(hex_val_plural(c), j) < 16;
+      lemma hex_val_plural_lt: ∀ \list<ℤ> c;
+        hex_num_p(c) ==> vector_lt_constant(hex_val_plural(c), 16);
+    } */
+
+/*@ // Description: Order: most-significant to least-significant
+    // Proof status: auto
+    axiomatic Numeric {
+      logic ℤ decimal_num_val(\list<ℤ> c)
+        = sum_digits_ms_to_ls(10, decimal_val_plural(c));
+      logic ℤ uphex_num_val(\list<ℤ> c)
+        = sum_digits_ms_to_ls(16, uphex_val_plural(c));
+      logic ℤ downhex_num_val(\list<ℤ> c)
+        = sum_digits_ms_to_ls(16, downhex_val_plural(c));
+      logic ℤ hex_num_val(\list<ℤ> c)
+        = sum_digits_ms_to_ls(16, hex_val_plural(c));
+
+      // These are specialisations of `sum_digits_ms_to_ls_ind`.
+      lemma decimal_val_peelr: ∀ \list<ℤ> c, ℤ d;
+        decimal_num_val(c ^ [| d |]) == 10 * decimal_num_val(c) + decimal_val(d);
+      lemma uphex_num_val_peelr: ∀ \list<ℤ> c, ℤ d;
+        uphex_num_val(c ^ [| d |]) == 16 * uphex_num_val(c) + uphex_val(d);
+      lemma downhex_num_val_peelr: ∀ \list<ℤ> c, ℤ d;
+        downhex_num_val(c ^ [| d |]) == 16 * downhex_num_val(c) + downhex_val(d);
+      lemma hex_num_val_peelr: ∀ \list<ℤ> c, ℤ d;
+        hex_num_val(c ^ [| d |]) == 16 * hex_num_val(c) + hex_val(d);
+    } */
+
+/*@ // Desc: upper bounds on lexed numbers
+    //   > These are specialisations of sum_digits_lt
+    // Proof status: auto
+    axiomatic NumericLt {
+      lemma decimal_num_val_lt: ∀ \list<ℤ> c;
+        decimal_num_p(c) ==> decimal_num_val(c) < expnat(10, \length(c));
+      lemma uphex_num_val_lt: ∀ \list<ℤ> c;
+        uphex_num_p(c) ==> uphex_num_val(c) < expnat(16, \length(c));
+      lemma downhex_num_val_lt: ∀ \list<ℤ> c;
+        downhex_num_p(c) ==> downhex_num_val(c) < expnat(16, \length(c));
+      lemma hex_num_val_lt: ∀ \list<ℤ> c;
+        hex_num_p(c) ==> hex_num_val(c) < expnat(16, \length(c));
+    } */
+
+/*@ lemma uphex_to_u32_nooverflow_help: ∀ ℤ n;
+      0 ≤ n ≤ 8 ⇒ expnat(16, n) ≤ UINT32_MAX + 1; */
+/*@ lemma uphex_to_u32_nooverflow: ∀ \list<ℤ> d;
+      uphex_num_p(d) ∧ 0 ≤ \length(d) ≤ 8 ⇒ uphex_num_val(d) ≤ UINT32_MAX; */
+
+/** Parse a big-endian, upper-case, hexadecimal number < 2**32
+
+  Hint: if $0 ≤ e - b ≤ 8$, `bounds` holds by
+  `uphex_to_u32_nooverflow`. */
+/*@ requires order: b <= e;
+    requires bounds: NS ⇒ uphex_num_val(vector_load_u8(c + b, e - b)) <= UINT32_MAX;
+    requires from_r: \valid_read(&c[b .. e - 1]);
+    requires from_rS: S ==> \valid_read(&c[0 .. e - 1]);
+    requires from_r0S: S ==> \valid_read(&c[0]);
+    requires num: NS ==> uphex_num_p(vector_load_u8(c + b, e - b));
+    terminates NS;
+    assigns \result \from c[0 .. e - 1], c[0];
+    ensures result: NS ==> \result
+      == uphex_num_val(vector_load_u8(c + b, e - b)); */
+uint32_t
+sHT_uphex_to_u32(uint8_t *c, size_t b, size_t e);
+
+// TODO: decimal uint8_t variant for IPv4 code
+// TODO: upper-case hexadecimal uint16_t variant for IPv6 code
+
 struct sHT_decimal_u32
 {
 	sHT_with_failbit

sHT/logic/arithmetic.h

@@ -4,8 +4,20 @@
 #ifndef _sHT_LOGIC_ARITHMETIC
 #define _sHT_LOGIC_ARITHMETIC
 
+#include <stdint.h>
 #include <sHT/logic/failbit.h>
 
+/** Non-overflowing integer multiply-add */
+/*@ requires NS ==> a * b + c <= UINT32_MAX;
+    terminates \true;
+    assigns \result \from a, b, c;
+    ensures NS ==> \result == a * b + c; */
+static inline uint32_t
+sHT_muladd_nooverflowNS_u32(uint32_t a, uint32_t b, uint32_t c)
+{
+	return a * b + c;
+}
+
 /** The variable really is in ℕ (for proofs), but
   the range supported by the computer is limited.
 

sHT/math/expnat.h

@@ -0,0 +1,45 @@
+// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
+// Copyright © 2019 Ariadne Devos
+
+#ifndef _sHT_MATH_EXPNAT_H
+#define _sHT_MATH_EXPNAT_H
+
+#include <sHT/math/vector.h>
+
+/*@ // Exponentiation
+    // Proof status: complete, automatic
+    axiomatic Expnat {
+      // exponentiation is repeated multiplication
+      logic ℤ expnat(ℤ b, ℤ e) = product([| b |] *^ e);
+
+      // Some disagree about this one: exp(0, 0) = 0 or 1?
+      // The latter is very convenient.
+      lemma expnat_empty: ∀ ℤ b; expnat(b, 0) == 1;
+      lemma expnat_one: ∀ ℤ b; expnat(b, 1) == b;
+
+      // Actually belongs to Frama-C's bag of lemmas
+      lemma expnat_split_help: ∀ ℤ b, e0, e1; e0 >= 0 && e1 >= 0
+        ==> [| b |] *^ (e0 + e1) == ([| b |] *^ e0 ^ [| b |] *^ e1);
+      lemma expnat_split: ∀ ℤ b, e0, e1; e0 >= 0 && e1 >= 0
+        ==> expnat(b, e0 + e1) == expnat(b, e0) * expnat(b, e1);
+      lemma expnat_ind: ∀ ℤ b, e; b >= 0 && e >= 0 ==> b * expnat(b, e) == expnat(b, e + 1);
+    } */
+
+/*@ // Title: Element-wise exponentiation in ℤ
+    // Note(Usage, Axiom): can be eliminated once lambdas are supported
+    // Proof status: incomplete, automatic
+    axiomatic IotaExpnat {
+      // (2, 5) ==> [| 16, 8, 4, 2, 1 |]
+      logic \list<ℤ> exp_countdown(ℤ b, ℤ n);
+
+      axiom exp_countdown_length: ∀ ℤ b, n; 0 <= n
+        ==> \length(exp_countdown(b, n)) == n;
+      axiom exp_countdown_at: ∀ ℤ b, n, i; 0 <= i < n
+        ==> \nth(exp_countdown(b, n), i) == expnat(b, n - i - 1);
+
+      // A check
+      lemma exp_countdown_last: ∀ ℤ b, n; 0 < n
+        ==> \nth(exp_countdown(b, n), n - 1) == 1;
+    } */
+
+#endif

sHT/math/expnat/lt.h

@@ -0,0 +1,24 @@
+// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
+// Copyright © 2019 Ariadne Devos
+
+#ifndef _sHT_MATH_EXPNAT_MULADD
+#define _sHT_MATH_EXPNAT_MULADD
+
+#include <stdint.h>
+#include <sHT/math/expnat.h>
+
+// Reverse Proof:
+// - a * x + b < expnat(a, e + 1) (and_intros)
+// - a * x + b < a * expnat(a, e) (peel expnat)
+// - b < a * expnat(a, e) - a * x (omega)
+// - b < a * (expnat(a, e) - x) (reverse_distributivity)
+// - b < a /\ 0 < a /\ 0 < expnat(a, e) - x (split_mult_order)
+// - 0 < expnat(b, e) - x (intuition)
+// - x < expnat(b, e) (omega)
+// - (assumption)
+// Qed.
+/*@ lemma expnat_muladd_lt: ∀ ℤ a, x, b, e;
+      0 < a && 0 ≤ e && x < expnat(a, e) && b < a
+      ==> a * x + b < expnat(a, e + 1); */
+
+#endif