📐assessment-contract

The groupant beside tools/enrich/src/assessment.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

Components

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.

Model text

descriptant

Assessment groupant

The approximant describes contract construction, report binding, four-grade comparison, invariants and cost. Typed models cover absent score-policy transitions, compatible score histories and minimal threshold repairs.

Scope is a projection of trusted reports and their comparison. The source hash in manifest.json binds the reviewed code. Detailed row checks do not authenticate a malicious report; hash collision resistance and grader trust are assumptions. A source-bound partial Rust syntax projection is materialized; macros and semantic analysis remain absent.

Evidence that changed the model

An isolated earlier composition probe accepted a foreign 7/12 baseline for a different 9/12 assessment and reported a false gain of two. Correct same-question comparison was 9/12 to 9/12. The identity-binding implementation rejects that foreign baseline. No production model was promoted in the probe.

Existing Lean binding/comparison laws and the 256-row table cover the declared mathematical projection; Rust tests check correspondence and 64 binding-guard assignments. Tests state the scope. Score feasibility does not prove that training can attain a particular improvement.

The specialized catalog expands this family to 20 models. Each record identifies its observation, relation, assumptions and check. Proposed checks remain distinguishable from evidence already obtained.

Executable catalog epoch (2026-10-29)

Five bounded production-correspondence tests now exercise twelve catalog relations: row-count, score-fiber, choice-fiber, flag-complement, aggregate-complement, integer-edge, first-error, extra-fields, row-order, option-labels, empty-input and teaching-input. The literal accepted set for a test/exam fixture distinguishes duplicate option positions from observable labels. Rejection mutations share the same production entrypoints as accepted cases. First-error evidence is limited to eight chosen guards; signed-boundary grades are private comparator fixtures. See case counts and limits. No production semantics changed.

Four-corner refinement epoch (2026-10-30)

Preserved the 20-model family and strengthened its shared relation in four-corner.md. Closed-form output preimage counts cover 1566 publicly bound score quadruples with unequal denominators. Separate identity, renaming and source/review checks expose the difference between report consistency and authentic execution. Their negative controls include foreign assessment corners, a noninjective label map and a compiled strict-old-tie mutation. All 11 focused tests pass after restoration; repeated release outcome lines match. Evidence records exact limits and hashes.

Corrected an overclaim in the forward description: only new scores undergo signed conversion, while old scores compare as unsigned. Same learner IDs do not guarantee same actual execution, and a fingerprint does not authenticate review approval. No production behavior or public API changed. The new syntax projection is partial; no semantic AST or full system proof is claimed.

approximant

Assessment binding and comparison approximant

Subject: assessment.rs; source hash in manifest.json. State: question-only lesson contract, expected learner identity, JSON report. Construction requires no explanation/facts/exercises and at least one test or exam. Rows follow tests then exams, preserving each within-kind index.

Binding is a conjunction: nonempty matching learner id; matching assessment fingerprint; zero lesson reads/updates; array rows and unsigned score/count; equal expected/reported cardinalities; score <= total; matching kind/index/ question/gold per row; chosen answer in the options; correct flag equivalent to choice=gold; recomputed row score equals aggregate. Success retains learner, assessment, total and score; detailed rows are projected away.

Comparison requires each new/old before-after pair to share its assessment and count, and both new/old pairs to share the same before/after learner identities. It returns gain=after-before, preserved=(old_after>=old_before), and recommend=(gain>0 and preserved). Only the two new scores must convert to signed 64-bit; old scores stay unsigned. No graded report is authenticated solely by these consistency checks.

Invariants: question identity preserved within each comparison pair; no claimed learning reads/updates; aggregate matches rows. These are report checks, not independent proof of what an untrusted process actually did.

Cost: construction/hash O(scored bytes), binding O(report bytes + option-string comparisons), four-grade comparison O(identity string lengths), plus constant integer arithmetic. Calling comparison O(1) assumes bounded identity lengths. Memory: contract holds cloned question/gold/options. No measured throughput or SHA injectivity proof follows from this cost model.

