cpio: recognize NUL-padded trailer names

cpio/LAWS.bend

@@ -2,7 +2,7 @@
 # the value; a header reads back as itself; and parsing an archive built from
 # any list of entries, in either format, gives the entries back. The last
 # holds for the entries an archive can hold (CpioEntry.valid: sizes that fit
-# in 32 bits, a name other than "TRAILER!!!", canonical Octets).
+# in 32 bits, a name other than "TRAILER!!!" followed only by NULs).
 #
 # Vectors: digits in both cases, a non-digit and a short field refused, the
 # crc format's checksum, the bytes of a one-file archive (computed from
@@ -66,6 +66,28 @@ law empty_archive_crc:
 law trailing_bytes:
   {C.Cpio.parse(B.Octets.append(C.Cpio.build(C.CpioCrc{}, [C.CpioEntry.file("a", 33188, B.Octets.of_string("hi"))]), B.Octets.zeros(12n))) == Done{[C.CpioEntry.file("a", 33188, B.Octets.of_string("hi"))]} : Result<&2, &2, C.CpioError, List<&2, C.CpioEntry>>}
 
+# namesize 12 includes two NULs; the two further NULs align the header.
+def padded_trailer() -> B.Octets:
+  B.Octets.append(C.CpioHeader.encode(C.CpioHeader{C.CpioNewc{}, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 12, 0}), B.Octets.append(B.Octets.of_string("TRAILER!!!"), B.Octets.zeros(4n)))
+
+law padded_trailer_empty:
+  {C.Cpio.parse(padded_trailer()) == Done{[]} : Result<&2, &2, C.CpioError, List<&2, C.CpioEntry>>}
+
+law padded_trailer_after_entry:
+  {C.Cpio.parse(B.Octets.append(B.Octets.take(116n, C.Cpio.build(C.CpioNewc{}, [C.CpioEntry.file("a", 33188, B.Octets.of_string("hi"))])), padded_trailer())) == Done{[C.CpioEntry.file("a", 33188, B.Octets.of_string("hi"))]} : Result<&2, &2, C.CpioError, List<&2, C.CpioEntry>>}
+
+law trailer_name_suffix:
+  {C.Cpio.is_trailer_name(B.Octets.append(C.Cpio.trailer_name(), B.Octets.zeros(3n))) == True{} : Bool}
+
+law non_trailer_suffix:
+  {C.Cpio.is_trailer_name(B.Octets.append(C.Cpio.trailer_name(), B.Octets.of_list([0, 65]))) == False{} : Bool}
+
+law non_trailer_entry:
+  {C.Cpio.parse(C.Cpio.build(C.CpioNewc{}, [C.CpioEntry{0, 0, 0, 0, 1, 0, 0, 0, 0, 0, B.Octets.append(C.Cpio.trailer_name(), B.Octets.of_list([0, 65])), B.Octets.empty()}])) == Done{[C.CpioEntry{0, 0, 0, 0, 1, 0, 0, 0, 0, 0, B.Octets.append(C.Cpio.trailer_name(), B.Octets.of_list([0, 65])), B.Octets.empty()}]} : Result<&2, &2, C.CpioError, List<&2, C.CpioEntry>>}
+
+law malformed_padded_trailer:
+  {C.Cpio.parse(B.Octets.append(C.CpioHeader.encode(C.CpioHeader{C.CpioNewc{}, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 12, 0}), B.Octets.append(B.Octets.of_string("TRAILER!!!"), B.Octets.of_list([0, 65])))) == Fail{C.CpioNoNul{}} : Result<&2, &2, C.CpioError, List<&2, C.CpioEntry>>}
+
 # Vectors: malformed archives
 
 law reject_empty:

cpio/PROOF.bend

@@ -564,3 +564,21 @@ def Laws.reject_no_nul():
 
 def Laws.valid_example():
   (({==}, ({==}, {==})), Unit{})
+
+def Laws.padded_trailer_empty():
+  {==}
+
+def Laws.padded_trailer_after_entry():
+  {==}
+
+def Laws.trailer_name_suffix():
+  {==}
+
+def Laws.non_trailer_suffix():
+  {==}
+
+def Laws.malformed_padded_trailer():
+  {==}
+
+def Laws.non_trailer_entry():
+  {==}

cpio/README.md

@@ -11,7 +11,7 @@ format's checksum. Byte strings are `Octets` (bend-osdev-bytes).
   "New CRC Format"; BSD-licensed documentation).
 * The Linux kernel's documentation of the initramfs buffer format
   (`Documentation/driver-api/early-userspace/buffer-format.rst`): the
-  documentation only, not the kernel's code.
+  documentation only, not the kernel's code: [initramfs buffer format](https://docs.kernel.org/driver-api/early-userspace/buffer-format.html).
 
 Each entry is a 110-byte header, the name, and the data. The header is the
 six-byte magic and thirteen fields of eight ASCII hex digits each: `ino`,
