feat: verify bit encoding consistency #23

Merged

jwilger merged 1 commit from feat/verify-bit-encoding-consistency into main

2026-06-05 22:33:44 -07:00

jwilger commented

2026-06-05 22:24:32 -07:00

Owner

Summary

Adds Lean4 and Quint obligations that require displayed view fields and external payload fields to use the same bit encoding as their corresponding modeled data-flow rows.
Wires the new Quint invariants into generated quint.json, emc verify, and MCP verify process plans.
Extends canonical artifact checks so emc check reports drift if the new obligations are missing from generated artifacts.

Rationale
Information completeness requires data-flow facts to preserve bit-level semantics at the point where data is presented or crosses an external boundary. The formal artifacts already required non-empty bit encodings and modeled data-flow coverage; this change makes the Lean4 and Quint artifacts mechanically compare those encodings for view and external payload targets.

Verification

cargo nextest run init_creates_deterministic_project_layout --no-tests=fail
cargo fmt --check && cargo nextest run -E 'binary(init_project) | binary(check_project) | binary(verify_project) | binary(mcp_verify)' --no-tests=fail && cargo build --quiet && git diff --check
nix develop -c sh -lc 'cd <generated-smoke-project> && lake env lean model/lean/RepairDesk.lean && quint typecheck model/quint/RepairDesk.qnt && quint verify --invariant modelViewFieldBitEncodingsMatchDataFlows,modelExternalPayloadFieldBitEncodingsMatchDataFlows,modelMeaningfulDataFlowsAreCovered model/quint/RepairDesk.qnt'
Negative smoke: corrupting the view-field bit encoding to UTF-16 string caused Lean to fail at modelViewFieldBitEncodingsMatchDataFlows and Quint to report a counterexample for modelViewFieldBitEncodingsMatchDataFlows.

Summary - Adds Lean4 and Quint obligations that require displayed view fields and external payload fields to use the same bit encoding as their corresponding modeled data-flow rows. - Wires the new Quint invariants into generated `quint.json`, `emc verify`, and MCP verify process plans. - Extends canonical artifact checks so `emc check` reports drift if the new obligations are missing from generated artifacts. Rationale Information completeness requires data-flow facts to preserve bit-level semantics at the point where data is presented or crosses an external boundary. The formal artifacts already required non-empty bit encodings and modeled data-flow coverage; this change makes the Lean4 and Quint artifacts mechanically compare those encodings for view and external payload targets. Verification - `cargo nextest run init_creates_deterministic_project_layout --no-tests=fail` - `cargo fmt --check && cargo nextest run -E 'binary(init_project) | binary(check_project) | binary(verify_project) | binary(mcp_verify)' --no-tests=fail && cargo build --quiet && git diff --check` - `nix develop -c sh -lc 'cd <generated-smoke-project> && lake env lean model/lean/RepairDesk.lean && quint typecheck model/quint/RepairDesk.qnt && quint verify --invariant modelViewFieldBitEncodingsMatchDataFlows,modelExternalPayloadFieldBitEncodingsMatchDataFlows,modelMeaningfulDataFlowsAreCovered model/quint/RepairDesk.qnt'` - Negative smoke: corrupting the view-field bit encoding to `UTF-16 string` caused Lean to fail at `modelViewFieldBitEncodingsMatchDataFlows` and Quint to report a counterexample for `modelViewFieldBitEncodingsMatchDataFlows`.

jwilger added 1 commit

2026-06-05 22:24:32 -07:00

feat: verify bit encoding consistency

CI / Nix flake check (pull_request) Successful in 2m44s

Details

CI / Request auto_review semantic review (pull_request) Successful in 2s

Details

auto_review auto_review: no findings

CI / Rust CI (pull_request) Successful in 6m52s

Details

38938d6101

auto-review approved these changes

2026-06-05 22:27:26 -07:00

auto-review left a comment

Walkthrough

src/core/layout.rs: Added new effects to require canonical declarations for bit encoding consistency checks.
src/core/project.rs: Updated project initialization to include new invariants in the generated quint.json.
src/core/verify.rs: Integrated new invariants into the verification process.
tests/init_project.rs: Added tests to ensure the new invariants are correctly defined and checked in Lean and Quint models.
tests/mcp_verify.rs and tests/verify_project.rs: Updated tests to include new invariants in the verification logs.

LLM usage and cost

Reasoning (gpt-4o) in=18262 out=319 cost=$0.096095
Cheap (gpt-4o-mini) in=623 out=48 cost=$0.000122
Estimated total USD: $0.096217 via https://api.openai.com and https://api.openai.com

The PR introduces new invariants to ensure bit encoding consistency between displayed view fields, external payload fields, and their corresponding data-flow rows. The changes are integrated into the verification process and tested for correctness. The modifications appear safe to merge. ## Walkthrough - **src/core/layout.rs**: Added new effects to require canonical declarations for bit encoding consistency checks. - **src/core/project.rs**: Updated project initialization to include new invariants in the generated `quint.json`. - **src/core/verify.rs**: Integrated new invariants into the verification process. - **tests/init_project.rs**: Added tests to ensure the new invariants are correctly defined and checked in Lean and Quint models. - **tests/mcp_verify.rs** and **tests/verify_project.rs**: Updated tests to include new invariants in the verification logs. ## LLM usage and cost - Reasoning (gpt-4o) in=18262 out=319 cost=$0.096095 - Cheap (gpt-4o-mini) in=623 out=48 cost=$0.000122 Estimated total USD: $0.096217 via https://api.openai.com and https://api.openai.com

jwilger merged commit 818d10e766 into main

2026-06-05 22:33:44 -07:00

jwilger referenced this pull request from a commit

2026-06-05 22:33:44 -07:00

feat: verify bit encoding consistency (#23)