Repository navigation
equivalence: a port's proof runs the programs its task LINKs to as Java - #4207
Merged
Merged
Conversation
…va (#4188) A case's "programs" (the programs its task LINKs to) ran on the Java side as their generated stubs when a port was proven, so anything they write never appeared there: CBSA INQACC and XFRFUN (-> ABNDPROC) and GenApp LGUPDB01 (-> LGUPVS01) could not prove however right the port was. prepare_project now resolves each LINKed program for a port's proof: the port's own service if it carries one, else the program's committed model port (the case proving it), else its deterministic translation from this checkout; the CICS report names each origin (report.json linked_programs). Re-proving the loop's stored attempts, unedited (--faults all): INQACC attempts 2-4 proven (14 scenarios); attempt 1 not proven LGUPDB01 attempts 1-4 proven (5 scenarios) XFRFUN attempts 1-3 not proven: ABND-CODE RUF3 vs the COBOL's RUF2 on the two null-date scenarios -- a difference in the model's port Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ
Contributor
…ven once LINKed programs run (#4188) (#4208) The porting loop's stored attempts (claude-sonnet-5-5, no tools, ticket prompt only), byte-identical to its records, each with provenance.json. The loop called them not proven because a port's proof ran the LINKed program (ABNDPROC, LGUPVS01) as its stub; with #4188 they prove unedited: cbsa-inqacc attempt 2: 14 scenarios, 22/25 paragraphs, 13/25 branches genapp-lgupdb01 attempt 1: 5 scenarios, 8/9 paragraphs, 17/38 branches Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
…t and the LINKed-program origins Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ
…ram has the DetSql seam (#4173 x #4188) A model port reaches Db2 its own way. Once #4188 runs a task's LINKed programs from their det ports, DetSql is on the classpath and the plan installed, but a fault on the model-ported program's own statement never fires: 'faults fired differ: cobol [..], java []'. The seam is now decided per statement owner (sql_seam_programs): a fault whose program's Java does not use DetSql makes the task not judged, with the no-hook reason; a fault on a det-ported LINKed program's statement is injected and judged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| def test_sql_seam_is_decided_per_statement_owner(tmp_path): | ||
| """#4173 x #4188: a model-ported main program has no seam even when a det-ported program it LINKs to puts | ||
| DetSql on the classpath; a fault on the det program's own statement can be injected and judged.""" | ||
| import equivalence_cics as ec |
|
|
||
|
|
||
| def test_a_det_main_program_has_the_seam(tmp_path): | ||
| import equivalence_cics as ec |
Owner
Author
|
Verification after the SQL-fault integration fix (868f2df... / 368096a, 879368a), merged here as 646369c. Root cause. #4200 decided the SQL fault seam once per task: it checked whether Fix. The seam is now decided per statement owner (
Both directions are unit-tested. Sweeps on the branch head:
🤖 Generated with Claude Code |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #4188.
The problem. A case's
"programs"(the programs its task LINKs to) ran on the Java side as generated stubs when a port was proven, so whatever they wrote never appeared there. CBSA INQACC and XFRFUN (which LINK ABNDPROC) and GenApp LGUPDB01 (which LINKs LGUPVS01) could not prove, however right the port was.The fix.
prepare_projectresolves each LINKed program for a port's proof, in this order:The CICS report names each program's origin (
report.json→linked_programs). Det-port runs (det_port.py) already translated the extras and are unchanged.Re-proving the loop's stored attempts, unedited (
--faults all):XFRFUN's remaining difference is in the model's port, not the harness: on the two null-date scenarios its ABND-CODE is
RUF3where the COBOL writesRUF2.The proven INQACC and LGUPDB01 ports are in a separate PR, [needs Joe's review].
Model sweep: running (the first run was cut off by a background time limit on a heavily loaded machine). The result will be posted here.
Tests:
test_linked_programs.py(committed-model-port origin, port-carried origin);ruff_audit --ciclean.🤖 Generated with Claude Code
https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