Add foundational support for class/record/sealed types

[tautschnig]

What was changed?

Adds foundational support for class / record / sealed types to the Java → Laurel front end (JavaToLaurelCompiler). Such types are modelled as opaque Laurel CompositeTypes — Strata treats an unbound composite type as an uninterpreted reference sort — which is enough to accept these values and reason about identity/reference-style properties.

Commits:

1. Accept and verify class/record/sealed types in parameter position — encode a class/interface type (incl. sealed hierarchies and records) as a CompositeType named after its fully-qualified name ($→., package kept for stability/uniqueness). Each referenced sort is declared (an empty compositeCommand, emitted once before the procedures that use it) so Strata's resolver can find it. Test: AcceptClassParam.
2. new T(...) construction — translate to an opaque new_(T) value. The sort is registered here too, so a type appearing only in new T(...) (never in a type position) is still declared and resolves. Test: NewOnlyRecordType.
3. instanceof — explicitly rejected with a clear JavaViolationException (the opaque encoding has no runtime tag).
4. Use fully-qualified names for procedure names — qualifiedMethodName used the outermost class's packageless simple name (Outer_method), inconsistent with the FQ composite-sort scheme; two same-named classes in different packages could collide. Aligned to the FQ scheme (the helper names both declarations and call sites, so they stay matched).

How has this been tested?

./gradlew :verifier:test passes, including AcceptClassParam (type-position acceptance) and NewOnlyRecordType (a record used solely in new position).

Modelling notes / known limitations

Opaque, reference-level foundation — enough for identity/aliasing-style reasoning, not yet a structural encoding:

• Values are opaque references; record components are not captured (needs a Laurel datatype encoding — future work). Constructor argument values/effects are not modelled.
• instanceof is not supported and fails fast at translation.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache-2.0.

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

Adds initial support for Java class/record reference types in the Java→Laurel translation by treating them as opaque, uninterpreted composite sorts, and introduces minimal handling for new and instanceof expressions.

Changes:

• Translate Type.ClassType to an opaque CompositeType using the Java type name.
• Convert new T(...) into an opaque Laurel new_(T) value (discarding constructor args after translation).
• Convert x instanceof T into a call to an instanceOf_<T>(x) predicate.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[fabiomadge]

Locally (origin/main, same Strata e115b8ec): a class/record-typed parameter doesn't verify — static void acceptParam(Point p){} → Error: Resolution failed: '...Point' is not defined. The opaque CompositeType is referenced but never declared (no compositeCommand/prelude entry), so Strata's resolver can't find the sort — looks like it needs an actual type declaration emitted.

(1) Is param-position acceptance meant to verify yet, or just translate? (2) No test in the PR, so CI doesn't catch it — one class-typed method would. (Same shape as my #441 note.)

[tautschnig]

@fabiomadge I believe I have addressed your comments with 12f22f6.

[fabiomadge]

Update on 12f22f6: the declaration fix works for types in type position (params/locals/returns verify, cross-unit too). But the new path has a gap — a type used only in new T(...), never in a type position, isn't registered, so it still hits the original error:

record Q(int x){}
static void make() { Object o = new Q(1); }
// Resolution failed: '...Q' is not defined

translateType does referencedCompositeTypes.add(sortName); the JCNewClass case forms the same name and calls new_(name) without registering it. One-line fix + a new-only test.

Minor: composite sorts use the FQ dotted name, but qualifiedMethodName uses packageless Outer_name — inconsistent (the FQ scheme is the safer one).

Soundness etc. look good (opaque impure composite = Java reference ==; distinct fresh objects not provably equal; instanceof rejects cleanly). Just the new-path gap.

[tautschnig]

@fabiomadge I believe all your comments have been addressed.

[fabiomadge]

Both my findings are fixed and verified: the composite sort is now declared, and the new-only-type gap is closed (referencedCompositeTypes.add(name) in the JCNewClass case) with a NewOnlyRecordType regression test — my repro verifies now. The qualifiedMethodName FQ-rename (addressing the naming-consistency note) passes the full verifier suite with no regressions.

Two non-blocking notes for the record: (1) records are modeled as opaque references — sound for identity/==, but component/value reasoning is deferred (documented); (2) the FQ method-name change is broad — I validated it via the full suite, but didn't exhaustively probe overloaded-name collisions (the existing TODO in that method still applies). Sound foundation. LGTM.