diff --git a/README.md b/README.md index 027a6b2a7d..191f91b659 100644 --- a/README.md +++ b/README.md @@ -114,7 +114,7 @@ publishing — all backed by YAML provable contracts that fail CI on drift. | Metric | Count | Source of truth | |-------:|------:|---| | Workspace crates | **81** workspace crates | `cargo metadata --no-deps` (NOT `ls crates/` — 4 are `exclude`d, 1 has no Cargo.toml) | -| Provable contracts | **1984** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) | +| Provable contracts | **1985** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) | | CLI commands | **113** CLI commands | `contracts/apr-cli-commands-v1.yaml` §`commands` (parse the list; `apr --help` also lists `help` itself, and `grep -c '^ - name:'` gives 119 — other same-indent `name:` keys exist in the file) | | Book CLI chapters | **114** chapters | `ls book/src/cli/*.md` | | Book lib chapters | **73** chapters | `ls book/src/lib/*.md` (parity with `pub mod`) | @@ -403,7 +403,7 @@ falsification_tests: prediction: apr validate bad-model.apr exits non-zero ``` -The tree carries 1984 contracts across inference, training, quantization, attention, FFN, +The tree carries 1985 contracts across inference, training, quantization, attention, FFN, tokenization, model formats, CLI safety — and this README itself. ## Migration from old crates diff --git a/contracts/bin-aprender-data--aprender-data-v1.yaml b/contracts/bin-aprender-data--aprender-data-v1.yaml index 9cdb324f89..d675e245e7 100644 --- a/contracts/bin-aprender-data--aprender-data-v1.yaml +++ b/contracts/bin-aprender-data--aprender-data-v1.yaml @@ -165,3 +165,9 @@ falsification_tests: test: 'cargo test -p aprender-data --test imbalance_edges' if_fails: 'a zero-count class gets weight, null labels are grouped, or an unsupported label type is silently accepted' mutation: 'change `if c == 0` in sqrt_inverse_weights; weights_zero_count_class_gets_zero turns RED (measured 2026-10-18)' + - id: FALSIFY-BIN-ALIMENTAR-008 + rule: 'the .ald format rejects malformed input and round-trips every compression' + prediction: 'dataset-type and compression codes round-trip and unknown codes are None; Header::from_bytes rejects short, bad-magic, unknown-type, unknown-compression and future-major input; save of no batches errors; a bit flip or truncation fails load' + test: 'cargo test -p aprender-data --test format_edges' + if_fails: 'a corrupt or foreign file is accepted, or a codec silently decodes as another' + mutation: 'map compression code 0x03 to ZstdL3 in Compression::from_u8; compression_codes_roundtrip_and_unknown_is_none turns RED (measured 2026-10-18)' diff --git a/contracts/contracts.nt b/contracts/contracts.nt index f0d8c3a042..646ee9e8da 100644 --- a/contracts/contracts.nt +++ b/contracts/contracts.nt @@ -13721,6 +13721,11 @@ "simd-scalar-parity-v1"^^ . "simd-scalar-parity"^^ . "1.0.0"^^ . + . + . + "contracts/simulate-edd-verification-tests-v1.yaml"^^ . + "simulate-edd-verification-tests-v1"^^ . + "pattern"^^ . . . . diff --git a/contracts/simulate-edd-verification-tests-v1.yaml b/contracts/simulate-edd-verification-tests-v1.yaml new file mode 100644 index 0000000000..a264bc7cf7 --- /dev/null +++ b/contracts/simulate-edd-verification-tests-v1.yaml @@ -0,0 +1,38 @@ +metadata: + version: 1.0.0 + created: '2026-10-18' + author: PAIML Engineering + description: "EDD-07 — EddValidator::validate_verification_tests reports each failing EMC verification test as a critical EDD-07 violation, passes silently when all hold, and records failures in the validator." + kind: pattern + references: + - "crates/aprender-simulate/src/edd/validation.rs — validate_verification_tests and its tests" + - "docs/findings/aprender-w5032.jsonl — coverage-gaps ranking that selected this function" + +equations: + edd07_reports_exactly_the_failing_tests: + formula: "errors == { t in emc.tests : |eval(t.inputs) - t.expected| > t.tolerance }, each code EDD-07 and severity Critical; validator.violations grows by |errors|" + domain: "an EquationModelCard with >= 1 verification test and an evaluator closure" + codomain: "Result<(), Vec>" + invariants: + - "A passing run leaves the validator's violations untouched" + - "A failing run appends to, never replaces, earlier violations" + - "The violation context carries the FAIL line with expected, actual and tolerance" + +proof_obligations: + - id: SEV-INV-001 + type: invariant + property: "Only failing tests are reported, as EDD-07 Critical with FAIL context" + formal: "∀ t ∈ {test_validate_verification_tests_failure_is_edd07_critical_with_context}: exit(t) = 0" + applies_to: edd07_reports_exactly_the_failing_tests + - id: SEV-INV-002 + type: invariant + property: "Failures accumulate in the validator across runs" + formal: "∀ t ∈ {test_validate_verification_tests_failures_accumulate_in_validator}: exit(t) = 0" + applies_to: edd07_reports_exactly_the_failing_tests + +falsification_tests: + - id: FALSIFY-SEV-001 + rule: "failures not recorded" + prediction: "deleting the self.violations.extend call turns the accumulate test RED" + test: "cargo test -p aprender-simulate --lib test_validate_verification_tests_failures_accumulate_in_validator" + if_fails: "a failed verification leaves no trace in the validator" diff --git a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json index 6bb276cb32..53b5fdbbb1 100644 --- a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json +++ b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json @@ -1,7 +1,7 @@ { - "census_id_set_sha256": "7597b4ad189f534dd58cda55c9b1fe29e6339ddb77fd5f40969b4a028eed8f88", + "census_id_set_sha256": "baac627e81511256895c61f340bd3c03eda199ac25c1e6fa5e1f9c380dea159f", "relations_sha256": "811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850", - "reasoner_git_sha": "461bf9ef1921a8fbea4bc338f21b566ec342a95e", + "reasoner_git_sha": "4514d359f4fdbff3b9973bbfcc286909378a1a88", "checkable_n": 87, "result": { "kind": "model", diff --git a/crates/aprender-data/tests/format_edges.rs b/crates/aprender-data/tests/format_edges.rs new file mode 100644 index 0000000000..209d3d3c57 --- /dev/null +++ b/crates/aprender-data/tests/format_edges.rs @@ -0,0 +1,232 @@ +//! Public-API edge cases for the .ald dataset format (coverage ticket, Rule 7). +//! Contract: FALSIFY-BIN-ALIMENTAR-008. + +use std::sync::Arc; + +use alimentar::format::{ + flags, load, save, Compression, DatasetType, Header, Metadata, SaveOptions, + FORMAT_VERSION_MAJOR, HEADER_SIZE, MAGIC, +}; +use arrow::{ + array::{Int32Array, RecordBatch, StringArray}, + datatypes::{DataType, Field, Schema}, +}; + +fn batch() -> RecordBatch { + let schema = Arc::new(Schema::new(vec![ + Field::new("id", DataType::Int32, false), + Field::new("name", DataType::Utf8, true), + ])); + RecordBatch::try_new( + schema, + vec![ + Arc::new(Int32Array::from(vec![1, 2, 3])), + Arc::new(StringArray::from(vec![Some("a"), None, Some("c")])), + ], + ) + .expect("batch") +} + +fn saved(opts: &SaveOptions) -> Vec { + let mut buf = Vec::new(); + save(&mut buf, &[batch()], DatasetType::Tabular, opts).expect("save"); + buf +} + +#[test] +fn dataset_type_codes_roundtrip_and_unknown_is_none() { + let all = [ + DatasetType::Tabular, + DatasetType::TimeSeries, + DatasetType::Graph, + DatasetType::Spatial, + DatasetType::TextCorpus, + DatasetType::TextClassification, + DatasetType::TextPairs, + DatasetType::SequenceLabeling, + DatasetType::QuestionAnswering, + DatasetType::Summarization, + DatasetType::Translation, + DatasetType::ImageClassification, + DatasetType::ObjectDetection, + DatasetType::Segmentation, + DatasetType::ImagePairs, + DatasetType::Video, + DatasetType::AudioClassification, + DatasetType::SpeechRecognition, + DatasetType::SpeakerIdentification, + DatasetType::UserItemRatings, + DatasetType::ImplicitFeedback, + DatasetType::SequentialRecs, + DatasetType::ImageText, + DatasetType::AudioText, + DatasetType::VideoText, + DatasetType::Custom, + ]; + for t in all { + assert_eq!(DatasetType::from_u16(t.as_u16()), Some(t), "{t:?}"); + } + for bad in [ + 0x0000, 0x0005, 0x0017, 0x0033, 0x0043, 0x0053, 0x0100, 0xFFFF, + ] { + assert_eq!(DatasetType::from_u16(bad), None, "0x{bad:04X}"); + } + assert_eq!(DatasetType::Tabular.as_u16(), 1); + assert_eq!(DatasetType::Custom.as_u16(), 0xFF); +} + +#[test] +fn compression_codes_roundtrip_and_unknown_is_none() { + for (c, code) in [ + (Compression::None, 0u8), + (Compression::ZstdL3, 1), + (Compression::ZstdL19, 2), + (Compression::Lz4, 3), + ] { + assert_eq!(c.as_u8(), code); + assert_eq!(Compression::from_u8(code), Some(c)); + } + assert_eq!(Compression::from_u8(4), None); + assert_eq!(Compression::from_u8(0xFF), None); + assert_eq!(Compression::default(), Compression::ZstdL3); +} + +#[test] +fn header_roundtrips_every_field() { + let mut h = Header::new(DatasetType::Graph); + h.metadata_size = 11; + h.payload_size = 22; + h.uncompressed_size = 33; + h.compression = Compression::Lz4; + h.flags = flags::SIGNED | flags::STREAMING; + h.schema_size = 44; + h.num_rows = 5_000_000_000; + let bytes = h.to_bytes(); + assert_eq!(bytes.len(), HEADER_SIZE); + assert_eq!(bytes[0..4], MAGIC); + let back = Header::from_bytes(&bytes).expect("parse"); + assert_eq!(back.dataset_type, DatasetType::Graph); + assert_eq!( + ( + back.metadata_size, + back.payload_size, + back.uncompressed_size, + back.schema_size + ), + (11, 22, 33, 44) + ); + assert_eq!(back.compression, Compression::Lz4); + assert_eq!(back.num_rows, 5_000_000_000); + assert!(back.is_signed() && back.is_streaming()); + assert!(!back.is_encrypted() && !back.is_licensed() && !back.is_trueno_native()); +} + +#[test] +fn header_flag_accessors_are_independent() { + for (bit, check) in [ + ( + flags::ENCRYPTED, + Header::is_encrypted as fn(&Header) -> bool, + ), + (flags::SIGNED, Header::is_signed), + (flags::STREAMING, Header::is_streaming), + (flags::LICENSED, Header::is_licensed), + (flags::TRUENO_NATIVE, Header::is_trueno_native), + ] { + let mut h = Header::new(DatasetType::Tabular); + assert!(!check(&h)); + h.flags = bit; + assert!(check(&h), "bit {bit:#b}"); + } +} + +#[test] +fn header_rejects_malformed_input() { + let good = Header::new(DatasetType::Tabular).to_bytes(); + + assert!( + Header::from_bytes(&good[..HEADER_SIZE - 1]).is_err(), + "short" + ); + assert!(Header::from_bytes(&[]).is_err(), "empty"); + + let mut bad_magic = good; + bad_magic[0] ^= 0xFF; + assert!(Header::from_bytes(&bad_magic).is_err(), "magic"); + + let mut bad_type = good; + bad_type[6] = 0xEE; + bad_type[7] = 0xEE; + let e = Header::from_bytes(&bad_type).unwrap_err().to_string(); + assert!(e.contains("Unknown dataset type"), "{e}"); + + let mut bad_comp = good; + bad_comp[20] = 0x7F; + let e = Header::from_bytes(&bad_comp).unwrap_err().to_string(); + assert!(e.contains("Unknown compression"), "{e}"); + + let mut future = good; + future[4] = FORMAT_VERSION_MAJOR + 1; + assert!(Header::from_bytes(&future).is_err(), "future major version"); +} + +#[test] +fn save_rejects_empty_batch_list() { + let mut buf = Vec::new(); + assert!(save(&mut buf, &[], DatasetType::Tabular, &SaveOptions::default()).is_err()); + assert!(buf.is_empty(), "nothing written on error"); +} + +#[test] +fn every_compression_roundtrips_rows_and_values() { + for c in [ + Compression::None, + Compression::ZstdL3, + Compression::ZstdL19, + Compression::Lz4, + ] { + let bytes = saved(&SaveOptions::default().with_compression(c)); + let loaded = load(&mut bytes.as_slice()).unwrap_or_else(|e| panic!("{c:?}: {e}")); + assert_eq!(loaded.header.compression, c); + assert_eq!(loaded.header.dataset_type, DatasetType::Tabular); + assert_eq!(loaded.header.num_rows, 3); + assert_eq!(loaded.batches.len(), 1); + let ids = loaded.batches[0] + .column(0) + .as_any() + .downcast_ref::() + .expect("int32"); + assert_eq!(ids.values().to_vec(), vec![1, 2, 3], "{c:?}"); + assert_eq!(loaded.batches[0].column(1).null_count(), 1, "{c:?}"); + } +} + +#[test] +fn metadata_roundtrips() { + let meta = Metadata { + name: Some("demo".into()), + tags: vec!["x".into(), "y".into()], + ..Metadata::default() + }; + let bytes = saved(&SaveOptions::default().with_metadata(meta)); + let loaded = load(&mut bytes.as_slice()).expect("load"); + assert_eq!(loaded.metadata.name.as_deref(), Some("demo")); + assert_eq!(loaded.metadata.tags, vec!["x", "y"]); +} + +#[test] +fn corrupted_or_truncated_file_is_rejected() { + let bytes = saved(&SaveOptions::default()); + let mut flipped = bytes.clone(); + let mid = flipped.len() / 2; + flipped[mid] ^= 0xFF; + assert!( + load(&mut flipped.as_slice()).is_err(), + "bit flip must fail the checksum" + ); + + let truncated = &bytes[..bytes.len() - 6]; + assert!(load(&mut &truncated[..]).is_err(), "truncation"); + assert!(load(&mut &bytes[..10]).is_err(), "header-only fragment"); + assert!(load(&mut &[][..]).is_err(), "empty input"); +} diff --git a/crates/aprender-simulate/src/edd/validation.rs b/crates/aprender-simulate/src/edd/validation.rs index b07d563e75..75ccb103d5 100644 --- a/crates/aprender-simulate/src/edd/validation.rs +++ b/crates/aprender-simulate/src/edd/validation.rs @@ -1559,4 +1559,54 @@ mod tests { let result_loose = richardson_extrapolation(&values, 2.0, 2.5, 1.0); assert!(result_loose.order_matches); } + + fn emc_with_tests(tests: &[(&str, f64, f64)]) -> EquationModelCard { + let mut b = EmcBuilder::new() + .name("Test") + .equation("x = y") + .citation(Citation::new(&["Test"], "Test", 2024)); + for (d, e, t) in tests { + b = b.add_verification_test(*d, *e, *t); + } + b.build().ok().unwrap() + } + + #[test] + fn test_validate_verification_tests_all_pass_records_nothing() { + let mut v = EddValidator::new(); + let emc = emc_with_tests(&[("a", 1.0, 0.1), ("b", 1.0, 0.5)]); + assert!(v.validate_verification_tests(&emc, |_| 1.05).is_ok()); + assert!(v.violations().is_empty()); + } + + #[test] + fn test_validate_verification_tests_failure_is_edd07_critical_with_context() { + let mut v = EddValidator::new(); + let emc = emc_with_tests(&[("good", 1.0, 0.1), ("bad", 5.0, 0.1)]); + let errs = v.validate_verification_tests(&emc, |_| 1.0).err().unwrap(); + assert_eq!(errs.len(), 1, "only the failing test is reported"); + assert_eq!(errs[0].code, "EDD-07"); + assert_eq!(errs[0].severity, ViolationSeverity::Critical); + assert!(errs[0].message.contains("Verification test failed: bad")); + assert!(errs[0] + .context + .as_deref() + .unwrap_or("") + .contains("FAIL: bad")); + } + + #[test] + fn test_validate_verification_tests_failures_accumulate_in_validator() { + let mut v = EddValidator::new(); + let emc = emc_with_tests(&[("x", 9.0, 0.1), ("y", 8.0, 0.1)]); + let errs = v.validate_verification_tests(&emc, |_| 0.0).err().unwrap(); + assert_eq!(errs.len(), 2); + assert_eq!(v.violations().len(), 2); + let _ = v.validate_verification_tests(&emc, |_| 0.0); + assert_eq!( + v.violations().len(), + 4, + "a second run appends, not replaces" + ); + } }