Repository navigation
[needs Joe's review] Model ports CBSA INQACC, GenApp LGUPDB01 (proven with #4188) - #4208
Merged
squid-protocol merged 1 commit intoOct 3, 2026
Conversation
…ven once LINKed programs run (#4188) 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 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ
Contributor
squid-protocol
merged commit Oct 3, 2026
3aae0f1
into
fix/model-proof-linked-programs
2 checks passed
squid-protocol
added a commit
that referenced
this pull request
Oct 3, 2026
…va (#4207) * equivalence: a port's proof runs the programs its task LINKs to as Java (#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 * Model ports CBSA INQACC, GenApp LGUPDB01: unedited model answers, proven 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> * equivalence: an SQL fault is injected only where its statement's program 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 * test_sql_faults: ruff format (quote style only) 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>
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.
Joe approves or declines this PR; nobody else merges it. A model wrote these ports, and we never approve a model-written port on Joe's behalf.
This PR is stacked on #4207 (#4188), which it needs to prove. It retargets to main once #4207 merges.
--faults all)cbsa-inqaccInqaccServicegenapp-lgupdb01Lgupdb01ServiceProvenance
cmpchecked).provenance.json: carries the ticket hash and token counts, plus aproven_afternote. The loop's own verdicts were "not proven", because a port's proof ran the LINKed program as its stub (equivalence: model-port proofs don't run a case's LINKed programs (INQACC, XFRFUN, LGUPDB01 unprovable) #4188); with equivalence: model-port proofs don't run a case's LINKed programs (INQACC, XFRFUN, LGUPDB01 unprovable) #4188 the stored attempts prove unedited.Not included: CBSA XFRFUN. It still differs in the model's port (ABND-CODE
RUF3against the COBOL'sRUF2on the null-date scenarios).🤖 Generated with Claude Code
https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