Document source: 58297516d707; code reference: 58297516d707. 中文. Source language: zh_CN; requested: en; actual: en; translation: reviewed.

Source documentation does not establish software or physical hardware qualification. See the support and qualification records for their exact scope.

Bounded I/O lifecycle property matrix

tools/testing/io_lifecycle_matrix.json maintains 203 reviewed finite properties covering STM32F407/GD32F470 UART, SPI, I2C, ADC, CAN, USB, raw Ethernet, capture/advanced timers, selected STM32G474 software-reference providers/factory, Native descriptor sequences and RS485 direction adaptation. Each property identifies instance mode, production TU, register model, actual Google case, assertions and production calls within that case, and the invariant and limits proved. Names and test counts alone cannot establish evidence that a property holds.

One execution chain

Run the maintained command:

python scripts/ci/tdd_gate.py --all --preset native-debug

The gate first runs tool tests and builds the actual CMake nexus_google_contracts. Capture then binds the current catalogue, CMake executable plan, compilation database, compiled objects, each target binary, and explicit SHA256 identities for production/test/model/public-contract sources. Each provider and test TU must belong to its specified Google target’s actual compilation context; shared Core/I/O TUs retain real library objects and commands. Missing objects or targets cannot fall back to matching source names. Capture also saves source, object and command identities for every local TU in selected targets from that actual compilation database, including generated factory bindings.c in the build directory. Sources must reside in the current checkout or build, and objects in the corresponding current-build target. Missing objects, symlinks, out-of-bound paths and changes to generated sources/objects during execution are rejected. This observation reuses the CMake graph rather than registering another build graph.

The existing runner performs complete discovery and unfiltered execution, retaining commands, return codes and fresh XML. Audit rechecks that inputs are unchanged, that discovery, XML and execution-summary case identities match exactly, and that every indexed property completed. The commit gate requires the entire CMake Google plan to finish and cannot use allow_subset. Only success produces:

• build/<preset>/tdd/io-property-inputs.json: pre-execution input identities.

• build/<preset>/tdd/execution.json: the sole runner’s actual complete execution results.

• build/<preset>/tdd/io-property-report.json: finite properties bound to those actual results.

A new round deletes old summaries and property reports; failures cannot leave previous success reports. If execution succeeds but audit fails, raw execution remains for diagnosis but no qualified property report is generated.

Property boundaries

Assertion anchors provide reviewable source navigation only. The tool excludes comments, strings and same-named assertions in other cases but cannot automatically prove an assertion’s logical meaning. Models must execute actual production providers; hardware dependencies are explicitly modeled, and model results cannot establish board waveform, electrical or physical timing qualification.

Current focus includes residue-free admission, epochs/cancellation, loan retention, quarantine/retry after failed stop, final IRQ/DMA withdrawal, late errors, counts/loss, FIFO/LIFO stream loans, finite deadlines, continuous-receive target replacement and resource exhaustion. This is neither all register combinations, all controllers, all event interleavings nor formal proof. Added properties include CAN abort/domain/loss, USB FIFO/clock/SETUP epochs, Ethernet descriptors/held RX tokens, and generated-factory failure cleanup, foreign-cold rejection, permissions and timer-output readback order. Other GPIO/Flash/basic PWM/watchdog suites derive no coverage from this matrix. The catalogue’s unproven field lists the complete unproved scope.

Factory properties actually call current generated entries; models replace only external CPU/MMIO ports. Some assertions use a fixture’s narrow Initialize or declared provider macros. Review must follow fixture definitions to confirm the real production entry rather than interpret arbitrary helper names as production proof. Assertion navigation binds whole sources and compiled contexts but does not automatically analyze reachability of every assertion under conditional compilation. Each target establishes finite behavior only for its actually selected branch.

Capture covers listed TUs, selected targets’ local TUs, models, contracts, and actual commands/objects. It does not claim automatic analysis of the complete header dependency closure or machine-code semantics. Clean-source SDKs, candidate source closure, offline reproduction and physical boards remain established by their respective delivery gates. Property reports explicitly state formal_proof=false and hardware_status=not_executed.

Developers may use the script’s capture/audit subcommands to inspect existing execution. Explicit --allow-subset produces only development-subset for diagnosis; it cannot replace the commit gate or a software candidate. The script neither runs tests nor creates a second target graph, and adds no instrumentation, RAM, worker or vtable slot to MCU instances.

After adding modes or fixing providers, review invariants, real assertions, models and limitations, then bind current sources through fresh build and execution. Historical test counts and hashes cannot become qualification for new sources. Original 80-property development matrices and raw logs preserve their historical bytes; the 203 properties require current-source capture/build/execute/audit, never extension of old successful reports to new properties.