Repository navigation
[NUMBERS-218] Fix representable minimum-value powers - #223
Merged
Merged
Conversation
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## master #223 +/- ##
============================================
+ Coverage 99.24% 99.68% +0.43%
- Complexity 1802 2505 +703
============================================
Files 70 77 +7
Lines 4779 6913 +2134
Branches 881 1346 +465
============================================
+ Hits 4743 6891 +2148
+ Misses 10 4 -6
+ Partials 26 18 -8 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
pilifs
added a commit
to pilifs/in-the-loop
that referenced
this pull request
Nov 1, 2026
A target may now name an overload by its parameter types, 'pkg.Class#pow(int, int)', in Java's spelling, simple or qualified. verifier::select_method does this for derive, equivalence and prove, and a bare overloaded name is refused with the list of overloads. Contract::file_name maps it to Class.pow-int-int.contract. The expression language accepts -2147483648, as Java does. Both came out of running the /verify-bytecode skill's pieces on apache/commons-numbers#223. Verified: the integration test an_overloaded_method_is_named_by_its_parameter_types and the expression unit tests pass. Written by session 2e359813; its commits were separated from a concurrent session's after both had finished. LLM-Trace-Summary: https://github.com/pilifs/in-the-loop/blob/main/llm-dlc/traces/a308f9d3-8d8a-42ca-b074-d388818c2418/summary.md LLM-Trace-Log: https://terminalvalue.net/raw-traces/a308f9d3-8d8a-42ca-b074-d388818c2418/079307709b5792435cd91cf29506691717ae3b62c55c743894dc107027c96092.jsonl.gz LLM-Trace: a308f9d3-8d8a-42ca-b074-d388818c2418 sha256:079307709b5792435cd91cf29506691717ae3b62c55c743894dc107027c96092
pilifs
added a commit
to pilifs/in-the-loop
that referenced
this pull request
Nov 1, 2026
…mmand installer plugins/jvmcontract/ is a Claude Code plugin whose skill, /verify-bytecode <pull request>, fetches a GitHub pull request as its merge base and head (scripts/fetch-pr.sh), compiles one module of each with Maven or Gradle and prints its classes and dependency classpath (scripts/build.sh, with a configuration-cache-safe Gradle init script), and then has the agent pick a proof per changed method: a regression proof with jvmcontract equivalence for static methods over primitives and integral arrays, a confined-change proof with --unchanged-unless when the pull request declares a change, a property proof of the Javadoc's @throws, @return and @PARAM claims with jvmcontract prove, a behavioural contract diff for finite-domain methods, and capability and API contract diffs for the module, always. SKILL.md is the procedure, reference.md the tool's commands, expression language, refusals and measured costs for the agent, and report-template.md the report's shape. The skill runs on model: opus (Opus 5.5) and is only invoked explicitly. install.sh installs the skill into ~/.claude/skills, builds jvmcontract with cargo install --git (installing Rust first if needed), and checks for a JDK, JBMC, gh, build tools and jq; .claude-plugin/marketplace.json at the repo root makes 'claude plugin install jvmcontract --marketplace pilifs/in-the-loop' the other one-command path. The plugin README gives the install, what it proves, and five libraries to try it on (Commons Numbers, Joda-Time, Commons Codec, jackson-core, Commons Lang); the repo README links it. The landing page for terminalvalue.net/verify-bytecode-skill/ is in the Terminal-Value repository, not here. On a real pull request, apache/commons-numbers#223, the regression proof of pow(int, int) found the fix's input pow(k=-2, e=31) (before: ArithmeticException, after: -2147483648) in 185 s; the Javadoc property proved in 1.4 s; the MIN_VALUE property proved on head in 1.0 s and was refuted on base in 0.7 s; the confined-change proof did not finish in 300 s. The Maven build of the external project could not be run in this session (the permission classifier declined it), so the changed file was compiled with javac alone; build.sh's Gradle path was verified on examples/apps/boxoffice and its Maven path only by reading. Verified: the new integration test an_overloaded_method_is_named_by_its_parameter_types and the expression unit tests pass; the whole suite passed except one JBMC test that failed under contention with a concurrent proof and passed alone; the Terminal-Value site builds with the new page. LLM-Trace-Summary: https://github.com/pilifs/in-the-loop/blob/main/llm-dlc/traces/2e359813-25c2-4259-888b-42d3a5f0eee6/summary.md LLM-Trace-Log: https://terminalvalue.net/raw-traces/2e359813-25c2-4259-888b-42d3a5f0eee6/55abdd123c57197876cc70f0f039c4e23d9e2dca4ac708bb3e37907e3abb5763.jsonl.gz LLM-Trace: 2e359813-25c2-4259-888b-42d3a5f0eee6 sha256:55abdd123c57197876cc70f0f039c4e23d9e2dca4ac708bb3e37907e3abb5763 LLM-Trace-Summary: https://github.com/pilifs/in-the-loop/blob/main/llm-dlc/traces/a308f9d3-8d8a-42ca-b074-d388818c2418/summary.md LLM-Trace-Log: https://terminalvalue.net/raw-traces/a308f9d3-8d8a-42ca-b074-d388818c2418/ce7ed5a6e273f4765971bab2633deeea41841ecc2e7205d924b292222a813f23.jsonl.gz LLM-Trace: a308f9d3-8d8a-42ca-b074-d388818c2418 sha256:ce7ed5a6e273f4765971bab2633deeea41841ecc2e7205d924b292222a813f23
pilifs
added a commit
to pilifs/in-the-loop
that referenced
this pull request
Nov 2, 2026
…as the first real-world example The 56 numbered examples, the four subject systems (apps/), the generator and the Java verifier (tools/), schema/ and index.json moved from examples/ to examples/demo/, and examples/real-world/ was added for pull requests to published libraries verified with the /verify-bytecode skill: a README with the verified pull requests and the table of libraries to try next (moved out of the plugin README), and commons-numbers-223/, a record of the run on apache/commons-numbers#223 (ArithmeticUtils.pow) with the witness, the four verdicts and their times as recorded on 2026-11-01, what the run did not reach (pow(long, int), the module-level diffs), how it was produced (the file compiled alone with javac because the Maven build could not run in that session), and the commands to rerun it. examples/README.md is now a short hub for the two kinds; approaches.md and setup/ stay shared. The root README, the lib README, the plugin READMEs and references, lib's tests and doc comments, and every path inside the examples (patches, example.json, result.json, SARIF, verifier output, contract headers) point at the new paths; build.py's repo root and link depth were adjusted. Verified: a link checker over every relative markdown link in the repo finds no broken link outside the six pre-existing template placeholders; cargo test --test integration passed (24 tests, reading the moved Box Office contracts); regenerating examples 004 and 015 with the moved build.py reproduced the moved files byte for byte (004's result.json gained two null fields the current generator writes); the three quick property proofs of the Commons Numbers record were rerun on the class compiled from the pull request's commits and gave the same verdicts (1.7 s, 1.1 s, 2.2 s). The landing page in the Terminal-Value repo still links to the old example paths; editing it was outside this repository. LLM-Trace-Summary: https://github.com/pilifs/in-the-loop/blob/main/llm-dlc/traces/a308f9d3-8d8a-42ca-b074-d388818c2418/summary.md LLM-Trace-Log: https://terminalvalue.net/raw-traces/a308f9d3-8d8a-42ca-b074-d388818c2418/9e309e52b8d7ee9e6c6a54091eb65197c2d5f2325188a315f515f90234047ade.jsonl.gz LLM-Trace: a308f9d3-8d8a-42ca-b074-d388818c2418 sha256:9e309e52b8d7ee9e6c6a54091eb65197c2d5f2325188a315f515f90234047ade LLM-Trace-Summary: https://github.com/pilifs/in-the-loop/blob/main/llm-dlc/traces/dfa830a1-4fb4-4d80-8e2c-d612b759742d/summary.md LLM-Trace-Log: https://terminalvalue.net/raw-traces/dfa830a1-4fb4-4d80-8e2c-d612b759742d/3a38e3ec5b12d2523af9b3e3b90819a6ca28d594ee6768e27710aad38c21e1e8.jsonl.gz LLM-Trace: dfa830a1-4fb4-4d80-8e2c-d612b759742d sha256:3a38e3ec5b12d2523af9b3e3b90819a6ca28d594ee6768e27710aad38c21e1e8 LLM-Trace-Summary: https://github.com/pilifs/in-the-loop/blob/main/llm-dlc/traces/2e359813-25c2-4259-888b-42d3a5f0eee6/summary.md LLM-Trace-Log: https://terminalvalue.net/raw-traces/2e359813-25c2-4259-888b-42d3a5f0eee6/4e63b53eff6e08ad53da41b80349dee876fd7a7e62cd15172d4302175da1f5e3.jsonl.gz LLM-Trace: 2e359813-25c2-4259-888b-42d3a5f0eee6 sha256:4e63b53eff6e08ad53da41b80349dee876fd7a7e62cd15172d4302175da1f5e3
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
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.
Summary
(-2)^31forintand(-2)^63forlong.Jira: https://issues.apache.org/jira/browse/NUMBERS-218
Validation
mvn clean verifypassed across the local reactor.AI assistance used.