x_inflate_dict

// A reference DEFLATE encoder (RFC 1951), written from the RFC alone, for the inflate laws that check decoded output
// (inflate_decode): a bit writer, stored blocks (3.2.4), fixed-Huffman blocks (3.2.6) and dynamic-Huffman blocks
// (3.2.7) with ANY valid code lengths, literals, and back-references (3.2.5).
//
//  - Bits are packed starting with the least significant bit of each byte; data elements (lengths, extra bits) are
//    written least significant bit first, Huffman codes most significant bit first (3.1.1);
//  - canonical codes (3.2.2): bl_count[len] = the number of codes of each length, next_code[1] = 0,
//    next_code[len] = (next_code[len - 1] + bl_count[len - 1]) << 1, then the symbols in increasing order get
//    consecutive codes of their length;
//  - a dynamic block: BFINAL, BTYPE = 10, HLIT = nlen - 257, HDIST = ndist - 1, HCLEN = 19 - 4 (all 19 code length
//    code lengths, 3 bits each, in the order 16 17 18 0 8 7 9 6 10 5 11 4 12 3 13 2 14 1 15), then the nlen + ndist
//    code lengths (one sequence) in the code length code: 0..15 literally, 16 = copy the previous length 3..6 times
//    (2 extra bits), 17 = 3..10 zeros (3 extra bits), 18 = 11..138 zeros (7 extra bits), then the symbols.
// inflate accepts a dynamic block's codes when (inflate.c, inftrees.c): nlen <= 286, ndist <= 30; the code length
// code is complete; the literal/length code has a code for 256 and is complete or a single code of length 1; the
// distance code is complete, a single code of length 1, or empty.  kraft() and code_ok() state these.
#ifndef ZLIB_HARNESS_DEFLATE_REF_H
#define ZLIB_HARNESS_DEFLATE_REF_H
#include "zlib_common.h"

struct bw {                     // a bit writer, least significant bit first (RFC 1951 3.1.1)
	unsigned char *buf;
	unsigned len;           // complete bytes
	unsigned nb;            // bits in buf[len]
};

static void bw_bit(struct bw *w, unsigned b)
{
	if (w->nb == 0)
		w->buf[w->len] = 0;
	w->buf[w->len] = (unsigned char) (w->buf[w->len] | ((b & 1) << w->nb));
	w->nb++;
	if (w->nb == 8) {
		w->nb = 0;
		w->len++;
	}
}

static void bw_bits(struct bw *w, unsigned v, unsigned n)       // a value, its least significant bit first
{
	for (unsigned i = 0; i < n; ++i)
		bw_bit(w, v >> i);
}

static void bw_code(struct bw *w, unsigned c, unsigned n)       // a Huffman code, its most significant bit first
{
	for (unsigned i = n; i > 0; --i)
		bw_bit(w, c >> (i - 1));
}

static void bw_byte(struct bw *w, unsigned char b)              // at a byte boundary
{
	w->buf[w->len] = b;
	w->len++;
}

static void bw_align(struct bw *w)
{
	if (w->nb != 0) {
		w->nb = 0;
		w->len++;
	}
}

// the fixed literal/length code (RFC 1951 3.2.6)
static void bw_fixed(struct bw *w, unsigned v)
{
	if (v < 144)
		bw_code(w, 0x30 + v, 8);
	else if (v < 256)
		bw_code(w, 0x190 + (v - 144), 9);
	else if (v < 280)
		bw_code(w, v - 256, 7);
	else
		bw_code(w, 0xc0 + (v - 280), 8);
}

// RFC 1951 3.2.5: length codes 257..285 and distance codes 0..29
static const unsigned short ref_lbase[29] = {3, 4, 5, 6, 7, 8, 9, 10, 11, 13, 15, 17, 19, 23, 27, 31, 35, 43, 51, 59,
					     67, 83, 99, 115, 131, 163, 195, 227, 258};
static const unsigned char ref_lext[29] = {0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 3, 4, 4, 4, 4, 5,
					   5, 5, 5, 0};
static const unsigned short ref_dbase[30] = {1, 2, 3, 4, 5, 7, 9, 13, 17, 25, 33, 49, 65, 97, 129, 193, 257, 385, 513,
					     769, 1025, 1537, 2049, 3073, 4097, 6145, 8193, 12289, 16385, 24577};
static const unsigned char ref_dext[30] = {0, 0, 0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6, 7, 7, 8, 8, 9, 9, 10, 10,
					   11, 11, 12, 12, 13, 13};

static unsigned len_code(unsigned len)          // the length code (0..28 for symbols 257..285) of a length 3..258
{
	unsigned i = 28;
	if (len < 258) {
		i = 0;
		while (i + 1 < 28 && ref_lbase[i + 1] <= len)
			i++;
	}
	return i;
}

