Repository navigation
Improve AutoCorrode automation and timing diagnostics - #281
Merged
Merged
Conversation
`ISABELLE_HEAPS_OVERRIDE` takes precedence over the configurable heap base and suffix in the recommended Isabelle settings, but the Makefile only checked and reported the suffix. It therefore warned for an already isolated worktree and could display a heap directory Isabelle would not use. This commit documents the required `etc/settings` setup and mirrors its precedence in the worktree diagnostics. An explicit override selects the exact heap directory; otherwise `ISABELLE_HEAP_BASE` replaces the default base and `ISABELLE_HEAP_SUFFIX` is appended. Signed-off-by: Hanno Becker <[email protected]>
TIME, TIME', TIME_pos, and TIME_pos' entered TIME_CB whenever their local flag was enabled, even if global Crush timing was disabled. The callback-free wrappers therefore measured tactic sequences only to discard the result. Gate these helpers on both flags and return the identity otherwise. Leave TIME_CB and TIME_CB' unchanged so callback users such as the step timeout still run when timing reports are disabled. Signed-off-by: Hanno Becker <[email protected]>
crush_step_tac_frame prepares ucincl_discharge_tac once per Crush invocation, but the returned closure rebuilt ucincl_solve_tac whenever it was applied to the freshly decorated per-step tactic. Prepare the context-dependent solver before returning the closure. This reuses theorem lookup, simp-context setup, and tactic decoration across all Crush steps while retaining the same proof context. Signed-off-by: Hanno Becker <[email protected]>
ucincl_must_discharge_tac constructed its context-dependent solver below the child-tactic argument. This prevented a partially applied wrapper from sharing the setup and differed from ucincl_discharge_tac. Move solver construction into the proof-context closure. Existing immediate call sites still construct it once; callers that retain the partially applied wrapper can now reuse it. Signed-off-by: Hanno Becker <[email protected]>
REPEAT_SMART assembled step and worklist messages before debug checked its configuration. Since debugging is disabled by default, every step paid for integer conversion, list rendering, and concatenation without emitting the result. Cache the debug level per invocation and accept message thunks so formatting happens only when the corresponding level is enabled. Signed-off-by: Hanno Becker <[email protected]>
Subgoal change detection called Thm.prems_of on both the old and new proof state for every compared goal pair. A successful step can compare several unaffected goals, repeating the same proof-state traversal. Extract both premise lists once per successful step and reuse them for the existing aeconv comparisons. Worklist ordering and change detection remain unchanged. Signed-off-by: Hanno Becker <[email protected]>
Downstream developments repeatedly reproved the same small facts about `find`, multiset inclusion, and set disjointness, and two multiset elimination rules were declared `[elim]` even though their conclusion is a free variable, so they never fired automatically. Add `find_Some_iff_distinct` to `ListAdditional`, `in_not_in_disjoint` to `SetAdditional`, and `distinct_subset_mset_set`, `distinct_from_sublist`, and `mset_take_submset [simp]` to `MultisetAdditional`. Promote `mset_set_minus_singletonE` and `mset_range_minus_singletonE` to `[elim!]`; both discharge an arbitrary goal from a contradictory premise, so eager application is safe. Signed-off-by: Lawrence Paulson <[email protected]>
AutoLocality eagerly materialized pairwise commutativity and cancellation theorems and coupled semantic registrations to physical simprocs. Setup grew quadratically, locale replay duplicated dispatchers, and cancellation repeatedly traversed large update telescopes. Keep certificate bundles in one structural operational-key map and use theorem-free secondary indexes to rank candidates before loading payloads. Derive only requested kernel rewrites in the invocation context and retain no process-global theorem cache. Install one generic simproc per rigid constant and arity family through standard local declarations. Transport both layers through morphisms, merge them symmetrically, and reactivate a local representative only when restricted simplification removes it. Structural lambda heads remain semantic-only. Construct cancellation with bounded recursive conversions, relative attribute indexes, root scheduling, and exact adjacent swaps through record zippers. Invocation-local typed memoization avoids rescanning buried telescope bodies without retaining theorems globally. Add lifecycle, locale, merge-diamond, polymorphism, shape, instrumentation, stress, and Crush regressions. The wide buried-update case falls from 11.715 seconds to 0.026 seconds. Signed-off-by: Hanno Becker <[email protected]>
AutoLocality stopped unfolding a helper as soon as any registration for the same constant existed. A differently specialized application then had neither a matching certificate nor its definition. Explicit fact attributes likewise hid matching certificates from the default locality bundle. Inspect maximal helper applications in the defining equation and use the typed registration selector for each occurrence. Keep unfolding the helper when any occurrence is unmatched. For fully covered helpers, pass the selected core and disjoint certificates to the generated proof through a proof-private fact, independently of their public attributes. Add regressions for a wrapper calling an unregistered specialization and for a wrapper around a custom-attributed helper. Signed-off-by: Hanno Becker <[email protected]>
Explicit `locality_autocancellation` and `locality_autocommutativity` facts required callers to repeat the record type even when their registrations identified it uniquely. Query the semantic registry for matching operation and attribute entries and accept the inferred form only when exactly one record remains. Keep the typed syntax as an explicit disambiguator. Missing or ambiguous registrations fail before theorem construction; the existing proof builders and their coverage remain unchanged. Add success, compatibility, and inherited-record ambiguity regressions, document both forms, and remove redundant record arguments from existing unambiguous users. Signed-off-by: Hanno Becker <[email protected]>
The existing jEdit timing panel reports whole command totals. It cannot show which internal operations of a custom tactic consume time or retain the cost of attempts that return no result. Introduce one profile around a tactic invocation. Nested `time` wrappers measure named operations inside it. The profile combines samples and publishes one compact report when the invocation finishes. PIDE traffic is bounded by invocations and signal names, not attempts. Keep measurement separate from destinations. Context-local sink factories can publish to PIDE, tracing output, or another consumer. Skip the clock entirely when no sink is active. Use a synchronized accumulator on an immutable context stack. Pull one ordinary lazy-sequence result, preserve it, and write nested samples only to the innermost profile. Schema version 2 carries invocation identity, outcome, totals, extrema, and fixed histogram buckets. The decoder continues to accept version 1. Add a standalone Isabelle component, ML API and tests, Scala decoder and scope model, and a jEdit dockable with call and aggregate views for command, proof, theory, and global scope. Signed-off-by: Hanno Becker <[email protected]>
Crush already names and times internal tactic attempts, including attempts that return no result. The measurements depended on `applyτ` and completed histories in proof contexts. Ordinary Crush calls could not publish durable aggregate data. Import the generic timing component and wrap `crush_base`, `fastcrush_base`, and `crush_base_step` with `profile_tactic`. Existing `TIME` wrappers feed active sinks. Low-level callbacks that always need a measurement use `measure_seq`. Remove `applyτ`, its display commands, stored histories, and obsolete examples. Keep the Crush selectors, threshold, and PIDE modifier as producer controls. The wrapper pulls one ordinary lazy-sequence result and does not add an implicit outer total. Signed-off-by: Hanno Becker <[email protected]>
Fine-grained timing reports are stored in compressed PIDE markup exports. `heap-db-inspect` reads only whole-command timings, leaving batch profiling data unavailable outside jEdit. Decode schema versions 1 and 2, including Isabelle XML element and body transports. Add aggregate and per-invocation views, source grouping, separate invocation and sample filters, and versioned JSON that keeps integer microseconds and histogram buckets. Count malformed, unsupported, and duplicate records instead of dropping them silently. Fall back to the `zstd` executable when the Python module is unavailable. Test both schemas, nested markup, deduplication, merging, percentiles, malformed input, and JSON output. Signed-off-by: Hanno Becker <[email protected]>
The I/Q, Isabelle Assistant, and I/P plugin Makefiles accepted the Isabelle installation root or its `bin` directory for the launcher. They still derived Scala and library paths from the raw value, so the `bin` form searched below `bin/contrib`. Normalize the launcher input once. Derive jEdit, Scala, the Isabelle JAR, and plugin dependencies from the installation root. Preserve explicit `ISABELLE`, `SCALA_HOME`, and `SCALAC` overrides. Signed-off-by: Hanno Becker <[email protected]>
The timing panel flattened each scope into one table. Adding a source hierarchy made Global decode every document command and build every row on the Swing event thread. Each level also rescanned the same invocations, so a large session could wedge jEdit before repainting. Make timing signals the roots and expand through theory, proof, command, and detail context as the scope permits. Build reusable call and aggregate indexes per command. Merge cached node indexes for Global scope, and preserve zero-sample calls as zero aggregates. Decode PIDE reports, build indexes, format rows, and construct expanded children in cancellable Isabelle futures. Initially create only signal roots, rebuild only changed nodes, reject superseded generations, and invalidate caches when the dockable closes. Apply thresholds at the displayed level and keep qualified proof names distinct. Persist column visibility and timing precision. Use numeric sorting for flat rows, replace Crush-specific categories with a generic name filter, and normalize the component Makefile path. Keep expansion stable across refreshes and disable sorting while hierarchical rows are visible. Signed-off-by: Hanno Becker <[email protected]>
Fine_Grained_Timing combined the proof session with the registered jEdit component. Registering the component to load its system options therefore exposed the session globally. Snapshot worktrees then found the same session again through `-d .` and failed with a duplicate session error. Keep the proof sources and session roots in `Fine_Grained_Timing`. Move the options, panel sources, resources, and build logic to the sessionless `Fine_Grained_Timing_Panel` component. Register only that component and keep `Fine_Grained_Timing` in `AutoCorrode/ROOTS`. Keep the session, theory, option, JAR, and markup names unchanged. Point the panel session test at the new source directory. Signed-off-by: Hanno Becker <[email protected]>
Crush tries the branches of its step tactic in list order. `aentails_cond_crule_tac` and `aentails_crule_tac` sat after `unfold_prems_tac`, `aentails_core_tac`, and `aentails_drule_tac`, so a goal that a registered `crule` closes directly was first put through premise unfolding and the core and drule branches. Move both crule branches directly after `aentails_cancel_tac`. A goal with a matching `crule` now takes it first; the relative order of the remaining branches is unchanged. This changes which proof `crush` finds for goals reachable both ways, so proofs that relied on the earlier branch order may need adjusting. Signed-off-by: Hanno Becker <[email protected]>
state_locality_for_op collected every Const-headed argument of a
partial application into baked_cnames, and default_simps then unfolded
each one's definition when discharging. For
locality_lemma for perf: <pspecial_c True> footprint [qc]
the baked argument is True, so HOL.True_def reached the simplifier.
True is simp's own normal form, so rewriting it via
True == ((%x::bool. x) = (%x. x))
destroys the normalisation that discharges side conditions and
collapses the output of if_split. The automatic discharge then
diverged instead of failing, and the command died with
Interrupt_Breakdown after Poly/ML could no longer grow the stack --
with nothing in the trace, because that code path carries a counter
but no trace point.
A baked constant is now unfolded only if
(1) its type mentions the record type -- a bool, numeral or string
literal carries no record structure, so unfolding it can reveal
no field; and
(2) it is not declared by the logical core, i.e. by a theory at or
below HOL.
Both guards are needed: only (1) excludes numerals, and only (2)
excludes undefined :: rec => _. The declaring theory is resolved
through the constant name space (Name_Space.theory_name, Theory.check,
Context.subthy) rather than by inspecting the long name, so a user
constant that merely sits in a HOL-prefixed namespace is not
misclassified.
Narrowing this list cannot rename any generated fact:
locality_public_id decides partial-application naming from p_term with
its own, deliberately broader, test.
AutoLocality_Test_Perf.thy now discharges, and
AutoLocality_Test_Shapes_Wide.thy still passes -- its w_apply_policy
policy_a footprints only close if policy_a_def is still unfolded, so
the narrowing does not overshoot.
Signed-off-by: Lawrence Paulson <[email protected]>
Isabelle2026 checks that document-preparation meta-comments nest
properly across a theory (Document_Output.check_nesting, called from
present_thy):
Meta-comments (*<*)...(*>*) need to be properly nested: this was
never checked in the past. INCOMPATIBILITY.
Both an unmatched (*>*) and an unclosed (*<*) are now errors, reported
as "Bad nesting of meta-comments". Six files were unbalanced, in two
shapes:
- missing opener before the final `end`: StdLib_Result,
StdLib_Option, StdLib_Contracts, References, Weak_Triple
- opener left unclosed at end of file: Basic_Micro_Rust
These are cosmetic defects in the boilerplate-hiding markup that never
affected any proof, which is why they accumulated unnoticed: only
document preparation reads the markers, and most sessions run with
document=false.
The change is balance-only, so it is equally valid under
Isabelle2025-2; it is separated from the Isabelle2026 migration proper
so it can be taken on its own.
Signed-off-by: Lawrence Paulson <[email protected]>
Fine-grained timing can publish each sample through multiple built-in outputs. `timing_threshold_us` is meant to discard short samples before they reach those outputs, but the threshold was checked only for PIDE reports. Enabling `fine_grained_timing_output` therefore printed samples that PIDE omitted. Check `timing_threshold_us` in the tracing sink as well. Keep sinks added through `add_sink` unchanged: they receive raw samples and remain responsible for filtering them. Signed-off-by: Hanno Becker <[email protected]>
Fine-grained timing records whether an Isabelle tactic or method invocation succeeds. A method can return an error as its first result, but the profiler treated any first result as success. For example, an invalid `goal_cases` argument was reported with `success="true"` even though the method had failed. Make the generic result profiler accept a predicate that identifies successful results. Tactic results always count as successful, while method results count as successful only when they are `Seq.Result`; `Seq.Error` remains a failure. Signed-off-by: Hanno Becker <[email protected]>
Fine-grained timing reports the elapsed time and outcome of an Isabelle tactic or method invocation. An invocation can produce more than one result while the prover backtracks. The profiler published only the first result, so later work could add nested samples or change the final outcome without updating the report. Summing all samples is also wrong: an outer timed call already includes time spent in nested calls. Keep measuring every result at the profiling boundary and publish cumulative reports under one invocation ID. Include the elapsed time of the outer call. The Scala panel and Python inspector now collect every report for a command and keep the one with the most samples, then prefer a successful outcome and the greatest outer elapsed time. Mark discarded Python reports as `superseded`. Timing reports use a versioned format. Version 2 now includes the outer elapsed time, while readers continue to accept older version 2 reports that do not contain it. Signed-off-by: Hanno Becker <[email protected]>
Fine-grained timing assigns samples to named Isabelle proofs by parsing the source text. A proof can open a nested `subgoal` block, whose `by` or `done` terminator belongs to that block rather than to the enclosing proof. The parser treated that terminator as the end of the outer proof, leaving a phantom block that could consume the next lemma. Track structured proof blocks and `subgoal` blocks separately. A nested `qed` closes both blocks, while a top-level `qed` ends the named proof. Also recognise `.`, `..`, and `\<proof>` as short proof terminators. Partition `global_interpretation` and `subclass` as goal-opening commands, alongside the other commands already recognised by the source parser. Signed-off-by: Hanno Becker <[email protected]>
The I/R tools read compressed PIDE markup exports to reconstruct source locations and fine-grained timing data. The Python zstandard decoder limited decompressed output to 50 MiB, although large exports can exceed that size and their frame headers often omit the decompressed size. Use an incremental decoder without a fixed output limit and require its end-of-frame marker. Distinguish an unavailable decoder from a corrupt or incomplete frame. Continue processing healthy fine-timing exports when one export is corrupt, and report skipped exports in text and JSON output. A missing decoder still aborts decoding because it affects every compressed export. Report `/timings` failures without terminating the I/R server, and let `/source-map` continue without timing annotations. The Python zstandard path was not exercised with the real module because it is not installed in this environment. Tests cover its end-of-file contract with a stand-in and exercise the command-line fallback classification. Signed-off-by: Hanno Becker <[email protected]>
The AutoCorrode build prepares Isabelle components such as `Word_Lib` and the fine-grained timing panel. Those components may already be registered by the Isabelle installation, by the user, or by another checkout. Registering the local paths unconditionally can add duplicate entries, and installing the timing panel should not modify the registry. Read the installation and user component registries before each build. Reuse a registered path with the requested basename, and register the local candidate only when no such entry exists. Keep panel installation limited to copying the JAR and remove its unused registration target. Signed-off-by: Hanno Becker <[email protected]>
Sibling theories can register the same locality dispatcher independently. Their per-theory dispatcher names and aliases can therefore differ even though the dispatch key identifies one dispatcher family. Merging the inventories must not reject that valid import. Merge `locality_dispatcher_inventory_entry` values by dispatch key and choose the lexicographically canonical source name and alias. Add boundary checks and a sibling-theory import regression. The dispatch-key table remains the identity of a dispatcher family. Signed-off-by: Hanno Becker <[email protected]>
Reports may mix warnings, nested children, and timing data. Invocations may be reported again after raising. The decoder and heap inspector previously lost that outcome. Decode entry children; preserve malformed and unsupported counts. Carry `raised` through model, text, and JSON. Rank snapshots by samples, then raised outcome, success, and timing. Add tests for mixed children, raised snapshots, and inspection output. Signed-off-by: Hanno Becker <[email protected]>
`micro_rust_record` derives updater, lens, and focus facts for every datatype-record field. The old generator repeatedly resolved field metadata, parsed generated propositions, and opened Isar proof transactions for each equation. Wide records therefore serialized a large amount of repeated preparation. Prepare one typed descriptor and carry constants, definitions, and theorems through the complete generator. Construct update propositions as terms, prove independent equations with `Goal.prove_future`, and consolidate them before registering facts in field order. Define lens and focus constants through `Local_Theory.define`. Keep `micro_rust_record` syntax, generated theorem names and attributes, field registration, localizable instances, and the existing HOL-record path unchanged. This does not alter Isabelle's datatype-record generator. For a synthetic 30-field record, the micro-generation phase fell from 9.447s to 2.405s. Add compatibility checks to `Micro_Rust_Shallow_Embedding_Tests`, including a polymorphic record and a `[no_fields]` record. They check the lens and focus constant types, selected update propositions, the attribute collections each generated fact lands in, field registration, and localizable instances. Signed-off-by: Hanno Becker <[email protected]>
A profiled method can raise while its sequence is being pulled. The exception previously escaped before invocation timing was accumulated or its PIDE snapshot was emitted, so samples gathered before the failure were lost. Capture the pull result, add its elapsed time to the invocation total, emit a failed snapshot for an exception, and re-raise the original exception. Successful pulls retain their existing result and backtracking behavior. Signed-off-by: Hanno Becker <[email protected]>
A helper used by a locality lemma can have registrations at more than one record position. If those registrations have different effects, certificate selection raises instead of reaching the definition-unfolding fallback. Treat only `Locality_Registry_Ambiguity` as an uncovered helper and let the normal discharge unfold it. Interrupts and unrelated exceptions still escape, and unambiguous registrations continue to use their certificates. Signed-off-by: Hanno Becker <[email protected]>
An invocation can yield, then raise while its caller backtracks. With equal sample counts, the panel kept the earlier success and hid the later failure and its longer timing. Record raised pulls in PIDE reports and carry that outcome through panel decoding and snapshot selection. Prefer raised over success for equal samples, while retaining success-wins behavior for ordinary failed-then-successful reports. Signed-off-by: Hanno Becker <[email protected]>
The Calls view grouped methods by nested sample aggregates, while its invocation rows showed outer timing. Calls without nested samples showed zero count and time, and slow calls could sort below faster calls. Aggregate Calls groups from outer timings. Count only timed invocations, retain timing ranges and histogram buckets, and leave the nested-sample Aggregate view unchanged. Signed-off-by: Hanno Becker <[email protected]>
A component file can retain a path from a deleted worktree. The old basename fallback treated it as live, so a new checkout skipped registration and later failed to find the component. Filter component-file entries by directory existence before applying the basename fallback. Exact path matches and registration of existing candidates remain unchanged. Signed-off-by: Hanno Becker <[email protected]>
A simplifier callback must decline when registry lookup finds incompatible registrations. Re-raising `Locality_Registry_Ambiguity` from a simproc aborts simp and auto goals even though no safe cancellation was available. Catch that exception in the entry, compatibility, and dispatch wrappers and return `NONE`, while explicit inference and interrupts retain their existing behavior. Add a plain Isabelle record regression for baked helper unfolding. Signed-off-by: Hanno Becker <[email protected]>
`context NAME begin` always prints the target it opens. `Toplevel.begin_main_target` calls `Local_Theory.pretty` every time, and no option turns this off. For a locale, `Locale.pretty_locale` runs `Locale.init` again and re-activates every locale element just to build the text. For a large locale that a development opens many times, building this printout can cost as much as opening the locale, and the text is rarely read. Add `quiet_context` as `Misc/Quiet_Context.thy`. `quiet_context NAME begin` and `quiet_context NAME opening BUNDLES begin` accept exactly the named forms of `context`. They build the local theory with the same call, `Target_Context.context_begin_named_cmd`, and enter it through `Toplevel.generic_theory`. This leaves the same toplevel node and presentation context and skips only the print. `end` closes the block as before. The keyword has kind `thy_decl_block`, the kind of `context`. The anonymous form `context fixes ... begin` is not covered. It goes through `begin_nested_target`, which never prints. Signed-off-by: Hanno Becker <[email protected]>
AutoCorrode's separation assertions mostly described exact resource ownership, but pure assertions and assertion lifting introduced imprecision. Additionally, the WP connective was defined to be closed under ucincl, allowing program proofs to ignore surplus resources. Make pure assertions precise, preserve exactness when lifting assertions, and remove ucincl from weakest preconditions. All resources must now be explicitly accounted for, instead of being silently discarded through upward closure in the WP semantics. can_alloc_reference remains one of the few intentionally ucincl resources so that it can absorb stack-allocated references. Extend crush and seplog to automate reasoning in this exact-resource model. Cancelling a ucincl resource now leaves UNIV in the goal, where it can absorb resources left unmatched by cancellation. Client proofs mostly stay structurally unchanged and only need ucincl-specific steps removed, such as `ucincl_auto` on contracts. A smaller number need adjusting where a residual UNIV conjunct now remains visible in the postcondition. Signed-off-by: Ike Mulder <[email protected]>
Crush leaves order and linear-arithmetic side conditions such as `n ≤ 6 ⟹ 0 < n ⟹ n - Suc 0 < 6` to its late clarsimp branches. Those run the simplifier on the whole goal, every premise included, and a Crush goal typically carries many premises unrelated to the bound. Add an `order` branch between `safe_tac` and `clarsimp_filtered`. It runs only when the conclusion or a top-level premise is `False` or a possibly negated `<` or `<=`; premises such as `∀i<n. P i` do not count. It then keeps only those premises and disequalities `a ≠ b`, reduces a non-order conclusion to `False` by `FalseE`, and must close the goal with `HOL_Order_Tac.tac` or `Lin_Arith.simple_tac`, under `SOLVED'`. It never instantiates schematics by `refl`, unlike the solvers of HOL's simpset. The retained shapes are `n ≤ 6 ⟹ 0 < n ⟹ n - Suc 0 < 6`, dead case-split branches such as `a < b ⟹ b ≤ a ⟹ P`, and `a ≠ b ⟹ ¬ a < b ⟹ b < a`. `crush_base_order`, `crush_base_order_premises`, `crush_base_order_disequality` and `crush_base_order_arith` cover these shapes; ML checks reject `True ⟹ True`, `x = x` and `∀i<n. P i ⟹ P 0`. Signed-off-by: Hanno Becker <[email protected]>
Migrate client contracts and proofs from the absorbing `apure` to resource-precise pure assertions. Use `emp` for exact triples and make residual ownership explicit where a contract deliberately forgets it. Define `apure` as the compatibility abbreviation `UNIV ⋆ ⟨P⟩` and remove its duplicate lemmas and automation. Pure reasoning now follows the precise assertion path throughout the logic and its clients. Preserve Crush scheduling: spatial drules run before a generated pure entailment becomes a HOL goal. Keep that obligation opaque until the late introduction phase, and retain the former falsehood behavior through the existing hoisting and simplification paths. Adapt dependent proofs to the unified automation. Signed-off-by: Hanno Becker <[email protected]>
Crush cancels a matching pair of separating conjuncts in `aentails_cancel_core_tac` in three steps: float the pair to the front, insert ⊤ after the selected right-hand factor (`aentails_insert_top_tac`), then close the entailment with `aentails_refl`/`asepconj_mono`/`asepconj_mono5` or the discard rule. The insertion is only sound for an upwards-closed factor, so it resolves with `aentails_insert_top_after_ucincl` and proves the resulting `ucincl ψ` with `ucincl_must_discharge_tac`. That discharge keeps every closure proof `ucincl_solve_tac` finds (`SOLVED'`, no `DETERM`). All of them leave the same remaining entailment. When the closing step then fails, the search backtracks into the closure search, takes the next proof and fails again on the identical goal, until the closure search is exhausted. For example, on a goal with 26 left-hand and 12 right-hand factors whose only candidate pair is `can_alloc_reference`, the first closure proof takes 8 ms but the whole failing cancellation takes 6.2 s. With the insertion committed to its first result, the same failing attempt takes 0.76 s. Wrap the insertion in `DETERM`. The rule's conclusion `φ ⟶ ψ ⋆ ξ` unifies with the floated goal in exactly one way, so the only results cut off are further proofs of the same `ucincl ψ`. Signed-off-by: Hanno Becker <[email protected]>
Proofs about machine words often need a word bound such as `x < y` turned into a bound on `unat x` before linear arithmetic can use it. `Crush_Arith.ltac` did this as an explicit branch modifier: it repeatedly simplified, substituted, ran full linear arithmetic and clarsimp, then retried with the full premise context. Extend the default Crush order branch with the two conversions such proofs need: `unat_mono` and `unat_ucast_lt`. Derive them only from filtered order facts, simplify each result once, and retain the existing `SOLVED'` guard so a failed attempt leaves the goal unchanged. Delete `arith.ML` and with it `Crush_Arith`, including `ltac`, `ltac_core` and `ltac_full`. Nothing in this repository uses them; proofs elsewhere that add `ltac` as a branch need to drop it. Signed-off-by: Hanno Becker <[email protected]>
Resolved rule instances can leave sort hypotheses on a Crush proof state after their terms disappear. The late simp and clarsimp branches then carry those hypotheses through every simplifier invocation. In one representative proof state, stripping reduced 18 sorts to two and cut the same simplifier call from 10.093 s to 6.111 s. Strip sort hypotheses at entry to the normal, filtered, and fallback clarsimp branches. Place normalization outside each branch body so its CHANGED_PROP checks compare against the normalized input. This keeps stripping from becoming a successful Crush step and leaves REPEAT_SMART and strict CHANGED branches unchanged. Signed-off-by: Hanno Becker <[email protected]>
Crush's scheduler `REPEAT_SMART` runs big steps: `DWELL` repeats a step on the first goal until the number of goals drops or the step fails. When the step fails, `REPEAT_SMART` puts that goal back at the front of the worklist, and the next iteration runs every branch again on the same state, failing again. Every goal that Crush gets stuck on therefore paid for its whole failing branch cascade twice. A big step that returns at least as many goals as it started with has stopped because its last step failed on the first goal of its result. When that goal heads the new worklist, go on right away as after a failure on it, with the rest of the worklist, instead of running the step on it again. The failure handling is factored out of `run_smart` for this: in aggressive mode (`crush`) the next item follows; otherwise (`fastcrush`) Crush stops, or keeps only the goals that share a schematic variable with the failed one. Only the repeat of a deterministic failure is skipped, so every Crush call returns the same result. With `crush_prioritize_changed_goals`, changed goals precede the failed goal in the new worklist; they run first as before, and the goal is then tried again. Signed-off-by: Hanno Becker <[email protected]>
A guard `GUARD x P` keeps `P` out of unification until `x` is no longer schematic; `crush_step_tac_frame` updates the guards before every step. A goal whose conclusion is such a pending guard cannot be closed: assumption, intro rules and dedicated branches all fail to see through the wrapper. Crush still runs every branch on it, the `clarsimp` variants included, before the worklist moves on. The most those branches can do is incidental clean-up of the goal's premises. This commit makes the frame fail the step at once on such a goal, right after the guard update. `REPEAT_SMART` then moves on and re-queues the goal once it changes; when the guarded schematic is fixed, the update drops the guard and the goal is processed as before. The check is `Crush_Guards.has_pending_guard_conclusion`, which uses the same "schematic head" test as the guard update itself. The frame is shared by `crush_base` and by tactics built on it. Proofs that never leave a guarded goal at the top level are unaffected. Signed-off-by: Hanno Becker <[email protected]>
`clarsimp_filtered` runs clarsimp with the premises that MePo deems irrelevant wrapped in `IGNORE`, and the next branch, `clarsimp_fallback`, runs unfiltered clarsimp when that fails. On a goal with at most `crush_relevance_filter_max_facts` premises, or one where MePo keeps every premise, the filter hides nothing: the filtered call already was the unfiltered one, and the fallback repeats it on the same goal and fails again. When `clarsimp_filtered` is enabled, let the fallback return no result for a goal of which MePo ignores no premise. To keep that check cheap, `MePo_Core.relevant_prems_in_goal` counts the premises before constifying the goal, with the same result as before. The fallback after a filtered call that did hide premises, and theories without filtered clarsimp, are unchanged. Signed-off-by: Hanno Becker <[email protected]>
`clarsimp_filtered` hides the premises that MePo deems irrelevant. MePo ranks premises by the constants they share with the conclusion and with premises it has already accepted, so a conclusion without any constant, typically `False`, relates to no premise, and the filtered call ran with every premise hidden. Such calls fail, including on goals that unfiltered clarsimp changes or closes, and the fallback then redoes each of them. Let `clarsimp_filtered` hide nothing when the conclusion has no constant; the call then is the unfiltered one, and the fallback is skipped as a repeat. `MePo_Core.conclusion_has_constants` decides this, counting parameters and free variables as MePo does. MePo's own ranking is unchanged, because `urust_determine_branch` relies on it differently: its conclusion is the condition of an `if`, and when that condition has become `True` or `False`, dropping every premise decides the arm at once. Putting the rule into `MePo_Core.relevant_prems` instead would make those calls keep all premises and slow them down considerably. Signed-off-by: Hanno Becker <[email protected]>
An operation with `d` unaffected record fields exports `d` disjoint-projection theorems. `derive_disjointness` built the same `d`-field no-op update telescope for every projection, causing roughly `d * d` update crossings although the exported result is linear. Refresh only the selected field for each projection and apply the matching commutativity theorem. Check that the theorem and field lists remain aligned, and extend the wide-record test to require 20 core, 20 disjointness, and one local-action theorem. Keep the command syntax, interactive core proof, generated theorem names and statements, attributes, continuation order, registry entry, and failure handling unchanged. Signed-off-by: Hanno Becker <[email protected]>
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
2 participants
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.
This PR improves AutoLocality and Crush performance by reducing redundant proof work, refining tactic scheduling, and deriving disjoint projections linearly. It also strengthens registration handling and regression coverage.
It adds fine-grained timing diagnostics and makes weakest preconditions resource-exact, with canonical handling of pure assertions.