rfc_a2ulabel_utf8

For s without . or NUL and an output of at least one byte: xn-- + s becomes exactly the UTF-8 form (RFC 3629) of the code points ossl_punycode_decode gives for s into 512 elements, and a NUL. The result is -1 when that decoding fails, when it gives a code point above U+10FFFF, or when the allocation fails; it is 0 when the output does not fit.

spec: 72 lines of C
with its headers: 124 lines
status: Proved; 9 of 19

On this page

The spec

The spec is the C program harness/rfc_a2ulabel_utf8.c, 72 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 rfc_a2ulabel_utf8: A label with the ACE prefix becomes the UTF-8 form of its Punycode decoding. For any octets s
// without '.' and NUL (any length the allocator provides), decoded by ossl_punycode_decode into at most 512 code
// points (ossl_a2ulabel's label buffer, LABEL_BUF_SIZE), and any outlen >= 1, with an object of exactly outlen octets
// holding any values: ossl_a2ulabel of "xn--" followed by s returns -1 when that decoding fails or gives a code point
// above 0x10FFFF; else it returns 1, writes the UTF-8 form of the code points (RFC 3629, which excludes the surrogates
// U+D800..U+DFFF: they get three octets like their neighbours) and a NUL, and leaves the later octets unchanged when
// they fit in outlen octets, and returns 0 when they do not (when the allocation of its WPACKET record succeeds).
#include "laws_common.h"

static size_t utf8(unsigned int c, unsigned char *o) {   // RFC 3629 3: the octets of a code point c <= 0x10FFFF
	if (c < 0x80) {
		o[0] = c;
		return 1;
	}
	if (c < 0x800) {
		o[0] = 0xC0 | c >> 6;
		o[1] = 0x80 | (c & 0x3F);
		return 2;
	}
	if (c < 0x10000) {
		o[0] = 0xE0 | c >> 12;
		o[1] = 0x80 | (c >> 6 & 0x3F);
		o[2] = 0x80 | (c & 0x3F);
		return 3;
	}
	o[0] = 0xF0 | c >> 18;
	o[1] = 0x80 | (c >> 12 & 0x3F);
	o[2] = 0x80 | (c >> 6 & 0x3F);
	o[3] = 0x80 | (c & 0x3F);
	return 4;
}

int main(void) {
	// Choose the inputs: "xn--" and any octets but '.' and NUL, any outlen >= 1 and outlen octets
	size_t len = upto(PTRDIFF_MAX - 5);
	unsigned char *label = any_bytes(len + 5);          // "xn--", s, NUL
	unsigned int *cps = malloc(512 * sizeof(unsigned int));
	size_t outlen = upto(PTRDIFF_MAX);
	unsigned char *out = any_bytes(outlen), *saved = copy_of(out, outlen), *want = malloc(4 * 512 + 1);
	if (label == NULL || cps == NULL || out == NULL || saved == NULL || want == NULL || outlen == 0)
		return 0;
	label[0] = 'x';
	label[1] = 'n';
	label[2] = '-';
	label[3] = '-';
	label[len + 4] = 0;
	for (size_t i = 4; i < len + 4; i++)
		gp_assume(label[i] != '.' && label[i] != 0);
	// The decoding of s, and its UTF-8 form with a NUL in want[0..size)
	unsigned int count = 512;
	int valid = ossl_punycode_decode((const char *) label + 4, len, cps, &count) == 1;
	size_t size = 0;
	for (unsigned int j = 0; valid && j < count; j++)
		if (cps[j] > 0x10FFFF)
			valid = 0;
		else
			size = size + utf8(cps[j], want + size);
	want[size] = 0;
	size++;
	ossl_shim_zalloc_failed = 0;
	int r = ossl_a2ulabel((const char *) label, (char *) out, outlen);
	// Check. crypto/punycode.c: "If it does not start with xn--, it becomes U-label as is. Otherwise we try to decode it."
	if (ossl_shim_zalloc_failed)
		gp_assert(r == -1);
	else if (!valid)
		gp_assert(r == -1);
	else if (size <= outlen)
		gp_assert(r == 1 && bytes_eq(out, want, size) && bytes_eq(out + size, saved + size, outlen - size));
	else
		gp_assert(r == 0);
	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/rfc_a2ulabel_utf8.v:

Rocq

Theorem rfc_a2ulabel_utf8 : 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 rfc_a2ulabel_utf8 : harness_safe OpensslPunycode.contracts.rfc_a2ulabel_utf8.whole_prog.
Proof. exact (proj1 (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