Slipstream/emc
3
0
Fork 0
Code Issues Pull requests Releases 4 Activity Actions

feat: verify data-flow transformation semantics #25

Merged
jwilger merged 1 commit from feat/verify-data-flow-transformations into main 2026-06-05 23:18:28 -07:00
Conversation 2 Commits 1 Files changed 9 +160 -98
jwilger commented 2026-06-05 23:10:32 -07:00
Owner
Copy link

Summary

  • Add Lean and Quint root obligations that classify every data-flow transformation as one formal category: identity, projection, derivation, default, absence, or transformation.
  • Wire the new Quint invariant into generated project config and default emc verify execution.
  • Update data-flow authoring fixtures to use the formal categories instead of prose transformation labels.

Rationale

  • Information completeness requires transformation/projection/default/absence semantics to be mechanically represented in the authoritative Lean4 and Quint artifacts.
  • This keeps semantic acceptance in Lean/Quint verification instead of adding a duplicate Rust validator.

Verification

  • cargo nextest run init_creates_deterministic_project_layout --no-tests=fail failed before implementation on the missing Lean transformation predicate.
  • cargo fmt --check && cargo nextest run -E 'binary(init_project) | binary(add_formal_slice_facts) | binary(check_project) | binary(verify_project) | binary(mcp_verify)' --no-tests=fail
  • Positive formal smoke via nix develop: lake env lean model/lean/RepairDesk.lean, quint typecheck model/quint/RepairDesk.qnt, and quint verify --invariant modelDataFlowTransformationsAreModeled model/quint/RepairDesk.qnt passed for a modeled projection data flow.
  • Negative formal smoke via nix develop: corrupting the data flow to copied without normalization made both Lean and Quint fail the new transformation obligation.
  • cargo fmt --check && cargo build --quiet && git diff --check
Summary - Add Lean and Quint root obligations that classify every data-flow transformation as one formal category: identity, projection, derivation, default, absence, or transformation. - Wire the new Quint invariant into generated project config and default `emc verify` execution. - Update data-flow authoring fixtures to use the formal categories instead of prose transformation labels. Rationale - Information completeness requires transformation/projection/default/absence semantics to be mechanically represented in the authoritative Lean4 and Quint artifacts. - This keeps semantic acceptance in Lean/Quint verification instead of adding a duplicate Rust validator. Verification - `cargo nextest run init_creates_deterministic_project_layout --no-tests=fail` failed before implementation on the missing Lean transformation predicate. - `cargo fmt --check && cargo nextest run -E 'binary(init_project) | binary(add_formal_slice_facts) | binary(check_project) | binary(verify_project) | binary(mcp_verify)' --no-tests=fail` - Positive formal smoke via `nix develop`: `lake env lean model/lean/RepairDesk.lean`, `quint typecheck model/quint/RepairDesk.qnt`, and `quint verify --invariant modelDataFlowTransformationsAreModeled model/quint/RepairDesk.qnt` passed for a modeled `projection` data flow. - Negative formal smoke via `nix develop`: corrupting the data flow to `copied without normalization` made both Lean and Quint fail the new transformation obligation. - `cargo fmt --check && cargo build --quiet && git diff --check`
feat: verify data-flow transformation semantics
All checks were successful
CI / Nix flake check (pull_request) Successful in 2m48s
Details
CI / Request auto_review semantic review (pull_request) Successful in 3s
Details
auto_review auto_review: 1 warning
CI / Rust CI (pull_request) Successful in 6m50s
Details
d8b6a42b10
auto-review approved these changes 2026-06-05 23:13:38 -07:00
auto-review left a comment
Copy link

This PR introduces formal classification of data-flow transformations into categories like identity, projection, and transformation, integrating these into Lean and Quint verification processes. The changes appear well-structured and include updates to tests and documentation. Ensure that all new invariants and classifications are correctly integrated and tested.

