---
title: "algorithm-sieve — Mova code model"
description: "Mova code model of algorithms/src/sieve/mod.rs: components with their labels, obernants and the model text."
url: "https://groupants.elamur.ai/free/en/mova/algorithms/src/sieve/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: <https://groupants.elamur.ai/free/en/mova/algorithms/src/sieve/mod.rs.groupant/>

# algorithm-sieve

The groupant beside algorithms/src/sieve/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 source derived instance
- **source:** [`algorithms/src/sieve/mod.rs`](https://github.com/ElamurAI/mova-free/blob/main/algorithms/src/sieve/mod.rs)
- **source SHA-256:** `48cc204f2b076553…`
- **repository folder:** [`algorithms/src/sieve/mod.rs.groupant`](https://github.com/ElamurAI/mova-free/tree/main/algorithms/src/sieve/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** | bounded checked | [Forward](#forward) |
| **ast** | partial | `syntax.json` |
| **cost** | symbolic unmeasured | [Cost](#cost) |
| **descriptant** | present | [descriptant](#descriptant) |
| **invariant** | source derived | [Invariant](#invariant) |
| **tests** | bounded executed | [evidence](#evidence) |

## 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 |
|---|---|---|---|
| `nonbehavior` | behavior_complement | partial source derived | [nonbehavior](#nonbehavior) |
| `prime_prefix_fibers` | reverse_reconstruction | partial source derived | [prime_prefix_fibers](#prime-prefix-fibers) |
| `prefix_relation` | metamorphic_relation | partial source derived | [prefix_relation](#prefix-relation) |
| `square_boundary` | boundary_specialization | partial source derived | [square_boundary](#square-boundary) |
| `resource_boundary` | resource_observation | partial source derived | [resource_boundary](#resource-boundary) |
| `factor_witness` | certificate_relation | partial source derived | [factor_witness](#factor-witness) |
| `gap_interval_converse` | reverse_reconstruction | partial source derived | [gap_interval_converse](#gap-interval-converse) |
| `typed_storage_traces` | resource_observation | partial source derived | [typed_storage_traces](#typed-storage-traces) |

## Model text


### descriptant

#### algorithm-sieve descriptant

2026-10-30: For n<2 return an empty vector. Otherwise check n+1 and byte-storage representability. On successful fallible reservations, return exactly the increasing primes <=n by Eratosthenes marking from p squared. SizeOverflow denotes checked count/byte capacity failure; AllocationFailed denotes a reported try_reserve_exact error. Output reservation is fallible as well as flags reservation.

The combiner relates source-bound partial syntax, forward recurrence, typed output-preimage and behavior-exclusion relations, invariants and finite observations. It preserves disagreement as an open obligation; structural consistency does not prove Rust semantics.

Primality is tested independently by trial division over every divisor 2..value, without a sieve or square-root stopping rule. Prefix tests check order and inclusivity. Capacity tests reject before any huge allocation request.

Prospective guarded inclusive marking and fully fallible storage model survived bounded checks. Replacing composite clearing flags[multiple]=0 by flags[multiple]=1 compiled and tests::inclusive_trial_divisor_oracle rejected it (one failure). A strict-clippy diagnostic changed the trial divisor spelling to is_multiple_of without changing the oracle. Real allocator exhaustion remains unforced.

##### Relation epoch, 2026-10-30

The combiner now separates full mathematical certificate/preimage relations from implementation selection and machine-resource premises. Implementation families contain eight typed relations; test families retain five with strengthened executed correspondence. Three targeted tests augment each prior suite, preserving earlier useful boundary observations. Finite tests and source projections leave general Rust semantics and allocator exhaustion unproved.

### model

## algorithm-sieve

### Forward

For n<2 return an empty vector. Otherwise check n+1 and byte-storage representability. On successful fallible reservations, return exactly the increasing primes <=n by Eratosthenes marking from p squared. SizeOverflow denotes checked count/byte capacity failure; AllocationFailed denotes a reported try_reserve_exact error. Output reservation is fallible as well as flags reservation.

### Invariant

Flags 0 and 1 are cleared. Before processing p, all composites having a prime factor <p have been cleared; clearing multiples of p from p squared preserves all primes and eventually removes every composite. p<=n/p implies p*p<=n without multiplication overflow. Increment occurs only when n-multiple>=p, so multiple+p<=n. Checked count*size_of(T)<=isize::MAX precedes reservation. The reserve helper is private and called on empty vectors; resize and output pushes stay within reserved capacities.

### Cost

O(n log log n) marking time plus O(n) initialization/count/output scan for n>=3; O(n) auxiliary flags plus O(pi(n)) output words. Symbolic cost; no timing claim.

### nonbehavior

In U of limits, allocator traces and candidate results, U minus R includes successful vectors with composites, omissions, duplicates, descending order or values above n; success after deterministic size rejection; and typed allocation failure without a reported reserve failure. Abort/nontermination is outside the modeled terminating Result universe.

### prime_prefix_fibers

A successful vector P admits all representable limits n for which P is exactly the inclusive prime prefix and allocation succeeds. Empty P admits n=0,1. For a nonempty prime prefix ending at p, limits range from p through one below the next prime, intersected with capacity constraints. Error observations retain size-rejection or allocator-failure antecedents; AllocationFailed does not identify a unique limit.

### prefix_relation

For successful calls with m<=n, sieve(m) is sieve(n) restricted to entries <=m. Resource success at one size does not imply success at another under arbitrary allocator state.

### square_boundary

For prime p with representable p*p, p*p is composite and omitted, whereas p itself is retained. The p<=n/p guard includes equality.

### resource_boundary

n=usize::MAX fails checked addition; n=isize::MAX fails byte capacity for n+1 before reservation. Output usize capacity multiplication and isize bound are checked separately. Real OOM is not forced; allocator failure mapping is source reviewed, process-level aborts excluded.

### Limits

Exact implementation; mathematical models are not formal proofs. Partial syntax does not expand macros or resolve types. No numerical approximation profile or unsupported error budget is introduced.

### factor_witness

For any successfully returned prime prefix at n and each composite v in [2,n], a least divisor d>1 is prime, d<=v/d, and d occurs in the prefix while v does not. Conversely a proper factor 1<d<v with d dividing v certifies exclusion. Values 0 and 1 have separate nonprime reasons; absence alone at a limit smaller than v does not certify compositeness.

### gap_interval_converse

Let P be a complete increasing prime prefix ending at p and q its next prime. A successful sieve(n)=P iff p<=n<q, intersected with size representability and successful reservations. This requires prefix completeness: an arbitrary sorted list of primes ending at p need not have any antecedent. Empty P admits exactly n=0,1. At machine boundaries express next prime mathematically and intersect with usize; allocator traces remain part of the antecedent.

### typed_storage_traces

For n>=2 deterministic gates require n+1<=isize::MAX for u8 flags and pi(n)*size_of(usize)<=isize::MAX for output; arithmetic multiplication/addition must be representable. Passing gates is not a success guarantee: either try_reserve_exact may report AllocationFailed. SizeOverflow and AllocationFailed are distinct observations; a reported allocation error does not reconstruct the failing reservation or n uniquely. The private reserve helper checks count bytes before allocation and preserves an existing vector on deterministic rejection; its production callers start empty.

### evidence

#### Evidence — 2026-10-30

Source SHA-256: 48cc204f2b0765533fa30718cdbf94874b9c5d37b3893da6b738316ec897c2d6.

Three tests in this algorithm pass in debug and release. The worktree crate passes 103 unit tests plus one doctest in both modes; strict all-target clippy with -D warnings passes. 385 independent prime-prefix cases for limits 0..=384, explicit 2/3/49 boundaries, a 4,096 limit fixture with 564 primes, 12 prefix checks, and deterministic impossible-capacity rejection.

Primality is tested independently by trial division over every divisor 2..value, without a sieve or square-root stopping rule. Prefix tests check order and inclusivity. Capacity tests reject before any huge allocation request.

Replacing composite clearing flags[multiple]=0 by flags[multiple]=1 compiled and tests::inclusive_trial_divisor_oracle rejected it (one failure). The mutation is applied to copied production source and compiled with rustc --test, not emulated by a different implementation. Logs and the Rust harness are external under MOVA_DATA/runs/octopus-alg3-number-2026-10-30. No huge allocation or actual OOM probe was performed.

No throughput measurement, semantic AST proof, full-system inference, or executable approximation claim is made. Root integration separately registers these leaves and checks parent bindings.

##### Relation epoch, 2026-10-30

Current source SHA-256: 48cc204f2b0765533fa30718cdbf94874b9c5d37b3893da6b738316ec897c2d6. Six tests in this module pass twice in debug and twice in release; single-thread result records match within each mode. Strict all-target Clippy passes. A copied production-source mutant compiles and is rejected by a newly added relation test. Partial syntax regenerated twice with identical bytes. External logs and Rust runner: MOVA_DATA/runs/octopus-next-number-2026-10-30. Earlier evidence above remains historical; no timing or universal semantic claim follows.

Current reproducible evidence SHA-256 bindings:

- sieve-debug-records.txt: 17da698fa4e55f12876c5a49993a04d3749a522a71ca62c37ce458919dd30b7d
- sieve-release-records.txt: 17da698fa4e55f12876c5a49993a04d3749a522a71ca62c37ce458919dd30b7d
- sieve-mutant-build.log: e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855
- sieve-mutant-rejected.log: e37aa094e9dc0a1e33e997dcd947eb298de3966ec0d64ac1b7bf873653367c00

### prospective

#### Prospective model — 2026-10-30

Before implementation: specialize the existing math/src/nt.rs sieve to usize without narrowing, checking limit+1 and all allocation capacities. A byte flag represents each inclusive candidate. Mark multiples beginning at p squared only while p<=limit/p, with subtraction guarding increment. After primes up to p are processed, no multiple of those primes remains flagged. Reserve exact output capacity after counting flags. Expected O(n log log n) time and O(n) space, including linear output scan. Allocation failure is a typed Result, subject to the allocator's try_reserve contract. Probe arithmetic capacity rejection without requesting enormous memory; ordinary OOM is not forced.