Repository navigation
harness compares every OCCURS occurrence; the whole table travels (Fixes #4765) - #4772
Merged
Merged
Conversation
… table travels (Fixes #4765) The harness's record layout listed an OCCURS group's fields once (the first occurrence), so a COMMAREA's table was compared at occurrence 1 only: a cbsa-inqacccu port that never wrote account 3's type was PROVEN on main. - layout_fields(..., occurrences=True): every occurrence a field, by name and subscript (COMM-ACC-TYPE(3), nested CELL(2,4)), with its OCCURS DEPENDING ON constraints; a COMMAREA is read by it, each side by its own ODO count (active_fields). A file's record names each occurrence (they were compared only as "bytes outside the layout"). - a scenario's COMMAREA is the whole record (it was cut at the first occurrence's end: INQACCCU's EIBCALEN was 123 of 1985 bytes, accounts 2..N written past it), every occurrence INITIALIZEd. - a LINKed task gets its COMMAREA's bytes too (CicsTask.withLinkArea); a port that takes them (a det port) is read from them; a DTO's values are the first occurrence (first_occurrences), the rest absent -- compared. - det: a DTO whose OCCURS fields appear once spans its declared record with or without a POINTER (LINK span, EIBCALEN), and RETURN / XCTL pass its bytes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D
squid-protocol
added this to the
Training Montage 🏋️ — Prepping to one-shot our 4th CICS to Java translation attempt milestone
squid-protocol
added
bug
Contributor
…4765) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D
# Conflicts: # tests/equivalence/det_sweep_coverage.json
squid-protocol
changed the title
squid-protocol
marked this pull request as ready for review
October 9, 2026 10:39
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
1 participant
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 #4765. Part of #4270.
The bug (proof strength). The harness's record layout (
equivalence_common.layout_fields) listed an OCCURS group's fields once, at occurrence 1, the same way the generated DTO does. So a COMMAREA's table was compared at its first occurrence only. Shown oncbsa-inqacccu: a mutant det port that never writes account 3'sCOMM-ACC-TYPEis PROVEN on origin/main. On this branch it is NOT PROVEN:commarea.COMM-ACC-TYPE(3): COBOL 'ISA', Java ''.A second harness bug was hiding under that one. The scenario COMMAREA was cut at the end of the first occurrence. INQACCCU ran with 123 of its 1985 bytes (
commarea.inwas 123 bytes), so accounts 2..N were written past EIBCALEN.What changed
layout_fields(..., occurrences=True): each occurrence is its own field, named by its subscripts (COMM-ACC-TYPE(3), nestedCELL(2,4)), with its OCCURS DEPENDING ON constraints. The COMMAREA is read with this layout, and each side is filtered by its own ODO count (active_fields). So a count that differs is reported as a difference, and so is an occurrence that only one side has. A count that is not a number keeps every occurrence: none are dropped on a guess. The default layout (what records are built from, and what generated inputs use) is unchanged.commarea_record), with every occurrence INITIALIZEd. A plain DTO-style name (COMM-EYE) means occurrence 1.CicsTask.withLinkArea). If the port takes them (task.linkArea(), which det ports do), its result is read from those bytes, every occurrence included. A DTO's values map to occurrence 1 (first_occurrences). Occurrences the DTO lacks show up as absent and are compared, never assumed equal.DetCics.commareaOut) instead of the first-occurrence DTO (Dto.extentvsDto.size).Tests:
tests/cobol_mainframe/test_occurs_compare_4765.py(15 tests) covers OCCURS, ODO, nested and elementary OCCURS, an occurrence-3 difference caught end to end throughoutputs/_java_events/compare_events, ODO counts that differ, DTO first-occurrence mapping, batch naming, and the det LINK/XCTL span.Re-proved
cbsa-inqacccu(COMMAREA goes from 18 to 246 fields;three-accountsnow compares accounts 2 and 3) andcarddemo-readacct(ARRYFILE goes from 4 to 12 fields). Both still prove.proof_sweep.py --det-only(Db2 local): 77 proven. The 3 not proven are the existing baseline entries (cardupdate Porting loop at scale: baseline-reuse proofs, run-many, adopt; COCRDUPC recorded as not proven #4085, intcalc-generated D1, mpmt COBOL oracle/translator: floating point and compiler options (COMP-1/2 hex float, NUMPROC, ARITH(EXTEND), TRUNC(OPT), INTDATE, COMP-5 byte order) #4271). Verdict: "sweep: as expected".proof_sweep.py --model-only: 28/28 proven, "as expected".evidence.py status --ciexits 0).cbsa-inqacccuhas no evidence record; its case.json notes are updated.pr_gates --fast5/5,--ratchets7/7 pass, 0 skipped.Not changed (follow-ups):
equivalence_call.compare_dtostill compares only DTO-mapped fields. Screens keep the old layout: no case's BMS map has an OCCURS. DTOs that differ from their declared length because of a trailing FILLER (CBSA CustctrlDfhcommarea, GenApp Lg*) keep their extent.🤖 Generated with Claude Code
https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D