[squid-protocol]

Part of #5278.

Checklist: partial [c:0c25aa7e] -- the COPAUA0C case and proven record already exist (22 scenarios, merged earlier); two branches stay uncovered: line 339 true (stated unprovable here) and line 963 false (MQCLOSE failure, needs MQ fault injection, own PR); the (verify) blockers.txt line is read on the next generated run.

What this does

Tried to cover COPAUA0C line 339 (WS-MSG-PROCESSED > WS-REQSTS-PROCESS-LIMIT, true) with a 502-request scenario (a repeat key on a stated MQ message). The run showed the branch cannot be proved:

• WS-RESP-LENGTH (line 46, VALUE 1) is the STRING ... WITH POINTER of every reply (730) and is never reset, so a task's replies pile up in the 200-byte W02-PUT-BUFFER; the MQPUT1 length (756) is the pointer.
• Measured: 1 to 3 identical requests prove equal on both sides; the 4th reply leaves the pointer at 201, a one-byte read past the buffer. GnuCOBOL reads the next byte of storage, the det port refuses (IndexOutOfBounds [0,201) of 200). IBM leaves that read undefined, so no defined proof reaches 501 requests.
• So the scenario and the repeat key were dropped (not shipped). The case's notes now state the branch as unprovable by name; a test pins the facts in the source (lines 46, 108, 339, the three WS-RESP-LENGTH uses); the record was re-proved (evidence.py prove: proven, 22 runs, 7 fault runs, no differences; coverage unchanged at 62/69 branches).

Class: COPAUA0C branches no defined input reaches vs. ones a scenario can add. Class table: 339 true = undefined-behaviour (this PR, by name); 700 x5 = infeasible (stated, #6108); 963 false = needs MQ fault injection (sibling gap).

Gates

pr_gates --fast 7/7, --ratchets 9/9 (via heavy-run.sh, JDK 17), test_evidence.py 47 passed, tree-wide guards 85 passed, the case test file 9 passed.

Lessons for agents

• A 502-request MQ scenario needs identical messages that collide: a repeated approve inserts the same PAUTDTL1 key at the fixed clock (I004); only a path that writes nothing to IMS repeats safely.
• A pointer-accumulating STRING ... WITH POINTER across loop iterations (never reset) makes a bounded buffer overrun after a few iterations: check the pointer before designing a high-count scenario.

🤖 Generated with Claude Code

[squid-protocol]

No description provided.

[squid-protocol]

PR #6153 @ bc14b99: 1 failed check(s)

== det (failure) -- real
https://github.com/squid-protocol/gitgalaxy/actions/runs/39900112591/job/120240218735
repro: tests/tools/box/heavy-run.sh python tests/tools/proof_sweep.py --det-only --skip-db2 --cases --work /tmp/gitgalaxy-scratch/ci-digest/sweep
errors:
##[error]Process completed with exit code 1.
log tail:
compression-level: 6
overwrite: false
include-hidden-files: false
archive: true
env:
pythonLocation: /opt/hostedtoolcache/Python/3.12.15/x64
PKG_CONFIG_PATH: /opt/hostedtoolcache/Python/3.12.15/x64/lib/pkgconfig
Python_ROOT_DIR: /opt/hostedtoolcache/Python/3.12.15/x64
Python2_ROOT_DIR: /opt/hostedtoolcache/Python/3.12.15/x64
Python3_ROOT_DIR: /opt/hostedtoolcache/Python/3.12.15/x64
LD_LIBRARY_PATH: /opt/hostedtoolcache/Python/3.12.15/x64/lib
##[endgroup]
With the provided path, there will be 174 files uploaded
Artifact name is valid!
Root directory input is valid!
Uploading artifact: det-sweep-ledger.zip
Beginning upload of artifact content to blob storage
Uploaded bytes 141691
Finished uploading artifact content to blob storage!
SHA256 digest of uploaded artifact is fc3dcbf392e0d29152736230b4bf39257106706ec2841af5d4ce61d9b0819810
Finalizing artifact upload
Artifact det-sweep-ledger successfully finalized. Artifact ID 12478223758
Artifact det-sweep-ledger has been successfully uploaded! Final size is 141691 bytes. Artifact ID is 12478223758
Artifact download URL: https://github.com/squid-protocol/gitgalaxy/actions/runs/39900112591/artifacts/12478223758
Post job cleanup.
[command]/usr/bin/git version
git version 2.55.0
Temporarily overriding HOME='/home/runner/work/_temp/ccea4948-7983-4a75-90a3-507db969c719' before making global git config changes
Adding repository directory to the temporary git global config as a safe directory
[command]/usr/bin/git config --global --add safe.directory /home/runner/work/gitgalaxy/gitgalaxy
Removing SSH command configuration
[command]/usr/bin/git config --local --name-only --get-regexp core.sshCommand
[command]/usr/bin/git submodule foreach --recursive sh -c "git config --local --name-only --get-regexp 'core.sshCommand' && git config --local --unset-all 'core.sshCommand' || :"
Removing HTTP extra header
[command]/usr/bin/git config --local --name-only --get-regexp http.https://github.com/.extraheader
[command]/usr/bin/git submodule foreach --recursive sh -c "git config --local --name-only --get-regexp 'http.https://github.com/.extraheader' && git config --local --unset-all 'http.https://github.com/.extraheader' || :"
Removing includeIf entries pointing to credentials config files
[command]/usr/bin/git config --local --name-only --get-regexp ^includeIf.gitdir:
[command]/usr/bin/git submodule foreach --recursive git config --local --show-origin --name-only --get-regexp remote.origin.url
Cleaning up orphan processes

[squid-protocol]

CI shepherd: the head of this PR (b3955b0) is not the one a maintainer labelled shepherd:merge on (new commits, or never approved), so the label was removed and nothing merges unreviewed code. Re-add the label when the new head is ready (shepherd:reapprove marks this PR until then).

[squid-protocol]

No description provided.

[squid-protocol]

No description provided.