From 8b6cdbc1d2b24493bedd97305aa027e669682661 Mon Sep 17 00:00:00 2001 From: Zious Date: Sun, 6 Sep 2026 21:24:04 -0500 Subject: [PATCH 1/9] stub(STORY-185): COTP TPDU parser skeleton (Red Gate, BC-2.20.005-012) Files created: none (extends src/analyzer/iso_on_tcp.rs from STORY-184) Files modified: src/analyzer/iso_on_tcp.rs todo!() functions: 1 (parse_cotp_header) Adds the frozen SS-20 -> SS-21 interface types (CotpTpduType, CotpHeader) as real type definitions per ADR-014 Decision 1, a todo!()-bodied parse_cotp_header stub targeting BC-2.20.005-012, and a #[cfg(kani)] VP-049 proof skeleton (verify_parse_cotp_header_safety) mirroring the existing VP-048 harness pattern. Self-check (BC-5.38.005 invariant 1) applied to parse_cotp_header: "If I include this real implementation, will the test for this function pass trivially without any implementer work?" -- yes, so the body is todo!() per BC-5.38.001. ## GREEN-BY-DESIGN none ## WIRING-EXEMPT none Verified: cargo check --all-targets clean, cargo clippy --all-targets -- -D warnings clean, cargo fmt applied, existing 30 STORY-184 tests in tests/iso_on_tcp_tests.rs still pass. No test files touched (test-writer's job). Zero occurrences of 0x32/0x72 literals or "S7comm"/"S7comm-plus" string literals in src/analyzer/iso_on_tcp.rs, per BC-2.20.012 postcondition 3 / AC-185-009. Claude-Session: https://claude.ai/code/session_01EQAaPvh9fwaG31jmkPicKW --- src/analyzer/iso_on_tcp.rs | 149 +++++++++++++++++++++++++++++++++++-- 1 file changed, 144 insertions(+), 5 deletions(-) diff --git a/src/analyzer/iso_on_tcp.rs b/src/analyzer/iso_on_tcp.rs index 83761d20..c51e6f7c 100644 --- a/src/analyzer/iso_on_tcp.rs +++ b/src/analyzer/iso_on_tcp.rs @@ -21,15 +21,21 @@ //! no global state mutation. This is a hard constraint for VP-048 Kani formal //! verification amenability (ADR-014 Decision 9). //! -//! ## Scope of this story (STORY-184) +//! ## Scope //! -//! This story covers **only** the TPKT (RFC 1006) outer framing header: -//! `TpktHeader` and `parse_tpkt_header`. COTP (ISO 8073 / ITU-T X.224) parsing — -//! `CotpHeader`, `CotpTpduType`, `parse_cotp_header` — is explicitly out of scope here -//! and is delivered by STORY-185 (VP-049). See ADR-014 Decision 9's scope note. +//! - STORY-184 delivered the TPKT (RFC 1006) outer framing header: `TpktHeader` and +//! `parse_tpkt_header` (BC-2.20.001–004; VP-048). +//! - STORY-185 adds the COTP (ISO 8073 / ITU-T X.224) inner TPDU header: +//! `CotpHeader`, `CotpTpduType`, `parse_cotp_header` (BC-2.20.005–012; VP-049). Note: +//! as of this story, `parse_cotp_header`'s body is a Red-Gate `todo!()` stub — the +//! implementation lands in this same story's implementer step; only the frozen types +//! and signature are final here. //! //! - `parse_tpkt_header` — 4-byte TPKT header parse; `None` on short/invalid input //! (BC-2.20.001–004); VP-048 Kani target. +//! - `parse_cotp_header` — COTP TPDU-type parse (CR/CC/DT) plus verbatim `protocol_id` +//! extraction; `None` on short/invalid/unrecognized input (BC-2.20.005–012); VP-049 +//! Kani target. //! //! ## Behavioral contracts //! - BC-2.20.001: `parse_tpkt_header` returns `None` for input shorter than 4 bytes. @@ -40,6 +46,20 @@ //! - BC-2.20.004: `parse_tpkt_header` returns `Some(TpktHeader)` for valid input //! (happy path); reserved byte (`data[1]`) is never validated; accept range is //! `[7, 65535]`; `length == 65535` is a legal accept. +//! - BC-2.20.005: `parse_cotp_header` returns `None` for input shorter than 2 bytes. +//! - BC-2.20.006: `parse_cotp_header` returns `None` when the Length Indicator declares +//! more bytes than are present (LI-truncation). +//! - BC-2.20.007: `parse_cotp_header` recognizes Connect Request (CR) TPDUs. +//! - BC-2.20.008: `parse_cotp_header` recognizes Connect Confirm (CC) TPDUs. +//! - BC-2.20.009: `parse_cotp_header` recognizes DT TPDUs with a non-empty payload and +//! extracts `protocol_id`. +//! - BC-2.20.010: `parse_cotp_header` recognizes DT TPDUs with an empty payload +//! (`protocol_id: None`). +//! - BC-2.20.011: `parse_cotp_header` returns `None` for an unrecognized TPDU-type +//! code (high nibble not in `{0xE0, 0xD0, 0xF0}`). +//! - BC-2.20.012: `protocol_id` is extracted verbatim, never interpreted (frozen SS-20 +//! to SS-21 boundary) — `parse_cotp_header` never compares the extracted byte against +//! any specific value. //! //! ## Architecture compliance (ADR-014 Decision 4 — licensing) //! Forbidden dependencies (BANNED/AVOID — licensing violation or unclear provenance): @@ -130,6 +150,105 @@ pub fn parse_tpkt_header(data: &[u8]) -> Option { }) } +// --------------------------------------------------------------------------- +// COTP (ISO 8073 / ITU-T X.224) data types — STORY-185 +// --------------------------------------------------------------------------- +// +// Frozen interface (ADR-014 Decision 1, Decision 2 disambiguation table, Decision 9). +// `iso_on_tcp.rs` (SS-20) performs zero interpretation of `protocol_id` — the +// upper-layer-protocol disambiguation table (ADR-014 Decision 2) lives entirely in +// `S7commAnalyzer` (SS-21), built starting in STORY-186/STORY-187. + +/// The three COTP (ISO 8073) TPDU types this parser discriminates. +/// +/// Frozen per ADR-014 Decision 1 — exactly these 3 variants. This is deliberately not +/// an exhaustive enumeration of all ISO 8073 TPDU codes (DR, DC, ED, AK, EA, RJ, ER, and +/// others exist on the wire but are not modeled — BC-2.20.011 requires that any of +/// those 13 remaining high-nibble values causes `parse_cotp_header` to return `None` +/// rather than being force-fit into one of these three variants). +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum CotpTpduType { + /// CR — Connect Request. Session establishment; no upper-layer payload. + ConnectRequest, + /// CC — Connect Confirm. Session establishment; no upper-layer payload. + ConnectConfirm, + /// DT — Data Transfer. Carries an upper-layer payload, optionally prefixed by a + /// single protocol-ID byte (see [`CotpHeader::protocol_id`]). + DataTransfer, +} + +/// Parsed COTP (ISO 8073 / ITU-T X.224) header, as extracted from the TPKT payload +/// slice (i.e. `data[4..length]` from an already-accepted `TpktHeader`, +/// BC-2.20.004's accept path). +/// +/// Frozen per ADR-014 Decision 1 — exactly these three fields, no additional fields. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct CotpHeader { + /// Which of the three modeled TPDU types this frame is. + pub tpdu_type: CotpTpduType, + /// The raw, uninterpreted protocol-ID byte immediately following the COTP + /// fixed-and-variable header, when present. + /// + /// `Some(byte)` only for a [`CotpTpduType::DataTransfer`] TPDU whose payload is + /// non-empty (BC-2.20.009); `None` for `ConnectRequest`/`ConnectConfirm` (no + /// upper-layer payload exists yet — BC-2.20.007, BC-2.20.008) or when the DT + /// payload is empty (BC-2.20.010). + /// + /// This byte is extracted **verbatim** — `parse_cotp_header` never compares it + /// against any specific value (BC-2.20.012, ADR-014 Decision 2). SS-21 + /// (`S7commAnalyzer`) owns all disambiguation of this value. + pub protocol_id: Option, + /// Byte offset into `tpkt_payload` where the upper-layer payload begins + /// (`1 + LI`, where `LI` is the Length Indicator at `tpkt_payload[0]`). + pub payload_offset: usize, +} + +// --------------------------------------------------------------------------- +// COTP parse function — STORY-185 +// --------------------------------------------------------------------------- + +/// Parse a COTP (ISO 8073 / ITU-T X.224) TPDU header from `tpkt_payload`, the byte +/// slice following an already-accepted 4-byte TPKT header. +/// +/// Pure-core free function (ADR-014 Decision 9) — no I/O, no global state mutation, +/// no side effects, deterministic. VP-049 Kani P0 target. +/// +/// # Returns +/// +/// - `None` if `tpkt_payload.len() < 2` (BC-2.20.005) — the minimum readable COTP +/// prefix is the Length Indicator (LI, offset 0) plus the TPDU-code byte (offset 1). +/// - `None` if `tpkt_payload.len() < 1 + LI` (BC-2.20.006) — the LI declares more +/// bytes than are present (LI-truncation guard); no out-of-bounds index for any `u8` +/// LI value, including `0`. +/// - `Some(CotpHeader { tpdu_type: ConnectRequest, protocol_id: None, payload_offset })` +/// if `tpkt_payload[1] & 0xF0 == 0xE0` (BC-2.20.007), where +/// `payload_offset == 1 + LI`. +/// - `Some(CotpHeader { tpdu_type: ConnectConfirm, protocol_id: None, payload_offset })` +/// if `tpkt_payload[1] & 0xF0 == 0xD0` (BC-2.20.008), where +/// `payload_offset == 1 + LI`. +/// - `Some(CotpHeader { tpdu_type: DataTransfer, protocol_id: Some(tpkt_payload[payload_offset]), +/// payload_offset })` if `tpkt_payload[1] & 0xF0 == 0xF0` and +/// `tpkt_payload.len() > payload_offset` (BC-2.20.009) — `protocol_id` is the +/// trailing byte, extracted verbatim. +/// - `Some(CotpHeader { tpdu_type: DataTransfer, protocol_id: None, payload_offset })` +/// if `tpkt_payload[1] & 0xF0 == 0xF0` and `tpkt_payload.len() == payload_offset` +/// exactly (BC-2.20.010) — no out-of-bounds index at `tpkt_payload[payload_offset]`. +/// - `None` for any other high-nibble value (BC-2.20.011) — the 13 remaining ISO 8073 +/// TPDU codes (DR, DC, ED, AK, EA, RJ, ER, and others) are never modeled and never +/// force-fit into CR, CC, or DT. +/// +/// These six outcomes are jointly exhaustive and mutually exclusive by construction +/// over all 16 high-nibble values (BC-2.20.011 invariant 3; AC-185-008). Formalizing +/// that partition, plus the `protocol_id` totality property (BC-2.20.012), is the +/// VP-049 Kani obligation: the assertions are added and executed in STORY-194 (formal +/// hardening); the `#[cfg(kani)]` skeleton below is scoped to check only +/// no-panic/bounds-safety over symbolic input — its proof is executed in STORY-194 +/// (not run in this story). +pub fn parse_cotp_header(tpkt_payload: &[u8]) -> Option { + let _ = tpkt_payload; + todo!("parse_cotp_header: implemented in STORY-185's implementer step (BC-2.20.005-012)") +} + // --------------------------------------------------------------------------- // VP-048 Kani proof — parse_tpkt_header safety (ADR-014 Decision 9) // --------------------------------------------------------------------------- @@ -159,4 +278,24 @@ mod kani_proofs { // Must not panic for any input: let _ = parse_tpkt_header(&data); } + + /// VP-049: `parse_cotp_header` must not panic for any input, up to the bounded + /// length (`len <= 300`). + /// + /// SCOPE (this story): no-panic / bounds-safety only, mirroring the VP-048 harness + /// pattern above. The full VP-049 proof obligation — TPDU-type classification + /// exhaustiveness over all 16 high-nibble values (BC-2.20.011 invariant 3) and + /// protocol-ID-extraction totality over all 256 `u8` values (BC-2.20.012) — is + /// deferred to STORY-194 (formal hardening), per this story's Kani obligation note. + #[kani::proof] + fn verify_parse_cotp_header_safety() { + let len: usize = kani::any(); + kani::assume(len <= 300); + let mut data = vec![0u8; len]; + for b in data.iter_mut() { + *b = kani::any(); + } + // Must not panic for any input, including the LI-truncation bounds check: + let _ = parse_cotp_header(&data); + } } From 4f370a4a41764337748e9ee432585fd2efd0c7c8 Mon Sep 17 00:00:00 2001 From: Zious Date: Sun, 6 Sep 2026 21:33:33 -0500 Subject: [PATCH 2/9] test(STORY-185): failing COTP TPDU parse tests (Red, BC-2.20.005-012) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds mod story_185 to tests/iso_on_tcp_tests.rs covering BC-2.20.005 through BC-2.20.012 for parse_cotp_header (COTP TPDU-type recognition and verbatim protocol_id extraction). 21 tests exercise the todo!() stub and fail (Red Gate, BC-5.38.001); one static source-inspection test (regression guard for 0x32/0x72 literals) legitimately passes without implementation. Pre-existing mod story_184 (30 tests) remains green and untouched. Includes an independent ISO 8073 holdout (DF-CANONICAL-FRAME-HOLDOUT-001) derived from RFC 905 ("ISO Transport Protocol Specification ISO DP 8073"), fetched and cross-checked directly (§13.2, §13.2.1, §13.2.2.2, Table 8, §13.7.1), rather than copied from this project's own BC text. Claude-Session: https://claude.ai/code/session_01EQAaPvh9fwaG31jmkPicKW --- tests/iso_on_tcp_tests.rs | 700 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 700 insertions(+) diff --git a/tests/iso_on_tcp_tests.rs b/tests/iso_on_tcp_tests.rs index 0bd70645..27ba63a3 100644 --- a/tests/iso_on_tcp_tests.rs +++ b/tests/iso_on_tcp_tests.rs @@ -773,3 +773,703 @@ mod story_184 { } } } + +/// Tests for STORY-185: S7comm COTP TPDU-Type Parser (pure-core free function). +/// +/// Covers BC-2.20.005 through BC-2.20.012 and the edge cases enumerated in each BC. +/// +/// ## Contract coverage +/// - BC-2.20.005: `parse_cotp_header` returns `None` for input shorter than 2 bytes. +/// - BC-2.20.006: `parse_cotp_header` returns `None` when the Length Indicator (LI) +/// declares more header bytes than are present (LI-truncation). +/// - BC-2.20.007: `parse_cotp_header` recognizes Connect Request (CR) TPDUs +/// (`tpkt_payload[1] & 0xF0 == 0xE0`), `protocol_id: None`. +/// - BC-2.20.008: `parse_cotp_header` recognizes Connect Confirm (CC) TPDUs +/// (`tpkt_payload[1] & 0xF0 == 0xD0`), `protocol_id: None`. +/// - BC-2.20.009: `parse_cotp_header` recognizes Data Transfer (DT) TPDUs +/// (`tpkt_payload[1] & 0xF0 == 0xF0`) with a non-empty payload and extracts +/// `protocol_id` verbatim. +/// - BC-2.20.010: `parse_cotp_header` recognizes DT TPDUs with an empty payload +/// (`protocol_id: None`). +/// - BC-2.20.011: `parse_cotp_header` returns `None` for an unrecognized TPDU-type +/// code (high nibble not in `{0xE0, 0xD0, 0xF0}`); never force-fit. +/// - BC-2.20.012: `protocol_id` is extracted verbatim, never interpreted (frozen SS-20 +/// to SS-21 boundary) — `parse_cotp_header` never compares the extracted byte +/// against any specific value. +/// +/// ## Test naming convention +/// Tests follow `test_BC_S_SS_NNN_xxx()` for BC-traceable tests, matching the +/// AC-185-00x `**Test:**` citations in STORY-185.md. The non_snake_case lint fires on +/// uppercase BC IDs — suppressed by the file-level `#![allow(non_snake_case)]` at the +/// top of this file, which applies crate-wide to this whole test binary. +/// +/// ## Provenance +/// Authored Red-first as TDD stubs (STORY-185 `tdd_mode: strict`; BC-2.20.005-012) +/// against the `todo!()` stub in `src/analyzer/iso_on_tcp.rs`'s `parse_cotp_header`. +/// These tests are expected to fail (compile, then panic on the `todo!()`) until the +/// STORY-185 implementer step replaces the stub body; Red Gate verification +/// (BC-5.38.001) runs `cargo test --test iso_on_tcp_tests` and requires every test in +/// this module to fail while the pre-existing `story_184` module continues to pass. +/// +/// ## Literal-avoidance note (BC-2.20.012 / AC-185-009) +/// Per BC-2.20.012's frozen SS-20/SS-21 boundary, `protocol_id` is a raw, uninterpreted +/// byte at this layer — S7comm (`0x32`) / S7comm-plus (`0x72`) disambiguation belongs to +/// SS-21 (`S7commAnalyzer`, STORY-186+), not to this module or its tests. This test +/// module therefore deliberately never writes the literal byte values `0x32` or `0x72`, +/// nor the strings "S7comm"/"S7comm-plus", anywhere in source text — the totality sweep +/// below (`test_BC_2_20_012_protocol_id_extraction_totality`) still exercises those two +/// byte *values* at runtime (they arise dynamically from a `0u8..=255u8` loop), without +/// either value ever appearing as a literal token in this file. +/// +/// ## Canonical test vectors and the independent ISO 8073 holdout +/// Most vectors below are canonical test vectors copied verbatim from BC-2.20.005-012. +/// Per DF-CANONICAL-FRAME-HOLDOUT-001, the `test_iso8073_rfc905_*` holdout tests near +/// the end of this module are authored independently of this project's BCs, derived +/// directly from RFC 905 ("ISO Transport Protocol Specification ISO DP 8073" — a +/// freely accessible IETF mirror of the ISO Transport Protocol text that the project's +/// own BCs cite as ISO 8073 / ITU-T X.224), fetched and cross-checked against this +/// project's BC citations while drafting this file. Citations below reference specific +/// RFC 905 section numbers and Table 8 ("TPDU code") verified directly against the +/// fetched document text, not assumed from memory. +// +// Per DF-TEST-NAMESPACE-001: all STORY-185 tests are grouped inside a dedicated +// `mod story_185` wrapper to prevent test-function name collisions with other +// stories' BC-prefixed names (in particular, the pre-existing `mod story_184` above). +mod story_185 { + use wirerust::analyzer::iso_on_tcp::{CotpHeader, CotpTpduType, parse_cotp_header}; + + // ========================================================================= + // BC-2.20.005: parse_cotp_header returns None for input shorter than 2 bytes + // AC-185-001 + // ========================================================================= + + /// BC-2.20.005 canonical vectors: empty slice and one-byte slice both return None. + /// + /// Canonical vectors from BC-2.20.005: `[]` (0 bytes) -> None; `[0x02]` (1 byte, + /// EC-002) -> None. Precondition: `tpkt_payload.len() < 2`. Postcondition 2: no + /// bytes accessed beyond the length check, no panic even for `len() == 0` (EC-001). + /// + /// Traces: BC-2.20.005 postconditions 1-3; AC-185-001; EC-001; EC-002; canonical + /// test vectors. + #[test] + fn test_BC_2_20_005_len_shorter_than_2_returns_none() { + let result_empty = parse_cotp_header(&[]); + assert_eq!( + result_empty, None, + "empty tpkt_payload must return None (BC-2.20.005 postcondition 1, EC-001)" + ); + + let result_one_byte = parse_cotp_header(&[0x02]); + assert_eq!( + result_one_byte, None, + "1-byte tpkt_payload must return None (BC-2.20.005 canonical vector, EC-002)" + ); + } + + /// BC-2.20.005 invariant: no panic for any 0- or 1-byte input, including all-zero + /// and all-0xFF content. + /// + /// Traces: BC-2.20.005 invariants 1-3; AC-185-001. + #[test] + fn test_BC_2_20_005_invariant_no_panic_across_short_inputs() { + let inputs: &[&[u8]] = &[&[], &[0x00], &[0xFF], &[0x02]]; + for &data in inputs { + let result = parse_cotp_header(data); + assert_eq!( + result, + None, + "input of len {} must return None for len < 2 (BC-2.20.005)", + data.len() + ); + } + } + + // ========================================================================= + // BC-2.20.006: parse_cotp_header returns None when LI declares more bytes than + // are present (LI-truncation) + // AC-185-002 + // ========================================================================= + + /// BC-2.20.006 canonical vectors: LI declares more remaining header bytes than + /// `tpkt_payload` actually contains. + /// + /// Canonical vectors from BC-2.20.006: `[0x06, 0xE0, 0x00, 0x01]` (LI=6, only 3 + /// bytes follow the LI octet; EC-001, truncated CR header) -> None; `[0x02, 0xF0]` + /// (LI=2, only 1 byte follows; EC-002, truncated DT header) -> None. + /// + /// Traces: BC-2.20.006 postconditions 1-2; AC-185-002; EC-001; EC-002; canonical + /// test vectors. + #[test] + fn test_BC_2_20_006_li_truncation_returns_none() { + let truncated_cr: &[u8] = &[0x06, 0xE0, 0x00, 0x01]; + assert_eq!( + parse_cotp_header(truncated_cr), + None, + "LI=6 declaring 6 more bytes with only 3 present must return None \ + (BC-2.20.006 canonical vector, EC-001)" + ); + + let truncated_dt: &[u8] = &[0x02, 0xF0]; + assert_eq!( + parse_cotp_header(truncated_dt), + None, + "LI=2 declaring 2 more bytes with only 1 present must return None \ + (BC-2.20.006 canonical vector, EC-002)" + ); + } + + /// BC-2.20.006 invariant 2: no out-of-bounds index / panic for LI values spanning + /// the full `u8` range, including the maximum LI value (255). + /// + /// Traces: BC-2.20.006 invariant 2; AC-185-002. + #[test] + fn test_BC_2_20_006_invariant_no_panic_across_li_value_sample() { + for li in [0x01u8, 0x0A, 0x7F, 0xFE, 0xFF] { + let data: [u8; 3] = [li, 0xE0, 0x00]; + let result = parse_cotp_header(&data); + assert_eq!( + result, None, + "LI={li:#04x} declaring more bytes than the 3-byte input contains must \ + return None with no panic (BC-2.20.006 invariant 2)" + ); + } + } + + /// BC-2.20.006 EC-003: `LI == 0` is a degenerate but not-truncated case + /// (`1 + 0 <= len`) — the truncation check passes and classification proceeds. The + /// TPDU-code byte (`tpkt_payload[1]`) doubles as the sole payload byte at + /// `payload_offset == 1`, since the fixed header contributes zero further bytes. + /// + /// Traces: BC-2.20.006 EC-003; AC-185-002 (boundary case demonstrating the + /// truncation guard does not over-reject `LI == 0`). + #[test] + fn test_BC_2_20_006_li_zero_not_truncated_proceeds_to_classification() { + let data: &[u8] = &[0x00, 0xF0]; + let result = parse_cotp_header(data); + assert_eq!( + result, + Some(CotpHeader { + tpdu_type: CotpTpduType::DataTransfer, + protocol_id: Some(0xF0), + payload_offset: 1, + }), + "LI=0 must not be rejected as truncated; classification proceeds to DT \ + recognition with payload_offset == 1 (BC-2.20.006 EC-003)" + ); + } + + // ========================================================================= + // BC-2.20.007: parse_cotp_header recognizes Connect Request (CR) TPDU + // AC-185-003 + // ========================================================================= + + /// BC-2.20.007 canonical vector: minimal CR TPDU (`LI == 6`). + /// + /// Canonical vector from BC-2.20.007: `[0x06, 0xE0, 0x00, 0x00, 0x00, 0x01, 0x00]` + /// (LI=6, CR, DST-REF=0x0000, SRC-REF=0x0001, class=0) -> + /// `Some(CotpHeader{tpdu_type: ConnectRequest, protocol_id: None, payload_offset: 7})`. + /// + /// Traces: BC-2.20.007 postconditions 1-2; AC-185-003; EC-004; canonical test vector. + #[test] + fn test_BC_2_20_007_connect_request_recognized() { + let data: &[u8] = &[0x06, 0xE0, 0x00, 0x00, 0x00, 0x01, 0x00]; + let result = parse_cotp_header(data); + assert_eq!( + result, + Some(CotpHeader { + tpdu_type: CotpTpduType::ConnectRequest, + protocol_id: None, + payload_offset: 7, + }), + "minimal CR TPDU must decode to ConnectRequest, protocol_id: None, \ + payload_offset: 7 (BC-2.20.007 canonical vector)" + ); + } + + /// BC-2.20.007 EC-002: a non-zero low nibble on the TPDU-code byte (`0xE1`) does + /// not affect CR recognition — only the high nibble is inspected. + /// + /// Traces: BC-2.20.007 invariant 2; AC-185-003; EC-002. + #[test] + fn test_BC_2_20_007_connect_request_nonzero_low_nibble_still_recognized() { + let data: &[u8] = &[0x06, 0xE1, 0x00, 0x00, 0x00, 0x01, 0x00]; + let result = parse_cotp_header(data); + assert_eq!( + result, + Some(CotpHeader { + tpdu_type: CotpTpduType::ConnectRequest, + protocol_id: None, + payload_offset: 7, + }), + "TPDU-code 0xE1 (non-zero low nibble) must still be recognized as CR \ + (BC-2.20.007 EC-002, high-nibble-only discrimination)" + ); + } + + /// BC-2.20.007 postcondition 3: `protocol_id` is unconditionally `None` for a CR + /// TPDU, even when bytes are present in `tpkt_payload` beyond the fixed CR header. + /// + /// Uses a trailing byte (`0xAB`) beyond `payload_offset` to prove that no + /// upper-layer-payload interpretation is ever attempted for CR. + /// + /// Traces: BC-2.20.007 postcondition 3; AC-185-003. + #[test] + fn test_BC_2_20_007_connect_request_protocol_id_none_even_with_trailing_bytes() { + let data: &[u8] = &[0x06, 0xE0, 0x00, 0x00, 0x00, 0x01, 0x00, 0xAB]; + let result = parse_cotp_header(data); + assert_eq!( + result, + Some(CotpHeader { + tpdu_type: CotpTpduType::ConnectRequest, + protocol_id: None, + payload_offset: 7, + }), + "protocol_id must remain None for CR even with a trailing byte present \ + beyond the fixed CR header (BC-2.20.007 postcondition 3)" + ); + } + + // ========================================================================= + // BC-2.20.008: parse_cotp_header recognizes Connect Confirm (CC) TPDU + // AC-185-004 + // ========================================================================= + + /// BC-2.20.008 canonical vector: minimal CC TPDU (`LI == 6`). + /// + /// Canonical vector from BC-2.20.008: `[0x06, 0xD0, 0x00, 0x01, 0x00, 0x00, 0x00]` + /// (LI=6, CC, DST-REF=0x0001, SRC-REF=0x0000, class=0) -> + /// `Some(CotpHeader{tpdu_type: ConnectConfirm, protocol_id: None, payload_offset: 7})`. + /// + /// Traces: BC-2.20.008 postconditions 1-3; AC-185-004; EC-004; canonical test vector. + #[test] + fn test_BC_2_20_008_connect_confirm_recognized() { + let data: &[u8] = &[0x06, 0xD0, 0x00, 0x01, 0x00, 0x00, 0x00]; + let result = parse_cotp_header(data); + assert_eq!( + result, + Some(CotpHeader { + tpdu_type: CotpTpduType::ConnectConfirm, + protocol_id: None, + payload_offset: 7, + }), + "minimal CC TPDU must decode to ConnectConfirm, protocol_id: None, \ + payload_offset: 7 (BC-2.20.008 canonical vector)" + ); + } + + /// BC-2.20.008 EC-002: a non-zero low nibble on the TPDU-code byte (`0xD1`) does + /// not affect CC recognition. + /// + /// Traces: BC-2.20.008 invariant 2; AC-185-004; EC-002. + #[test] + fn test_BC_2_20_008_connect_confirm_nonzero_low_nibble_still_recognized() { + let data: &[u8] = &[0x06, 0xD1, 0x00, 0x01, 0x00, 0x00, 0x00]; + let result = parse_cotp_header(data); + assert_eq!( + result, + Some(CotpHeader { + tpdu_type: CotpTpduType::ConnectConfirm, + protocol_id: None, + payload_offset: 7, + }), + "TPDU-code 0xD1 (non-zero low nibble) must still be recognized as CC \ + (BC-2.20.008 EC-002, high-nibble-only discrimination)" + ); + } + + // ========================================================================= + // BC-2.20.009: parse_cotp_header recognizes DT with non-empty payload and + // extracts protocol_id + // AC-185-005 + // ========================================================================= + + /// BC-2.20.009 canonical-vector-shaped test (EC-004 variant): minimal DT TPDU + /// (`LI == 2`) with a non-`0x32`/`0x72` protocol-ID byte (`0x01`, simulating an + /// MMS/ICCP or otherwise-unrecognized upper-layer protocol), extracted verbatim. + /// + /// Per this test module's literal-avoidance note, the canonical `0x32`/`0x72` + /// vectors from BC-2.20.009's own table are not reproduced verbatim here (that + /// would place the literals `0x32`/`0x72` in this file); EC-004's `0x01` vector is + /// used instead, which is equally a canonical BC-2.20.009 test vector. + /// + /// Traces: BC-2.20.009 postconditions 1-3; AC-185-005; EC-004; canonical test vector. + #[test] + fn test_BC_2_20_009_dt_nonempty_payload_extracts_protocol_id() { + let data: &[u8] = &[0x02, 0xF0, 0x80, 0x01]; + let result = parse_cotp_header(data); + assert_eq!( + result, + Some(CotpHeader { + tpdu_type: CotpTpduType::DataTransfer, + protocol_id: Some(0x01), + payload_offset: 3, + }), + "minimal DT TPDU with a non-empty payload must extract protocol_id \ + verbatim, payload_offset: 3 (BC-2.20.009 canonical vector, EC-004)" + ); + } + + /// BC-2.20.009 postcondition 2: `protocol_id` is exactly the byte at + /// `tpkt_payload[payload_offset]` — only the first trailing byte, never a later one, + /// regardless of how many further bytes follow. + /// + /// Traces: BC-2.20.009 postcondition 2; AC-185-005. + #[test] + fn test_BC_2_20_009_dt_protocol_id_is_first_trailing_byte_only() { + let data: &[u8] = &[0x02, 0xF0, 0x80, 0x01, 0x02, 0x03, 0x04]; + let result = parse_cotp_header(data); + assert_eq!( + result, + Some(CotpHeader { + tpdu_type: CotpTpduType::DataTransfer, + protocol_id: Some(0x01), + payload_offset: 3, + }), + "protocol_id must be exactly tpkt_payload[payload_offset] (0x01), never a \ + later trailing byte (BC-2.20.009 postcondition 2)" + ); + } + + /// BC-2.20.009 / BC-2.20.012 boundary values: the protocol-ID byte is extracted + /// verbatim at both `u8` extremes (`0x00` and `0xFF`), with identical `tpdu_type` + /// and `payload_offset` across both. + /// + /// Traces: BC-2.20.009 postcondition 2; BC-2.20.012 EC-003, EC-004; AC-185-005. + #[test] + fn test_BC_2_20_009_dt_protocol_id_extracted_for_boundary_byte_values() { + let data_min: &[u8] = &[0x02, 0xF0, 0x80, 0x00]; + assert_eq!( + parse_cotp_header(data_min), + Some(CotpHeader { + tpdu_type: CotpTpduType::DataTransfer, + protocol_id: Some(0x00), + payload_offset: 3, + }), + "protocol-ID byte 0x00 (minimum u8) must be extracted verbatim \ + (BC-2.20.012 EC-004)" + ); + + let data_max: &[u8] = &[0x02, 0xF0, 0x80, 0xFF]; + assert_eq!( + parse_cotp_header(data_max), + Some(CotpHeader { + tpdu_type: CotpTpduType::DataTransfer, + protocol_id: Some(0xFF), + payload_offset: 3, + }), + "protocol-ID byte 0xFF (maximum u8) must be extracted verbatim \ + (BC-2.20.012 EC-003)" + ); + } + + // ========================================================================= + // BC-2.20.010: parse_cotp_header recognizes DT with empty payload — + // protocol_id is None + // AC-185-006 + // ========================================================================= + + /// BC-2.20.010 canonical vector: minimal DT TPDU (`LI == 2`) with zero trailing + /// payload bytes (`tpkt_payload.len() == payload_offset` exactly). + /// + /// Canonical vector from BC-2.20.010: `[0x02, 0xF0, 0x80]` (LI=2, DT, TPDU-NR=0x80, + /// no trailing payload byte) -> + /// `Some(CotpHeader{tpdu_type: DataTransfer, protocol_id: None, payload_offset: 3})`. + /// + /// Traces: BC-2.20.010 postconditions 1-2; AC-185-006; EC-001; canonical test vector. + #[test] + fn test_BC_2_20_010_dt_empty_payload_protocol_id_none() { + let data: &[u8] = &[0x02, 0xF0, 0x80]; + let result = parse_cotp_header(data); + assert_eq!( + result, + Some(CotpHeader { + tpdu_type: CotpTpduType::DataTransfer, + protocol_id: None, + payload_offset: 3, + }), + "minimal DT TPDU with zero trailing payload bytes must return \ + protocol_id: None, payload_offset: 3 (BC-2.20.010 canonical vector)" + ); + } + + // ========================================================================= + // BC-2.20.011: parse_cotp_header returns None for an unrecognized TPDU-type code + // AC-185-007, AC-185-008 + // ========================================================================= + + /// BC-2.20.011 canonical vectors: DR, DC, ER, and all-zero TPDU-code bytes are + /// never force-fit into CR/CC/DT. + /// + /// Canonical vectors from BC-2.20.011: `[0x02, 0x80, 0x00]` (DR-shaped) -> None; + /// `[0x02, 0xC0, 0x00]` (DC-shaped) -> None; `[0x02, 0x70, 0x00]` (ER-shaped) -> + /// None; `[0x02, 0x00, 0x00]` (all-zero) -> None. + /// + /// Traces: BC-2.20.011 postconditions 1-2; AC-185-007; EC-001, EC-002, EC-003, + /// EC-004; canonical test vectors. + #[test] + fn test_BC_2_20_011_unrecognized_tpdu_type_returns_none() { + let cases: &[(&[u8], &str)] = &[ + (&[0x02, 0x80, 0x00], "DR-shaped (0x8_)"), + (&[0x02, 0xC0, 0x00], "DC-shaped (0xC_)"), + (&[0x02, 0x70, 0x00], "ER-shaped (0x7_)"), + (&[0x02, 0x00, 0x00], "all-zero TPDU-code byte"), + ]; + for (data, label) in cases { + assert_eq!( + parse_cotp_header(data), + None, + "{label} must return None, never force-fit into CR/CC/DT \ + (BC-2.20.011 canonical vector)" + ); + } + } + + /// AC-185-008 / BC-2.20.011 invariant 3: the four-way TPDU-type match is + /// exhaustive and non-overlapping over all 16 possible high-nibble values of + /// `tpkt_payload[1]`. Every input below shares the same shape (`LI = 2`, 3 bytes + /// total: LI, TPDU-code, one trailing byte) so that CR/CC (no payload check) and DT + /// (payload check against `payload_offset == 3`, exactly satisfied by this 3-byte + /// shape) all reach a defined, well-typed outcome; the remaining 13 nibble values + /// must all reject. + /// + /// This is a unit-level spot check, not exhaustive over all `&[u8]` shapes (that is + /// the VP-049 Kani obligation, deferred to STORY-194) — it exhaustively covers the + /// 16-value high-nibble domain for one fixed input shape. + /// + /// Traces: BC-2.20.011 invariant 3; AC-185-008. + #[test] + fn test_BC_2_20_011_tpdu_type_match_is_exhaustive() { + for nibble in 0x0u8..=0xF { + let code_byte = nibble << 4; + let data: [u8; 3] = [0x02, code_byte, 0x00]; + let result = parse_cotp_header(&data); + let expected = match nibble { + 0xE => Some(CotpHeader { + tpdu_type: CotpTpduType::ConnectRequest, + protocol_id: None, + payload_offset: 3, + }), + 0xD => Some(CotpHeader { + tpdu_type: CotpTpduType::ConnectConfirm, + protocol_id: None, + payload_offset: 3, + }), + 0xF => Some(CotpHeader { + tpdu_type: CotpTpduType::DataTransfer, + protocol_id: None, + payload_offset: 3, + }), + _ => None, + }; + assert_eq!( + result, expected, + "high nibble {nibble:#x} must classify to exactly one outcome \ + (AC-185-008, BC-2.20.011 invariant 3)" + ); + } + } + + // ========================================================================= + // BC-2.20.012: protocol_id is extracted verbatim, never interpreted + // AC-185-009 + // ========================================================================= + + /// BC-2.20.012 postconditions 1-2: the protocol-ID extraction is a total identity + /// mapping over every possible `u8` value — an exhaustive sweep over all 256 + /// values, not a random sample, so this totality claim is fully covered rather than + /// probabilistically covered. `tpdu_type` and `payload_offset` must stay constant + /// across the entire sweep; only `protocol_id` varies with the input byte. + /// + /// This sweep necessarily also exercises the two byte values a downstream SS-21 + /// disambiguation table would treat specially, but neither value is ever written as + /// a literal token in this file (see the file-level literal-avoidance note) — both + /// arise only at runtime from the `0u8..=255u8` loop bound. + /// + /// Traces: BC-2.20.012 postconditions 1-2; invariant 2; AC-185-009. + #[test] + fn test_BC_2_20_012_protocol_id_extraction_totality() { + for byte in 0u8..=255u8 { + let data: [u8; 4] = [0x02, 0xF0, 0x80, byte]; + let result = parse_cotp_header(&data); + assert_eq!( + result, + Some(CotpHeader { + tpdu_type: CotpTpduType::DataTransfer, + protocol_id: Some(byte), + payload_offset: 3, + }), + "protocol_id extraction must be the identity function for byte \ + {byte:#04x} (BC-2.20.012 postcondition 1, exhaustive 256-value sweep)" + ); + } + } + + /// BC-2.20.012 postcondition 3 / AC-185-009 static regression guard: the source + /// file must contain zero occurrences of the literals `0x32` or `0x72` anywhere — + /// these are the classic-S7comm and S7comm-plus protocol-ID values respectively, + /// and their interpretation belongs entirely to `S7commAnalyzer` (SS-21), never to + /// this module's parsing logic. + /// + /// This is a whole-file substring check (not scoped to excluding doc comments): as + /// of this story, `src/analyzer/iso_on_tcp.rs` contains zero occurrences of either + /// literal anywhere, including in doc comments, so a whole-file check is the + /// correct, unambiguous regression guard — a future doc comment introducing either + /// literal would itself be exactly the kind of drift this guard exists to catch. + /// + /// Traces: BC-2.20.012 postcondition 3; AC-185-009 (static regression-guard test). + #[test] + fn test_BC_2_20_012_static_regression_guard_no_hardcoded_protocol_literals() { + let source = std::fs::read_to_string(concat!( + env!("CARGO_MANIFEST_DIR"), + "/src/analyzer/iso_on_tcp.rs" + )) + .expect("src/analyzer/iso_on_tcp.rs must be readable for the regression guard"); + + // Constructed via concatenation so this file itself never contains the literal + // substrings "0x32"/"0x72" as contiguous text either. + let classic_s7comm_literal = ["0x", "32"].concat(); + let s7comm_plus_literal = ["0x", "72"].concat(); + + assert!( + !source.contains(&classic_s7comm_literal), + "src/analyzer/iso_on_tcp.rs must not contain the literal {classic_s7comm_literal} \ + anywhere (BC-2.20.012 postcondition 3) — S7comm disambiguation belongs to SS-21" + ); + assert!( + !source.contains(&s7comm_plus_literal), + "src/analyzer/iso_on_tcp.rs must not contain the literal {s7comm_plus_literal} \ + anywhere (BC-2.20.012 postcondition 3) — S7comm-plus disambiguation belongs to SS-21" + ); + } + + // ========================================================================= + // DF-CANONICAL-FRAME-HOLDOUT-001: independent ISO 8073 holdout vectors. + // + // Unlike every vector above (which traces to this project's own BC-2.20.005-012 + // text), the vectors below are derived directly from RFC 905 ("ISO Transport + // Protocol Specification ISO DP 8073"), an IETF-published, freely accessible + // mirror of the ISO Transport Protocol specification text — fetched directly and + // cross-checked line-by-line while drafting this file, independently of this + // project's own BC citations to ISO 8073 / ITU-T X.224. + // + // Verified citations (RFC 905, section numbers and Table 8 read directly from the + // fetched document text): + // - §13.2 "Structure": TPDUs contain, in order, the LI field, the fixed part, + // the variable part (if present), then the data field. + // - §13.2.1 "Length indicator field": LI occupies the first octet of the TPDU; + // its value is "the header length in octets including parameters, but + // excluding the length indicator field and user data, if any." + // - §13.2.2.2 "TPDU code": contained in octet 2 of the header. + // - Table 8 "TPDU code" (page 115): CR = `1110 xxxx` (clause 13.3), CC = + // `1101 xxxx` (clause 13.4), DR = `1000 0000` (clause 13.5), DT = `1111 0000` + // (clause 13.7). + // - §13.7.1 "Structure", format (a) "Normal format for Classes 0 and 1": DT TPDU + // = LI | DT code (octet 2) | TPDU-NR and EOT (octet 3) | User Data (octet 4+). + // ========================================================================= + + /// ISO 8073 holdout: Table 8's `1110 xxxx` CR code and `1101 xxxx` CC code both + /// reserve bits 4-1 (the low nibble) for CDT signaling, confirming (independently + /// of BC-2.20.007/008's own EC-002 vectors) that only the high nibble discriminates + /// TPDU type — using different low-nibble values than either BC's canonical + /// vectors. + /// + /// Traces: DF-CANONICAL-FRAME-HOLDOUT-001 (spec-independent holdout, not a BC + /// vector); RFC 905 §13.2.2.2, Table 8. + #[test] + fn test_iso8073_rfc905_table8_cr_cc_low_nibble_is_free_holdout() { + let cr_data: &[u8] = &[0x06, 0xEF, 0x00, 0x00, 0x00, 0x01, 0x00]; + assert_eq!( + parse_cotp_header(cr_data), + Some(CotpHeader { + tpdu_type: CotpTpduType::ConnectRequest, + protocol_id: None, + payload_offset: 7, + }), + "RFC 905 Table 8: CR code is 1110 xxxx — low nibble 0xF must not prevent \ + CR recognition" + ); + + let cc_data: &[u8] = &[0x06, 0xDA, 0x00, 0x01, 0x00, 0x00, 0x00]; + assert_eq!( + parse_cotp_header(cc_data), + Some(CotpHeader { + tpdu_type: CotpTpduType::ConnectConfirm, + protocol_id: None, + payload_offset: 7, + }), + "RFC 905 Table 8: CC code is 1101 xxxx — low nibble 0xA must not prevent \ + CC recognition" + ); + } + + /// ISO 8073 holdout: Table 8's Disconnect Request (DR) code is the fixed octet + /// `1000 0000` (clause 13.5) — a TPDU type this project's `CotpTpduType` (frozen to + /// exactly 3 variants) deliberately does not model. `parse_cotp_header` must reject + /// it, not force-fit it to the "closest" recognized type. + /// + /// Traces: DF-CANONICAL-FRAME-HOLDOUT-001 (spec-independent holdout, not a BC + /// vector); RFC 905 §13.2.2.2, Table 8, clause 13.5. + #[test] + fn test_iso8073_rfc905_table8_dr_code_not_modeled_holdout() { + let data: &[u8] = &[0x02, 0x80, 0x00]; + assert_eq!( + parse_cotp_header(data), + None, + "RFC 905 Table 8: DR (Disconnect Request) code 1000 0000 is not one of the \ + 3 frozen CotpTpduType variants and must return None" + ); + } + + /// ISO 8073 holdout: RFC 905 §13.7.1 format (a) ("Normal format for Classes 0 and + /// 1") defines the DT TPDU's fixed part as exactly 2 octets — the DT code (octet 2) + /// and the combined TPDU-NR/EOT byte (octet 3) — so `LI == 2` and user data begins + /// at octet 4, i.e. `payload_offset == 1 + LI == 3`. This vector uses a distinct + /// TPDU-NR/EOT byte (`0xC0`) and a distinct user-data byte (`0x99`) from every + /// BC-2.20.009/010 canonical vector, to independently confirm the LI-to- + /// payload-offset arithmetic rather than reusing a BC-derived byte pattern. + /// + /// Traces: DF-CANONICAL-FRAME-HOLDOUT-001 (spec-independent holdout, not a BC + /// vector); RFC 905 §13.2.1, §13.7.1 format (a). + #[test] + fn test_iso8073_rfc905_s13_7_1_dt_class0_normal_format_holdout() { + let data: &[u8] = &[0x02, 0xF0, 0xC0, 0x99]; + assert_eq!( + parse_cotp_header(data), + Some(CotpHeader { + tpdu_type: CotpTpduType::DataTransfer, + protocol_id: Some(0x99), + payload_offset: 3, + }), + "RFC 905 §13.7.1 format (a): class-0 DT fixed part is exactly 2 octets \ + (DT code + TPDU-NR/EOT), so payload_offset == 1 + LI == 3 and the trailing \ + byte is the verbatim protocol-ID" + ); + } + + /// ISO 8073 holdout: RFC 905 §13.2.1 states the LI value "shall be the header + /// length in octets including parameters, but excluding the length indicator field + /// and user data" — i.e. LI counts everything in the header *after* the LI octet + /// itself. This vector reconstructs a minimal CR TPDU (fixed part = TPDU-code + + /// 2-byte DST-REF + 2-byte SRC-REF + 1-byte class/options = 6 octets, so `LI == 6`) + /// using DST-REF/SRC-REF values distinct from BC-2.20.007's own canonical vector, + /// to independently confirm `payload_offset == 1 + LI` rather than reusing a + /// BC-derived byte pattern. + /// + /// Traces: DF-CANONICAL-FRAME-HOLDOUT-001 (spec-independent holdout, not a BC + /// vector); RFC 905 §13.2.1, §13.2 structure diagram, clause 13.3. + #[test] + fn test_iso8073_rfc905_s13_2_1_li_excludes_itself_holdout() { + let data: &[u8] = &[0x06, 0xE3, 0xAA, 0xBB, 0xCC, 0xDD, 0x00]; + assert_eq!( + parse_cotp_header(data), + Some(CotpHeader { + tpdu_type: CotpTpduType::ConnectRequest, + protocol_id: None, + payload_offset: 7, + }), + "RFC 905 §13.2.1: LI=6 counts the 6 octets of the CR fixed part following \ + the LI octet itself, so payload_offset == 1 + LI == 7, independent of the \ + DST-REF/SRC-REF byte values chosen" + ); + } +} From 0d26a80a2219f70072a6def70e99a93e32424eda Mon Sep 17 00:00:00 2001 From: Zious Date: Sun, 6 Sep 2026 21:36:02 -0500 Subject: [PATCH 3/9] wip(STORY-185): test_BC_2_20_005 passes (len<2 guard) Claude-Session: https://claude.ai/code/session_01EQAaPvh9fwaG31jmkPicKW --- src/analyzer/iso_on_tcp.rs | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/analyzer/iso_on_tcp.rs b/src/analyzer/iso_on_tcp.rs index c51e6f7c..57f1b95d 100644 --- a/src/analyzer/iso_on_tcp.rs +++ b/src/analyzer/iso_on_tcp.rs @@ -245,8 +245,17 @@ pub struct CotpHeader { /// no-panic/bounds-safety over symbolic input — its proof is executed in STORY-194 /// (not run in this story). pub fn parse_cotp_header(tpkt_payload: &[u8]) -> Option { - let _ = tpkt_payload; - todo!("parse_cotp_header: implemented in STORY-185's implementer step (BC-2.20.005-012)") + if tpkt_payload.len() < 2 { + return None; + } + let li = tpkt_payload[0] as usize; + if tpkt_payload.len() < 1 + li { + return None; + } + todo!( + "parse_cotp_header: TPDU-type classification implemented in a later \ + STORY-185 TDD step (BC-2.20.007-012)" + ) } // --------------------------------------------------------------------------- From ff5f9b01ce2f33e305e9a61fd9ffe7c185090cad Mon Sep 17 00:00:00 2001 From: Zious Date: Sun, 6 Sep 2026 21:38:02 -0500 Subject: [PATCH 4/9] wip(STORY-185): CR/CC/DT classification + protocol_id extraction passes (BC-2.20.007-012) Implements the TPDU-type match (CR 0xE0, CC 0xD0, DT 0xF0, else None) and verbatim protocol_id extraction for DT. 51/52 story_185+story_184 tests green; test_BC_2_20_006_invariant_no_panic_across_li_value_sample fails on its own sample value 0x01 (not a truncation case per BC-2.20.006's own formula against a 3-byte buffer) -- flagged as a test bug, not fixed here per no-test-modification constraint. Claude-Session: https://claude.ai/code/session_01EQAaPvh9fwaG31jmkPicKW --- src/analyzer/iso_on_tcp.rs | 31 +++++++++++++++++++++++++++---- 1 file changed, 27 insertions(+), 4 deletions(-) diff --git a/src/analyzer/iso_on_tcp.rs b/src/analyzer/iso_on_tcp.rs index 57f1b95d..930d7c96 100644 --- a/src/analyzer/iso_on_tcp.rs +++ b/src/analyzer/iso_on_tcp.rs @@ -252,10 +252,33 @@ pub fn parse_cotp_header(tpkt_payload: &[u8]) -> Option { if tpkt_payload.len() < 1 + li { return None; } - todo!( - "parse_cotp_header: TPDU-type classification implemented in a later \ - STORY-185 TDD step (BC-2.20.007-012)" - ) + let payload_offset = 1 + li; + let tpdu_code = tpkt_payload[1]; + match tpdu_code & 0xF0 { + 0xE0 => Some(CotpHeader { + tpdu_type: CotpTpduType::ConnectRequest, + protocol_id: None, + payload_offset, + }), + 0xD0 => Some(CotpHeader { + tpdu_type: CotpTpduType::ConnectConfirm, + protocol_id: None, + payload_offset, + }), + 0xF0 => { + let protocol_id = if tpkt_payload.len() > payload_offset { + Some(tpkt_payload[payload_offset]) + } else { + None + }; + Some(CotpHeader { + tpdu_type: CotpTpduType::DataTransfer, + protocol_id, + payload_offset, + }) + } + _ => None, + } } // --------------------------------------------------------------------------- From aa3f7a54d534d2bdf4940cb9bf5416b52148d2dd Mon Sep 17 00:00:00 2001 From: Zious Date: Sun, 6 Sep 2026 21:40:49 -0500 Subject: [PATCH 5/9] wip(STORY-185): update module docs + CHANGELOG for completed COTP parser Removes stale Red-Gate todo!() note from the module doc comment now that parse_cotp_header is implemented; adds an [Unreleased] CHANGELOG entry (AC-158-001) describing the COTP TPDU header parser. VP-049 Kani harness codegen verified clean (`cargo kani --only-codegen`); full proof execution remains deferred to STORY-194 per this story's scope note. Claude-Session: https://claude.ai/code/session_01EQAaPvh9fwaG31jmkPicKW --- CHANGELOG.md | 12 ++++++++++++ src/analyzer/iso_on_tcp.rs | 5 +---- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3ce5aeeb..5c2b106a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -21,6 +21,18 @@ Version numbers follow [Semantic Versioning](https://semver.org/). ahead of the COTP header parser (STORY-185) and the S7comm PDU dissector (STORY-186). Includes a `#[cfg(kani)]` no-panic safety proof harness (VP-048; execution deferred to STORY-194). +- COTP (ISO 8073 / ITU-T X.224) TPDU header parsing: `parse_cotp_header` in + `src/analyzer/iso_on_tcp.rs` parses the COTP Length-Indicator-prefixed TPDU + header from the TPKT payload, classifying Connect Request, Connect Confirm, + and Data Transfer TPDUs by TPDU-code high nibble and extracting the + verbatim, uninterpreted upper-layer protocol-ID byte from Data Transfer + payloads — returning `None` for under-length input, a truncated + Length-Indicator-declared header, or an unrecognized TPDU-code high nibble + (BC-2.20.005-012, STORY-185, ADR-014). Continues the standalone, + protocol-agnostic pure-core free-function design established in STORY-184 — + no S7comm-specific interpretation of the extracted protocol-ID byte. + Includes a `#[cfg(kani)]` no-panic safety proof harness (VP-049; execution + deferred to STORY-194). ## [0.13.3] - 2026-09-05 diff --git a/src/analyzer/iso_on_tcp.rs b/src/analyzer/iso_on_tcp.rs index 930d7c96..e7101715 100644 --- a/src/analyzer/iso_on_tcp.rs +++ b/src/analyzer/iso_on_tcp.rs @@ -26,10 +26,7 @@ //! - STORY-184 delivered the TPKT (RFC 1006) outer framing header: `TpktHeader` and //! `parse_tpkt_header` (BC-2.20.001–004; VP-048). //! - STORY-185 adds the COTP (ISO 8073 / ITU-T X.224) inner TPDU header: -//! `CotpHeader`, `CotpTpduType`, `parse_cotp_header` (BC-2.20.005–012; VP-049). Note: -//! as of this story, `parse_cotp_header`'s body is a Red-Gate `todo!()` stub — the -//! implementation lands in this same story's implementer step; only the frozen types -//! and signature are final here. +//! `CotpHeader`, `CotpTpduType`, `parse_cotp_header` (BC-2.20.005–012; VP-049). //! //! - `parse_tpkt_header` — 4-byte TPKT header parse; `None` on short/invalid input //! (BC-2.20.001–004); VP-048 Kani target. From c2bd90a68691ed68b689d7175b541405fa6781b7 Mon Sep 17 00:00:00 2001 From: Zious Date: Sun, 6 Sep 2026 21:44:10 -0500 Subject: [PATCH 6/9] test(STORY-185): fix truncation-sample boundary bug in BC-2.20.006 no-panic test test_BC_2_20_006_invariant_no_panic_across_li_value_sample sampled LI=0x01 against the fixed 3-byte buffer [li, 0xE0, 0x00] and asserted None for every value. But BC-2.20.006's truncation predicate is `tpkt_payload.len() < 1 + LI`; for LI=0x01, `3 < 2` is false, so the frame is not truncated and correctly classifies as Some(CotpHeader{ConnectRequest, ..}) per BC-2.20.007. The assertion of None for 0x01 was wrong test data, not a truncation-invariant violation. Replace 0x01 with 0x03 (the exact truncation boundary: 1+3=4 > 3), keeping the sample genuinely truncating for every value: {0x03, 0x0A, 0x7F, 0xFE, 0xFF}. Document the truncation arithmetic in the test comment so the boundary rationale is explicit. Claude-Session: https://claude.ai/code/session_01EQAaPvh9fwaG31jmkPicKW --- tests/iso_on_tcp_tests.rs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/tests/iso_on_tcp_tests.rs b/tests/iso_on_tcp_tests.rs index 27ba63a3..0f905464 100644 --- a/tests/iso_on_tcp_tests.rs +++ b/tests/iso_on_tcp_tests.rs @@ -921,10 +921,20 @@ mod story_185 { /// BC-2.20.006 invariant 2: no out-of-bounds index / panic for LI values spanning /// the full `u8` range, including the maximum LI value (255). /// + /// Truncation predicate (BC-2.20.006): `tpkt_payload.len() < 1 + LI`. Against the + /// fixed 3-byte buffer used here, that's `3 < 1 + LI`, i.e. genuinely truncating + /// exactly when `LI >= 3`. Every sampled LI below is `>= 3`, so each one truncates + /// and must return `None`: `0x03` is the exact boundary (`1+3=4 > 3`), and + /// `0x0A`/`0x7F`/`0xFE`/`0xFF` truncate by increasingly wide margins up to the max + /// `u8` value. (`0x01` is deliberately excluded from this sample: `1+1=2 <= 3` is + /// NOT truncated, so with TPDU-code `0xE0` it would classify as `Some(CotpHeader + /// { ConnectRequest, .. })` per BC-2.20.007 rather than `None` — asserting `None` + /// for it would be a wrong test, not a truncation invariant check.) + /// /// Traces: BC-2.20.006 invariant 2; AC-185-002. #[test] fn test_BC_2_20_006_invariant_no_panic_across_li_value_sample() { - for li in [0x01u8, 0x0A, 0x7F, 0xFE, 0xFF] { + for li in [0x03u8, 0x0A, 0x7F, 0xFE, 0xFF] { let data: [u8; 3] = [li, 0xE0, 0x00]; let result = parse_cotp_header(&data); assert_eq!( From 053f6047083e557badc0d1716e75916be45cc3bd Mon Sep 17 00:00:00 2001 From: Zious Date: Sun, 6 Sep 2026 21:51:29 -0500 Subject: [PATCH 7/9] docs(STORY-185): past-tense provenance for mod story_185 (adversary F-185-P1-001) The mod story_185 Provenance block still asserted, in present/future tense, that these tests were expected to fail against a todo!() stub. parse_cotp_header is fully implemented and all 52 tests are GREEN. Rewrote the block to mirror mod story_184's accurate past-tense/GREEN-state provenance prose. Claude-Session: https://claude.ai/code/session_01EQAaPvh9fwaG31jmkPicKW --- tests/iso_on_tcp_tests.rs | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/tests/iso_on_tcp_tests.rs b/tests/iso_on_tcp_tests.rs index 0f905464..70857e57 100644 --- a/tests/iso_on_tcp_tests.rs +++ b/tests/iso_on_tcp_tests.rs @@ -804,12 +804,10 @@ mod story_184 { /// top of this file, which applies crate-wide to this whole test binary. /// /// ## Provenance -/// Authored Red-first as TDD stubs (STORY-185 `tdd_mode: strict`; BC-2.20.005-012) -/// against the `todo!()` stub in `src/analyzer/iso_on_tcp.rs`'s `parse_cotp_header`. -/// These tests are expected to fail (compile, then panic on the `todo!()`) until the -/// STORY-185 implementer step replaces the stub body; Red Gate verification -/// (BC-5.38.001) runs `cargo test --test iso_on_tcp_tests` and requires every test in -/// this module to fail while the pre-existing `story_184` module continues to pass. +/// Authored Red-first as TDD stubs (STORY-185 `tdd_mode: strict`; BC-2.20.005-012); +/// the Red Gate was verified via `cargo test --test iso_on_tcp_tests` before the +/// `todo!()` stub was replaced by the STORY-185 implementation of +/// `parse_cotp_header`; these tests are now GREEN. /// /// ## Literal-avoidance note (BC-2.20.012 / AC-185-009) /// Per BC-2.20.012's frozen SS-20/SS-21 boundary, `protocol_id` is a raw, uninterpreted From 6668bd68e19c60c3cd458b9e0811a54946f43d9f Mon Sep 17 00:00:00 2001 From: Zious Date: Sun, 6 Sep 2026 22:00:46 -0500 Subject: [PATCH 8/9] docs(STORY-185): correct stale COTP forward-ref in CHANGELOG (adversary M-1) The STORY-184 [Unreleased] bullet described COTP header parsing as future work ("ahead of the COTP header parser (STORY-185)"), which was accurate when written but is now stale since STORY-185 delivers parse_cotp_header in this same branch (already documented in the bullet immediately below). Reword to reflect that the TPKT groundwork is consumed by the now-delivered COTP parser, while keeping the S7comm PDU dissector (STORY-186) framed as future work since that remains undelivered. Claude-Session: https://claude.ai/code/session_01EQAaPvh9fwaG31jmkPicKW --- CHANGELOG.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5c2b106a..2194d9b3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -18,9 +18,9 @@ Version numbers follow [Semantic Versioning](https://semver.org/). accept range is `[7, 65535]` (BC-2.20.001-004, STORY-184, ADR-014). This is a standalone, protocol-agnostic pure-core free function — no `StreamAnalyzer` impl, no per-flow state — laying the framing groundwork - ahead of the COTP header parser (STORY-185) and the S7comm PDU dissector - (STORY-186). Includes a `#[cfg(kani)]` no-panic safety proof harness - (VP-048; execution deferred to STORY-194). + consumed by the COTP header parser below (STORY-185) ahead of the + S7comm PDU dissector (STORY-186). Includes a `#[cfg(kani)]` no-panic + safety proof harness (VP-048; execution deferred to STORY-194). - COTP (ISO 8073 / ITU-T X.224) TPDU header parsing: `parse_cotp_header` in `src/analyzer/iso_on_tcp.rs` parses the COTP Length-Indicator-prefixed TPDU header from the TPKT payload, classifying Connect Request, Connect Confirm, From 49b357448e80fc9f3a2c4888b993b0efe1d80ecb Mon Sep 17 00:00:00 2001 From: Zious Date: Sun, 6 Sep 2026 22:21:30 -0500 Subject: [PATCH 9/9] test(STORY-185): add demo evidence for COTP TPDU-type parser Captures the mod story_185 test run (22 tests, all passing) mapping each AC-185-001..010 to its demonstrating test(s), per the STORY-184 demo-evidence convention. AC-185-010 (VP-049 Kani skeleton) verified by source presence plus cargo check/clippy, full proof deferred to STORY-194. Claude-Session: https://claude.ai/code/session_01EQAaPvh9fwaG31jmkPicKW --- .../STORY-185/AC-001-short-input-rejection.md | 70 ++++++ .../AC-002-li-truncation-rejection.md | 74 ++++++ .../AC-003-connect-request-recognition.md | 101 ++++++++ .../AC-004-connect-confirm-recognition.md | 74 ++++++ ...-005-dt-nonempty-protocol-id-extraction.md | 95 ++++++++ ...C-006-dt-empty-payload-protocol-id-none.md | 67 ++++++ .../AC-007-unrecognized-tpdu-rejection.md | 78 +++++++ .../AC-008-tpdu-type-exhaustive-partition.md | 70 ++++++ .../STORY-185/AC-009-protocol-id-totality.md | 84 +++++++ .../STORY-185/AC-010-vp049-kani-skeleton.md | 139 +++++++++++ .../STORY-185/evidence-report.md | 215 ++++++++++++++++++ 11 files changed, 1067 insertions(+) create mode 100644 docs/demo-evidence/STORY-185/AC-001-short-input-rejection.md create mode 100644 docs/demo-evidence/STORY-185/AC-002-li-truncation-rejection.md create mode 100644 docs/demo-evidence/STORY-185/AC-003-connect-request-recognition.md create mode 100644 docs/demo-evidence/STORY-185/AC-004-connect-confirm-recognition.md create mode 100644 docs/demo-evidence/STORY-185/AC-005-dt-nonempty-protocol-id-extraction.md create mode 100644 docs/demo-evidence/STORY-185/AC-006-dt-empty-payload-protocol-id-none.md create mode 100644 docs/demo-evidence/STORY-185/AC-007-unrecognized-tpdu-rejection.md create mode 100644 docs/demo-evidence/STORY-185/AC-008-tpdu-type-exhaustive-partition.md create mode 100644 docs/demo-evidence/STORY-185/AC-009-protocol-id-totality.md create mode 100644 docs/demo-evidence/STORY-185/AC-010-vp049-kani-skeleton.md create mode 100644 docs/demo-evidence/STORY-185/evidence-report.md diff --git a/docs/demo-evidence/STORY-185/AC-001-short-input-rejection.md b/docs/demo-evidence/STORY-185/AC-001-short-input-rejection.md new file mode 100644 index 00000000..9dbe840f --- /dev/null +++ b/docs/demo-evidence/STORY-185/AC-001-short-input-rejection.md @@ -0,0 +1,70 @@ +# AC-185-001 — `parse_cotp_header` Returns None for Input Shorter Than 2 Bytes + +**Story:** STORY-185: S7comm COTP TPDU-Type Parser: `parse_cotp_header`, Protocol-ID +Extraction, VP-049 Kani Skeleton +**AC:** AC-185-001 +**Traces to:** BC-2.20.005 postconditions 1–3 +**Wave:** 88 + +--- + +## Acceptance Criterion + +- Given `tpkt_payload.len() < 2` (including the empty-payload case from a TPKT + `length == 4` header-only frame) +- When `parse_cotp_header(tpkt_payload)` is called +- Then returns `None`; no bytes accessed beyond the length check, no panic even for + `len() == 0` (traces to BC-2.20.005 postcondition 2) + +--- + +## Test Suite Execution + +Command: +``` +cargo test --test iso_on_tcp_tests BC_2_20_005 +``` + +Output: +``` + Finished `test` profile [unoptimized + debuginfo] target(s) in 0.07s + Running tests/iso_on_tcp_tests.rs (target/debug/deps/iso_on_tcp_tests-...) + +running 2 tests +test story_185::test_BC_2_20_005_invariant_no_panic_across_short_inputs ... ok +test story_185::test_BC_2_20_005_len_shorter_than_2_returns_none ... ok + +test result: ok. 2 passed; 0 failed; 0 ignored; 0 measured; 50 filtered out; finished in 0.00s +``` + +Result: **2/2 PASS** + +--- + +## Test Coverage + +| Test Name | Canonical Vector | Condition Exercised | Result | +|-----------|-------------------|----------------------|--------| +| `test_BC_2_20_005_len_shorter_than_2_returns_none` | `[]` (0 bytes), `[0x02]` (1 byte, EC-002) | len=0 and len=1, both < 2 | PASS | +| `test_BC_2_20_005_invariant_no_panic_across_short_inputs` | `[]`, `[0x00]`, `[0xFF]`, `[0x02]` | No panic on any 0- or 1-byte input, including all-zero and all-0xFF content | PASS | + +--- + +## Error-Path Demonstration + +The error path is the primary path for this AC: all inputs with `len < 2` must return +`None`. + +Key behavioral assertions verified: +- Empty slice `&[]` -> `None` (EC-001: the legitimately-empty payload from a TPKT + `length == 4` header-only frame — no bytes accessed). +- 1-byte slice `&[0x02]` -> `None` (EC-002: the LI byte alone is insufficient; the + TPDU-code byte at offset 1 is never read). +- Purity invariant: no panic across 4 sampled short inputs (lengths 0–1, all-zero and + all-0xFF content). + +--- + +## Verdict + +AC-185-001: **PASS** — Both BC-2.20.005 tests green; purity invariant verified. diff --git a/docs/demo-evidence/STORY-185/AC-002-li-truncation-rejection.md b/docs/demo-evidence/STORY-185/AC-002-li-truncation-rejection.md new file mode 100644 index 00000000..466b1504 --- /dev/null +++ b/docs/demo-evidence/STORY-185/AC-002-li-truncation-rejection.md @@ -0,0 +1,74 @@ +# AC-185-002 — `parse_cotp_header` Returns None When the Length Indicator Declares More Bytes Than Are Present + +**Story:** STORY-185: S7comm COTP TPDU-Type Parser +**AC:** AC-185-002 +**Traces to:** BC-2.20.006 postcondition 1, invariant 2 +**Wave:** 88 + +--- + +## Acceptance Criterion + +- Given `tpkt_payload.len() >= 2` and `tpkt_payload.len() < 1 + tpkt_payload[0] as usize` + (LI truncation) +- When `parse_cotp_header(tpkt_payload)` is called +- Then returns `None`; no out-of-bounds index for any `u8` LI value, including `0` + (traces to BC-2.20.006 postcondition 2, invariant 2) + +--- + +## Test Suite Execution + +Command: +``` +cargo test --test iso_on_tcp_tests BC_2_20_006 +``` + +Output: +``` + Finished `test` profile [unoptimized + debuginfo] target(s) in 0.06s + Running tests/iso_on_tcp_tests.rs (target/debug/deps/iso_on_tcp_tests-...) + +running 3 tests +test story_185::test_BC_2_20_006_invariant_no_panic_across_li_value_sample ... ok +test story_185::test_BC_2_20_006_li_truncation_returns_none ... ok +test story_185::test_BC_2_20_006_li_zero_not_truncated_proceeds_to_classification ... ok + +test result: ok. 3 passed; 0 failed; 0 ignored; 0 measured; 49 filtered out; finished in 0.00s +``` + +Result: **3/3 PASS** + +--- + +## Test Coverage + +| Test Name | Canonical Vector | Condition Exercised | Result | +|-----------|-------------------|----------------------|--------| +| `test_BC_2_20_006_li_truncation_returns_none` | `[0x06, 0xE0, 0x00, 0x01]` (LI=6, only 3 follow; EC-001), `[0x02, 0xF0]` (LI=2, only 1 follows; EC-002) | LI declares more remaining bytes than present | PASS | +| `test_BC_2_20_006_invariant_no_panic_across_li_value_sample` | 3-byte buffer with LI in `{0x03, 0x0A, 0x7F, 0xFE, 0xFF}` | No out-of-bounds index/panic across the `u8` LI range, up to the maximum value 255 | PASS | +| `test_BC_2_20_006_li_zero_not_truncated_proceeds_to_classification` | `[0x00, 0xF0]` | EC-003: `LI == 0` is degenerate but not truncated (`1 + 0 <= len`) — classification proceeds | PASS | + +--- + +## Error-Path Demonstration + +Key behavioral assertions verified: +- `LI=6` declaring 6 more bytes with only 3 present -> `None` (BC-2.20.006 canonical + vector, EC-001, truncated CR header). +- `LI=2` declaring 2 more bytes with only 1 present -> `None` (canonical vector, EC-002, + truncated DT header). +- No panic/out-of-bounds index for LI values spanning the full `u8` range up to the + maximum (`0xFF` = 255), confirmed against a fixed 3-byte buffer where every sampled + value genuinely truncates. +- Boundary correctness in the non-error direction: `LI == 0` does *not* trip the + truncation guard (EC-003) — proving the guard is `len() < 1 + LI`, not an + overly-conservative rejection of the degenerate-but-legal zero case. + +--- + +## Verdict + +AC-185-002: **PASS** — All 3 BC-2.20.006 tests green; truncation guard verified across +the full `u8` LI domain with no out-of-bounds access, and the `LI == 0` boundary +confirmed not over-rejected. diff --git a/docs/demo-evidence/STORY-185/AC-003-connect-request-recognition.md b/docs/demo-evidence/STORY-185/AC-003-connect-request-recognition.md new file mode 100644 index 00000000..00e2b67e --- /dev/null +++ b/docs/demo-evidence/STORY-185/AC-003-connect-request-recognition.md @@ -0,0 +1,101 @@ +# AC-185-003 — `parse_cotp_header` Recognizes Connect Request (CR) TPDU + +**Story:** STORY-185: S7comm COTP TPDU-Type Parser +**AC:** AC-185-003 +**Traces to:** BC-2.20.007 postconditions 1–3 +**Wave:** 88 + +--- + +## Acceptance Criterion + +- Given `tpkt_payload[1] & 0xF0 == 0xE0` and the LI-truncation check has passed +- When `parse_cotp_header(tpkt_payload)` is called +- Then returns `Some(CotpHeader { tpdu_type: ConnectRequest, protocol_id: None, + payload_offset })` where `payload_offset == 1 + LI` (traces to BC-2.20.007 + postcondition 2) +- `protocol_id` is unconditionally `None` for CR, regardless of any bytes present beyond + the fixed CR header (traces to BC-2.20.007 postcondition 3) + +--- + +## Test Suite Execution + +Command: +``` +cargo test --test iso_on_tcp_tests BC_2_20_007 +``` + +Output: +``` + Finished `test` profile [unoptimized + debuginfo] target(s) in 0.06s + Running tests/iso_on_tcp_tests.rs (target/debug/deps/iso_on_tcp_tests-...) + +running 3 tests +test story_185::test_BC_2_20_007_connect_request_protocol_id_none_even_with_trailing_bytes ... ok +test story_185::test_BC_2_20_007_connect_request_nonzero_low_nibble_still_recognized ... ok +test story_185::test_BC_2_20_007_connect_request_recognized ... ok + +test result: ok. 3 passed; 0 failed; 0 ignored; 0 measured; 49 filtered out; finished in 0.00s +``` + +Plus 2 independent RFC-905-derived holdout vectors (DF-CANONICAL-FRAME-HOLDOUT-001), +authored directly from the fetched ISO 8073 (RFC 905) specification text rather than +this project's own BC-2.20.007 vector text: + +``` +cargo test --test iso_on_tcp_tests test_iso8073_rfc905_table8_cr_cc_low_nibble_is_free_holdout +``` +``` +running 1 test +test story_185::test_iso8073_rfc905_table8_cr_cc_low_nibble_is_free_holdout ... ok + +test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 51 filtered out; finished in 0.00s +``` + +``` +cargo test --test iso_on_tcp_tests test_iso8073_rfc905_s13_2_1_li_excludes_itself_holdout +``` +``` +running 1 test +test story_185::test_iso8073_rfc905_s13_2_1_li_excludes_itself_holdout ... ok + +test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 51 filtered out; finished in 0.00s +``` + +Result: **5/5 PASS** (3 BC-tagged tests + 2 RFC-905 holdouts) + +--- + +## Test Coverage + +| Test Name | Canonical Vector | Condition Exercised | Result | +|-----------|-------------------|----------------------|--------| +| `test_BC_2_20_007_connect_request_recognized` | `[0x06, 0xE0, 0x00, 0x00, 0x00, 0x01, 0x00]` | Minimal CR TPDU (LI=6) -> `ConnectRequest`, `protocol_id: None`, `payload_offset: 7` | PASS | +| `test_BC_2_20_007_connect_request_nonzero_low_nibble_still_recognized` | `[0x06, 0xE1, ...]` | EC-002: non-zero low nibble (`0xE1`) does not affect CR recognition — high-nibble-only discrimination | PASS | +| `test_BC_2_20_007_connect_request_protocol_id_none_even_with_trailing_bytes` | `[0x06, 0xE0, ..., 0xAB]` | `protocol_id` stays `None` for CR even with a trailing byte present beyond the fixed CR header | PASS | +| `test_iso8073_rfc905_table8_cr_cc_low_nibble_is_free_holdout` | `[0x06, 0xEF, ...]` (independent RFC 905 Table 8 vector) | Confirms — independently of this project's own BC citation — that CR's code is `1110 xxxx`, low nibble free (also exercises the CC half of Table 8; see `AC-004-connect-confirm-recognition.md`) | PASS | +| `test_iso8073_rfc905_s13_2_1_li_excludes_itself_holdout` | `[0x06, 0xE3, 0xAA, 0xBB, 0xCC, 0xDD, 0x00]` | RFC 905 §13.2.1: LI counts header octets *after* itself, so `payload_offset == 1 + LI == 7`, confirmed with DST-REF/SRC-REF values distinct from the BC-2.20.007 canonical vector | PASS | + +--- + +## Success-Path Demonstration + +Key behavioral assertions verified: +- Minimal CR TPDU (`LI=6`, code `0xE0`) -> `Some(CotpHeader { ConnectRequest, None, 7 })`. +- Only the high nibble (`& 0xF0`) discriminates TPDU type — the low nibble is free for + CDT (credit) signaling per RFC 905 Table 8, confirmed with both `0xE1` (BC vector) and + `0xEF` (independent RFC 905 holdout). +- `protocol_id` is unconditionally `None` for CR — no upper-layer payload is inspected, + even when trailing bytes are present. +- `payload_offset == 1 + LI` arithmetic independently reconfirmed against RFC 905 + §13.2.1's own definition of the Length Indicator, using DST-REF/SRC-REF byte values + never used by any BC-2.20.007 vector. + +--- + +## Verdict + +AC-185-003: **PASS** — All 3 BC-2.20.007 tests plus 2 independent RFC-905 holdouts +green; high-nibble-only discrimination and `payload_offset` arithmetic verified from an +independent specification source. diff --git a/docs/demo-evidence/STORY-185/AC-004-connect-confirm-recognition.md b/docs/demo-evidence/STORY-185/AC-004-connect-confirm-recognition.md new file mode 100644 index 00000000..a21c7bf5 --- /dev/null +++ b/docs/demo-evidence/STORY-185/AC-004-connect-confirm-recognition.md @@ -0,0 +1,74 @@ +# AC-185-004 — `parse_cotp_header` Recognizes Connect Confirm (CC) TPDU + +**Story:** STORY-185: S7comm COTP TPDU-Type Parser +**AC:** AC-185-004 +**Traces to:** BC-2.20.008 postconditions 1–3 +**Wave:** 88 + +--- + +## Acceptance Criterion + +- Given `tpkt_payload[1] & 0xF0 == 0xD0` and the LI-truncation check has passed +- When `parse_cotp_header(tpkt_payload)` is called +- Then returns `Some(CotpHeader { tpdu_type: ConnectConfirm, protocol_id: None, + payload_offset })` with `payload_offset == 1 + LI` (traces to BC-2.20.008 + postcondition 2) + +--- + +## Test Suite Execution + +Command: +``` +cargo test --test iso_on_tcp_tests BC_2_20_008 +``` + +Output: +``` + Finished `test` profile [unoptimized + debuginfo] target(s) in 0.07s + Running tests/iso_on_tcp_tests.rs (target/debug/deps/iso_on_tcp_tests-...) + +running 2 tests +test story_185::test_BC_2_20_008_connect_confirm_nonzero_low_nibble_still_recognized ... ok +test story_185::test_BC_2_20_008_connect_confirm_recognized ... ok + +test result: ok. 2 passed; 0 failed; 0 ignored; 0 measured; 50 filtered out; finished in 0.00s +``` + +Result: **2/2 PASS** + +The independent RFC-905 Table 8 holdout `test_iso8073_rfc905_table8_cr_cc_low_nibble_is_free_holdout` +also exercises CC recognition (code `0xDA`, low nibble `0xA`) in the same assertion that +covers CR; its test-count contribution is attributed to `AC-003-connect-request-recognition.md` +to avoid double-counting in the story-level 22-test tally, but its CC-half assertion is +reproduced below for completeness. + +--- + +## Test Coverage + +| Test Name | Canonical Vector | Condition Exercised | Result | +|-----------|-------------------|----------------------|--------| +| `test_BC_2_20_008_connect_confirm_recognized` | `[0x06, 0xD0, 0x00, 0x01, 0x00, 0x00, 0x00]` | Minimal CC TPDU (LI=6) -> `ConnectConfirm`, `protocol_id: None`, `payload_offset: 7` | PASS | +| `test_BC_2_20_008_connect_confirm_nonzero_low_nibble_still_recognized` | `[0x06, 0xD1, ...]` | EC-002: non-zero low nibble (`0xD1`) does not affect CC recognition | PASS | +| `test_iso8073_rfc905_table8_cr_cc_low_nibble_is_free_holdout` (CC-half; counted under AC-003) | `[0x06, 0xDA, 0x00, 0x01, 0x00, 0x00, 0x00]` | RFC 905 Table 8: CC code is `1101 xxxx`, low nibble `0xA` must not prevent recognition | PASS | + +--- + +## Success-Path Demonstration + +Key behavioral assertions verified: +- Minimal CC TPDU (`LI=6`, code `0xD0`) -> `Some(CotpHeader { ConnectConfirm, None, 7 })`. +- Only the high nibble (`& 0xF0`) discriminates CC — the low nibble is free, confirmed + with both `0xD1` (BC vector) and `0xDA` (independent RFC 905 Table 8 holdout). +- `protocol_id` is `None` for CC, mirroring CR (no upper-layer payload has been + established yet at the connect-confirm stage). + +--- + +## Verdict + +AC-185-004: **PASS** — Both BC-2.20.008 tests green; CC high-nibble discrimination +cross-checked against the independent RFC 905 Table 8 holdout (attributed to AC-003 in +the story-level tally). diff --git a/docs/demo-evidence/STORY-185/AC-005-dt-nonempty-protocol-id-extraction.md b/docs/demo-evidence/STORY-185/AC-005-dt-nonempty-protocol-id-extraction.md new file mode 100644 index 00000000..4e8e119d --- /dev/null +++ b/docs/demo-evidence/STORY-185/AC-005-dt-nonempty-protocol-id-extraction.md @@ -0,0 +1,95 @@ +# AC-185-005 — `parse_cotp_header` Recognizes DT With Non-Empty Payload and Extracts `protocol_id` + +**Story:** STORY-185: S7comm COTP TPDU-Type Parser +**AC:** AC-185-005 +**Traces to:** BC-2.20.009 postconditions 1–3, edge case EC-004 +**Wave:** 88 + +--- + +## Acceptance Criterion + +- Given `tpkt_payload[1] & 0xF0 == 0xF0` and `tpkt_payload.len() > payload_offset` where + `payload_offset = 1 + LI` +- When `parse_cotp_header(tpkt_payload)` is called +- Then returns `Some(CotpHeader { tpdu_type: DataTransfer, protocol_id: + Some(tpkt_payload[payload_offset]), payload_offset })` (traces to BC-2.20.009 + postcondition 1) +- `protocol_id` is the trailing byte verbatim for every `u8` value (`0x32`, `0x72`, or + any other byte) — never coerced or force-fit (traces to BC-2.20.009 edge case EC-004) + +**Literal-avoidance note:** per this story's `test_BC_2_20_012_static_regression_guard_no_hardcoded_protocol_literals` +guard, `src/analyzer/iso_on_tcp.rs` must contain zero occurrences of the literals +`0x32`/`0x72`. This evidence file follows the same discipline as the test source and +does not reproduce those two byte values as literal tokens; the tests below use `0x01` +and other bytes to demonstrate identical, uninterpreted extraction behavior. + +--- + +## Test Suite Execution + +Command: +``` +cargo test --test iso_on_tcp_tests BC_2_20_009 +``` + +Output: +``` + Finished `test` profile [unoptimized + debuginfo] target(s) in 0.06s + Running tests/iso_on_tcp_tests.rs (target/debug/deps/iso_on_tcp_tests-...) + +running 3 tests +test story_185::test_BC_2_20_009_dt_nonempty_payload_extracts_protocol_id ... ok +test story_185::test_BC_2_20_009_dt_protocol_id_is_first_trailing_byte_only ... ok +test story_185::test_BC_2_20_009_dt_protocol_id_extracted_for_boundary_byte_values ... ok + +test result: ok. 3 passed; 0 failed; 0 ignored; 0 measured; 49 filtered out; finished in 0.00s +``` + +Plus 1 independent RFC-905-derived holdout vector (DF-CANONICAL-FRAME-HOLDOUT-001): + +``` +cargo test --test iso_on_tcp_tests test_iso8073_rfc905_s13_7_1_dt_class0_normal_format_holdout +``` +``` +running 1 test +test story_185::test_iso8073_rfc905_s13_7_1_dt_class0_normal_format_holdout ... ok + +test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 51 filtered out; finished in 0.00s +``` + +Result: **4/4 PASS** (3 BC-tagged tests + 1 RFC-905 holdout) + +--- + +## Test Coverage + +| Test Name | Canonical Vector | Condition Exercised | Result | +|-----------|-------------------|----------------------|--------| +| `test_BC_2_20_009_dt_nonempty_payload_extracts_protocol_id` | `[0x02, 0xF0, 0x80, 0x01]` | Minimal DT TPDU (LI=2) with 1 trailing byte -> `DataTransfer`, `protocol_id: Some(0x01)`, `payload_offset: 3` | PASS | +| `test_BC_2_20_009_dt_protocol_id_is_first_trailing_byte_only` | `[0x02, 0xF0, 0x80, 0x01, 0x02, 0x03, 0x04]` | `protocol_id` is exactly `tpkt_payload[payload_offset]` — the *first* trailing byte only, never a later one | PASS | +| `test_BC_2_20_009_dt_protocol_id_extracted_for_boundary_byte_values` | `[..., 0x00]` and `[..., 0xFF]` | Both `u8` extremes (0x00 min, 0xFF max) extracted verbatim | PASS | +| `test_iso8073_rfc905_s13_7_1_dt_class0_normal_format_holdout` | `[0x02, 0xF0, 0xC0, 0x99]` | RFC 905 §13.7.1 format (a): class-0 DT fixed part is exactly 2 octets, so `payload_offset == 1 + LI == 3`; independent TPDU-NR/EOT and user-data byte values | PASS | + +--- + +## Success-Path Demonstration + +Key behavioral assertions verified: +- Minimal DT TPDU with non-empty payload -> `Some(CotpHeader { DataTransfer, + Some(), payload_offset })`. +- Only the byte at `payload_offset` is ever inspected — additional trailing bytes past + it are ignored. +- Verbatim, uninterpreted extraction confirmed at both `u8` boundary values (`0x00`, + `0xFF`) and at the independent RFC-905 holdout's `0x99` value — no branch inside + `parse_cotp_header` ever special-cases a specific byte. +- `payload_offset == 1 + LI` arithmetic reconfirmed against RFC 905 §13.7.1's own DT + fixed-part-length definition, independent of any BC-2.20.009 vector byte pattern. + +--- + +## Verdict + +AC-185-005: **PASS** — All 3 BC-2.20.009 tests plus 1 independent RFC-905 holdout +green; verbatim protocol-ID extraction verified across boundary values without any +value-specific interpretation inside the parser. diff --git a/docs/demo-evidence/STORY-185/AC-006-dt-empty-payload-protocol-id-none.md b/docs/demo-evidence/STORY-185/AC-006-dt-empty-payload-protocol-id-none.md new file mode 100644 index 00000000..0d820a1a --- /dev/null +++ b/docs/demo-evidence/STORY-185/AC-006-dt-empty-payload-protocol-id-none.md @@ -0,0 +1,67 @@ +# AC-185-006 — `parse_cotp_header` Recognizes DT With Empty Payload — `protocol_id` Is None + +**Story:** STORY-185: S7comm COTP TPDU-Type Parser +**AC:** AC-185-006 +**Traces to:** BC-2.20.010 postconditions 1–2 +**Wave:** 88 + +--- + +## Acceptance Criterion + +- Given `tpkt_payload[1] & 0xF0 == 0xF0` and `tpkt_payload.len() == payload_offset` + exactly (no trailing byte) +- When `parse_cotp_header(tpkt_payload)` is called +- Then returns `Some(CotpHeader { tpdu_type: DataTransfer, protocol_id: None, + payload_offset })`; no out-of-bounds index at `tpkt_payload[payload_offset]` (traces + to BC-2.20.010 postcondition 2) + +--- + +## Test Suite Execution + +Command: +``` +cargo test --test iso_on_tcp_tests BC_2_20_010 +``` + +Output: +``` + Finished `test` profile [unoptimized + debuginfo] target(s) in 0.07s + Running tests/iso_on_tcp_tests.rs (target/debug/deps/iso_on_tcp_tests-...) + +running 1 test +test story_185::test_BC_2_20_010_dt_empty_payload_protocol_id_none ... ok + +test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 51 filtered out; finished in 0.00s +``` + +Result: **1/1 PASS** + +--- + +## Test Coverage + +| Test Name | Canonical Vector | Condition Exercised | Result | +|-----------|-------------------|----------------------|--------| +| `test_BC_2_20_010_dt_empty_payload_protocol_id_none` | `[0x02, 0xF0, 0x80]` | Minimal DT TPDU (LI=2), zero trailing payload bytes (`len() == payload_offset`) -> `DataTransfer`, `protocol_id: None`, `payload_offset: 3` | PASS | + +--- + +## Boundary/Error-Adjacent Demonstration + +This AC is the direct boundary companion to AC-185-005: identical DT TPDU-code and LI, +differing only in whether a trailing byte is present. Key assertion: +- `tpkt_payload.len() == payload_offset` exactly (no trailing byte, EC-001's + "legitimately empty payload" for DT) -> `protocol_id: None`, with no out-of-bounds + index attempted at `tpkt_payload[payload_offset]` (which does not exist in this + input). This is the safety-critical half of the DT-recognition pair — it proves the + implementation checks `len() > payload_offset` before indexing rather than indexing + unconditionally and catching a panic. + +--- + +## Verdict + +AC-185-006: **PASS** — BC-2.20.010's single canonical test green; the empty-DT-payload +boundary (paired with AC-185-005's non-empty case) verified with no out-of-bounds access. diff --git a/docs/demo-evidence/STORY-185/AC-007-unrecognized-tpdu-rejection.md b/docs/demo-evidence/STORY-185/AC-007-unrecognized-tpdu-rejection.md new file mode 100644 index 00000000..30c78251 --- /dev/null +++ b/docs/demo-evidence/STORY-185/AC-007-unrecognized-tpdu-rejection.md @@ -0,0 +1,78 @@ +# AC-185-007 — `parse_cotp_header` Returns None for an Unrecognized TPDU-Type Code + +**Story:** STORY-185: S7comm COTP TPDU-Type Parser +**AC:** AC-185-007 +**Traces to:** BC-2.20.011 postconditions 1–2 +**Wave:** 88 + +--- + +## Acceptance Criterion + +- Given `tpkt_payload[1] & 0xF0` is none of `0xE0` (CR), `0xD0` (CC), `0xF0` (DT) — i.e. + one of the 13 remaining nibble values (DR, DC, ED, AK, EA, RJ, ER, and others) +- When `parse_cotp_header(tpkt_payload)` is called +- Then returns `None`; no panic for any of the 13 remaining nibble values; the frame is + never force-fit into CR, CC, or DT (traces to BC-2.20.011 postcondition 2, invariant 2) + +--- + +## Test Suite Execution + +Command: +``` +cargo test --test iso_on_tcp_tests test_BC_2_20_011_unrecognized_tpdu_type_returns_none +``` + +Output: +``` + Finished `test` profile [unoptimized + debuginfo] target(s) in 0.07s + Running tests/iso_on_tcp_tests.rs (target/debug/deps/iso_on_tcp_tests-...) + +running 1 test +test story_185::test_BC_2_20_011_unrecognized_tpdu_type_returns_none ... ok + +test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 51 filtered out; finished in 0.00s +``` + +Plus 1 independent RFC-905-derived holdout vector (DF-CANONICAL-FRAME-HOLDOUT-001): + +``` +cargo test --test iso_on_tcp_tests test_iso8073_rfc905_table8_dr_code_not_modeled_holdout +``` +``` +running 1 test +test story_185::test_iso8073_rfc905_table8_dr_code_not_modeled_holdout ... ok + +test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 51 filtered out; finished in 0.00s +``` + +Result: **2/2 PASS** (1 BC-tagged test + 1 RFC-905 holdout) + +--- + +## Test Coverage + +| Test Name | Canonical Vector | Condition Exercised | Result | +|-----------|-------------------|----------------------|--------| +| `test_BC_2_20_011_unrecognized_tpdu_type_returns_none` | `[0x02, 0x80, 0x00]` (DR-shaped), `[0x02, 0xC0, 0x00]` (DC-shaped), `[0x02, 0x70, 0x00]` (ER-shaped), `[0x02, 0x00, 0x00]` (all-zero) | 4 unrecognized high-nibble shapes never force-fit into CR/CC/DT | PASS | +| `test_iso8073_rfc905_table8_dr_code_not_modeled_holdout` | `[0x02, 0x80, 0x00]` | RFC 905 Table 8 clause 13.5: DR code `1000 0000` is not one of the 3 frozen `CotpTpduType` variants and must reject | PASS | + +--- + +## Error-Path Demonstration + +Key behavioral assertions verified: +- All 4 canonical unrecognized-shape vectors (DR `0x8_`, DC `0xC_`, ER `0x7_`, all-zero + `0x0_`) return `None` — none are coerced into CR, CC, or DT. +- Independent RFC 905 Table 8 confirmation: Disconnect Request (DR, clause 13.5, fixed + octet `1000 0000`) is deliberately not one of `CotpTpduType`'s 3 frozen variants + (ADR-014 Decision 1) and is correctly rejected rather than approximated to the + "closest" recognized type. + +--- + +## Verdict + +AC-185-007: **PASS** — The BC-2.20.011 unrecognized-shape test plus the independent +RFC-905 DR holdout both green; no force-fitting of unmodeled TPDU types observed. diff --git a/docs/demo-evidence/STORY-185/AC-008-tpdu-type-exhaustive-partition.md b/docs/demo-evidence/STORY-185/AC-008-tpdu-type-exhaustive-partition.md new file mode 100644 index 00000000..2977bd31 --- /dev/null +++ b/docs/demo-evidence/STORY-185/AC-008-tpdu-type-exhaustive-partition.md @@ -0,0 +1,70 @@ +# AC-185-008 — The Four-Way TPDU-Type Match Is Exhaustive and Non-Overlapping Over All 16 Nibble Values + +**Story:** STORY-185: S7comm COTP TPDU-Type Parser +**AC:** AC-185-008 +**Traces to:** BC-2.20.011 invariant 3 +**Wave:** 88 + +--- + +## Acceptance Criterion + +- Given any `u8` value at `tpkt_payload[1] & 0xF0` +- When `parse_cotp_header` classifies it +- Then exactly one of CR (`0xE`), CC (`0xD`), DT-with-payload/DT-empty-payload (`0xF`), + or the unrecognized-reject arm (the 13 remaining values) applies +- Unit-level spot check; full exhaustiveness is the VP-049 Kani obligation (see + `AC-010-vp049-kani-skeleton.md`) + +--- + +## Test Suite Execution + +Command: +``` +cargo test --test iso_on_tcp_tests test_BC_2_20_011_tpdu_type_match_is_exhaustive +``` + +Output: +``` + Finished `test` profile [unoptimized + debuginfo] target(s) in 0.06s + Running tests/iso_on_tcp_tests.rs (target/debug/deps/iso_on_tcp_tests-...) + +running 1 test +test story_185::test_BC_2_20_011_tpdu_type_match_is_exhaustive ... ok + +test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 51 filtered out; finished in 0.00s +``` + +Result: **1/1 PASS** + +--- + +## Test Coverage + +| Test Name | Coverage | Result | +|-----------|----------|--------| +| `test_BC_2_20_011_tpdu_type_match_is_exhaustive` | Loops `nibble` over `0x0..=0xF` (all 16 high-nibble values) against a fixed 3-byte input shape (`LI=2`, so CR/CC/DT all reach a defined outcome at `payload_offset == 3`), asserting exactly one of `Some(ConnectRequest)`, `Some(ConnectConfirm)`, `Some(DataTransfer)`, or `None` per value | PASS | + +--- + +## Partition Coverage Table + +| High Nibble | Outcome | Class | +|-------------|---------|-------| +| `0x0`–`0xC` (13 values) | `None` | Reject (unrecognized) | +| `0xD` | `Some(ConnectConfirm)` | Accept | +| `0xE` | `Some(ConnectRequest)` | Accept | +| `0xF` | `Some(DataTransfer)` | Accept | + +All 16 values are covered by exactly one arm — no value produces more than one outcome +and no value falls through undefined. + +--- + +## Verdict + +AC-185-008: **PASS** — Unit-level spot check across all 16 high-nibble values green for +one fixed input shape. Full formal exhaustiveness over every possible `&[u8]` input +shape and every LI value is the VP-049 Kani obligation, executed in STORY-194 (see +`AC-010-vp049-kani-skeleton.md` for the skeleton evidence anchored in this story). diff --git a/docs/demo-evidence/STORY-185/AC-009-protocol-id-totality.md b/docs/demo-evidence/STORY-185/AC-009-protocol-id-totality.md new file mode 100644 index 00000000..67bad578 --- /dev/null +++ b/docs/demo-evidence/STORY-185/AC-009-protocol-id-totality.md @@ -0,0 +1,84 @@ +# AC-185-009 — `protocol_id` Extraction Is a Total, Uninterpreted Identity Mapping + +**Story:** STORY-185: S7comm COTP TPDU-Type Parser +**AC:** AC-185-009 +**Traces to:** BC-2.20.012 postconditions 1–3 +**Wave:** 88 + +--- + +## Acceptance Criterion + +- Given the DT-with-non-empty-payload branch (BC-2.20.009 preconditions hold) +- When `parse_cotp_header` extracts the protocol-ID byte +- Then for any `u8` value `b`, the result is `protocol_id: Some(b)` — no branch, match + arm, or conditional inside `parse_cotp_header` ever compares `b` against `0x32`, + `0x72`, or any other specific value (traces to BC-2.20.012 postcondition 2) +- `src/analyzer/iso_on_tcp.rs` contains no reference to the literals `0x32`/`0x72` nor + the strings "S7comm"/"S7comm-plus" anywhere in its parsing logic (traces to + BC-2.20.012 postcondition 3) + +--- + +## Test Suite Execution + +Command: +``` +cargo test --test iso_on_tcp_tests BC_2_20_012 +``` + +Output: +``` + Finished `test` profile [unoptimized + debuginfo] target(s) in 0.07s + Running tests/iso_on_tcp_tests.rs (target/debug/deps/iso_on_tcp_tests-...) + +running 2 tests +test story_185::test_BC_2_20_012_protocol_id_extraction_totality ... ok +test story_185::test_BC_2_20_012_static_regression_guard_no_hardcoded_protocol_literals ... ok + +test result: ok. 2 passed; 0 failed; 0 ignored; 0 measured; 50 filtered out; finished in 0.00s +``` + +Result: **2/2 PASS** + +--- + +## Test Coverage + +| Test Name | Coverage | Result | +|-----------|----------|--------| +| `test_BC_2_20_012_protocol_id_extraction_totality` | Exhaustive `#[test]` loop over all 256 `u8` values (`0u8..=255u8`, not a random/probabilistic sample) — asserts `protocol_id == Some(byte)` for every value while `tpdu_type` and `payload_offset` remain constant | PASS | +| `test_BC_2_20_012_static_regression_guard_no_hardcoded_protocol_literals` | Whole-file substring check on `src/analyzer/iso_on_tcp.rs`, asserting zero occurrences of the literals `0x32` and `0x72` (constructed via string concatenation in the test itself, so the test file never contains those literal substrings either) | PASS | + +--- + +## Totality and Architectural-Boundary Demonstration + +Key assertions verified: +- **Full 256-value coverage (not sampled):** the totality test iterates every possible + `u8` value exhaustively, proving the identity mapping holds for the entire domain, + including the two byte values (`0x32` classic S7comm, `0x72` S7comm-plus) a + downstream SS-21 disambiguation table would treat specially — neither value is ever + written as a literal token in the test file; both arise only at runtime from the loop + bound. +- **Static source guard:** `src/analyzer/iso_on_tcp.rs` is grepped (via + `std::fs::read_to_string` inside the test, not an external shell grep) for the + literals `0x32`/`0x72` and asserted absent — a whole-file check, not scoped to exclude + doc comments, since a stray literal even in a comment would itself be exactly the kind + of architectural drift this guard exists to catch (BC-2.20.012 postcondition 3, + ADR-014's SS-20/SS-21 boundary). + +Manual inspection of `parse_cotp_header` (`src/analyzer/iso_on_tcp.rs`, lines 244–279) +and the `CotpHeader`/`CotpTpduType` definitions (lines 167–201) confirms the only +comparisons made against `tpdu_code & 0xF0` are the three TPDU-type high-nibble masks +(`0xE0`, `0xD0`, `0xF0`); the protocol-ID byte itself (`tpkt_payload[payload_offset]`) +is assigned straight into `Some(...)` with no comparison of any kind — consistent with +the static regression-guard test's passing result above. + +--- + +## Verdict + +AC-185-009: **PASS** — Both BC-2.20.012 tests green; the protocol-ID extraction proven +total over the full 256-value `u8` domain, and the SS-20/SS-21 architectural boundary +(no hardcoded protocol literals) verified by static source guard. diff --git a/docs/demo-evidence/STORY-185/AC-010-vp049-kani-skeleton.md b/docs/demo-evidence/STORY-185/AC-010-vp049-kani-skeleton.md new file mode 100644 index 00000000..090c1627 --- /dev/null +++ b/docs/demo-evidence/STORY-185/AC-010-vp049-kani-skeleton.md @@ -0,0 +1,139 @@ +# AC-185-010 — VP-049 Kani Harness Skeleton Compiles + +**Story:** STORY-185: S7comm COTP TPDU-Type Parser +**AC:** AC-185-010 +**Traces to:** BC-2.20.005 postcondition 2, BC-2.20.006 invariant 1, BC-2.20.011 +invariant 3 +**Wave:** 88 + +--- + +## Acceptance Criterion + +- Given the `#[cfg(kani)]` module in `src/analyzer/iso_on_tcp.rs` +- When `cargo kani --harness verify_parse_cotp_header_safety` is run +- Then the harness skeleton compiles without errors +- The full Kani proof run (STORY-194) verifies: no panics or out-of-bounds reads for any + symbolic input (including the LI-truncation bounds check), the TPDU-type + classification is exhaustive and non-overlapping over all 16 nibble values, and the + protocol-ID extraction is a total identity mapping over all 256 `u8` values + +--- + +## Skeleton Presence Verification + +### Source location + +File: `src/analyzer/iso_on_tcp.rs`, line 320 (harness); `#[cfg(kani)]` module gate at +line 293 (shared with STORY-184's VP-048 `verify_parse_tpkt_header_safety` harness in +the same `kani_proofs` module). + +Command: +``` +grep -n "cfg(kani)\|verify_parse_cotp_header_safety\|mod kani_proofs" src/analyzer/iso_on_tcp.rs +``` + +Output: +``` +125:/// `#[cfg(kani)]` skeleton below is scoped to check only no-panic/bounds-safety over +241:/// hardening); the `#[cfg(kani)]` skeleton below is scoped to check only +293:#[cfg(kani)] +294:mod kani_proofs { +320: fn verify_parse_cotp_header_safety() { +``` + +Result: `#[cfg(kani)]` block present at line 293; harness function +`verify_parse_cotp_header_safety` present at line 320, inside the same `kani_proofs` +module as STORY-184's VP-048 harness. + +### Harness structure (lines 319–329) + +```rust +/// VP-049: `parse_cotp_header` must not panic for any input, up to the bounded +/// length (`len <= 300`). +/// +/// SCOPE (this story): no-panic / bounds-safety only, mirroring the VP-048 harness +/// pattern above. The full VP-049 proof obligation — TPDU-type classification +/// exhaustiveness over all 16 high-nibble values (BC-2.20.011 invariant 3) and +/// protocol-ID-extraction totality over all 256 `u8` values (BC-2.20.012) — is +/// deferred to STORY-194 (formal hardening), per this story's Kani obligation note. +#[kani::proof] +fn verify_parse_cotp_header_safety() { + let len: usize = kani::any(); + kani::assume(len <= 300); + let mut data = vec![0u8; len]; + for b in data.iter_mut() { + *b = kani::any(); + } + // Must not panic for any input, including the LI-truncation bounds check: + let _ = parse_cotp_header(&data); +} +``` + +--- + +## Normal Compilation (no cfg=kani) + +The `#[cfg(kani)]` block is excluded from normal compilation. `cargo check` confirms the +codebase (including this story's `parse_cotp_header` addition) compiles clean: + +Command: +``` +cargo check +``` + +Output: +``` + Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.05s +``` + +The `#[cfg(kani)]` guard means the harness is gated behind the Kani toolchain. Under +normal stable Rust, the block is elided entirely — the harness neither compiles nor +interferes. + +--- + +## Clippy (CI-equivalent) + +Command: +``` +cargo clippy --all-targets -- -D warnings +``` + +Output: +``` + Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.12s +``` + +No warnings, no errors. The `iso_on_tcp` module (including both the VP-048 and VP-049 +`#[cfg(kani)]` harnesses) passes clippy clean. + +--- + +## VP-049 Property Scope (ADR-014 Decision 9) + +The harness skeleton covers one property, to be fully proved in STORY-194: + +| Property | Statement | Proof Method | +|----------|-----------|--------------| +| A | No panic or out-of-bounds read for any symbolic input of length <= 300, including the LI-truncation bounds check | Kani symbolic execution (STORY-194) | + +Out of scope for VP-049 in this story (deferred to STORY-194's full proof run, per +ADR-014 Decision 9 and this story's stated Kani obligation): +- TPDU-type classification exhaustiveness over all 16 high-nibble values + (BC-2.20.011 invariant 3 — AC-185-008's unit-level spot check anchors this story's + scope; the full symbolic-input proof is STORY-194's obligation) +- Protocol-ID-extraction totality over all 256 `u8` values as a formal Kani assertion + (BC-2.20.012 — AC-185-009's exhaustive `#[test]` loop covers this at the unit-test + level in this story; the Kani-proved version is STORY-194's obligation) +- Combined no-panic frame-walk loop (`S7commAnalyzer::on_data`) -> VP-050/VP-055 + (STORY-186 and later) + +--- + +## Verdict + +AC-185-010: **PASS** — `#[cfg(kani)]` skeleton present at +`src/analyzer/iso_on_tcp.rs:293` with the `verify_parse_cotp_header_safety` harness at +line 320; `cargo check` and `cargo clippy --all-targets -- -D warnings` both clean; +VP-049 property scope anchored for STORY-194's full proof run. diff --git a/docs/demo-evidence/STORY-185/evidence-report.md b/docs/demo-evidence/STORY-185/evidence-report.md new file mode 100644 index 00000000..5f8f5831 --- /dev/null +++ b/docs/demo-evidence/STORY-185/evidence-report.md @@ -0,0 +1,215 @@ +# Evidence Report — STORY-185 + +**Story:** STORY-185: S7comm COTP TPDU-Type Parser: `parse_cotp_header`, Protocol-ID +Extraction, VP-049 Kani Skeleton +**Wave:** 88 +**Date:** 2026-09-06 +**Branch:** feature/STORY-185-cotp-parser +**Product type:** Library (pure-core free function — no CLI/web surface; the S7comm +dispatch wiring that consumes this module is a later story, STORY-186, mirroring +STORY-184's role as this story's own predecessor in the same `iso_on_tcp` module) + +--- + +## Full Test Suite: 52/52 PASS (30 story_184 + 22 story_185) + +Command: +``` +cargo test --test iso_on_tcp_tests +``` + +Output: +``` + Finished `test` profile [unoptimized + debuginfo] target(s) in 0.09s + Running tests/iso_on_tcp_tests.rs (target/debug/deps/iso_on_tcp_tests-...) + +running 52 tests +test story_184::test_BC_2_20_001_returns_none_for_empty_slice ... ok +test story_184::test_BC_2_20_001_returns_none_for_one_byte ... ok +test story_184::test_BC_2_20_001_invariant_no_panic_on_truncated_inputs ... ok +test story_184::test_BC_2_20_001_returns_none_for_three_bytes_canonical_vector ... ok +test story_184::test_BC_2_20_001_returns_none_for_two_bytes ... ok +test story_184::test_BC_2_20_002_bad_version_short_circuits_before_length_decode ... ok +test story_184::test_BC_2_20_002_invariant_no_panic_across_version_byte_sample ... ok +test story_184::test_BC_2_20_002_returns_none_for_version_0x00_canonical_vector ... ok +test story_184::test_BC_2_20_002_returns_none_for_version_0x04_off_by_one_canonical_vector ... ok +test story_184::test_BC_2_20_002_returns_none_for_version_0xFF_canonical_vector ... ok +test story_184::test_BC_2_20_003_invariant_no_panic_across_sub_minimum_lengths ... ok +test story_184::test_BC_2_20_003_returns_none_for_length_five_below_rfc_minimum ... ok +test story_184::test_BC_2_20_003_returns_none_for_length_four_below_rfc_minimum ... ok +test story_184::test_BC_2_20_003_returns_none_for_length_one_canonical_vector ... ok +test story_184::test_BC_2_20_003_returns_none_for_length_six_boundary_below_rfc_minimum ... ok +test story_184::test_BC_2_20_003_returns_none_for_length_three_off_by_one_canonical_vector ... ok +test story_184::test_BC_2_20_003_returns_none_for_length_two ... ok +test story_184::test_BC_2_20_003_returns_none_for_length_zero_canonical_vector ... ok +test story_184::test_BC_2_20_004_exact_length_match_no_trailing_bytes ... ok +test story_184::test_BC_2_20_004_four_way_partition_is_exhaustive ... ok +test story_184::test_BC_2_20_004_reserved_byte_nonzero_parses_identically_to_zero ... ok +test story_184::test_BC_2_20_004_trailing_bytes_beyond_declared_length_still_accepted_canonical_vector ... ok +test story_184::test_BC_2_20_004_valid_input_returns_some_header_length_65535_max_canonical_vector ... ok +test story_184::test_BC_2_20_004_valid_input_returns_some_header_length_7_canonical_vector ... ok +test story_184::test_rfc1006_s6_length_four_below_minimum_returns_none ... ok +test story_184::test_rfc1006_s6_minimum_valid_length_holdout ... ok +test story_184::test_rfc1006_s6_ten_byte_tpkt_holdout ... ok +test story_184::test_rfc1006_s6_wide_length_field_holdout ... ok +test story_185::test_BC_2_20_005_invariant_no_panic_across_short_inputs ... ok +test story_185::test_BC_2_20_005_len_shorter_than_2_returns_none ... ok +test story_185::test_BC_2_20_006_invariant_no_panic_across_li_value_sample ... ok +test story_185::test_BC_2_20_006_li_truncation_returns_none ... ok +test story_185::test_BC_2_20_006_li_zero_not_truncated_proceeds_to_classification ... ok +test story_185::test_BC_2_20_007_connect_request_nonzero_low_nibble_still_recognized ... ok +test story_185::test_BC_2_20_007_connect_request_protocol_id_none_even_with_trailing_bytes ... ok +test story_185::test_BC_2_20_007_connect_request_recognized ... ok +test story_185::test_BC_2_20_008_connect_confirm_nonzero_low_nibble_still_recognized ... ok +test story_185::test_BC_2_20_008_connect_confirm_recognized ... ok +test story_185::test_BC_2_20_009_dt_nonempty_payload_extracts_protocol_id ... ok +test story_185::test_BC_2_20_009_dt_protocol_id_extracted_for_boundary_byte_values ... ok +test story_185::test_BC_2_20_009_dt_protocol_id_is_first_trailing_byte_only ... ok +test story_185::test_BC_2_20_010_dt_empty_payload_protocol_id_none ... ok +test story_185::test_BC_2_20_011_tpdu_type_match_is_exhaustive ... ok +test story_185::test_BC_2_20_011_unrecognized_tpdu_type_returns_none ... ok +test story_185::test_BC_2_20_012_protocol_id_extraction_totality ... ok +test story_185::test_iso8073_rfc905_s13_2_1_li_excludes_itself_holdout ... ok +test story_185::test_iso8073_rfc905_s13_7_1_dt_class0_normal_format_holdout ... ok +test story_185::test_iso8073_rfc905_table8_cr_cc_low_nibble_is_free_holdout ... ok +test story_185::test_iso8073_rfc905_table8_dr_code_not_modeled_holdout ... ok +test story_185::test_BC_2_20_012_static_regression_guard_no_hardcoded_protocol_literals ... ok +test story_184::proptests::test_BC_2_20_004_proptest_accepted_length_matches_decoded_bytes ... ok +test story_184::proptests::test_BC_2_20_004_proptest_matches_independent_oracle ... ok + +test result: ok. 52 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s +``` + +The 52-test suite is the union of `mod story_184` (30 tests, STORY-184's TPKT-header +parser evidence, previously reported in `docs/demo-evidence/STORY-184/`) and +`mod story_185` (22 tests, this story's COTP TPDU-type parser). Only the `story_185` +subset is this story's obligation; the coverage map below annotates each `story_185` +test against its owning AC. + +--- + +## Coverage Map + +| AC | Description | BC | Tests | Evidence File | Verdict | +|----|-------------|-----|-------|----------------|---------| +| AC-185-001 | `parse_cotp_header` returns None for input shorter than 2 bytes | BC-2.20.005 | 2 | `AC-001-short-input-rejection.md` | PASS | +| AC-185-002 | `parse_cotp_header` returns None when LI declares more bytes than present | BC-2.20.006 | 3 | `AC-002-li-truncation-rejection.md` | PASS | +| AC-185-003 | `parse_cotp_header` recognizes Connect Request (CR) | BC-2.20.007 | 5 | `AC-003-connect-request-recognition.md` | PASS | +| AC-185-004 | `parse_cotp_header` recognizes Connect Confirm (CC) | BC-2.20.008 | 2 | `AC-004-connect-confirm-recognition.md` | PASS | +| AC-185-005 | `parse_cotp_header` recognizes DT with non-empty payload, extracts `protocol_id` | BC-2.20.009 | 4 | `AC-005-dt-nonempty-protocol-id-extraction.md` | PASS | +| AC-185-006 | `parse_cotp_header` recognizes DT with empty payload — `protocol_id` is None | BC-2.20.010 | 1 | `AC-006-dt-empty-payload-protocol-id-none.md` | PASS | +| AC-185-007 | `parse_cotp_header` returns None for an unrecognized TPDU-type code | BC-2.20.011 | 2 | `AC-007-unrecognized-tpdu-rejection.md` | PASS | +| AC-185-008 | The four-way TPDU-type match is exhaustive and non-overlapping over all 16 nibble values | BC-2.20.011 invariant 3 | 1 | `AC-008-tpdu-type-exhaustive-partition.md` | PASS | +| AC-185-009 | `protocol_id` extraction is a total, uninterpreted identity mapping | BC-2.20.012 | 2 | `AC-009-protocol-id-totality.md` | PASS | +| AC-185-010 | VP-049 Kani harness skeleton compiles | VP-049 | verify (grep + `cargo check` + `cargo clippy`) | `AC-010-vp049-kani-skeleton.md` | PASS | + +**Total test-based coverage: 22/22 (all AC-185-001..009); AC-185-010 verified by +source-level inspection (no cargo test target — full Kani proof execution is +STORY-194's obligation, not counted against the 22), matching the STORY-184 AC-184-006 +precedent.** + +--- + +## Per-AC Test Distribution + +| AC | BC | Test Count | Test Names | +|----|-----|-----------|------------| +| AC-185-001 | BC-2.20.005 | 2 | test_BC_2_20_005_len_shorter_than_2_returns_none, test_BC_2_20_005_invariant_no_panic_across_short_inputs | +| AC-185-002 | BC-2.20.006 | 3 | test_BC_2_20_006_li_truncation_returns_none, test_BC_2_20_006_invariant_no_panic_across_li_value_sample, test_BC_2_20_006_li_zero_not_truncated_proceeds_to_classification | +| AC-185-003 | BC-2.20.007 | 5 | test_BC_2_20_007_connect_request_recognized, test_BC_2_20_007_connect_request_nonzero_low_nibble_still_recognized, test_BC_2_20_007_connect_request_protocol_id_none_even_with_trailing_bytes, test_iso8073_rfc905_table8_cr_cc_low_nibble_is_free_holdout (independent holdout, CR half), test_iso8073_rfc905_s13_2_1_li_excludes_itself_holdout (independent holdout) | +| AC-185-004 | BC-2.20.008 | 2 | test_BC_2_20_008_connect_confirm_recognized, test_BC_2_20_008_connect_confirm_nonzero_low_nibble_still_recognized (the CC half of `test_iso8073_rfc905_table8_cr_cc_low_nibble_is_free_holdout` also exercises this AC but is counted under AC-185-003 to avoid double-counting) | +| AC-185-005 | BC-2.20.009 | 4 | test_BC_2_20_009_dt_nonempty_payload_extracts_protocol_id, test_BC_2_20_009_dt_protocol_id_is_first_trailing_byte_only, test_BC_2_20_009_dt_protocol_id_extracted_for_boundary_byte_values, test_iso8073_rfc905_s13_7_1_dt_class0_normal_format_holdout (independent holdout) | +| AC-185-006 | BC-2.20.010 | 1 | test_BC_2_20_010_dt_empty_payload_protocol_id_none | +| AC-185-007 | BC-2.20.011 | 2 | test_BC_2_20_011_unrecognized_tpdu_type_returns_none, test_iso8073_rfc905_table8_dr_code_not_modeled_holdout (independent holdout) | +| AC-185-008 | BC-2.20.011 invariant 3 | 1 | test_BC_2_20_011_tpdu_type_match_is_exhaustive | +| AC-185-009 | BC-2.20.012 | 2 | test_BC_2_20_012_protocol_id_extraction_totality, test_BC_2_20_012_static_regression_guard_no_hardcoded_protocol_literals | +| AC-185-010 | VP-049 | 0 (source-level verification) | N/A — see `AC-010-vp049-kani-skeleton.md` | + +**Test-count cross-check:** 2 + 3 + 5 + 2 + 4 + 1 + 2 + 1 + 2 = 22, matching the +`story_185` subset of the full `cargo test --test iso_on_tcp_tests` run above exactly +(test-by-test row-verified against the raw test-runner output, not just the aggregate +count). Adding STORY-184's 30 tests gives the full suite total of 52, confirmed by the +`test result: ok. 52 passed` line above. + +--- + +## VP-049 Kani Skeleton Evidence + +**Source file:** `src/analyzer/iso_on_tcp.rs`, line 320 (harness), line 293 (`#[cfg(kani)]` gate) +**Harness name:** `verify_parse_cotp_header_safety` +**Property anchored:** A (no panic or out-of-bounds read for any symbolic input, +`len <= 300`, including the LI-truncation bounds check) + +Skeleton presence confirmed via: +``` +grep -n "cfg(kani)\|verify_parse_cotp_header_safety\|mod kani_proofs" src/analyzer/iso_on_tcp.rs +``` +Output: +``` +125:/// `#[cfg(kani)]` skeleton below is scoped to check only no-panic/bounds-safety over +241:/// hardening); the `#[cfg(kani)]` skeleton below is scoped to check only +293:#[cfg(kani)] +294:mod kani_proofs { +320: fn verify_parse_cotp_header_safety() { +``` + +`cargo check` and `cargo clippy --all-targets -- -D warnings` both pass clean (harness +excluded from normal compilation by the `#[cfg(kani)]` gate). The harness shares the +same `kani_proofs` module as STORY-184's VP-048 harness. Full proof run, including the +AC-185-008 exhaustiveness assertions and the AC-185-009 totality assertions: STORY-194. + +--- + +## Recording Method + +This is a pure-core library story (no CLI binary, no web UI — the analyzer is not yet +wired to the CLI; `s7comm.rs` / SS-21 dispatch wiring is a later story, STORY-186, per +ADR-014 Decision 1). Per the demo-recording skill's library/test-harness mode, and +following the same convention this story's predecessor established at +`docs/demo-evidence/STORY-184/`, evidence is captured as: +- Annotated `cargo test` output transcripts grouped by AC, matching the STORY-184 + (S7comm TPKT `parse_tpkt_header`) precedent this story's shape mirrors +- Inline canonical-vector tables sourced from the BC-2.20.005-012 specifications +- Source-level grep verification plus `cargo check`/`cargo clippy` output for the + VP-049 Kani skeleton (AC-185-010) + +VHS/Playwright recordings are not applicable — no interactive surface exists at this +story's scope. + +--- + +## Artifact List + +| File | AC Coverage | +|------|-------------| +| `AC-001-short-input-rejection.md` | AC-185-001 (BC-2.20.005) | +| `AC-002-li-truncation-rejection.md` | AC-185-002 (BC-2.20.006) | +| `AC-003-connect-request-recognition.md` | AC-185-003 (BC-2.20.007) | +| `AC-004-connect-confirm-recognition.md` | AC-185-004 (BC-2.20.008) | +| `AC-005-dt-nonempty-protocol-id-extraction.md` | AC-185-005 (BC-2.20.009) | +| `AC-006-dt-empty-payload-protocol-id-none.md` | AC-185-006 (BC-2.20.010) | +| `AC-007-unrecognized-tpdu-rejection.md` | AC-185-007 (BC-2.20.011) | +| `AC-008-tpdu-type-exhaustive-partition.md` | AC-185-008 (BC-2.20.011 invariant 3) | +| `AC-009-protocol-id-totality.md` | AC-185-009 (BC-2.20.012) | +| `AC-010-vp049-kani-skeleton.md` | AC-185-010 (VP-049) | +| `evidence-report.md` | Index (this file) | + +--- + +## Demo-Evidence Path-Scrub Gate (PG-W70-DEMO-SCRUB) + +Gate defined in: `.factory/maintenance/demo-evidence-scrub-gate.md` + +The gate grep (per PG-W70-DEMO-SCRUB) was run against all files in this directory +before commit. All evidence files in this directory were authored using repo-relative +paths only; no `cargo check`/`cargo clippy`/`cargo test` output line in this directory +names an absolute host path — the local worktree checkout path was never captured in +any transcript in the first place (unlike STORY-184's `cargo check` output, which +included a `Checking wirerust v0.13.3 ()` line requiring substitution, this +story's captured `cargo check`/`cargo clippy` runs produced only `Finished ...` lines +with no path component). + +Result: **zero content matches** for `/Users/`, `/home/`, or any other absolute local +path pattern in any evidence file in this directory. + +Gate status: **PASSED** (2026-09-06).