[zero-aska]

This is the first slice of the plan in #1, which I claimed there. It is built to bar v2, in the same shape as hostname, punycode, bech32 and hpack. Two self-reviews have run on it, the first of the statements against X.690 and X.680 and the second of the tests and the page, each finding checked by a second agent; the changes they led to are listed at the end.

What it does

One DER element (Rec. ITU-T X.690, 02/2021), nested to any depth, read and written on List UInt8, with the tree type Der.Element (Spec/Element.lean):

• Der.decode b: the element at the start of the input, and the octets after it;
• Der.decodeAll b: the element that is the whole input;
• Der.encode e, for any tree;
• Der.valid e: whether this slice accepts a tree;
• Der.readInt c and Der.writeInt z: the contents octets of an INTEGER.

The reader checks what DER fixes for one element:

• identifier octets with tag numbers of any size, the high form only from 31 and with no leading zero digit (8.1.2);
• length octets in the definite form and the fewest octets: the long form only from 128, no leading zero octet, at most 126 octets, and neither 0x80 nor 0xFF as the first (8.1.3, 10.1);
• the form of every universal type: 8, 11, 16, 17 and 29 constructed, 15 and 37 up either way, the rest primitive (clause 8, 10.2), and tag 0 refused;
• BOOLEAN 00 or FF (11.1), INTEGER and ENUMERATED in the fewest octets (8.3.2, 8.4), NULL empty (8.8.2).

The contents of the other types, the order of SET components and DEFAULT components are left for later slices. A reader with no schema cannot check the last two. Spec/Defs.lean lists the clauses left unchecked.

What is proved

Spec.lean has 11 statements. lake comparator --paranoid accepts them under all six kernels bundled with Lean 4.35.0, using only propext, Classical.choice and Quot.sound, in about 20 seconds. There is no sorry outside the challenge file.

Spec/Defs.lean writes the encoding from X.690: identifier (8.1.2), lengthOctets (8.1.3, 10.1), der, IntegerContents (8.3.1, 8.3.2), integerValue (8.3.3), and Valid, the elements this slice accepts. It shares nothing with the code but the tree type.

• decode_iff: decode b = some (v, rest) ↔ Valid v ∧ b = der v ++ rest. The reader accepts exactly a DER encoding of an element this slice accepts, followed by anything. So it never reads past the end of its input, every element lies inside its parent's contents, and writing back what it read gives the same octets.
• encoding_unique: two accepted elements whose encodings start the same input are equal, and so is what follows. This is the plan's non-malleability claim. It is about the tree: for the contents of types this slice does not check, two contents octet strings for the same value are two trees.
• encode_eq, valid_iff: the writer writes der for every tree, and Der.valid decides Valid.
• decode_encode, decodeAll_iff: reading what the writer wrote gives the element back, and the whole input is one element exactly when it is an encoding.
• readInt_iff, writeInt_spec, writeInt_unique: readInt accepts exactly the contents X.690 allows and gives their two's complement value, writeInt writes allowed contents, and they are the only ones for that integer.
• x690_examples, x690_rejects: X.690's examples (lengths 38 and 201, BOOLEAN TRUE, the primitive "Jones" of 8.23.5), a tag number of 201 in the high form worked by hand, and nineteen inputs that each break a rule, among them the two constructed forms of "Jones" that DER forbids.

The proofs go through a reader with fuel and a limit: each element must fit in the octets its parent has left, and the fuel never runs out because each element takes at least two octets.

Time

No proof bounds time. The reader is written to be linear in its input: it measures an element's contents with take and never the rest of the input, and adds up long tag numbers and lengths by halves. A tree nested 100,000 deep reads in 0.2 s. The writer is not linear in the nesting depth: each level copies what it holds, so its time grows with the square of the depth; writing 10,000 levels takes about 1.6 s and 100,000 about 190 s. Der.valid writes and measures what each level holds, so its time grows about with the cube of the depth: about 3.4 s for 1,000 levels and 38 s for 2,000. The tests time only nested requests, each in a process of its own that must answer within 60 seconds: reading 10,000 and 100,000 levels, writing 10,000, and valid on 1,000. The page says so.

