Constrained Resource Identifiers (CRIs) are a compact CBOR form of URIs for small devices. The draft that defines them resolves a CRI reference in one section and converts it to an equivalent URI reference in another. On three inputs the two procedures lead to different addresses, so a device and a gateway following different sections could reach different resources.
The problem
draft-ietf-core-href-30 defines, in Section 5.3, how a CRI reference is resolved against a base CRI, and in Section 6.1 how a CRI reference is converted to what the draft calls the equivalent URI reference. If the two are equivalent, resolving the CRI reference and then converting the result must give the same URI as converting the reference and resolving it with RFC 3986.
They do not, on three inputs. (A) The reference ["t", null, ["p"]], the CRI for t:/p, resolved against s://h yields t://h/p by Section 5.3, whereas the equivalent URI reference has no authority and RFC 3986 gives a reference with a scheme its own authority. (B) The reference [1], which removes the last segment of the base path, is converted to the empty URI reference, which denotes the base itself. (C) The reference [1, ["", "a"]] is converted to /a, an absolute path, whereas Section 5.3 gives /b//a for the base path /b/c.
How it was shown
Each case is written out step by step, and one sentence of correction is proposed for each. On an enumeration of 720,120 base–reference pairs with an authority, the two computations differ on 93,810; after the corrections they differ on none of the 713,660 pairs that remain convertible (the corrections refuse 10,540 pairs and admit 4,080 that the draft's syntax check rejects).
In Lean 4 (core library only; axioms propext and Quot.sound; no sorry) the counterexamples are checked by kernel evaluation, and the corrected conversion of a discard-form reference, resolved per RFC 3986, is proved equal to the Section 5.3 resolution for every base with an authority and paths of any length. No claim is made about bases without an authority. The Python model of RFC 3986 Section 5.2 was checked against the 42 examples of its Section 5.4 before use.
Check it by hand
Response
The three cases were posted to the CoRE working group list on 29 Oct 2026, while the draft was in its final review before publication. On 31 Oct an author of the draft replied, thanking for the analysis, saying it would take a few days to check against existing implementations, noting that the corrections need editorial fitting and that Section 5.3 was intended for relative references, and stating that bugs need to be fixed and the necessary corrections will be made.
As of 6 Nov 2026, revision -30 is the current one.
Links
Cite as
Nobuo Otoi (ba-cybersecurity.com). Three Counterexamples and One-Sentence Corrections for IETF Internet-Draft draft-ietf-core-href-30, with a Lean Proof for the Path Rule. 2026. https://doi.org/10.5281/zenodo.23760463.
@misc{otoi2026cri,
author = {Otoi, Nobuo},
title = {Three Counterexamples and One-Sentence Corrections for IETF Internet-Draft draft-ietf-core-href-30, with a Lean Proof for the Path Rule},
year = {2026},
doi = {10.5281/zenodo.23760463},
publisher = {Zenodo},
howpublished = {\url{https://ba-cybersecurity.com/research/cri-reference-resolution/}},
note = {Preprint, version 1. Code and proofs: https://github.com/otoinobuo/cri-verify}
}
Preprint published 29 Oct 2026 · List post 29 Oct 2026 · Author's reply 31 Oct 2026 · This page: updated 7 Nov 2026 · Permanent address: https://ba-cybersecurity.com/research/cri-reference-resolution/