Page actions
instrument mechanism / verified-clean
IPv6 Address Explorer mechanism
The inspectable method record for IPv6 Address Explorer, kept separate from implementation and qualification.
Model scope
The formulas are standard in principle, but the specification is not sufficiently precise to pass verification. The exact compression tie rule, inclusive network-range definition, supported input grammar, and special-purpose classification precedence must be documented. The honest_label field is empty; it should state that classification depends on a bundled, potentially stale IANA registry and that textual normalization follows a defined canonical-output policy.
- The prefix-masking formula is only named, not fully specified: network_start should be address AND mask, and network_end should be network_start plus 2^(128-prefix_length)-1; it must be defined whether the reported network range is inclusive.
- The zero-run compression rule is underspecified: canonical IPv6 text requires compressing only the longest run of two or more zero hextets, with the leftmost run winning ties.
- Address-class determination needs explicit precedence and exact ranges. In particular, special-purpose registry entries can overlap broad categories such as global unicast, and the meaning of global must be defined.
- The supported IPv6 input grammar is unspecified, including whether IPv4-embedded notation, uppercase hexadecimal, and zone identifiers such as %25eth0 are accepted.
Units and conventions
- prefix_length is an integer number of bits in the range 0 through 128.
- Each IPv6 address represents 128 bits split into eight 16-bit hextets; hexadecimal values are case-insensitive on input.
- Network ranges are inclusive and consist of network_start through network_end.
- Canonical output uses lowercase hexadecimal, suppresses leading zeroes in hextets, and applies the canonical :: compression rule.
- The test vectors classify addresses using link-local fe80::/10, ULA fc00::/7, multicast ff00::/8, and global unicast 2000::/3 after excluding more-specific special-purpose registry entries.
Inspectable vector
One of 4 source-bound review vectors:
{
"inputs": {
"ipv6_address": "2001:4860:4860:0000:0000:0000:0000:8888",
"prefix_length": 64
},
"expected_outputs": {
"expanded_form": "2001:4860:4860:0000:0000:0000:0000:8888",
"compressed_form": "2001:4860:4860::8888",
"network_range": {
"network_start": "2001:4860:4860:0000:0000:0000:0000:0000",
"network_end": "2001:4860:4860:0000:ffff:ffff:ffff:ffff"
},
"address_class": "global"
},
"working": "Parse into hextets [2001,4860,4860,0000,0000,0000,0000,8888]. The longest zero run is hextets 4-7, so compress it: 2001:4860:4860::8888. For /64, retain the first 4 hextets and zero the last 4: network_start = 2001:4860:4860:0000:0000:0000:0000:0000. Host bits = 128-64 = 64. Maximum host value = 2^64-1 = 0xffffffffffffffff, which is four ffff hextets. Therefore network_end = 2001:4860:4860:0000:ffff:ffff:ffff:ffff. The address begins with 2000::/3 and is not in the listed special ranges, so it is global."
}Failure boundary
BREAK_CLAIMED · SELF_FLAGGED
The computational cases remain exactly representable when implemented with 128-bit arithmetic, but the link-local vector exposes an under-specified convention: a bare fe80::1 lacks the interface zone needed for many real operations. The explorer must distinguish syntactic classification from scoped operational validity. Extreme all-ones input also breaks implementations that use JavaScript Number arithmetic instead of exact 128-bit handling.
Other records
Sources and evidence
These pointers bind the page to evidence. They do not grant authority or collapse verification into deployment.
VERIFIED_LEDGER.jsonevidence-tranche3/tranche3-results.jsonBOUNDARY_HAZARD_CATALOG.json