Checked variable-width signed reads omit sign extension

bytes::Buf::try_get_int, bytes::Buf::try_get_int_le, bytes::Buf::try_get_int_ne

Found in Report #8 v1 · Updated 2026-10-25 22:52 UTC

While working toward Aeneas formal verification, we examined the expected signed-read
contract. That obligation was not established; source review and native reproduction
confirmed the discrepancy below. Failure to complete a proof alone is not evidence
of a bug, and the retained records do not show Lean producing this counterexample.

In bytes 1.12.1, the checked variable-width signed readers can return a positive
number for a negative two's-complement input. For example, one byte 0xff denotes
-1, but try_get_int(1) returns Ok(255):

use bytes::Buf;

let mut input = &[0xff_u8, 0x42][..];
let value = input.try_get_int(1);
assert_eq!(input, &[0x42]); // The requested byte was consumed.
assert_eq!(value, Ok(-1)); // Fails: actual result is Ok(255).

The retained native regression checks big-, little- and native-endian variants on
all-0xff inputs at widths 1 through 8, including the exact residual slice. At widths
1 through 7, checked reads return 2^(8*n)-1 while the corresponding get_int methods
return -1. Width 8 is a passing control: both return -1. The 2026-10-23 minimal
counterexample record uses Rust 1.91.1 on aarch64-apple-darwin with default features
disabled. These observations are native counterexamples, not Lean verification
of the public variable-width readers or evidence of a memory-safety failure.

Source inspection explains the discrepancy: the checked implementations fill an
eight-byte array initially containing zeroes and convert it to i64, whereas the
unchecked counterparts apply sign extension. The expected signed contract remains
an unmet obligation; it was not weakened to accept the observed result.

See the pinned Buf implementation.
This is a known issue reproduced in the pinned 1.12.1 release.
Upstream PR #839 was merged on
2026-09-03 as 7930d93.
As checked on 2026-10-25, master contains the fix but the latest release remains
1.12.1, which is affected. The native-endian reader is fixed through delegation.

Change history

v1 · created · 2026-10-25 07:08 UTC

{
  "title": "Checked variable-width signed reads omit sign extension",
  "body": "While working toward Aeneas formal verification, we examined the expected signed-read\ncontract. That obligation was not established; source review and native reproduction\nconfirmed the discrepancy below. Failure to complete a proof alone is not evidence\nof a bug, and the retained records do not show Lean producing this counterexample.\n\nIn bytes 1.12.1, the checked variable-width signed readers can return a positive\nnumber for a negative two's-complement input. For example, one byte 0xff denotes\n-1, but try_get_int(1) returns Ok(255):\n\n```rust\nuse bytes::Buf;\n\nlet mut input = &[0xff_u8, 0x42][..];\nlet value = input.try_get_int(1);\nassert_eq!(input, &[0x42]); // The requested byte was consumed.\nassert_eq!(value, Ok(-1)); // Fails: actual result is Ok(255).\n```\n\nThe retained native regression checks big-, little- and native-endian variants on\nall-0xff inputs at widths 1 through 8, including the exact residual slice. At widths\n1 through 7, checked reads return 2^(8*n)-1 while the corresponding get_int methods\nreturn -1. Width 8 is a passing control: both return -1. The 2026-10-23 minimal\ncounterexample record uses Rust 1.91.1 on aarch64-apple-darwin with default features\ndisabled. These observations are native counterexamples, not Lean verification\nof the public variable-width readers or evidence of a memory-safety failure.\n\nSource inspection explains the discrepancy: the checked implementations fill an\neight-byte array initially containing zeroes and convert it to i64, whereas the\nunchecked counterparts apply sign extension. The expected signed contract remains\nan unmet obligation; it was not weakened to accept the observed result.\n\nSee the [pinned Buf implementation](https://github.com/tokio-rs/bytes/blob/76c0fbb54ed4336caf9d2311658a2f4a5627c21d/src/buf/buf_impl.rs#L2086).\nThis is a known issue reproduced in the pinned 1.12.1 release.\n[Upstream PR #839](https://github.com/tokio-rs/bytes/pull/839) was merged on\n2026-09-03 as [7930d93](https://github.com/tokio-rs/bytes/commit/7930d93d583757e922014312d4aa3e58a415131f).\nAs checked on 2026-10-25, master contains the fix but the latest release remains\n1.12.1, which is affected. The native-endian reader is fixed through delegation.",
  "validity": "reported",
  "upstream_status": "not_reported"
}

v2 · link_added · 2026-10-25 17:00 UTC

{
  "id": "11a98b81-63e7-43c4-9fc9-fc0b5f22daf9",
  "kind": "pr",
  "url": "https://github.com/tokio-rs/bytes/pull/839",
  "version": null,
  "target_report_id": null,
  "target_revision_no": null,
  "edit_version": 1
}

v3 · edited · 2026-10-25 22:52 UTC

{
  "api_item_ids": [
    "1b77ced09052120c8cefa97a0cb7d40fddba14888a3d62fe9854e6bf0f3383f8",
    "b9ab08717527313b7598388ce846dada966431e2de2ce5ae0e58f8196dfe40aa",
    "84ae1970c71ccbd7de66bdcc70656df7503afe3d289951b7c0e2055c2edd6789"
  ],
  "edit_version": 2
}

Checked variable-width signed reads omit sign extension

Checked variable-width signed reads omit sign extension

Related links