Support external library contracts in Latte and LiquidTypeChecking

.github/workflows/maven-2.yml

@@ -3,7 +3,7 @@ on:
   push:
     branches: [main]
   pull_request:
-    branches: [main]
+    branches: [main, feat/latte-liquid-typechecking]
 
 jobs:
   verify:

README.md

@@ -2,7 +2,7 @@
 
 Latte now runs as an ownership and aliasing pass before an independently implemented refinement checker. Both passes use the same Spoon AST. The old mutable checker has been replaced; no LiquidJava verifier implementation was copied.
 
-The verifier now covers floating-point arithmetic, exception and switch flow, deferred bodies, recursive aliases, allocation recency, inherited contracts, field-backed state, arrays and loop/effect analysis. The imported suite has **165 exact matches out of 311 inputs**; this is not full LiquidJava compatibility. All 410 upstream Java fixtures are preserved. See [compatibility status](docs/compatibility.md) for the implemented behavior, policy differences and precision limits.
+The verifier now covers floating-point arithmetic, exception and switch flow, deferred bodies, recursive aliases, allocation recency, inherited contracts, field-backed state, arrays and loop/effect analysis. The imported suite has **180 exact matches out of 311 inputs**; this is not full LiquidJava compatibility. All 410 upstream Java fixtures are preserved. See [compatibility status](docs/compatibility.md) for the implemented behavior, policy differences and precision limits.
 
 ## Build and run
 
@@ -19,7 +19,7 @@ The first example succeeds. The second reports a state refinement failure and ex
 
 The small library jar is `target/latte-0.0.1-SNAPSHOT.jar`. The runnable `latte-cli.jar` also includes Spoon and Z3, including the native solver libraries supplied by `z3-turnkey`.
 
-`mvn test` runs 465 tests, including the focused tests, legacy Latte regressions and 165 promoted upstream regression inputs. A separate imported-fixture test enforces the intentional fresh-reference comparison difference. `mvn verify -Pcompatibility` also runs **every** imported input and writes `target/liquidjava-compatibility.json`. A successful build does not mean that all upstream expectations match.
+`mvn test` runs 522 tests, including the focused tests, legacy Latte regressions and 180 promoted upstream regression inputs. A separate imported-fixture test enforces the intentional fresh-reference comparison difference. `mvn verify -Pcompatibility` also runs **every** imported input and writes `target/liquidjava-compatibility.json`. A successful build does not mean that all upstream expectations match.
 
 ## Ownership policy
 