static unsigned dist_code(unsigned dist)        // the distance code of a distance 1..32768
{
	unsigned j = 0;
	while (j + 1 < 30 && ref_dbase[j + 1] <= dist)
		j++;
	return j;
}

static void bw_fixed_match(struct bw *w, unsigned len, unsigned dist)
{
	const unsigned i = len_code(len), j = dist_code(dist);
	bw_fixed(w, 257 + i);
	bw_bits(w, len - ref_lbase[i], ref_lext[i]);
	bw_code(w, j, 5);
	bw_bits(w, dist - ref_dbase[j], ref_dext[j]);
}

// canonical codes (RFC 1951 3.2.2) of lens[0..n-1] (lengths <= 15) into codes[0..n-1]
static void canonical(const unsigned char *lens, unsigned n, unsigned short *codes)
{
	unsigned count[16], next[16];
	for (unsigned l = 0; l < 16; ++l)
		count[l] = 0;
	for (unsigned i = 0; i < n; ++i)
		count[lens[i]]++;
	count[0] = 0;
	unsigned c = 0;
	next[0] = 0;
	for (unsigned l = 1; l < 16; ++l) {
		c = (c + count[l - 1]) << 1;
		next[l] = c;
	}
	for (unsigned i = 0; i < n; ++i) {
		if (lens[i] != 0) {
			codes[i] = (unsigned short) next[lens[i]];
			next[lens[i]]++;
		} else {
			codes[i] = 0;
		}
	}
}

// the Kraft sum of lens[0..n-1] in units of 2^-15 (a complete code: 2^15), and the number of codes
static unsigned long kraft(const unsigned char *lens, unsigned n, unsigned *used)
{
	unsigned long k = 0;
	unsigned u = 0;
	for (unsigned i = 0; i < n; ++i) {
		if (lens[i] != 0) {
			k += 1ul << (15 - lens[i]);
			u++;
		}
	}
	*used = u;
	return k;
}

// does inflate accept these lengths (see the header comment)?  type 0: code length code, 1: literal/length, 2: distance
static int code_ok(const unsigned char *lens, unsigned n, int type)
{
	unsigned used;
	const unsigned long k = kraft(lens, n, &used);
	if (k == 32768)
		return 1;
	if (type == 0)
		return 0;
	if (used == 1 && k == 16384)
		return 1;                       // a single code of length 1
	return type == 2 && used == 0;          // no distance code at all
}

#endif

// Shared by the zlib harnesses (zlib 1.3.2 core: adler32.c, crc32.c, deflate.c, trees.c, inflate.c, inffast.c,
// inftrees.c, compress.c, uncompr.c, zutil.c).
//
// A harness draws every input from quickproof.h (nondet_*, pick), restricts it with gp_assume, and states each property
// with gp_assert (undefined behaviour when the property fails).  Buffers have exactly the size the claim allows.  Every
// call of inflate() or deflate() gets its input and its output space as objects of their own, allocated with exactly
// avail_in and avail_out bytes (exact_copy, exact_space): an access before next_in, after next_in + avail_in, before
// next_out or after next_out + avail_out is then outside an object, i.e. undefined behaviour in the semantics of the
// theorem, so "inflate reads only the input it is offered and writes only the space it is offered" is part of every
// law's "no undefined behaviour".
//
// The reference facts, written from the definitions, not from zlib:
//  - Adler-32 (RFC 1950 8.2): s1 = 1 + the sum of the bytes, s2 = the sum of the successive values of s1, both mod
//    65521; the checksum is s2 * 65536 + s1.  ref_adler32 updates a checksum byte by byte;
//  - CRC-32 (RFC 1952 8, ISO 3309): the reflected polynomial 0xedb88320, register preset to all ones and inverted at
//    the end.  ref_crc32 updates a checksum bit by bit;
//  - the zlib wrapper (RFC 1950): 2 header bytes, an optional 4-byte dictionary id (big-endian Adler-32 of the
//    dictionary), the deflate data, then the big-endian Adler-32 of the uncompressed data;
//  - the gzip wrapper (RFC 1952): a header of at least 10 bytes (1f 8b 08 FLG MTIME(4) XFL OS, then the optional
//    fields), the deflate data, then the little-endian CRC-32 and the little-endian length mod 2^32 of the data;
//  - the inflate windowBits of zlib.h: 8..15 (zlib wrapper, 2^windowBits window), 0 (zlib wrapper, the window size of
//    the header), -8..-15 (raw deflate), + 16 (gzip wrapper only; 16 itself: the window size of the header), + 32
//    (zlib or gzip, detected); everything else is rejected with Z_STREAM_ERROR.
#ifndef ZLIB_HARNESS_COMMON_H
#define ZLIB_HARNESS_COMMON_H
#include <stddef.h>
#include <stdint.h>
#include <stdlib.h>
#include "quickproof.h"
#include "zlib.h"