See four-corner refinement for the success relation, first behavior complement, second full-output preimages, denominator constraints, identity transformations and bounded production-oracle evidence.

catalog

Specialized obernant catalog

Subject/source hash: manifest.json. Each model is a partial source-derived relation on its stated observation. Normal execution and pinned dependencies are shared assumptions. Checks are proposed oracles unless existing evidence is explicitly cited. Related specializations need not be independent.

row-count

Type: cardinality_preimage. Status: partial_source_derived_model.

Domain and relation: Successful binding requires reported array length L=total T=expected N and 0<=right<=N. Every successful tuple violating that conjunction is excluded.

Assumptions and check: JSON numeric extraction and N>0 assumed. The catalog extension/mutation test rejects missing rows, total mismatch and out-of-range score on a two-row contract.

score-fiber

Type: score_partition. Status: partial_source_derived_model.

Domain and relation: For Boolean correctness vectors, B(r)={c | sum(c)=r}, with binomial(N,r) members before option constraints.

Assumptions and check: Intersect with attainable row outcomes; binomial count assumes both outcomes per position. The catalog choice/score test enumerates 576 reports, finding exactly four accepted outcomes and score-fiber sizes [1,2,1].

choice-fiber

Type: choice_preimage. Status: partial_source_derived_model.

Domain and relation: For gold g and option strings O, B(correct=true)={g}; B(false)=set(O) minus {g}. Duplicated strings collapse under this observation.

Assumptions and check: Only valid row choices. The catalog choice/score test checks both distinct labels and an outside label per row, including duplicate gold and wrong labels in the contract.

flag-complement

Type: flag_consistency_complement. Status: partial_source_derived_model.

Domain and relation: A successful tuple with correct!=(choice==gold) belongs to the absent-behavior model, including incompatible JSON value types.

Assumptions and check: Earlier row/choice guards pass. The catalog choice/score test enumerates Boolean and incompatible flags; the extension test also flips only a valid report's flag.

aggregate-complement

Type: aggregate_consistency_complement. Status: partial_source_derived_model.

Domain and relation: Successful binding excludes right != sum_i[choice_i=gold_i]. The constraint concerns row consistency, not answer semantics.

Assumptions and check: Earlier guards pass. The catalog choice/score test enumerates all declared scores 0..3 for two rows, rejecting every contradictory aggregate.

hash-fiber

Type: identity_equivalence. Status: partial_source_derived_model.

Domain and relation: Equal scored lesson projections imply equal assessment hashes; the same hash does not uniquely identify the full lesson because other fields are omitted.

Assumptions and check: Cryptographic collision resistance is assumed, not proved. Existing retention identity tests vary scored and unscored fields.

learner-pair

Type: learner_pair_constraint. Status: partial_source_derived_model.

Domain and relation: For four grade IDs ordered new_before,new_after,old_before,old_after, comparison requires id0=id2 and id1=id3.

Assumptions and check: Before and after may themselves be equal. Check single-slot mutations and equal-before/after compatible fixtures.

assessment-pair

Type: assessment_pair_constraint. Status: partial_source_derived_model.

Domain and relation: Comparison requires assessment ID and total equal within each before/after pair. The new and old assessments may differ from each other.

Assumptions and check: Already bound grades; learner pairing still required. Existing mixed-pair test covers one mismatch; old-pair/total variations remain proposed.

integer-edge

Type: numeric_boundary_preimage. Status: partial_source_derived_model.

Domain and relation: A successful signed new-score difference requires both new scores<=i64::MAX; their difference is within [-i64::MAX,i64::MAX].

Assumptions and check: Old scores use unsigned comparison. The catalog signed-edge test constructs private grades for 13 boundary cases; these are comparator unit fixtures, not feasible gigantic assessment allocations.

first-error

Type: first_failure_partition. Status: partial_source_derived_model.

Domain and relation: For ordered guards g1..gk and first observable failure j, compatible antecedents satisfy all earlier guards and not gj; later guards are unconstrained.

