Browse OpenSSL punycode specs (5 of 19)
Proofs / OpenSSL punycode / The standard
rfc_basic_first
If any byte before the last - is 0x80 or above, decoding fails. On success, the code points below 0x80 are exactly the bytes before the last -, in order (RFC 3492 3.1, 6.2).
- spec
- 38 lines of C
- with its headers
- 90 lines
- status
- Proved
- 5 of 19
On this page
The spec
The spec is the C program harness/rfc_basic_first.c, 38 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_basic_first: The octets before the last delimiter are the basic code points of the output, in order (RFC
// 3492 3.1). For any input (any octets, any length the allocator provides) and any capacity (any unsigned int), with
// an array of exactly that many elements holding any values: if an octet before the last '-' is not basic (0x80 or
// more), ossl_punycode_decode returns 0; when it returns 1, the code points of the output below 0x80, in order, are
// exactly the octets before the last '-' (none when there is no '-'), and all its other code points are inserted
// ones (0x80 or more: the decoder's n starts at initial_n = 0x80 and only grows).
#include "laws_common.h"
int main(void) {
// Choose the inputs: any octets, any capacity, any initial contents of the array
size_t len = upto(PTRDIFF_MAX);
unsigned char *input = any_bytes(len);
unsigned int cap = nondet_u32();
unsigned int *out = any_uints(cap);
if (input == NULL || out == NULL)
return 0;
size_t literal = last_delimiter(input, len); // the number of octets before the last '-'
unsigned int count = cap;
int r = ossl_punycode_decode((const char *) input, len, out, &count);
// Check. RFC 3492 6.2: "consume all code points before the last delimiter (if there is one) and copy them to
// output, fail on any non-basic code point"
for (size_t i = 0; i < literal; i++)
if (input[i] >= 0x80)
gp_assert(r == 0);
// Check. RFC 3492 3.1: "All basic code points appearing in the extended string are represented literally at the
// beginning of the basic string, in their original order, followed by a delimiter if (and only if) the number of
// basic code points is nonzero."
if (r == 1) {
size_t next = 0; // the literal octets seen so far
for (unsigned int j = 0; j < count; j++)
if (out[j] < 0x80) {
gp_assert(next < literal && out[j] == input[next]);
next++;
}
gp_assert(next == literal);
}
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_basic_first.v:
Theorem rfc_basic_first : 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:
Theorem rfc_basic_first : harness_safe OpensslPunycode.contracts.rfc_basic_first.whole_prog.
Proof. exact (proj1 (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.cpatch/units/packet_ext.cpatch/shim/ossl_shim.cquickproof/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.cand the parts ofcrypto/packet.cit 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.