Walkthrough

  • docs/event-model/formal-modeling-rules.md

    • Updated to reflect that every datum now has transformation semantics, changing a yellow checkmark to green.

  • src/core/layout.rs

    • Added RequireCanonicalDeclaration for modelDataFlowHasModeledTransformationSemantics and modelDataFlowTransformationsAreModeled.

  • src/core/project.rs

    • Added modelDataFlowTransformationsAreModeled to the list of invariants in project configuration.

  • src/core/verify.rs

    • Integrated modelDataFlowTransformationsAreModeled into the verification process.

  • tests/connect_workflow.rs

    • Updated test cases to use formal transformation categories instead of prose labels.

  • tests/init_project.rs

    • Added assertions to check for the presence of transformation semantics in both Lean and Quint project roots.

  • tests/mcp_verify.rs and tests/verify_project.rs

    • Updated to include the new invariant in the verification logs.

LLM usage and cost

This PR introduces formal classification of data-flow transformations into categories like identity, projection, and transformation, integrating these into Lean and Quint verification processes. The changes appear well-structured and include updates to tests and documentation. Ensure that all new invariants and classifications are correctly integrated and tested. ## Walkthrough - **docs/event-model/formal-modeling-rules.md** - Updated to reflect that every datum now has transformation semantics, changing a yellow checkmark to green. - **src/core/layout.rs** - Added `RequireCanonicalDeclaration` for `modelDataFlowHasModeledTransformationSemantics` and `modelDataFlowTransformationsAreModeled`. - **src/core/project.rs** - Added `modelDataFlowTransformationsAreModeled` to the list of invariants in project configuration. - **src/core/verify.rs** - Integrated `modelDataFlowTransformationsAreModeled` into the verification process. - **tests/connect_workflow.rs** - Updated test cases to use formal transformation categories instead of prose labels. - **tests/init_project.rs** - Added assertions to check for the presence of transformation semantics in both Lean and Quint project roots. - **tests/mcp_verify.rs** and **tests/verify_project.rs** - Updated to include the new invariant in the verification logs. ## LLM usage and cost - Reasoning (gpt-4o) in=19316 out=1018 cost=$0.111850 - Cheap (gpt-4o-mini) in=10146 out=69 cost=$0.001563 Estimated total USD: $0.113413 via https://api.openai.com and https://api.openai.com
src/core/layout.rs
auto-review commented 2026-06-05 23:13:38 -07:00
Owner
Copy link

🟡 Warning: Lines 6–14: Ensure that the logic for checking transformation semantics is consistent across both Lean and Quint implementations, as discrepancies could lead to verification issues.

🟡 **Warning:** **Lines 6–14:** Ensure that the logic for checking transformation semantics is consistent across both Lean and Quint implementations, as discrepancies could lead to verification issues.
jwilger commented 2026-06-05 23:16:59 -07:00
Author
Owner
Copy link

Addressed the transformation-consistency warning with the current implementation and verification evidence:

  • The generated Lean predicate and generated Quint predicate enumerate the same six categories: identity, projection, derivation, default, absence, and transformation.
  • tests/init_project.rs asserts both generated predicates and their root theorem/invariant are present in the generated artifacts.
  • The formal smoke verified both sides: a projection data flow passed lake env lean, quint typecheck, and quint verify --invariant modelDataFlowTransformationsAreModeled; changing the same data flow to copied without normalization made both Lean and Quint fail the transformation obligation.

I did not add a Rust semantic validator for these categories because the PR intentionally leaves acceptance to the Lean/Quint artifacts.

Addressed the transformation-consistency warning with the current implementation and verification evidence: - The generated Lean predicate and generated Quint predicate enumerate the same six categories: `identity`, `projection`, `derivation`, `default`, `absence`, and `transformation`. - `tests/init_project.rs` asserts both generated predicates and their root theorem/invariant are present in the generated artifacts. - The formal smoke verified both sides: a `projection` data flow passed `lake env lean`, `quint typecheck`, and `quint verify --invariant modelDataFlowTransformationsAreModeled`; changing the same data flow to `copied without normalization` made both Lean and Quint fail the transformation obligation. I did not add a Rust semantic validator for these categories because the PR intentionally leaves acceptance to the Lean/Quint artifacts.
Sign in to join this conversation.
Reviewers
No reviewers
auto-review
Labels
Clear labels
  
bug
Something is not working

  
duplicate
This issue or pull request already exists

  
enhancement
New feature

  
help wanted
Need some help

  
invalid
Something is wrong

  
question
More information is needed

  
wontfix
This won't be fixed

No labels
bug
duplicate
enhancement
help wanted
invalid
question
wontfix
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
2 participants
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
Slipstream/emc!25
No description provided.