Assumptions and check: Keep combined checks at message granularity. The catalog first-error test checks all 255 nonempty subsets of eight ordered faults, comparing the exact first message. Guards outside this selected subset remain unenumerated.

extra-fields

Type: extension_invariance. Status: partial_source_derived_model.

Domain and relation: Reports differing only in unconsulted keys have equal projection to fields read by bind, hence equal binding behavior.

Assumptions and check: No consulted value/type may be overwritten. The catalog extension test checks six JSON extension types at top and row levels, then verifies each cannot rescue a contradictory flag.

row-order

Type: row_permutation_counterfactual. Status: partial_source_derived_model.

Domain and relation: A fixed contract excludes successful permutations that mismatch kind/index/question/gold at any position, even with unchanged aggregate.

Assumptions and check: Identical observable rows may make a permutation invisible. The catalog extension/mutation test reverses distinct test/exam rows and requires rejection.

option-labels

Type: label_ambiguity. Status: partial_source_derived_model.

Domain and relation: The preimage of a chosen label includes all option positions with that string. String-only reports cannot recover an option index.

Assumptions and check: Correctness uses gold-text equality; duplicated labels are not distinct choices. The catalog choice/score test uses duplicated gold and wrong labels and compares the accepted set to four literal string outcomes.

empty-input

Type: empty_input_complement. Status: partial_source_derived_model.

Domain and relation: When both tests and exams are empty, all Ok constructor outcomes are absent.

Assumptions and check: Question-only Lesson domain. The catalog constructor test crosses four test/exam-presence cases with eight teaching-field subsets, including empty rejection.

teaching-input

Type: training_input_complement. Status: partial_source_derived_model.

Domain and relation: A nonempty explanation, facts or exercises excludes a successful contract constructor, even when questions exist.

Assumptions and check: Local contract input separation, not global leakage prevention. The catalog constructor test checks all seven nonempty teaching-field subsets against each of four question-presence cases.

decision-edge

Type: decision_boundary. Status: partial_source_derived_model.

Domain and relation: With v>=u fixed, recommendation changes at a=b+1; with a>b fixed, it changes at v=u.

Assumptions and check: Fixed feasible totals; score edits are counterfactual, not achievable training claims. Existing table contains both sides for interior0..3 values.

header-rows

Type: header_row_coupling. Status: partial_source_derived_model.

Domain and relation: Changing a report hash header to another contract permits success only if all scored row metadata also matches; header equality is insufficient.

Assumptions and check: Fully consistent forged reports may still pass. Existing foreign-assessment test retags the hash and verifies row-level rejection.

See four-corner refinement for the success relation, first behavior complement, second full-output preimages, denominator constraints, identity transformations and bounded production-oracle evidence.

tests

Checks: assessment-contract

The test code currently lives in the source's assessment::tests module. This sidecar can also hold vectors, tables, probe plans and evidence summaries.

cargo test --release -p mova-enrich --lib assessment::tests

• Forward correspondence: compare the actual score policy with the 256-case Lean table.
• Inverse binding: all 64 combinations of the six binding guards are checked.
• Simple negative cases: foreign questions, mismatched rows and inconsistent aggregates do not bind.
• Group probe: the historical false +2 comparison is rejected by finish-improve.

Current test references preserve their original scopes; their presence is not a claim of full system verification.

Checked 2026-10-29: all 16 mova-enrich library tests passed. An independent Rust probe checked all 256 table rows, counted 60 recommending and 196 nonrecommending score quadruples, and checked coordinatewise threshold repairs. This extends bounded model evidence; it is not a new universal Lean theorem.

Executable catalog correspondence (2026-10-29)

Five source-local catalog_* tests call the production constructor, binder or comparator. The finite accepted-set oracle uses literal expected report outcomes, not a second implementation of the binding guards.

