--- title: "algorithm-heap-sort — Mova code model" description: "Mova code model of algorithms/src/heap_sort/mod.rs: components with their labels, obernants and the model text." url: "https://groupants.elamur.ai/free/en/mova/algorithms/src/heap_sort/mod.rs.groupant/" --- Elamur: [Mova](https://md.mova.elamur.ai/free/en/) · [Dictionary](https://md.dictionary.elamur.ai/free/en/) · [Research](https://md.research.elamur.ai/free/en/) · **Groupants** This page as HTML: # algorithm-heap-sort The groupant beside algorithms/src/heap_sort/mod.rs in the Mova repository: what the code computes, what it never does, how to go back from its outputs, its invariants, cost and checks. ## Facts - **kind:** groupant - **status:** partial descriptive instance - **source:** [`algorithms/src/heap_sort/mod.rs`](https://github.com/ElamurAI/mova-free/blob/main/algorithms/src/heap_sort/mod.rs) - **source SHA-256:** `a8fd695ce2150dee…` - **repository folder:** [`algorithms/src/heap_sort/mod.rs.groupant`](https://github.com/ElamurAI/mova-free/tree/main/algorithms/src/heap_sort/mod.rs.groupant) - **repository commit:** `855da7bd4a7b` > **Implementation material.** A Mova code model describes this code at one source revision: partial models, finite checks and their stated scope. It is not a reviewed general exposition, and its labels are shown as written, never raised. ## Components | component | label | where | |---|---|---| | **approximant** | partial | [approximant](#approximant) | | **ast** | partial | `syntax.json` | | **descriptant** | present | [descriptant](#descriptant) | | **invariant** | partial | [approximant](#approximant) | | **tests** | existing checks referenced | [checks](#checks) | ## Obernants The typed relations around the forward model: the behaviour complement (what the code never does), the reverse reconstruction (every input compatible with an output) and specialised views. | id | type | label | where | |---|---|---|---| | `behavior_complement` | behavior_complement | partial source derived model | [behavior_complement](#behavior-complement) | | `reverse_reconstruction` | reverse_reconstruction | partial source derived model | [reverse_reconstruction](#reverse-reconstruction) | | `suffix_extraction` | suffix_extraction | partial source derived model | [suffix_extraction](#suffix-extraction) | | `order_equivariance` | order_equivariance | partial source derived model | [order_equivariance](#order-equivariance) | | `resource_bound` | resource_bound | partial source derived model | [resource_bound](#resource-bound) | ## Model text Migration: consolidated into model.md, 2026-11-04, operator decision; fresh hash-bound references to the former files were rebound to the sections below. ### descriptant #### heap_sort mod groupant Epoch 2026-10-29: prospective predictions saved outside repository before implementation. Original std-only code/fixtures; four algorithm tests pass twice. Compiled red control: choose smaller child instead of larger child. Combiner: source identity, recurrence, invariant and checks constrain a conditional model. Complement and converse answer different questions; no additive inverse identity. Syntax is partial with opaque macros and no type or name resolution. Finite evidence is not proof of all inputs or parent wiring. Lawful Ord and successful execution are assumed; trait panics and allocation failures are outside successful-call semantics. Preserve these observations in future epochs. No runtime speedup claim. ### approximant #### Forward, invariant and cost Build max heap bottom-up, swap root with shrinking suffix endpoint, then sift down. Invariant: Active prefix is a max heap; finalized suffix is sorted and dominates prefix. Cost: O(n log n) time, O(1) auxiliary space; lawful Ord and constant comparison/swap assumed. ### models ## Heap-sort typed models Subject/revision: mod.rs at manifest SHA. Observe one normally terminating call under lawful stable Ord. Models are partial source-derived specifications. Trait panics and process/resource failures are outside successful-call semantics. ### behavior_complement U consists of input/output slice pairs. The absent-outcome model includes every output not ascending or with a different element multiset. This is an exact specification complement on values with equality consistent with Ord. Equal-key identity order is unrestricted. The larger-child-choice mutant is rejected by exhaustive_bucket_oracle; bounded tests are not universal proof. ### reverse_reconstruction For sorted y, compatible inputs include every permutation of its values. With distinct values this is the exact sorting preimage; equal-key identities retain ambiguity rather than a stability promise. Original order is not uniquely recoverable. Bucket tests check the multiset projection, not full inverse search. ### suffix_extraction Type: phase_invariant. After k extractions, the final k cells are ascending and at least every active-prefix cell. Swap the max root into the next suffix cell, then restore the prefix heap. This source-derived internal phase model is not directly instrumented by output-only tests. ### order_equivariance Type: order_isomorphism. An injective order-preserving map f satisfies sort(f(x))=f(sort(x)) at value level. Reverse ordering changes the relation and sorts numeric values descending. A custom non-Clone Reverse wrapper is an executed changed-order witness. Arbitrary relabelings need not preserve order. ### resource_bound Type: resource_model. Bottom-up building O(n), n extractions each O(log n), total O(n log n) comparisons/swaps and O(1) auxiliary storage. root