@@ -65,6 +65,10 @@ class Example {
 
 [Examples](examples/refinements) cover accepted local aliases, unique and borrowed references, rejected shared references, escapes, stale aliases, field-backed state, arrays, floating-point behavior, control flow and inherited/deferred contracts. Their expected diagnostic kinds and lines are checked by the test suite.
 
+## External Java libraries
+
+Use `@ExternalRefinementsFor` to provide ownership and refinement contracts for JDK or third-party library methods, constructors and fields. Both passes resolve the same contracts on the Spoon AST. See the [external contract guide](docs/external-refinements.md) and [checked examples](examples/refinements/ExternalLibraryContracts.java). Use `--classpath` for library JARs; multiple input paths are analyzed together.
+
 ## AST handoff and embedding
 
 ```java
@@ -100,7 +104,7 @@ The state stores, points-to sets, predicates and proof results are immutable Jav
 - `latte.api`: the two-pass pipeline, diagnostics and CLI.
 - `liquidjava.specification`: freshly defined annotation API with familiar LiquidJava syntax.
 
-External refinements are deliberately deferred. Recursive paths, older loop allocations, unknown calls and exceptions are conservatively approximated; loop inference supports a finite set of inductive bounds. Recursive constructor expansion requires a finite heap summary and currently reports `UNSUPPORTED`. Constructors without source bodies retain conservative effects. These approximations can reject valid programs. Unsupported constructs and solver timeouts are failures. The checker remains a prototype, and the complete compatibility report is the source of truth for port coverage.
+External library contracts are supported through `@ExternalRefinementsFor`; see [syntax, ownership rules and classpath usage](docs/external-refinements.md). Recursive paths, older loop allocations, unknown calls and exceptions are conservatively approximated; loop inference supports a finite set of inductive bounds. Recursive constructor expansion requires a finite heap summary and currently reports `UNSUPPORTED`. Constructors without source bodies retain conservative effects. These approximations can reject valid programs. Unsupported constructs and solver timeouts are failures. The checker remains a prototype, and the complete compatibility report is the source of truth for port coverage.
 
 Run `mvn spotless:apply` after editing Java. Formatting is checked by `mvn verify` and CI.
 

docs/compatibility.md

@@ -8,6 +8,8 @@ The pipeline checks refinements on parameters, locals, fields, assignments, call
 
 The follow-up implementation adds:
 
+- External library contracts shared by Latte and LiquidTypeChecking, including ownership, overloads, constructors, inherited members, fields, state transitions and reference predicates. A per-model registry validates Java signatures and publishes bindings on the Spoon AST. The CLI and embedding API accept library classpaths and multiple source inputs. See [external specifications](external-refinements.md).
+
 - IEEE 754 `float` and `double` arithmetic, rounding, signed zero, NaN, infinities, Java remainder, numeric promotion and narrowing conversions. Java integral operations retain finite-width overflow, signed division/remainder and masked shift counts.
 - Explicit normal, return, throw, break, continue and yield completions. Catches and finally blocks preserve the state at the relevant completion; finally can replace an earlier return. Resource closing, switch fall-through, switch expressions and common implicit exceptions are modeled. Deferred lambda bodies and method references are checked against their functional contracts.
 - Compositional return-alias summaries, including local assignments, conditional returns, delegated returns and recursion. A finite path domain widens recursive paths to reachable subgraphs. Allocation recency distinguishes the newest object at a site from older instances. The original `MyNodeComplete` regression now passes.
@@ -28,12 +30,12 @@ Abstract ghost transitions remain specifications. Their consistency, preconditio
 
 At this checkpoint:
 
-- **165 of 311** imported inputs match the upstream expected diagnostics exactly. The earlier checkpoint had 166; fresh-reference reasoning now intentionally differs on one more fixture, described below.
-- All 165 exact matches are required parameterized tests in `supported-inputs.txt`. `ReferenceFreshnessTest` separately requires the corrected diagnostics for the unchanged reference-comparison fixture.
-- **465 tests** cover these imported inputs, focused regressions, examples and the legacy Latte suite.
+- **180 of 311** imported inputs match the upstream expected diagnostics exactly. External specifications add 15 exact matches to the previous 165. Fresh-reference reasoning retains the intentional difference described below.
+- All 180 exact matches are required parameterized tests in `supported-inputs.txt`. `ReferenceFreshnessTest` separately requires the corrected diagnostics for the unchanged reference-comparison fixture.
+- **522 tests** cover these imported inputs, focused regressions, examples and the legacy Latte suite.
 - Every imported input completes without an uncaught analysis exception.
 - Every upstream negative input is rejected, except the two explicit semantic differences below.
-- The only `UNSUPPORTED` diagnostics in the complete imported audit concern external refinements, appearing in 60 inputs. This does not mean that all other inputs match upstream expectations.
+- External declarations are checked instead of rejected wholesale. Exact-match accounting still distinguishes ownership-policy differences, invalid specifications and precision limits.
 
 Run from `latte/`:
 
@@ -52,7 +54,7 @@ mvn exec:java -Dexec.mainClass=latte.compatibility.CompatibilityAudit \
 
 ## Compatibility differences and precision limits
 
-External refinement specifications remain intentionally deferred. Shared reference refinements are rejected under the requested ownership policy. Existing upstream examples with unannotated reference parameters, shared fields or externally managed objects need suitable ownership contracts before their object-state refinements can be retained.
+External refinement specifications now bind to actual Java library declarations for both passes; see [the contract guide](external-refinements.md). Invalid targets and member signatures are errors, including fixtures where upstream expected only a warning. Shared reference refinements are rejected under the requested ownership policy. Existing upstream examples with unannotated reference parameters, shared fields or externally managed objects need suitable ownership contracts before their object-state refinements can be retained.
 
 Some upstream expectations assume mathematical arithmetic for Java expressions. The new checker rejects those claims when overflow or IEEE rounding supplies a counterexample. Examples include `CorrectFunctionDeclarations`, `CorrectOperatorAssignments`, `CorrectSimpleIfElse` and `CorrectChars`. Predicate-only decimal expressions use mathematical reals; when combined with a floating Java value, they are converted to that floating sort.
 
@@ -65,7 +67,7 @@ These are named exceptions to the negative-input gate, not exceptions for entire
 
 `ErrorIfReferenceComparison.java` still reports its two feasible double-close errors (lines 30 and 39). Its third expected error, at line 21, assumes that a preexisting parameter can equal a newly allocated object. Java allocation freshness rules out that branch. The unchanged fixture is checked by a dedicated regression test and remains a mismatch in the upstream diagnostic audit.
 
-Reference-array examples are in `examples/refinements/ReferenceArrayAliases.java`. Known local elements remain refinable, including borrowed and unique objects. Arbitrary index expressions are summarized by Latte and constrained by symbolic select/store operations in LiquidTypeChecking; this can lose ownership precision. Unknown external elements and implicit rows of multidimensional allocations remain shared summaries, with distinct possible values on different reads. Mutations involving unknown element sets conservatively invalidate object state. Explicit nested array initializers retain their individual array identities. Library containers such as `ArrayList` still require external ownership and alias contracts; this array fix does not add those contracts.
+Reference-array examples are in `examples/refinements/ReferenceArrayAliases.java`. Known local elements remain refinable, including borrowed and unique objects. Arbitrary index expressions are summarized by Latte and constrained by symbolic select/store operations in LiquidTypeChecking; this can lose ownership precision. Unknown external elements and implicit rows of multidimensional allocations remain shared summaries, with distinct possible values on different reads. Mutations involving unknown element sets conservatively invalidate object state. Explicit nested array initializers retain their individual array identities. Library containers such as `ArrayList` can now have external ownership and state contracts. These do not infer arbitrary element ownership or aliases from a size specification.
 
 The analysis remains conservative. Recursive return paths widen after four field steps. Older objects at a repeated allocation site are summarized as shared, so refinements requiring their individual identities may be rejected. Loop inference uses a finite set of candidate bounds rather than arbitrary invariants. Exception and unknown-call effects can lose precision. Unspecified field updates are invalidated rather than inferred as exact method postconditions. Multiple inherited cases guarantee the facts common to the applicable alternatives. Solver timeouts are verification failures, never successful proofs.
 

docs/external-refinements.md

@@ -0,0 +1,79 @@
+# External library contracts
+
+Place a specification type alongside the application sources, annotated with the library's qualified Java name. The verifier uses the existing annotation syntax for both Latte ownership and LiquidTypeChecking refinements. Library source changes are unnecessary.
+
+```java
+@ExternalRefinementsFor("java.util.ArrayList")
+@RefinementPredicate("int size(ArrayList list)")
+interface ArrayListContracts<E> {
+    @StateRefinement(to = "size(this) == 0")
+    void ArrayList();
+
+    @StateRefinement(to = "size(this) == size(old(this)) + 1")
+    boolean add(E value);
+
+    @StateRefinement(from = "true")
+    @Refinement("_ == size(this)")
+    int size();
+}
+```
+
+A constructor is represented by a `void` method with the target class's simple name. Methods use their Java names, parameter types and result types. Parameter names may differ from the library: predicates use the names in the specification. Overloads are matched by erased Java parameter types, including generic bounds. Static library methods can be written as ordinary interface method declarations. Receiver state annotations require an instance method or constructor.
+
+```java
+java.util.ArrayList<Integer> list = new java.util.ArrayList<>();
+java.util.ArrayList<Integer> alias = list;
+alias.add(42);
+@Refinement("_ == 1") int count = list.size();
+```
+
+Both variables have the same Latte identity, so the transition through `alias` changes the state read through `list`. State predicates and state sets belong to `java.util.ArrayList`, independently of the specification type's name. Contracts on inherited Java members are found through the target's class and interface hierarchy. Constructors are never inherited.
+
+## Ownership and effects
+
+Use `specification.Borrowed`, `Unique`, `Free` and `Shared` on external parameters, results and fields with the same meaning as source contracts. Shared references remain ineligible for refinements. A state contract does not upgrade a shared receiver into an owned one.
+
+```java
+@ExternalRefinementsFor("java.util.Arrays")
+interface ArrayContracts {
+    void fill(@Borrowed int[] values, int value);
+}
+```
+
+Here Latte retains local ownership of `values`; LiquidTypeChecking invalidates its old contents because borrowing permits mutation. A reference argument without an ownership annotation is shared and can escape. A `@Free` parameter consumes all local aliases, and a `@Free` result can carry refinements. Constructor parameters follow the same rules. The checked [examples](../examples/refinements/ExternalLibraryContracts.java) include valid local aliases and rejected stale values, consumed aliases and shared receivers.
+
+A receiver contract with only `from`, including `from = "true"`, promises to preserve its state. A `to` clause describes a transition. Without a receiver state clause, a specified instance method may change the receiver. Reference parameters may change regardless of their ownership annotation. Calls missing from the specification retain conservative unknown-call behavior.
+
+Specifications are trusted public contracts; library bodies, placeholder bodies and field initializers are not verified as implementations. State transitions and reference results must accurately describe the library. External calls also conservatively invalidate potentially affected application fields; ownership and receiver contracts do not promise global purity. Library internals and element identities are not inferred from a container-size contract. For example, this ArrayList specification does not establish an ownership or alias relationship between an inserted object and a later `get` result.
+
+External fields can carry refinements and ownership annotations. Actual Java declarations determine whether fields are static; placeholder initializer values never describe the library's storage. Writes in application code must satisfy the field contract. A shared reference field still cannot carry a refinement.
+
+## Library classpath
+
+The JDK is available automatically. For third-party libraries, pass their JARs or class directories. Multiple input paths are analyzed together, so specifications may live separately from the application:
+
+```sh
+java -jar latte/target/latte-cli.jar \
+    --classpath 'lib/library.jar:lib/dependency.jar' \
+    specs src/main/java
+```
+
+The classpath separator is platform-specific (`:` on Unix, `;` on Windows). `-cp` is an alias for `--classpath`.
+
+Embedding uses the same pipeline:
+
+```java
+var result = Verification.verify(
+    List.of("specs", "src/main/java"),
+    List.of("lib/library.jar", "lib/dependency.jar"));
+```
+
+`Verification.verify(Launcher)` also accepts a caller-configured Spoon launcher. Reading signatures does not initialize or execute library classes.
+
+The per-model registry is stored on the Spoon root package under `latte.analysis.external.v1`. Resolved executable references retain their external binding; `ExternalSpecifications.resolve(reference)` exposes the contract. Both passes use that lookup, while ordinary ownership, effects and transfer metadata remain on the same AST. Reanalysis rebuilds the registry; there is no process-global specification cache.
+
+## Validation and boundaries
+
+Unresolvable types, missing members, incompatible result or field types, misplaced annotations and duplicate specifications for the same target are errors. The verifier does not silently ignore an invalid contract. Keep one specification type per target and include its dependencies on the classpath.
+
+Expanded varargs calls currently require an explicit array argument when using an external contract. The verifier reports `UNSUPPORTED` for implicit packing rather than applying an array contract to individual elements. Varargs method references require a lambda that passes an explicit array. Ordinary reference-array ownership limitations still apply. Contract validation is not a replacement for Java compilation or a proof of the library implementation.

examples/refinements/ExternalLibraryContracts.java

@@ -0,0 +1,59 @@
+import liquidjava.specification.*;
+import specification.*;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+@RefinementPredicate("int size(ArrayList list)")
+interface ArrayListContracts<E> {
+  @StateRefinement(to = "size(this) == 0")
+  void ArrayList();
+
+  @StateRefinement(to = "size(this) == size(old(this)) + 1")
+  boolean add(E element);
+
+  @StateRefinement(from = "true")
+  @Refinement("_ == size(this)")
+  int size();
+
+  @StateRefinement(from = "size(this) > 0", to = "size(this) == size(old(this)) - 1")
+  E remove(@Refinement("_ >= 0 && _ < size(this)") int index);
+}
+
+@ExternalRefinementsFor("java.util.Arrays")
+interface ArrayContracts {
+  void fill(@Borrowed int[] values, int value);
+}
+
+@ExternalRefinementsFor("java.util.Objects")
+interface ObjectContracts {
+  @Free
+  @Refinement("_ != null")
+  Object requireNonNull(@Free Object value);
+}
+
+class ExternalLibraryContracts {
+  void aliasesShareLibraryState() {
+    java.util.ArrayList<Integer> list = new java.util.ArrayList<>();
+    java.util.ArrayList<Integer> alias = list;
+    alias.add(42);
+    @Refinement("_ == 1") int size = list.size();
+    list.remove(1); // Expect: REFINEMENT
+  }
+
+  void borrowedArrayRemainsLocal() {
+    int[] values = {0};
+    java.util.Arrays.fill(values, 3);
+    @Refinement("_ != null") int[] alias = values;
+    @Refinement("_ == 0") int stale = alias[0]; // Expect: REFINEMENT
+  }
+
+  void ownershipTransfer() {
+    Object value = new Object();
+    Object oldAlias = value;
+    @Refinement("_ != null") Object result = java.util.Objects.requireNonNull(value);
+    Object consumed = oldAlias; // Expect: PERMISSION
+  }
+
+  void sharedReceiver(java.util.ArrayList<Integer> list) {
+    list.size(); // Expect: SHARED_REFINEMENT
+  }
+}