Differential tests

tests/TEST-RESULTS.md: 1,613,447 inputs, seed 20261027, 0 failures, with no oracle left out.

• A model of X.690 in Python, sharing nothing with the Lean code, must answer X.690's examples as the standard gives them (14 of 14). Every answer of the tool equals the model's. The model reads the tool's encoding back as the tree for every tree the slice accepts (100,536), and for all 200,412 trees asked valid, the answer holds exactly when the encoding reads back as the tree.

• Four oracles:

  • Go golang.org/x/crypto/cryptobyte v0.25.0, pinned by go.mod and go.sum;
  • Go encoding/asn1 of the installed Go, go1.24.7: not pinned, and the record gives the version;
  • the Rust asn1 crate 0.24.1, pinned by Cargo.lock;
  • OpenSSL 3.0.13 libcrypto, whose version the script checks, through a C wrapper.

  Each reads elements with its own reader and checks BOOLEAN and INTEGER with its own readers. encoding/asn1, rust-asn1 and OpenSSL also check NULL; cryptobyte has no NULL reader. OpenSSL also checks ENUMERATED, with d2i_ASN1_ENUMERATED.

• Named differences. A disagreement is allowed only for a named reason the model confirms: read, with the rules the oracle reads by, gives the oracle's answer. Beyond that, for every element each oracle reads (1,085,584), the model with that oracle's rules must give its answer, whether or not it agrees with the tool, and it does for all of them. The largest:

  • cryptobyte refuses every tag number of 31 or more (139,219);
  • encoding/asn1 and OpenSSL refuse tag numbers above 2^31 - 1, and rust-asn1 above 2^32 - 1;
  • OpenSSL reads BER: lengths with leading zeros (26,465) or in the long form below 128 (17,622), the indefinite length (7,214), and any octet as a BOOLEAN (4,087). Beyond BER, it also reads encodings BER forbids as well: a first subsequent tag octet 0x80 (47,215; 8.1.2.4.2 c) and the high form below 31 (36,142; 8.1.2.2);
  • all four read universal tag 0 and universal types in the wrong form, and the Go and Rust oracle programs check no ENUMERATED contents.

• Inputs:

  • every input of up to two octets;
  • every identifier and initial length octet;
  • lengths of 5 to 126 octets that a reader skipping leading zeros, or keeping the length modulo 2^32 or 2^64, would fit to the contents after them;
  • lengths around each form boundary, up to 100,000, also with up to 126 length octets;
  • tag numbers up to 2^64 and of 1,000 octets;
  • every universal tag 0 to 40 in both forms;
  • every INTEGER and ENUMERATED of up to two octets;
  • chains nested 10,000 and 100,000 deep, and valid on chains 1,000 deep;
  • the 484 ECDSA P-256 signatures of Wycheproof, checked by SHA-256 (all 7 flagged BerEncodedSignature refused; the 3 flagged ones accepted are elements this slice accepts, wrong in something it does not check);
  • 100,000 random trees, encoded, mutated nine ways (among them lengths with 1 to 125 leading zero octets), and a copy of each with one element the slice does not accept, which the model checks;
  • malformed requests and the command line.

• Planted bugs: tests/plant_bugs.py plants 37 bugs, 31 in Der/Basic.lean and 6 in Main.lean, and compares with the model alone; all 37 are caught (tests/PLANTED-BUGS.md). Among them:

  • the long form read below 128, a leading zero length octet, and 0x80 read as length 0;
  • a leading zero length octet read from 5 length octets on, and a length kept modulo 2^32;
  • a tag number below 31 in the high form, and a first subsequent tag octet 0x80;
  • a BOOLEAN 01, an INTEGER with a redundant leading octet, and an ENUMERATED not checked;
  • an element running one octet past its parent;
  • valid taking a class of 4, or not looking inside a constructed element.

