Contracts, VC naming, and kernel fixes

New given clauses for def contracts (0b71f58)

def contracts can now declare logical variables with a given clause, scoped over requires and ensures and quantified in the generated f.spec theorem. This makes intrinsic verification more expressive and clearer, especially for specs that need standalone logical parameters.

Verification conditions now inherit program-friendly names (8bbc72e)

VC generation now names variables after the program they come from, so proofs see meaningful binders instead of autogenerated placeholders. The new binder-hint machinery also makes those names accessible in more places, reducing the need for manual rename_i-style cleanup.

sym => no longer breaks when preprocessing closes the goal (0290ba6)

grind's sym mode now detects when preprocessing has already solved the goal and avoids reprocessing an assigned metavariable. That fixes a real interactive bug where contradiction-like hypotheses could close the goal before the tactic sequence ran.

Kernel is_prop fix applied to inductive.h (dea8490)

The kernel now uses the corrected proposition test in inductive.h instead of an inlined buggy version. This matters for recursor reduction and structure-to-constructor conversion, and it closes off the underlying is_prop issue in a core code path.

Package code quality checks are now first-class in lake lint (d6e84ed)

lake lint --code-quality can now discover and run package-level checks registered with @[package_code_quality_check], including extra modules supplied via new CLI/package options. Results are emitted alongside linter output as JSON, making code-quality reporting more complete and automation-friendly.

While-loop invariants were simplified around an exit flag (01fe110)

Verification loop invariants now use a dedicated Bool → ... shape instead of encoding exit state through a sum type. This is a refactor that makes the API easier to use and align with the way forIn/repeat loops are actually modeled.

repeat/forIn specs now speak in false/true instead of sum constructors (01fe110)

The Std.WP.Gadget.ForIn spec lemmas and elaboration path were updated to match the new invariant shape, with the loop exit flag explicitly threaded through the VC generation pipeline. This keeps the specification language closer to the program semantics and simplifies downstream reasoning.

Other misc changes

• Kernel regression test added for the is_prop issue.
• CI/test harness hardened to prevent tracked-file writes.
• simp spec precondition bookkeeping tightened.
• Stage0 and assorted test updates.