Repository navigation
CBACT01C proven (carddemo-readacct): COBDATFT model, variable-length records, register A1/C10/L3/F3; Devin's CBACT01C ports judged - #4198
Merged
Conversation
…e-length records, C10 sign tolerance, Devin CBACT01C ports Deferred by the coordinator mid-way (usage window). State: carddemo-readacct proves for our det port (13 runs, 16/16 paragraphs, 41/44 branches); register entries C10 / L3 / F3 not yet written; no sweep run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ
devin_port.py: the WIP's CBACT01C ports and output decoders, plus main's lossless stderr decode (#3813). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ
…rcised), L3 (WORKING-STORAGE with no VALUE), A1 (COBDATFT) The case notes cite A1 for the COBDATFT model, L3 for its two unwritten bytes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ
…'s bounds, RECORD VARYING parsing, COBDATFT as a library call Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ
…xt before a packed field); a z/OS RDW decoder for codev's VBRCFILE; CBACT01C results doc Results on carddemo-readacct (base run, 6 environments): codev #13/#14 proven; eval arms A and B, #229, #168 and #214 write every data file byte for byte (#214 not under ar-EG/th-TH); #167 partial (VB records unframed); #220 crashes on the overpunch. docs/research/devin-cbact01c-harness.md. 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}
| from datetime import datetime | ||
| from pathlib import Path | ||
| from typing import Any, Optional | ||
| from typing import Any, Callable, Optional |
Contributor
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ
Owner
Author
|
Model sweep on this branch: 23/23 proven, as expected. Det sweep (from earlier): 49/51 proven, as expected: the new carddemo-readacct case is proven, and the two known non-proofs are unchanged. |
squid-protocol
added a commit
that referenced
this pull request
Oct 3, 2026
…cture against verdict; register A1/C10/L3/F3; counts 49/51 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ
squid-protocol
added a commit
that referenced
this pull request
Oct 3, 2026
…canner, many translators (draft) (#4192) * docs(research): COBOL->Java translation, observed -- one harness, one scanner, many translators (draft) Blameless, post-hoc observational study across GitGalaxy's det and model ports, IBM WCA4Z's LGACDB01 artifact, Devin workshop ports, SENTINEL IDE, lasserre, Lightyear and an academic API-recovery study. Sections for SENTINEL I/O (#4191), Lightyear/SENTINEL harness runs and the external-fault experiment are marked pending. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ * docs(research): §10 translation strategies compared, and what each teaches Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ * docs(research): §4 SENTINEL I/O after #4193 -- agreement depends on the scanner recognising a translator's runtime vocabulary Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ * docs(research): §6/§8 filled from #4194 -- Lightyear and SENTINEL base runs, missing-file experiment; §9-§11 updated Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ * docs(research): CBACT01C in §6.1 and §7 (#4198) -- 9 Devin runs, structure against verdict; register A1/C10/L3/F3; counts 49/51 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ * docs(research): scenario count scoped to the 50-case sweep Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ * docs(research): SQL fault injection (#4200) -- instruments, Db2 coverage before/after, our own bugs fixed, register M2/X6/X10/X11 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>
squid-protocol
added a commit
that referenced
this pull request
Oct 3, 2026
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ
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.
Finishes the work started on
wip/devin-cbact01c-cobdatft. That branch is merged with main here, not force-pushed.New proven case:
carddemo-readacct(CardDemo CBACT01C). Our det port proves on 13 runs (base plus faults), covering 16/16 paragraphs and 41/44 branches. Three cache-off translations produced byte-identical Java.tests/equivalence/le/cobdatft.c, cobolrtCobdatft.java). Its paths that depend on the load module are refused (exit 98).split_varseq,diff_varseq) and in the det translator and runtime (fd_entries,DetFiles.VarSequential). Until now the translator wrote VB records as 80-byte fixed ones.oracle_assumptions.md:Devin's CBACT01C ports on the new case: base run, 6 JVM locale environments; full table in
docs/research/devin-cbact01c-harness.md.String.formatis called without a localeStructure against verdict: the one proven program is the largest attempt (970 lines, close to the det port's 1,047-line service) and the only one with a complete codec kit. Size alone doesn't predict correctness.
Adapter fixes: the
lines-hex-packeddecoder never advanced past the text before a packed field. It's fixed and tested, with a newvb-rdwdecoder for codev's z/OS RDW framing.Sweeps: det 49/51 proven, "as expected" (the new case proven; the two known non-proofs unchanged). The model sweep is posted below when it finishes.
Tests:
test_varrec_cobdatft.py(5), decoder tests intest_devin_port.py, andtest_source_reads.py.ruff_audit --ciis clean.Not done in this pass: the survey's 8 fixed-width CBACT01C ports, which would need a field-by-field comparison tier.
🤖 Generated with Claude Code
https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