Not proved

These are listed on the page:

• the contents of REAL, BIT STRING, OBJECT IDENTIFIER, RELATIVE-OID, the IRI types, the strings, the times, and the components of EXTERNAL, EMBEDDED PDV and CHARACTER STRING;
• rules that depend on the ASN.1 type: SET and SET OF order, and DEFAULT components;
• time and memory;
• the request handling in Main.lean, which the tests cover.

Re-check

lake build
lake comparator --paranoid
python3 tests/run_tests.py      # Go, cargo and libssl-dev for the oracles
python3 tests/plant_bugs.py

Changes from the self-review

• ENUMERATED is checked like INTEGER (8.4), in Valid, the code, the model and the tests.
• encode_eq holds for every tree, and Der.valid with valid_iff says which trees the slice accepts.
• x690_examples adds a tag number of 201 in the high form, worked by hand; x690_rejects grows to nineteen inputs with two ENUMERATED ones, and its length with a leading zero octet now breaks that rule alone.
• The pages list the clauses whose contents are not checked, say that encoding_unique is about the tree, and state the SET order and the length bound as they are.
• The test record no longer calls every Wycheproof signature the tool accepts a DER element.

From the second review, of the tests and the page:

• Lengths: the tests now read lengths of 5 to 126 octets with leading zero octets, and with values that wrap to 128 modulo 2^32 and 2^64, each followed by the contents a wrong reading would fit; the random trees pad a length with 1 to 125 zero octets, not always one; and two planted bugs the tests missed before, a leading zero octet read from 5 length octets on and a length kept modulo 2^32, are caught.
• Time: the page says Der.valid takes time growing about with the cube of the nesting depth (3.4 s for 1,000 levels, 38 s for 2,000), not the square, and that the tests time only nested requests; they now ask valid of chains 1,000 deep under the 60-second limit.
• Oracle rules: on every element an oracle reads, the model with that oracle's rules must give its answer, and any element where it does not is a failure, not only a count.
• Spoiled trees: the copy with one element the slice does not accept no longer gives a constructed element the reserved universal number 15, which made about 0.6% of them acceptable; the model checks that it accepts none of them.
• OpenSSL's reasons no longer call a tag number below 31 in the high form, a first subsequent tag octet 0x80 or the initial length octet 0xFF BER, since BER forbids them too, and say BER allows the constructed form only for the string types and the types encoded as strings.
• The oracle descriptions say cryptobyte checks BOOLEAN and INTEGER and has no NULL reader, and that encoding/asn1 is the installed Go's, its version recorded, not pinned.
• The page says the writer writes Spec.der for every tree, which is the encoding X.690 gives for a tree this slice accepts, apart from the contents of the types it does not check; and that the class can be any number, with Der.valid accepting only 0 to 3 (also in SPEC.md and the docstring of Spec/Element.lean). The docstrings of Der.encode, Spec.der and Spec.encode_eq say the same.
• The OpenSSL oracle checks ENUMERATED with d2i_ASN1_ENUMERATED; with that in OpenSSL's rules, the model still gives OpenSSL's answer on every element, and no difference from the tool is put down to ENUMERATED for it.

Review asks

• The universal-tag forms. The constructed set {8, 11, 16, 17, 29} and the reserved tags 15 and 37 up come from X.680 Table 1 and the clauses of X.690 cited in Spec/Defs.lean. Is accepting both forms for the reserved tags right, or should they be refused? One Wycheproof vector, a SEQUENCE retagged as universal 15, shows the effect.
• The length bound. Valid asks for lengths below 256^126, from 8.1.3.5 c. Is that the right way to state it?
• What a schema-free reader can claim. Is the page clear enough that "one encoding per element" is about the tree, not about ASN.1 values of a given type?

🤖 Generated with Claude Code

https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd