mm0b_parser: pin the fixture's index format, and say why AlignFile is align(8)

The two fixes these tests were written alongside are already here: `e820dc3f`
made `AlignFile` `align(8)` and regenerated `test_resources/peano.mmb` as part
of the CI work, and the fixture bytes are identical to the ones regenerated on
`mmb-explorer`. What did not come with them is the coverage and the reasoning,
picked up here from that branch (`65933edd`, `00d19428`).

`peano_index` parses the fixture *with* its index and checks that names
resolve. `peano0` parses it as a `BareMmbFile`, which ignores the index
entirely, so it kept passing while the fixture's index went a format version
behind — which is how the fixture came to be stale unnoticed. A test that never
looks at the index cannot report one that has rotted.

The `AlignFile` doc comment records why it must be `align(8)` and not
`align(1)`: `repr(align(N))` only ever raises a type's alignment, so `align(1)`
on a `[u8; N]` is a no-op and the array lands wherever the compiler puts a
1-aligned local, making the parse fail with `Unaligned` depending on nothing but
stack layout. `MmbFile::parse` now states the requirement from the other side,
since it is the caller who has to satisfy it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Author: digama0

mm0-rs/components/mm0b_parser/src/parser.rs

@@ -882,6 +882,11 @@ impl<'a, X: MmbIndexBuilder<'a>> MmbFile<'a, X> {
   /// Parse a [`MmbFile`] from a file, provided as a byte slice.
   /// This does the minimum checking to construct the parsed object,
   /// it is not a verifier.
+  ///
+  /// `buf` must be **8-byte aligned**, since [`Header`] is `align(8)`; otherwise
+  /// this returns [`ParseError::Unaligned`]. A `Vec<u8>` from `fs::read` is
+  /// suitably aligned in practice, but a subslice at an arbitrary offset, or a
+  /// short array literal, may not be — wrap such data in an `align(8)` struct.
   pub fn parse(buf: &'a [u8]) -> Result<Self, ParseError> {
     use ParseError::{BadIndexParse, BadSorts, BadTerms, BadThms};
     let (zc_header, sorts) =

mm0-rs/components/mm0b_parser/tests/basic.rs

@@ -1,8 +1,14 @@
-use mm0b_parser::{BareMmbFile, ParseError};
+use mm0b_parser::{BareMmbFile, BasicMmbFile, NumdStmtCmd, ParseError};
 use std::fs::OpenOptions;
 use std::io::Read;
 use std::path::PathBuf;
 
+/// Force the test data to the 8-byte alignment [`BareMmbFile::parse`] requires.
+///
+/// This must be `align(8)`, not `align(1)`: `repr(align(N))` can only *raise* a
+/// type's alignment, so `align(1)` is a no-op on a `[u8; N]` and leaves the array
+/// wherever the compiler happens to put a 1-aligned local — making the parse fail
+/// with [`ParseError::Unaligned`] depending only on stack layout.
 #[repr(align(8))]
 struct AlignFile<T>(T);
 
@@ -16,8 +22,7 @@ fn try_next_decl_infinite_loop() {
   assert!(matches!(iter.next().unwrap().unwrap_err(), ParseError::BadProofLen(40)));
 }
 
-#[test]
-fn peano0() {
+fn peano_bytes() -> Vec<u8> {
   let mut mmb_bytes = Vec::new();
   let mut mmb_file = OpenOptions::new()
     .read(true)
@@ -26,5 +31,33 @@ fn peano0() {
     .unwrap();
   mmb_file.read_to_end(&mut mmb_bytes).unwrap();
   assert!(!mmb_bytes.is_empty());
-  assert!(BareMmbFile::parse(mmb_bytes.as_slice()).is_ok());
+  mmb_bytes
+}
+
+#[test]
+fn peano0() {
+  assert!(BareMmbFile::parse(peano_bytes().as_slice()).is_ok());
+}
+
+/// Parse the fixture *with* its index, and check that names resolve.
+///
+/// `peano0` only parses as a [`BareMmbFile`], which ignores the index entirely,
+/// so it keeps passing even if the fixture's index is stale or malformed — which
+/// is exactly how the fixture came to be a format version behind. This test pins
+/// the index format down.
+#[test]
+fn peano_index() {
+  let bytes = peano_bytes();
+  let file = BasicMmbFile::parse(bytes.as_slice()).expect("fixture index should parse");
+  let names = file
+    .proof()
+    .take(4)
+    .map(|decl| match decl.unwrap().0 {
+      NumdStmtCmd::Sort { sort_id } => file.sort_name(sort_id).into_owned(),
+      NumdStmtCmd::TermDef { term_id, .. } => file.term_name(term_id).into_owned(),
+      NumdStmtCmd::Axiom { thm_id } | NumdStmtCmd::Thm { thm_id, .. } =>
+        file.thm_name(thm_id).into_owned(),
+    })
+    .collect::<Vec<_>>();
+  assert_eq!(names, ["wff", "im", "not", "ax_1"]);
 }