shttpd/lex/nat-generic.c

// 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;
}