Skip to content

Latest commit

 

History

History
135 lines (116 loc) · 6.03 KB

File metadata and controls

135 lines (116 loc) · 6.03 KB

Shared-Infrastructure Consistency Lint

Generated by tools/convergence/convergence_report.py.

What this is. A static lint that verifies each backend emitter references the shared planning/lowering helpers and gates (field-step ordering, union-tag validation, lowered-contract validation, and so on). A shared mark means the marker for that class is present in the emitter source: it certifies infrastructure consistency, not runtime behavioral equivalence. Behavioral equivalence is enforced separately: emitted step order by the emit-order verifier (tools/convergence/emit_order_verifier.py, ctest llvmdsdl-emit-order-verifier), which compares each string backend's abstract serialize/deserialize op trace per (type, direction) against the equivalence class proven safe by the Dafny oracle (spec/dafny/CyphalSerdes.dfy); and wire bytes by the parity and malformed-input gates, which consume executed test pass/fail. Read each number here as markers present, not as a correctness proof or a convergence guarantee.

Summary

Backend Markers present Classes shared / total
c 100 14 / 14
cpp 100 14 / 14
go 100 14 / 14
python 100 14 / 14
rust 100 14 / 14
ts 100 14 / 14

Project floor (minimum markers-present score across backends): 100

Per-Backend Classifications

c

Semantic class Status
Field step ordering shared
Union tag mask and validation shared
Scalar cast/normalize and sign extension shared
Variable array prefix normalize and length validation shared
Fixed array cardinality validation shared
Delimited payload header validation shared
Section capacity pre-check shared
Alignment/padding orchestration shared
Malformed-input diagnostic category text shared
Lowered contract schema/version validation shared
Helper-binding completeness gates shared
Verifier-first invariant enforcement shared
Contract-v2 wire-program usage shared
Fallback-free semantic execution gates shared

cpp

Semantic class Status
Field step ordering shared
Union tag mask and validation shared
Scalar cast/normalize and sign extension shared
Variable array prefix normalize and length validation shared
Fixed array cardinality validation shared
Delimited payload header validation shared
Section capacity pre-check shared
Alignment/padding orchestration shared
Malformed-input diagnostic category text shared
Lowered contract schema/version validation shared
Helper-binding completeness gates shared
Verifier-first invariant enforcement shared
Contract-v2 wire-program usage shared
Fallback-free semantic execution gates shared

go

Semantic class Status
Field step ordering shared
Union tag mask and validation shared
Scalar cast/normalize and sign extension shared
Variable array prefix normalize and length validation shared
Fixed array cardinality validation shared
Delimited payload header validation shared
Section capacity pre-check shared
Alignment/padding orchestration shared
Malformed-input diagnostic category text shared
Lowered contract schema/version validation shared
Helper-binding completeness gates shared
Verifier-first invariant enforcement shared
Contract-v2 wire-program usage shared
Fallback-free semantic execution gates shared

python

Semantic class Status
Field step ordering shared
Union tag mask and validation shared
Scalar cast/normalize and sign extension shared
Variable array prefix normalize and length validation shared
Fixed array cardinality validation shared
Delimited payload header validation shared
Section capacity pre-check shared
Alignment/padding orchestration shared
Malformed-input diagnostic category text shared
Lowered contract schema/version validation shared
Helper-binding completeness gates shared
Verifier-first invariant enforcement shared
Contract-v2 wire-program usage shared
Fallback-free semantic execution gates shared

rust

Semantic class Status
Field step ordering shared
Union tag mask and validation shared
Scalar cast/normalize and sign extension shared
Variable array prefix normalize and length validation shared
Fixed array cardinality validation shared
Delimited payload header validation shared
Section capacity pre-check shared
Alignment/padding orchestration shared
Malformed-input diagnostic category text shared
Lowered contract schema/version validation shared
Helper-binding completeness gates shared
Verifier-first invariant enforcement shared
Contract-v2 wire-program usage shared
Fallback-free semantic execution gates shared

ts

Semantic class Status
Field step ordering shared
Union tag mask and validation shared
Scalar cast/normalize and sign extension shared
Variable array prefix normalize and length validation shared
Fixed array cardinality validation shared
Delimited payload header validation shared
Section capacity pre-check shared
Alignment/padding orchestration shared
Malformed-input diagnostic category text shared
Lowered contract schema/version validation shared
Helper-binding completeness gates shared
Verifier-first invariant enforcement shared
Contract-v2 wire-program usage shared
Fallback-free semantic execution gates shared