metadata:
  version: "1.0.0"
  author: "Sovereign AI Stack"
  description: "Batch data loading contract for alimentar"
  crate: "alimentar"
  references:
    - "Smith et al., Dont Decay the Learning Rate Increase the Batch Size, ICLR 2018"

equations:
  batch_size_invariant:
    formula: "actual_batch_size <= requested_batch_size"
    domain: "requested_batch_size > 0"
    invariants:
      - "Last batch may be smaller (remainder)"
      - "Sum of all batch sizes = total dataset size"

proof_obligations:
  - type: invariant
    property: "No data loss during batching"
    formal: "sum(batch_sizes) = dataset_size"
    applies_to: all

falsification_tests:
  - id: FALSIFY-BATCH-001
    rule: "Batch completeness"
    test: "test_corpus_to_record_batch"
    prediction: "verified"
    if_fails: "Contract violation — data lost during batching"

kani_harnesses:
  - id: KANI-BATCH-001
    obligation: PO-BATCH-001
    property: "Batch completeness for bounded inputs"
    bound: 8
    strategy: bounded_int
    harness: verify_batch_loading

qa_gate:
  id: QA-BATCH
  name: "batch loading contract"
  min_coverage: 0.90
  max_complexity: 20
  required_tests: []
