Browse OpenSSL punycode specs (16 of 19)

rt_roundtrip

Any number of any 32-bit code points, encoded by an RFC 3492 encoder written in the spec, when the encoder succeeds and the encoding is shorter than 2^32 - 1 bytes (OpenSSL's input limit): OpenSSL decodes them back whenever (largest code point - 127) × count ≤ 2^32. Beyond that bound it decodes them back or refuses them (0), never to other code points.

spec: 91 lines of C
with its headers: 143 lines
status: Proved; 16 of 19

On this page

The spec

The spec is the C program harness/rt_roundtrip.c, 91 lines, shown whole as it is in the repository at 7556530. It includes harness/laws_common.h (52 lines). Its first comment states the property in full, with every bound.

// Law rt_roundtrip: OpenSSL decodes what RFC 3492's encoder writes. For any m code points (any number the allocator
// provides, any 32-bit values), encoded by encode() below (RFC 3492 6.3, the overflow checks of 6.4, maxint = 2^32 - 1)
// into an object of any size: when the encoding fits and has fewer than 2^32 - 1 octets (the most OpenSSL takes),
// ossl_punycode_decode, into an array of exactly m elements holding any values, gives back the m code points (result
// 1) whenever (largest code point - 127) * m <= 2^32; otherwise it gives them back or fails (0, *pout_length
// unchanged): there its i (insertion position plus delta) can pass 2^32 - 1 where the encoder's delta does not.
#include "laws_common.h"

static uint64_t rfc_adapt(uint64_t delta, uint64_t numpoints, int firsttime) {   // RFC 3492 6.1, adapt
	uint64_t k = 0;
	delta = firsttime ? delta / 700 : delta / 2;                            // damp = 700
	delta = delta + delta / numpoints;
	for (; delta > 455; k = k + 36)                                        // ((base - tmin) * tmax) div 2; base
		delta = delta / 35;                                                 // base - tmin
	return k + 36 * delta / (delta + 38);                                   // skew = 38
}
static int put(unsigned char *out, size_t room, size_t *len, uint64_t c) {   // output c, if there is room
	if (*len >= room)
		return 0;
	out[*len] = (unsigned char) c;
	*len = *len + 1;
	return 1;
}
static uint64_t digit(uint64_t d) { return d < 26 ? 'a' + d : '0' + d - 26; }   // RFC 3492 5, in lowercase
// RFC 3492 6.3 in 64-bit arithmetic: 1 with the encoding in out[0..*len), or 0 on an overflow or when out is full
static int encode(const unsigned int *cps, size_t m, unsigned char *out, size_t room, size_t *len) {
	uint64_t n = 128, delta = 0, bias = 72, b = 0, h, q, k, t;            // initial_n, initial_bias
	*len = 0;
	for (size_t j = 0; j < m; j++)        // "copy them to the output in order, followed by a delimiter if b > 0"
		if (cps[j] < 128) {
			if (!put(out, room, len, cps[j]))
				return 0;
			b = b + 1;
		}
	if (b > 0 && !put(out, room, len, '-'))
		return 0;
	for (h = b; h < m; n = n + 1) {
		uint64_t min = UINT64_MAX;        // "let m = the minimum {non-basic} code point >= n in the input"
		for (size_t j = 0; j < m; j++)
			if (cps[j] >= n && cps[j] < min)
				min = cps[j];
		if (delta > 0xFFFFFFFF || min - n > (0xFFFFFFFF - delta) / (h + 1))   // "fail on overflow"
			return 0;
		delta = delta + (min - n) * (h + 1);
		n = min;
		for (size_t j = 0; j < m; j++) {
			if (cps[j] < n) {             // "increment delta, fail on overflow"
				delta = delta + 1;
				if (delta > 0xFFFFFFFF)
					return 0;
			}
			if (cps[j] == n) {            // "output" delta as a generalized variable-length integer
				q = delta;
				for (k = 36;; k = k + 36) {   // t: tmin = 1, tmax = 26
					t = k <= bias ? 1 : k >= bias + 26 ? 26 : k - bias;
					if (q < t)
						break;
					if (!put(out, room, len, digit(t + (q - t) % (36 - t))))
						return 0;
					q = (q - t) / (36 - t);
				}
				if (!put(out, room, len, digit(q)))
					return 0;
				bias = rfc_adapt(delta, h + 1, h == b);
				delta = 0;
				h = h + 1;
			}
		}
		delta = delta + 1;
	}
	return 1;
}

int main(void) {
	// Choose the inputs: any number of any code points, any room for the encoding
	size_t m = upto(PTRDIFF_MAX / sizeof(unsigned int)), room = upto(PTRDIFF_MAX), len;
	unsigned int *cps = any_uints(m), *out = any_uints(m);
	unsigned char *encoding = malloc(room);
	if (cps == NULL || out == NULL || encoding == NULL || !encode(cps, m, encoding, room, &len) || len >= 0xFFFFFFFF)
		return 0;
	uint64_t largest = 0;
	for (size_t j = 0; j < m; j++)
		largest = cps[j] > largest ? cps[j] : largest;
	unsigned int count = (unsigned int) m;
	int r = ossl_punycode_decode((const char *) encoding, len, out, &count);
	// Check
	if (largest <= 127 || largest - 127 <= ((uint64_t) 1 << 32) / m)
		gp_assert(r == 1);
	gp_assert(r == 1 ? count == m && uints_eq(out, cps, m) : r == 0 && count == m);
	return 0;
}

harness/laws_common.h, 52 lines

// laws_common.h: trivial helpers shared by the short laws (each law includes it once). No models, no algorithms.
#include <stdint.h>
#include <stdlib.h>
#include "quickproof.h"
#include "crypto/punycode.h"                         // ossl_punycode_decode, ossl_a2ulabel
// OpenSSL's allocator in this build (patch/shim/ossl_shim.c): set to 1 when CRYPTO_zalloc fails (malloc may fail at
// any call in the theorems), and the number of its blocks not freed yet.
extern int ossl_shim_zalloc_failed;
extern long ossl_shim_live;
static size_t upto(size_t max) {                     // any value from 0 to max
	size_t value = nondet_size();
	return value < max ? value : max;
}
static unsigned char *any_bytes(size_t n) {          // a new object of n arbitrary bytes (NULL if malloc fails)
	unsigned char *bytes = malloc(n);
	if (bytes != NULL)
		nondet_bytes(bytes, n);
	return bytes;
}
static unsigned int *any_uints(size_t n) {           // a new array of n arbitrary unsigned ints (NULL if malloc fails)
	unsigned int *values = malloc(n * sizeof(unsigned int));
	for (size_t i = 0; values != NULL && i < n; i++)
		values[i] = nondet_u32();
	return values;
}
static unsigned char *copy_of(const unsigned char *source, size_t n) {   // a new object holding source[0..n-1]
	if (source == NULL)                                                   // (NULL if source is or malloc fails)
		return NULL;
	unsigned char *copy = malloc(n);
	for (size_t i = 0; copy != NULL && i < n; i++)
		copy[i] = source[i];
	return copy;
}
static int bytes_eq(const unsigned char *a, const unsigned char *b, size_t n) {   // a[0..n-1] == b[0..n-1]
	for (size_t i = 0; i < n; i++)
		if (a[i] != b[i])
			return 0;
	return 1;
}
static int uints_eq(const unsigned int *a, const unsigned int *b, size_t n) {     // a[0..n-1] == b[0..n-1]
	for (size_t i = 0; i < n; i++)
		if (a[i] != b[i])
			return 0;
	return 1;
}
static size_t last_delimiter(const unsigned char *s, size_t n) {   // the position of the last '-', 0 if none
	size_t last = 0;
	for (size_t i = 0; i < n; i++)
		if (s[i] == '-')
			last = i;
	return last;
}

The theorem

QuickProof generated this statement from the spec, in src/contracts/rt_roundtrip.v:

Rocq

Theorem rt_roundtrip : harness_safe whole_prog.

src/contracts/laws.v states it on the spec's own program, whole_prog (the spec linked with the code under test), with its proof:

Rocq

Theorem rt_roundtrip : harness_safe OpensslPunycode.contracts.rt_roundtrip.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 OpensslPunycode.contracts.suite.suite)))))))))))))))). Qed.

Read as a statement about runs, it says that no run of the program has undefined behaviour or a failing check, for every value the spec can draw. That reading rests on VST's adequacy theorem, which is not yet instantiated in Rocq (formerly Coq) for QuickProof's environment.

The C files (units) its program links

crypto/punycode.c
patch/units/packet_ext.c
patch/shim/ossl_shim.c
quickproof/libc/libc.c

What it leaves out

What the first comment of the spec excludes, and its bounds.
Like every spec of this proof: termination (a run that never returns is not a counterexample), one thread, and binaries built by a compiler (the theorem is about the code as CompCert defines C for x86-64, in a release build, compiled against a small header shim instead of OpenSSL's generated headers).
The rest of OpenSSL: only crypto/punycode.c and the parts of crypto/packet.c it reaches are code under test.

The summary page says what the proof as a whole covers.

How it was proved

AI agents wrote the proof, and Rocq checks it. qp verify passes on this repository: this statement is the one generated from the spec at the contract commit, and its proof uses only Rocq's standard axioms and VST's abstract malloc library.

The spec#

The theorem#

What it leaves out#

How it was proved#

The spec

The theorem

What it leaves out

How it was proved