• catalog_choice_and_score_preimages_match_independent_sets: 576 candidates (3 choices per row, 4 flag values per row, 4 declared scores). Exactly four bind; score fibers contain 1, 2 and 1 members. Duplicate gold and wrong labels collapse to string outcomes; outside labels, incompatible flags and wrong aggregates reject. Fixtures cross a test and an exam with independent metadata.
• catalog_unknown_fields_preserve_binding_but_consulted_mutations_reject: six extension values preserve all four bound fields; six corresponding contradictory flags still reject. Eight consulted-field mutations and one reversed-row mutation reject.
• catalog_first_error_partitions_multifault_reports: all 255 nonempty subsets of eight ordered faults return the first fault's literal error message. This covers the selected guard subsequence, not every error path.
• catalog_signed_edges_reject_unrepresentable_new_scores_only: 13 private grade fixtures cover signed extrema, adjacent scores, six overflow rejections, and unsigned regression comparisons beyond the signed range. These fixtures exercise the comparator directly; no enormous assessment is allocated.
• catalog_constructor_excludes_empty_and_teaching_inputs: all 32 combinations of test/exam presence and teaching-field presence. Three accept, 29 reject; teaching errors precede empty-question errors.

These remain bounded tests of source-derived relations. They do not establish hash injectivity, report authenticity, universal coverage or a reconstruction service. Unexercised catalog assumptions remain explicitly partial.

Mutation negative control (2026-10-29): temporarily replacing production choice == gold with choice != gold made the accepted-set test fail (exit 101), displaying four incorrect tuples against the four literal expected tuples. The mutation was restored before final checks and is not committed.

Validation (2026-10-29): the targeted release command above passed all eight assessment tests twice (five new, three existing; 13 other library tests filtered out). Test output from running 8 tests onward was byte-identical. Dependency warnings were pre-existing. No teacher calls, GPU runs or unrelated full suites were used.

Four-corner refinement evidence (2026-10-30)

Source SHA-256: c111b671217c6d3679428fe96e22e220acd88ec8f2d9922ec07fdfa7f727c1d0. Three additional source-local deep_* tests exercise the public constructor, binder and comparator with small owned fixtures. Model and counts define the finite universe and distinguish fiber cardinality from pointwise correspondence. All 11 assessment tests pass in debug, release twice, and debug again after mutation restoration. Release per-test outcome lines are identical; wall-clock durations are excluded. No teacher, network, training or assessment dataset was used.

Negative control: the compiled mutation old_after.right > old_before.right incorrectly rejects old-score ties. The new closed-form fiber test fails (exit 101), and the restored source passes all 11 tests. No mutant is retained.

Focused Clippy (--lib --tests --no-deps) passes with existing warnings outside assessment.rs; there are no diagnostics for the owned file. The initial dependency-inclusive invocation fails on pre-existing world idioms.rs modulo_one and know.rs never_loop errors; those files were not changed. Changed-file modelcheck reports the sole changed source and no missing model. Leaf validation passes; groupant inventory reports only stale source bindings in the two ancestor manifests, which the integrating owner refreshes.

Syntax was generated twice with byte-identical results. The assessment sidecar has no nested fragments requiring source-binding refresh. Full syntax SHA-256: 3594ad680310aea1f4ceaf9092019c99497ec5f2a7c7674b852717ad940e0a7a.

External evidence is under $MOVA_DATA/runs/octopus-deep-assessment-2026-10-30. Hashes identify evidence content; logs are not production authenticity proofs.

complementer

Partial complementer: assessment score policy

Status: relational specification of one projection; no reconstruction solver. Source revision: 18ecb4fc8 (assessment.rs source SHA is in manifest.json). The domain is four nonnegative scores for already bound grades with fixed assessment identities and their declared question-count bounds.

Write q = (before, after, old_before, old_after). The forward projection is

recommend(q) = (before < after) and (old_before <= old_after).

Its reverse relation is

B(true)  = {q | before < after and old_before <= old_after}.
B(false) = {q | after <= before or old_after < old_before}.

Intersect both sets with the domain's score bounds and binding constraints. These are multiple possible score histories compatible with a recommendation. For example (0,1,0,0) and (1,2,0,0) both belong to B(true), when the bounds permit them. A Boolean recommendation does not identify which occurred.

