Re: block/t10-pi.c: blk_integrity_interval() prot_iter misalignment with extended metadata

Hi,

Thanks for the quick look. Quick context: this bug came out of a personal
research project migrating parts of the Linux block layer to Lean 4 for
formal verification -- one of the first real results from it, found while
contrasting blk_integrity_interval() against blk_tuple_remap_end() (which
handles the equivalent case correctly).

Part of the tooling is AI-assisted. My rule for that: nothing goes out
unless it clears at least two independent, mechanically checkable proofs.
For this bug that's the C reproducer (compiles and runs) and a Lean proof
(compiles with zero sorry/axioms of its own), plus `git apply --check` for
the patches.

Attached (patch_submission.zip):

  patch/0001-*.patch  The fix I proposed originally: advance prot_iter
                       past the remaining opaque bytes in the split-tuple
                       path, matching blk_tuple_remap_end().
  patch/0002-*.patch  Separate, smaller fix: bvec_iter_advance() instead
                       of _single() in the fast path (precondition
                       violation from my original report). Happy to drop
                       this one if you'd rather keep it to one fix.
  poc.c                The userspace reproducer, included again.
  report_...md         The full write-up.
  lean-proof/          Standalone Lean 4 project (own lakefile, zero deps,
                        `lake build`) proving the patched logic always
                        advances the iterator by exactly metadata_size
                        bytes -- not just on test vectors.
  blktests/            Draft tests/meta/ script -- theoretical only, not
                        run against a real blktests checkout.

Both patches apply cleanly, individually and stacked (verified with
`git apply --check`).

On blktests: real limitation I'd rather flag than paper over. Reproducing
this needs (a) an integrity format with opaque trailing metadata
(metadata_size > pi_offset + pi_tuple_size, e.g. NVMe extended metadata)
and (b) a bio layout splitting the tuple across bvec segments.
scsi_debug's dif=/dix= only does plain 8-byte T10 DIF, no opaque padding,
so it can't hit (a). I don't know if nvmet-loop can be configured for
this without real hardware. The included draft only validates the
arithmetic model, not a real device.


Thanks,
Ricardo M. Biot

On Fri, Aug 14, 2026 at 8:38 AM Christoph Hellwig <[email protected]> wrote:
>
> On Wed, Aug 12, 2026 at 02:37:28PM +0200, Ricardo AlgRicSpain wrote:
> > Hi,
> >
> > blk_integrity_interval() (block/t10-pi.c:270-305) advances prot_iter
> > inconsistently:
> >
> > - fast path (t10-pi.c:282): advances metadata_size - pi_offset bytes
> > - split-tuple path (t10-pi.c:285-287, 296-299): advances only
> >   pi_tuple_size bytes via blk_integrity_copy_to_tuple/copy_from_tuple
> >
> > When metadata_size - pi_offset > pi_tuple_size (e.g. NVMe extended
> > metadata) and the tuple splits across bvec segments, prot_iter
> > under-advances by the trailing opaque bytes, and the offset accumulates
> > across subsequent intervals, breaking guard/data correspondence on
> > verify and generate.
> >
> > Suggested fix: after copy_to_tuple/copy_from_tuple, advance the
> > remaining bytes:
> >
> >     bvec_iter_advance(iter->bip->bip_vec, &iter->prot_iter,
> >             iter->bi->metadata_size - iter->bi->pi_offset -
> >             iter->bi->pi_tuple_size);
> >
> > ...matching what blk_tuple_remap_end() already does (t10-pi.c:426-436).
> >
> > Standalone C PoC reproducing the misalignment attached (poc.c).
>
> Please send a patch with your proposed fix.  Wiring up your reproducer
> in blktests would also be very helpful.
>