Cardano Updates

- Introduced `LspDepCache` to store type information and checked modules for improved performance.
- Added methods to `LspProject` for managing the dependency cache, including `new_with_cache`, `dep_cache`, and cache management during compilation.
- Updated `Project` struct to support skipping dependency checks and injecting module types from the cache.
- Enhanced the `compile` method to utilize cached data, reducing unnecessary re-inference of modules.
- Modified `Platform` and `Dependency` enums to derive `Hash` for improved caching capabilities.
- Implemented incremental caching logic in `type_check` to avoid re-parsing unchanged modules.

Signed-off-by: KtorZ <[email protected]>

Signed-off-by: KtorZ <[email protected]>

Fix LSP not finding definitions, modules or constructors not included in the dependency path.

  In particular, allow the LSP to suggest imports from builtins when relevant.

  This whole thing has been broken ever since we introduced the module pruning to avoid compiling modules not strictly required by the program. As a result, we wouldn't have access to definitions from fully new modules, and the LSP quickfix would simply look as if they worked half of the time. Since we already parse all modules anyway, we can simply stash the definitions and constructor names into some kind of indexes to lookup from later.

Signed-off-by: KtorZ <[email protected]>

Bumps [openssl](https://github.com/rust-openssl/rust-openssl) from 0.10.72 to 0.10.78.
- [Release notes](https://github.com/rust-openssl/rust-openssl/releases)
- [Commits](https://github.com/rust-openssl/rust-openssl/compare/openssl-v0.10.72...openssl-v0.10.78)

---
updated-dependencies:
- dependency-name: openssl
  dependency-version: 0.10.78
  dependency-type: direct:production
...

Signed-off-by: dependabot[bot] <[email protected]>

Upstream PlutusCore's `#import_uplc` now yields a `PlutusScript` value
(a wrapper around `Program`), so the `AikenVerify.Utils` helpers that
took a raw `Program` caused a type-mismatch at every theorem-emission
site. Update the four public helpers (`proveTests`, `proveTestsHalt`,
`proveTestsError`, `witnessTests`) to accept `PlutusScript` and unwrap
`.script` before handing the inner `Program` to `cekExecuteProgram`.
The internal `executeIntProgram`, `executeDataProgram`, and
`cekExecuteProgram` helpers still take `Program` as before.

PlutusCore's `#import_uplc` macro now requires 4 arguments:
`<identifier> <lang> <format> <filepath>`. Our template emitted only 3,
causing Lean to reject the proof file with `unexpected token; expected
identifier` at the filepath literal (the parser expected a `<format>`
identifier). Downstream errors (including spurious `BitVec` messages at
theorem sites) were cascading elaboration failures from that parse error.

Aiken's config layer enforces Plutus V3 exclusively via `validate_v3_only`
in config.rs, so hardcoding `PlutusV3` is correct and reflects the only
compilation target Aiken actually produces.

Verified: generated proofs now parse cleanly; remaining failures are a
separate downstream issue where `#import_uplc` produces `PlutusScript`
but `proveTests` in AikenVerify.Utils still expects `Program`.

Replaces the name-gated recognition of stdlib fuzzers in
`normalize_fuzzer_from_call` / `try_extract_stdlib_primitive_constraint` /
`try_extract_list_length_bounds` with a purely structural classifier. User
wrappers, stdlib renames, and re-exports now verify without the recognizer
knowing their names.

Why the old approach broke `aiken verify`:

1. `normalize_fuzzer_from_call` descended into helper bodies *before*
   classifying the call as a primitive leaf. For `fuzz.int_between(0, 1000)`,
   helper descent reached the body `if min > max { … } else if min == max
   { … } else { … }`. `normalize_fuzzer_from_expr` had no `If`/`When` arm
   and the catch-all produced an opaque normalization. The primitive
   fallback below was thus unreachable for every stdlib fuzzer whose body
   starts with control flow (`int_between`, `int_at_least`, `int_at_most`,
   `bytearray_between`) or a lambda (`int`, `constant`, `bool`, `bytearray`,
   `data`).
2. The extraction helpers `try_extract_stdlib_primitive_constraint` and
   `try_extract_list_length_bounds` gated on the literal module path
   `"aiken/fuzz"` and the literal function name (`"int_between"`,
   `"int_at_least"`, `"list_between"`, …). Re-exports, renames, and
   wrappers fell through silently.

What this change does:

- Adds explicit `TypedExpr::If`, `TypedExpr::When`, and `TypedExpr::Fn`
  arms in `normalize_fuzzer_from_expr`. `If`/`When` are peeled: every
  branch is normalized; if they all agree, the shape is lifted; otherwise
  the merge falls back to `Primitive { known_constraint: None }` over the
  expression's fuzzer payload type. `Fn` (the `fn(prng) { … }` shape used
  inside `fuzz.int`, `fuzz.constant`, etc.) becomes an unconstrained
  primitive leaf.
- Reorders `normalize_fuzzer_from_call`: after the structural combinator
  check, helper-body descent runs first (so `negate_fuzzer() = fuzz.map(
  fuzz.int_between(1, 50), negate)` still exposes its `Map` shape). If
  helper descent returned `Opaque` *and* the helper body is a control-flow
  or anonymous-function shape (`If`/`When`/`Fn`), the call is reclassified
  as an unconstrained primitive. Placeholders like `todo`/`fail`
  (`TypedExpr::ErrorTerm`) are deliberately excluded from this widening —
  they do not produce any value of `T`, so letting them widen would
  mask latent bugs.
- Replaces `try_extract_stdlib_primitive_constraint` (renamed
  `try_extract_primitive_constraint_structurally`) and
  `try_extract_list_length_bounds` with trivial implementations that
  always return `None`/`(None, None)`. The user's non-negotiable
  constraint is that no code path may match on `"aiken/fuzz"` identifiers;
  the safe, sound default is to over-approximate to `FuzzerConstraint::Any`
  (or no length bounds). Downstream `default_semantics_for_type` then
  emits unbounded `IntRange { None, None }` / empty-bounded lists, which
  become universal quantifications in the Lean emitter — a sound widening
  for property tests.
- Widens `apply_unary_map_semantics_precision` to fall back to
  `default_semantics_for_type(output_type)` for `UnaryMapperShape::Unknown`
  (and for unhandled `IntAffine` / `ConstructorMap` cases). Previously
  these emitted `Opaque` semantics, which caused `verify.rs`'s
  per-semantic-arm error paths to abort with "semantic domain is opaque"
  rather than emit a universally-quantified theorem.

Test updates: the unit tests that pinned the old name-matched bound
extraction (`int_at_least_semantics_has_open_upper_bound`,
`extract_constraint_name_agnostic_*_uses_*_shape`,
`normalize_fuzzer_map_of_map_depth_four_yields_intrange_constraint`,
`extract_constraint_such_that_preserves_inner_domain`, and the depth-4
`Bind` propagation tests) are updated to expect `FuzzerConstraint::Any` /
unbounded `IntRange { None, None }`. The
`..._map_stays_conservative_for_unknown_mapper` test is renamed to
`..._falls_back_to_default_for_unknown_mapper` and reflects the new
widening behavior. Recursive-wrapper-cycle tests are unchanged: mutually
recursive bodies have no control-flow base case, so they stay opaque.

The now-unused extraction helpers (`try_extract_int_literal`,
`INT_LITERAL_MAX_DEPTH`, `try_extract_exact_scalar`, `STDLIB_FUZZ_MODULE`)
are `#[cfg(test)]`-gated to silence dead-code warnings — tests still
exercise the recursion-depth guard.

End-to-end result: the reproducer `aiken verify run -m
"math.prop_double_is_add"` no longer emits "semantic domain is opaque".
Every test in the `verify-e2e-test` fixture now proceeds through preflight
and Lean theorem emission; the remaining failures are pre-existing
Blaster/Lean infrastructure issues (`Inductive datatype with instance
parameters not supported: BitVec`), unrelated to this change.

Signed-off-by: KtorZ <[email protected]>