#define GP_BASE 65521ul             // the Adler-32 modulus (RFC 1950)
#define GP_POLY 0xedb88320ul        // the CRC-32 polynomial, reflected (RFC 1952)

// Adler-32 of buf[0..n-1] continued from the checksum a (both halves < 65521 for a checksum).
static unsigned long ref_adler32(unsigned long a, const unsigned char *buf, unsigned long n)
{
	unsigned long s1 = a & 0xffff;
	unsigned long s2 = (a >> 16) & 0xffff;
	for (unsigned long i = 0; i < n; ++i) {
		s1 = (s1 + buf[i]) % GP_BASE;
		s2 = (s2 + s1) % GP_BASE;
	}
	return (s2 << 16) | s1;
}

// The CRC-32 register update by one byte, without pre- or post-conditioning (the register is the 32 low bits).
static unsigned long ref_crc_byte(unsigned long c, unsigned char b)
{
	c ^= b;
	for (int k = 0; k < 8; ++k) {
		if (c & 1)
			c = (c >> 1) ^ GP_POLY;
		else
			c = c >> 1;
	}
	return c;
}

// CRC-32 of buf[0..n-1] continued from the checksum c (its 32 low bits).
static unsigned long ref_crc32(unsigned long c, const unsigned char *buf, unsigned long n)
{
	c = (~c) & 0xffffffff;
	for (unsigned long i = 0; i < n; ++i)
		c = ref_crc_byte(c, buf[i]);
	return (~c) & 0xffffffff;
}

static unsigned long be32(const unsigned char *p)
{
	return ((unsigned long) p[0] << 24) | ((unsigned long) p[1] << 16) | ((unsigned long) p[2] << 8) | p[3];
}

static unsigned long le32(const unsigned char *p)
{
	return ((unsigned long) p[3] << 24) | ((unsigned long) p[2] << 16) | ((unsigned long) p[1] << 8) | p[0];
}

static int bytes_same(const unsigned char *a, const unsigned char *b, unsigned long n)
{
	for (unsigned long i = 0; i < n; ++i)
		if (a[i] != b[i])
			return 0;
	return 1;
}

static void bytes_copy(unsigned char *d, const unsigned char *s, unsigned long n)
{
	for (unsigned long i = 0; i < n; ++i)
		d[i] = s[i];
}

// A new object of exactly n bytes holding src[0..n-1] (NULL when the allocation fails).
static unsigned char *exact_copy(const unsigned char *src, unsigned n)
{
	unsigned char *p = malloc(n);
	if (p != NULL)
		bytes_copy(p, src, n);
	return p;
}

// A new object of exactly n bytes with any contents, and a snapshot of them in *snap (NULL when an allocation fails).
static unsigned char *exact_space(unsigned n, unsigned char **snap)
{
	unsigned char *p = malloc(n);
	unsigned char *q = malloc(n);
	if (p == NULL || q == NULL) {
		free(p);
		free(q);
		*snap = NULL;
		return NULL;
	}
	nondet_bytes(p, n);
	bytes_copy(q, p, n);
	*snap = q;
	return p;
}

// inflateInit2's windowBits check (zlib.h): accepted values.
static int inflate_wbits_ok(int w)
{
	if (w < 0)
		return w >= -15 && w <= -8;
	if (w >= 48)
		return 0;
	w &= 15;
	return w == 0 || (w >= 8 && w <= 15);
}

// Is a value one of inflate()'s documented return codes (zlib.h)?
static int inflate_code_ok(int r)
{
	return r == Z_OK || r == Z_STREAM_END || r == Z_NEED_DICT || r == Z_DATA_ERROR || r == Z_STREAM_ERROR ||
	       r == Z_MEM_ERROR || r == Z_BUF_ERROR;
}

// A z_stream with the default allocator (zalloc, zfree, opaque all Z_NULL: zlib uses zcalloc/zcfree, i.e. malloc and
// free) and any values in the fields the caller does not have to set.
static void stream_defaults(z_stream *s)
{
	s->zalloc = Z_NULL;
	s->zfree = Z_NULL;
	s->opaque = Z_NULL;
	s->next_in = Z_NULL;
	s->avail_in = 0;
	s->next_out = Z_NULL;
	s->avail_out = 0;
	pick(s->total_in);
	pick(s->total_out);
	pick(s->adler);
	pick(s->data_type);
	pick(s->reserved);
}

#endif