@@ -27,7 +27,10 @@ Choices this package makes where the specification leaves them open: it
 writes upper-case hex digits and reads either case; it writes the trailer
 with `nlink` 1 and every other field 0; it does not pad the archive to a
 block (an initramfs may be padded; `Cpio.parse` ignores everything after the
-trailer's name); it skips padding without checking that it is zero.
+trailer's name); it skips padding without checking that it is zero. A trailer name may have
+additional NUL bytes within `namesize`. Other names are returned as raw bytes
+with only the final required NUL removed; embedded or additional NULs are not
+normalized.
 
 ## Files
 
@@ -56,7 +59,7 @@ trailer's name); it skips padding without checking that it is zero.
 | `CpioHeader.encode(h) -> Octets`, `CpioHeader.decode(o) -> Result<…, CpioHeaderAt>` | one header's 110 bytes, and reading one back (`CpioHeaderAt{header, rest}`) |
 | `CpioEntry.header(fmt, e)` | the header `Cpio.build` writes for an entry |
 | `Cpio.checksum(o)` | the crc format's check: the sum of the bytes, modulo 2^32 |
-| `Cpio.trailer_name()`, `Cpio.is_trailer_name(name)` | `TRAILER!!!` |
+| `Cpio.trailer_name()`, `Cpio.is_trailer_name(name)` | `TRAILER!!!`; recognition also accepts an all-NUL suffix |
 | `CpioEntry.valid(e)`, `CpioEntry.valid_all(es)` | the entries an archive can hold (see Laws) |
 
 `hexfield.bend`:
@@ -99,7 +102,7 @@ Everything else in the two files (the list-level `fields.*`, `hdr.*`,
     `CpioEntry.valid_all` admits, `Cpio.parse(Cpio.build(fmt, es)) ==
     Done{es}`, proved by induction on the list. `CpioEntry.valid` asks that
     the data, and the name with its NUL, are shorter than 2^32 bytes (they
-    must fit their size fields); and that the name is not `TRAILER!!!`.
+    must fit their size fields); and that the name is not `TRAILER!!!` followed by zero or more NULs.
     Reading the name and data back as `Octets` uses bytes' interface law
     `octets_of_to` (`of_list(to_list(o)) == o` for every `o`).
   * `valid_example`: the hypothesis is satisfiable (an ordinary one-file
@@ -110,7 +113,8 @@ Everything else in the two files (the list-level `fields.*`, `hdr.*`,
   the trailer ignored; and one archive for each error: empty input, no
   trailer, a truncated header, truncated data, the `070707` magic, a non-hex
   digit, a bad checksum, a name size of 0, a name without its NUL; and the
-  newc format ignoring its check field.
+  newc format ignoring its check field. Padded trailers, a preceding entry,
+non-trailer suffixes and a malformed padded name are also checked.
 
 ## Tests
 
@@ -171,7 +175,7 @@ and 250 small ones) as a regression test.
 * Sizes are computed on `Nat`, and lengths are counted by walking the lists:
   linear in the archive's size (see Sizes).
 * `Cpio.build` does not refuse an entry whose data is 2^32 bytes or longer, or
-  whose name is `TRAILER!!!`; such an archive does not parse back.
+  whose name is `TRAILER!!!` followed by zero or more NULs; such an archive does not parse back.
 
 ## Dependencies
 
@@ -180,6 +184,9 @@ values (`LAWS.bend`).
 
 ## Status
 
+2026-10-31: `scripts/check.sh cpio` and `VERDICT=1 scripts/check.sh cpio`
+pass (proofs, examples and 100 reference cases); `scripts/deps.sh cpio` passes.
+
 Bend 2.0.39 (2026-10-26, native, three packages at a time): `PROOF.bend`
 (3 s, 0.38 GB peak; `--verdict` 6 s, 0.43 GB peak) ALL PROOFS CHECK, with
 and without `--verdict`.

cpio/VERSION

@@ -1 +1 @@
-0.1.0.0
+0.2.0.0

cpio/cpio.bend

@@ -334,8 +334,26 @@ def same(xs: List<&2, U32>, ys: List<&2, U32>) -> Bool:
 def trailer.name() -> List<&2, U32>:
   [84, 82, 65, 73, 76, 69, 82, 33, 33, 33]
 
+def trailer.zeros(xs: List<&2, U32>) -> Bool:
+  match xs:
+    case Nil{}:
+      True{}
+    case Con{h, t}:
+      Bool.and(U32.is_eq(U32.and(h, 255), 0), trailer.zeros(t))
+
+def trailer.prefix(prefix: List<&2, U32>, name: List<&2, U32>) -> Bool:
+  match prefix:
+    case Nil{}:
+      trailer.zeros(name)
+    case Con{h, t}:
+      match name:
+        case Nil{}:
+          False{}
+        case Con{v, rest}:
+          Bool.and(U32.is_eq(U32.and(v, 255), h), trailer.prefix(t, rest))
+
 def trailer.is(name: List<&2, U32>) -> Bool:
-  same(name, trailer.name())
+  trailer.prefix(trailer.name(), name)
 
 # Reading an entry