The finite Lean table enumerates the forward policy on scores 0..3. Selecting its rows by recommendation gives the exact reverse relation on that finite domain. Existing Rust correspondence checks the forward rows. It does not yet implement a reverse-query endpoint.

The binding Boolean itself has one accepting assignment (all six guards true) and 63 rejecting assignments. A rejection bit alone cannot identify which guard failed. Existing checks cover those assignments; more diagnostic output can narrow compatible failures.

This projection cannot reconstruct questions from their hashes, arbitrary report contents, or actual learning causes. Preserve the grade records, identities, source/model revisions and any observation that justifies pruning.

See complementer semantics for the general preimage relation, identity laws and approximation requirements.

See four-corner refinement for the success relation, first behavior complement, second full-output preimages, denominator constraints, identity transformations and bounded production-oracle evidence.

four-corner

Four-corner comparison refinement

Subject: current assessment.rs SHA-256 in manifest.json. This refines the existing 20 typed models; it adds no executable approximation profile or error budget. Domain: successful public construction and binding on nonempty, question-only contracts, with new total N and regression total M. All new scores fit i64; old scores remain u64. Hash collision resistance and honest report production are separate assumptions.

Write the grades as (new-before, new-after, old-before, old-after), scores (b,a,u,v), learner identities (s0,s1,s2,s3), and assessment identities (h0,h1,h2,h3). Admissibility K requires h0=h1, h2=h3, the corresponding totals equal, and s0=s2, s1=s3. Neither h0=h2 nor s0!=s1 is required. New and old denominators can differ. Total zero is outside public constructor reachability; private comparator fixtures can describe a larger domain.

First: behavior complement

For fixed compatible identities and totals let Q=[0,N]^2 x [0,M]^2 and let O=Z x Bool x Bool. In the transition universe U=Q x O, define R(q,(d,p,r)) iff a=b+d, p=[v>=u], r=[d>0 and p]. The exact abstract behavior complement is U minus R. It includes every recommendation at zero gain, every recommendation with regression, and every output gain outside [-N,N]. If identities are included in the input universe, a successful output when K is false is also absent. Errors are a separate observation: this success-only projection does not predict their ordering.

This is exact algebra for the declared projection, not a universal proof of Rust, report authenticity, or reachable learning trajectories. Public binder fixtures establish bounded observations; private unrepresentable scores do not claim huge assessments are constructible.

Second: reverse output preimages

For output o=(d,p,r), the compatible histories are all q in Q satisfying a=b+d, [v>=u]=p, and r=[d>0 and p], together with K. Infeasible r or |d|>N has the empty preimage. Otherwise its size is

(N+1-|d|) * (M+1)*(M+2)/2  when p=true
(N+1-|d|) * M*(M+1)/2      when p=false.

For recommendation alone, the true fiber size is N*(N+1)(M+1)(M+2)/4. This retains ambiguity: even a full output forgets baseline scores and individual choices, while recommendation loses gain too. Rows with no distinct wrong label restrict realizability; the counts assume each row offers a gold and a distinct wrong label. At b=N no positive gain is feasible. Old-score ties preserve regression; new-score ties never improve. These are score-space facts, not claims that training attains a preimage.

Identity and equivariance

Simultaneously apply bijections to learner labels and answer labels, rename questions consistently, and reconstruct both contracts and reports with fresh fingerprints. Equality, membership, scores and comparison outputs are preserved. The transformation acts on the whole four-corner configuration, not just report headers. A noninjective answer renaming can merge a wrong label into gold and change correctness, so it is excluded.

Fingerprint inputs include course, lesson number, tests and exams, including ordered wrong-option lists. Row validation reads kind/index/question/gold and choice but does not read course, lesson number or the whole option list from the report. Thus editing course, lesson number, option order or unused options changes the contract fingerprint; an old header rejects, but a consistently retagged otherwise matching report can pass. There is no review signature, source authenticity or review approval check here. Review metadata is unconsulted; higher-level orchestration must establish those obligations. Equal before/after learner labels with contradictory reports can also pass: the comparator enforces shared identities, not deterministic provenance.

