rfc_samples

The 19 sample strings of RFC 3492 7.1 decode to exactly the code points the RFC lists.

spec: 79 lines of C
with its headers: 131 lines
status: Proved; 4 of 19

On this page

The spec

The spec is the C program harness/rfc_samples.c, 79 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_samples: The sample strings of RFC 3492 7.1, (A) to (S), decode to the code points the RFC lists. Each
// Punycode string is decoded into an array of exactly as many elements as the RFC lists code points, holding any
// values: ossl_punycode_decode returns 1, reports that number and gives those code points, in order. (In (D), (I) to
// (N) and (P) the RFC writes some code points with "U+" instead of "u+", and in (I) one digit in uppercase: its
// optional mixed-case annotation (appendix A), which a decoder may ignore; the code points are the numbers listed.)
#include "laws_common.h"

// RFC 3492 7.1: the Punycode strings ("the ACE prefix is not shown") and how many code points each has
static const char *const encoded[19] = {
	"egbpdaj6bu4bxfgehfvwxn", "ihqwcrb4cv8a8dqg056pqjye", "ihqwctvzc91f659drss3x8bo0yb",
	"Proprostnemluvesky-uyb24dma41a", "4dbcagdahymbxekheh6e0a7fei0b",
	"i1baa7eci9glrd9b2ae1bj0hfcgg6iyaf8o0a1dig0cd", "n8jok5ay5dzabd5bym9f0cm5685rrjetr6pdxa",
	"989aomsvi5e83db1d2a355cv1e0vak1dwrv93d5xbh15a0dt30a5jpsd879ccm6fea98c",
	"b1abfaaepdrnnbgefbaDotcwatmq2g4l", "PorqunopuedensimplementehablarenEspaol-fmd56a",
	"TisaohkhngthchnitingVit-kjcr8268qyxafd2f1b9g", "3B-ww4c5e180e575a65lsy2b",
	"-with-SUPER-MONKEYS-pc58ag80a8qai00g7n9n", "Hello-Another-Way--fc4qua05auwb3674vfr0b",
	"2-u9tlzr9756bt3uc0v", "MajiKoi5-783gue6qz075azm5e", "de-jg4avhby1noc0d", "d9juau41awczczp",
	"-> $1.00 <--"
};
static const unsigned char points[19] = {17, 9, 9, 22, 22, 30, 18, 24, 28, 40, 31, 8, 24, 25, 8, 13, 9, 7, 11};
// RFC 3492 7.1: the code points of (A) to (S), one sample after the other
static const unsigned int decoded[355] = {
	/* A */ 0x0644, 0x064A, 0x0647, 0x0645, 0x0627, 0x0628, 0x062A, 0x0643, 0x0644, 0x0645, 0x0648, 0x0634,
	        0x0639, 0x0631, 0x0628, 0x064A, 0x061F,
	/* B */ 0x4ED6, 0x4EEC, 0x4E3A, 0x4EC0, 0x4E48, 0x4E0D, 0x8BF4, 0x4E2D, 0x6587,
	/* C */ 0x4ED6, 0x5011, 0x7232, 0x4EC0, 0x9EBD, 0x4E0D, 0x8AAA, 0x4E2D, 0x6587,
	/* D */ 0x0050, 0x0072, 0x006F, 0x010D, 0x0070, 0x0072, 0x006F, 0x0073, 0x0074, 0x011B, 0x006E, 0x0065,
	        0x006D, 0x006C, 0x0075, 0x0076, 0x00ED, 0x010D, 0x0065, 0x0073, 0x006B, 0x0079,
	/* E */ 0x05DC, 0x05DE, 0x05D4, 0x05D4, 0x05DD, 0x05E4, 0x05E9, 0x05D5, 0x05D8, 0x05DC, 0x05D0, 0x05DE,
	        0x05D3, 0x05D1, 0x05E8, 0x05D9, 0x05DD, 0x05E2, 0x05D1, 0x05E8, 0x05D9, 0x05EA,
	/* F */ 0x092F, 0x0939, 0x0932, 0x094B, 0x0917, 0x0939, 0x093F, 0x0928, 0x094D, 0x0926, 0x0940, 0x0915,
	        0x094D, 0x092F, 0x094B, 0x0902, 0x0928, 0x0939, 0x0940, 0x0902, 0x092C, 0x094B, 0x0932, 0x0938,
	        0x0915, 0x0924, 0x0947, 0x0939, 0x0948, 0x0902,
	/* G */ 0x306A, 0x305C, 0x307F, 0x3093, 0x306A, 0x65E5, 0x672C, 0x8A9E, 0x3092, 0x8A71, 0x3057, 0x3066,
	        0x304F, 0x308C, 0x306A, 0x3044, 0x306E, 0x304B,
	/* H */ 0xC138, 0xACC4, 0xC758, 0xBAA8, 0xB4E0, 0xC0AC, 0xB78C, 0xB4E4, 0xC774, 0xD55C, 0xAD6D, 0xC5B4,
	        0xB97C, 0xC774, 0xD574, 0xD55C, 0xB2E4, 0xBA74, 0xC5BC, 0xB9C8, 0xB098, 0xC88B, 0xC744, 0xAE4C,
	/* I */ 0x043F, 0x043E, 0x0447, 0x0435, 0x043C, 0x0443, 0x0436, 0x0435, 0x043E, 0x043D, 0x0438, 0x043D,
	        0x0435, 0x0433, 0x043E, 0x0432, 0x043E, 0x0440, 0x044F, 0x0442, 0x043F, 0x043E, 0x0440, 0x0443,
	        0x0441, 0x0441, 0x043A, 0x0438,
	/* J */ 0x0050, 0x006F, 0x0072, 0x0071, 0x0075, 0x00E9, 0x006E, 0x006F, 0x0070, 0x0075, 0x0065, 0x0064,
	        0x0065, 0x006E, 0x0073, 0x0069, 0x006D, 0x0070, 0x006C, 0x0065, 0x006D, 0x0065, 0x006E, 0x0074,
	        0x0065, 0x0068, 0x0061, 0x0062, 0x006C, 0x0061, 0x0072, 0x0065, 0x006E, 0x0045, 0x0073, 0x0070,
	        0x0061, 0x00F1, 0x006F, 0x006C,
	/* K */ 0x0054, 0x1EA1, 0x0069, 0x0073, 0x0061, 0x006F, 0x0068, 0x1ECD, 0x006B, 0x0068, 0x00F4, 0x006E,
	        0x0067, 0x0074, 0x0068, 0x1EC3, 0x0063, 0x0068, 0x1EC9, 0x006E, 0x00F3, 0x0069, 0x0074, 0x0069,
	        0x1EBF, 0x006E, 0x0067, 0x0056, 0x0069, 0x1EC7, 0x0074,
	/* L */ 0x0033, 0x5E74, 0x0042, 0x7D44, 0x91D1, 0x516B, 0x5148, 0x751F,
	/* M */ 0x5B89, 0x5BA4, 0x5948, 0x7F8E, 0x6075, 0x002D, 0x0077, 0x0069, 0x0074, 0x0068, 0x002D, 0x0053,
	        0x0055, 0x0050, 0x0045, 0x0052, 0x002D, 0x004D, 0x004F, 0x004E, 0x004B, 0x0045, 0x0059, 0x0053,
	/* N */ 0x0048, 0x0065, 0x006C, 0x006C, 0x006F, 0x002D, 0x0041, 0x006E, 0x006F, 0x0074, 0x0068, 0x0065,
	        0x0072, 0x002D, 0x0057, 0x0061, 0x0079, 0x002D, 0x305D, 0x308C, 0x305E, 0x308C, 0x306E, 0x5834,
	        0x6240,
	/* O */ 0x3072, 0x3068, 0x3064, 0x5C4B, 0x6839, 0x306E, 0x4E0B, 0x0032,
	/* P */ 0x004D, 0x0061, 0x006A, 0x0069, 0x3067, 0x004B, 0x006F, 0x0069, 0x3059, 0x308B, 0x0035, 0x79D2,
	        0x524D,
	/* Q */ 0x30D1, 0x30D5, 0x30A3, 0x30FC, 0x0064, 0x0065, 0x30EB, 0x30F3, 0x30D0,
	/* R */ 0x305D, 0x306E, 0x30B9, 0x30D4, 0x30FC, 0x30C9, 0x3067,
	/* S */ 0x002D, 0x003E, 0x0020, 0x0024, 0x0031, 0x002E, 0x0030, 0x0030, 0x0020, 0x003C, 0x002D
};

int main(void) {
	size_t at = 0;                                      // where the code points of sample s start
	for (int s = 0; s < 19; s++) {
		size_t len = 0;
		while (encoded[s][len] != 0)
			len++;
		unsigned int *out = any_uints(points[s]);
		if (out == NULL)
			return 0;
		unsigned int count = points[s];
		int r = ossl_punycode_decode(encoded[s], len, out, &count);
		// Check
		gp_assert(r == 1 && count == points[s] && uints_eq(out, decoded + at, count));
		at += points[s];
		free(out);
	}
	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_samples.v:

Rocq

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