Repository navigation
Porting loop at scale: baseline-reuse proofs, run-many, adopt; COCRDUPC recorded as not proven - #4085
Merged
Merged
Conversation
…COCRDUPC recorded as not proven - Each loop proves the generated service while the model writes the first attempt; every attempt's proof then reuses that run's COBOL side and built project (equivalence.py --reuse): 13 s a proof instead of 45 for CardDemo's sign-on. Measured per loop: the model ~140 s an attempt, generating the project 27 s, a full proof 43 s. - run-many: loops side by side, one process each, starts staggered. - adopt: a proven port into its case unchanged, with provenance.json from the loop's records; refuses a loop that did not prove. - uses_ports files are merged before --reuse compares overlays (a borrowed CSUTLDTC port made every reused proof of CORPT00C fail). - README: COCRDUPC (card update) is not proven on purpose -- its update writes blanks into a PIC 9(3) CVV, which a typed field cannot hold; COACTUPC's case is written, its port pending (too large for one answer). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ
Contributor
This was referenced Oct 2, 2026
Merged
Merged
This was referenced Oct 9, 2026
Merged
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.
Measured on CardDemo's online programs: per attempt, the model takes about 140 s, project generation 27 s, and a full proof 43 s.
--reuseagainst that run: 13 s instead of 45 for sign-on, and the whole loop drops from 221 s to 153 s. A port that replaces files other than the generated service is proven in full.run-manyruns many loops side by side, one process each, with staggered starts.adoptcopies a proven port into its case unchanged and writesprovenance.jsonfrom the loop's records. It refuses a loop that did not prove.uses_portsfiles are now merged before--reusecompares overlays. Before this, every reused proof of CORPT00C failed on the borrowed CSUTLDTC port.PIC 9(3)CVV, which a typed Java field cannot hold.porting_loop.md, section "At scale", covering the new commands and drafting cases with agents.Full suite: 13262 passed. audit_check: all clear.
🤖 Generated with Claude Code
https://claude.ai/code/session_01RZE6us7fUL6Hynk59rWLvZ