Oracles and cost

The full-output histogram oracle binds all four grades through the public constructor/binder path for N=1..4 and M=1..3: 1566 score quadruples. Closed-form lattice counts predict complete observed output fibers, including unequal denominators. Histogram agreement checks cardinalities and impossible outputs, not pointwise history membership; the existing 256-case Lean table provides complementary pointwise recommendation coverage on 0..3.

A second oracle checks all 16 assignments of two learner labels; precisely masks 0,5,10,15 satisfy the corner equalities. Four same-denominator foreign assessment replacements reject. One simultaneous bijective transformation preserves the full output, while a collapsed-label countermodel rejects a false-answer report. A third oracle checks four source identity changes and three unconsulted review values. These observations correct stronger identity and authentication interpretations; no normal API or production policy changes.

Comparison remains O(identity bytes) with constant arithmetic. Test fixture construction and binding scale with the enumerated row count; no runtime speedup, analytical approximation guarantee or composition-wide bound is claimed. The AST is a source-bound partial syntax projection, not semantic analysis or expanded macros.

nonbehavior

Behavior-complement obernant: score-policy projection

Type: behavior_complement. Status: partial mathematical projection, not a general generated model of absent Rust behavior. Subject: assessment score policy; source identity is in manifest.json.

Let q=(before,after,old_before,old_after) range over nonnegative scores within fixed assessment question-count bounds. Let b be a Boolean recommendation. Define the explicit transition universe U={(q,b)} on that domain and

recommend(q) = (before < after) and (old_before <= old_after).
R = {(q,b) in U | b = recommend(q)}.
C = {(q,b) in U | b != recommend(q)} = U minus R.

C describes transitions this deterministic policy does not perform. For instance a true recommendation at zero gain is in C; a true recommendation with positive gain and no regression is in R. This is a formula for the absent behavior, rather than just a list of rejection tests.

C is exact for the declared abstract policy. Its use as an approximant of the full system is limited to this projection. It is not a proved inner or outer bound on all Rust behavior. No conclusions about parser semantics, forged reports, IO failures or unbounded learning histories follow from it.

The existing 256-row Lean table and Rust forward-correspondence checks provide bounded evidence on scores 0..3. This turn adds no new formal complement theorem or executable complement generator. Source/model changes require renewed correspondence checks.

Unlike reverse_reconstruction, this type keeps the transition direction and complements membership within U. Its meaning changes if U or the observation projection changes; record those assumptions with each specialized instance.

See four-corner refinement for the success relation, first behavior complement, second full-output preimages, denominator constraints, identity transformations and bounded production-oracle evidence.

threshold-repair

Threshold-repair obernant

Type: threshold_repair. Domain: already bound, compatible score quadruples (b,a,u,v) with new total N and regression total M. Only post-training counts a and v may increase; totals, questions, learners and baseline counts stay fixed.

For recommendation=true, minimal nonnegative coordinate repairs are da=max(0,b+1-a), dv=max(0,u-v). Feasible score repairs require a+da<=N and v+dv<=M. If b=N, no improvement exists at that fixed new assessment size. These are coordinatewise minima in integer score space.

For N=M=3 there are 6 ordered new improvement pairs and 10 nonregression old pairs: 60 of 256 quadruples recommend, 196 do not. In general the accepted count is N*(N+1)/2 * (M+1)*(M+2)/2.

This inverse feasibility model identifies assessment thresholds and saturation. It does not assert a training intervention can achieve those score repairs. Changing an assessment to manufacture a gain violates the binding domain. The existing 256-row table provides bounded evidence for the cardinality model.

See four-corner refinement for the success relation, first behavior complement, second full-output preimages, denominator constraints, identity transformations and bounded production-oracle evidence.

This page in Markdown → https://md.groupants.elamur.ai/free/en/mova/tools/enrich/src/assessment.rs.groupant/