diff --git a/cpio/LAWS.bend b/cpio/LAWS.bend index e97a7a1..f55221f 100644 --- a/cpio/LAWS.bend +++ b/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: diff --git a/cpio/PROOF.bend b/cpio/PROOF.bend index 182f82c..45bbf6e 100644 --- a/cpio/PROOF.bend +++ b/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(): + {==} diff --git a/cpio/README.md b/cpio/README.md index cbce3d8..f017e5f 100644 --- a/cpio/README.md +++ b/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`. diff --git a/cpio/VERSION b/cpio/VERSION index 482e997..e396b40 100644 --- a/cpio/VERSION +++ b/cpio/VERSION @@ -1 +1 @@ -0.1.0.0 +0.2.0.0 diff --git a/cpio/cpio.bend b/cpio/cpio.bend index 92f47db..5ed4baa 100644 --- a/cpio/cpio.bend +++ b/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