Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
109 changes: 109 additions & 0 deletions crates/labcolors-core/src/recheck.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,11 @@ use crate::constraints::{
HardDecision, ReadabilityPassV1, ReadabilityPolarityV1, ReadabilityViolationV1,
assess_visible_point_hard,
};
use crate::joint::{
CandidateOrdinalV1, DeclaredTotalOrderV1, JointCandidateSetV1, PointwiseFullHardReportV1,
PointwiseHardFeasibilityV1, PointwiseJointPointProgramV1, PointwiseJointReportErrorV1,
PointwiseSelectedRecheckErrorV1, PointwiseVerifiedSelectionV1, SelectionPolicyErrorV1,
};
use crate::observation::{RevisionBoundObservationV1, ScenarioId};
use crate::solve::Floor;

Expand Down Expand Up @@ -627,3 +632,107 @@ impl ReadabilityRecheckReportV1 {
.map(|case| case.provenance())
}
}

// ---------------------------------------------------------------------------
// V2a joint feasible-across-all-samples re-solve bridge (C8d step 3).
//
// The full-support recheck above proves ONE already-chosen candidate over the
// whole support. This bridge wires the generic V2a joint selection (joint.rs) so
// a re-solve returns exactly ONE candidate that is hard-feasible across the WHOLE
// observed scenario set — every backdrop sample admitted as its own case — or a
// typed Indeterminate when no jointly-feasible tuple exists. It never returns a
// candidate that breaks a sample: `classify` demands every case pass, so the
// least-margin / worst sample is only ever a post-hoc diagnostic witness, never a
// solve input (the Pointwise every-case law, DAG mandate `V2a + F2 -> C8d`).
//
// ANTI-DRIFT: joint.rs stays generic. The readability semantics live entirely in
// `DisplayReadabilityCurveV1` (constraints/readability.rs); this bridge only
// INSTANTIATES the existing generic `PointwiseJointPointProgramV1<E>` with
// `E = DisplayReadabilityCurveV1`, exactly as the exact path instantiates it with
// `ExactSrgb8IdentityV1`. No readability enum or import ever crosses into
// joint.rs — the readability curve reaches the joint engine only through the same
// sealed `Evaluator` + `HardClassifier` seam every other predicate uses.
// ---------------------------------------------------------------------------

/// The readability specialisation of the generic two-paint joint program: the
/// same `PointwiseJointPointProgramV1<E>` the exact path uses, instantiated with
/// the frozen display-domain readability curve as `E`.
pub(crate) type ReadabilityJointProgramV1 = PointwiseJointPointProgramV1<DisplayReadabilityCurveV1>;

/// The full hard report of a readability joint program over one immutable
/// observation revision.
pub(crate) type ReadabilityJointReportV1 =
PointwiseFullHardReportV1<DisplayReadabilityCurveV1, RevisionBoundObservationV1>;

/// One re-verified readability joint selection: exactly one candidate, freshly
/// re-executed across every admitted sample on the same revision.
pub(crate) type ReadabilityJointVerifiedSelectionV1 =
PointwiseVerifiedSelectionV1<DisplayReadabilityCurveV1, RevisionBoundObservationV1>;

/// Typed outcome of a joint readability re-solve evaluated across the WHOLE
/// observed scenario set.
#[derive(Debug, Clone, PartialEq)]
pub(crate) enum JointReadabilityResolutionV1 {
/// Exactly one candidate, jointly feasible across every admitted backdrop
/// sample and freshly re-verified on the same observation revision before it
/// is handed back. A set-breaching candidate can never reach this variant.
Feasible(Box<ReadabilityJointVerifiedSelectionV1>),
/// No jointly-feasible candidate exists. The full hard report is retained so
/// the breaching sample(s) can be identified after the fact — a diagnostic
/// witness only, never fed back into the solve as a target.
Indeterminate(Box<ReadabilityJointReportV1>),
}

/// Why a joint readability re-solve could not produce a typed resolution.
#[derive(Debug, Clone, PartialEq)]
pub(crate) enum JointReadabilityResolveErrorV1 {
/// The joint program rejected the candidate domain or observation before any
/// feasibility verdict could be formed.
Report(PointwiseJointReportErrorV1<DisplayReadabilityCurveV1>),
/// The declared tie-break was not a total order over the candidate domain.
Policy(SelectionPolicyErrorV1),
/// A candidate that classified feasible failed its fresh re-verify — an
/// invariant drift between the selection pass and the recheck pass.
ReverifyDrift,
/// Cardinality overflow or an allocator refusal during the fresh re-verify.
ResourceExhausted,
}

/// Re-solve across the whole observed scenario set: evaluate every candidate
/// tuple over every admitted backdrop sample, keep only the candidates that pass
/// EVERY sample, tie-break by the declared total order, then freshly re-verify
/// the winner across the whole set before returning it. When no candidate passes
/// every sample the result is a typed [`JointReadabilityResolutionV1::Indeterminate`],
/// never a target that breaks a sample.
pub(crate) fn resolve_across_all_samples(
program: &ReadabilityJointProgramV1,
candidates: JointCandidateSetV1,
observation: RevisionBoundObservationV1,
order: Vec<CandidateOrdinalV1>,
) -> Result<JointReadabilityResolutionV1, JointReadabilityResolveErrorV1> {
let report = program
.evaluate(candidates, observation)
.map_err(JointReadabilityResolveErrorV1::Report)?;
match report.classify() {
PointwiseHardFeasibilityV1::Infeasible(report) => Ok(
JointReadabilityResolutionV1::Indeterminate(Box::new(report)),
),
PointwiseHardFeasibilityV1::NonEmpty(feasible) => {
let policy = DeclaredTotalOrderV1::new(feasible.candidate_set(), order)
.map_err(JointReadabilityResolveErrorV1::Policy)?;
match feasible.select(policy).recheck() {
Ok(verified) => Ok(JointReadabilityResolutionV1::Feasible(Box::new(verified))),
Err(PointwiseSelectedRecheckErrorV1::Violation(_))
| Err(PointwiseSelectedRecheckErrorV1::InvariantDrift) => {
Err(JointReadabilityResolveErrorV1::ReverifyDrift)
}
Err(PointwiseSelectedRecheckErrorV1::ResourceExhausted) => {
Err(JointReadabilityResolveErrorV1::ResourceExhausted)
}
// The readability curve is `Infallible`, so the evaluator arm is
// uninhabited: it can never be constructed.
Err(PointwiseSelectedRecheckErrorV1::Evaluator(error)) => match error {},
}
}
}
}
176 changes: 174 additions & 2 deletions crates/labcolors-core/src/recheck_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,15 +2,20 @@ use proptest::prelude::*;

use crate::Srgb8;
use crate::appearance::{EncodedPointPaintV1, OccurrenceId, PaintId, SurfaceInputPortId};
use crate::constraints::{HardDecision, ReadabilityPolarityV1};
use crate::constraints::{DisplayReadabilityCurveV1, HardDecision, ReadabilityPolarityV1};
use crate::joint::{
CandidateOrdinalV1, JointCandidateSetV1, JointCandidateTupleV1, JointConstraintIdV1,
JointVisibleTargetV1, PointwiseJointHardConstraintV1, PointwiseJointPointProgramV1,
};
use crate::observation::{
ObservationPayloadInput, ObservationState, ObservationStreamId, ObservationUpdateInput,
ObservedScenarioSetInput, Revision, ScenarioId, ScenarioInput, SurfaceInputBinding,
};
use crate::recheck::{
BoundReadabilityRecheckV1, CompiledFixedRecheckV1, CompiledReadabilityRecheckV1,
ExactOccurrenceRequirementV1, FixedRecheckBindErrorV1, FixedRecheckDecisionV1,
ReadabilityOccurrenceV1, RecheckProtocolErrorV1, checked_evidence_count,
JointReadabilityResolutionV1, ReadabilityOccurrenceV1, RecheckProtocolErrorV1,
checked_evidence_count, resolve_across_all_samples,
};
use crate::solve::Floor;

Expand All @@ -21,6 +26,12 @@ const SURFACE_A: SurfaceInputPortId = SurfaceInputPortId::new(21);
const SURFACE_B: SurfaceInputPortId = SurfaceInputPortId::new(22);
const STREAM: ObservationStreamId = ObservationStreamId::new(31);

// Joint re-solve bridge fixtures (C8d step 3): two distinct linked paints over a
// single observed root backdrop surface.
const JLOWER: PaintId = PaintId::new(41);
const JUPPER: PaintId = PaintId::new(42);
const JROOT: SurfaceInputPortId = SurfaceInputPortId::new(51);

fn scenario(
id: u32,
bindings: impl IntoIterator<Item = (SurfaceInputPortId, [u8; 3])>,
Expand Down Expand Up @@ -441,3 +452,164 @@ proptest! {
prop_assert!(matches!(decision, FixedRecheckDecisionV1::Verified(_)));
}
}

/// A readability-driven two-paint joint program whose single hard constraint
/// requires the LOWER role to clear the AA-text floor against the observed root
/// backdrop. This is the GENERIC joint program instantiated with the frozen
/// readability curve — no readability type crosses into joint.rs.
fn readability_joint_program() -> PointwiseJointPointProgramV1<DisplayReadabilityCurveV1> {
PointwiseJointPointProgramV1::with_evaluator(
DisplayReadabilityCurveV1,
JROOT,
JLOWER,
JUPPER,
vec![PointwiseJointHardConstraintV1::new(
JointConstraintIdV1::new(1),
JointVisibleTargetV1::Lower,
Floor::AaText,
)],
)
.expect("distinct paints and a unique constraint compile")
}

fn joint_lower(bytes: [u8; 3]) -> EncodedPointPaintV1 {
encoded_paint(JLOWER, Srgb8::new(bytes), 1.0).unwrap()
}

fn joint_upper() -> EncodedPointPaintV1 {
encoded_paint(JUPPER, Srgb8::new([255, 255, 255]), 1.0).unwrap()
}

#[test]
fn joint_recheck_flags_sample_broken_by_resolve() {
// N1 (core-level second-solve-breaks-first): a black lower role is exactly
// what a solve TARGETING the white sample (A) would pick. Over the WHOLE
// observed set it clears A (contrast 21) but breaks the dark sample B
// (#3C3C3C, contrast ≈ 1.9 < AA). The joint re-solve over every admitted
// sample returns a TYPED Indeterminate whose breaching cell carries B's
// provenance — even though B was never the solve target. Worst is a post-hoc
// witness, never a solve input.
let candidates = JointCandidateSetV1::new(vec![JointCandidateTupleV1::new(
CandidateOrdinalV1::new(0),
joint_lower([0, 0, 0]),
joint_upper(),
)])
.unwrap();
let observed = observation(
1,
vec![JROOT],
vec![
scenario(1, [(JROOT, [255, 255, 255])]), // A: white — the solve target.
scenario(2, [(JROOT, [60, 60, 60])]), // B: broken by that resolve.
],
);

let resolution = resolve_across_all_samples(
&readability_joint_program(),
candidates,
observed,
vec![CandidateOrdinalV1::new(0)],
)
.unwrap();

let JointReadabilityResolutionV1::Indeterminate(report) = resolution else {
panic!("a candidate that breaks sample B cannot be jointly feasible");
};

// The breaching sample is identified by its provenance — sample B (id 2).
let breaching = report
.cells()
.iter()
.find(|cell| !cell.decision().is_pass())
.expect("the dark backdrop must break the black role");
assert_eq!(
report.provenance(breaching.case_index()),
Some(&[ScenarioId::new(2)][..])
);
// The actual solve target (sample A, id 1) passed — a DIFFERENT sample broke.
let passing = report
.cells()
.iter()
.find(|cell| cell.decision().is_pass())
.expect("the white target sample must pass");
assert_eq!(
report.provenance(passing.case_index()),
Some(&[ScenarioId::new(1)][..])
);
assert_ne!(breaching.case_index(), passing.case_index());
}

#[test]
fn resolve_is_jointly_reverified() {
// N2: two candidates over samples A (white, id 1) and B (#767676, id 2):
// ordinal 0 = #555555 lower — passes A (7.46) but BREAKS B (1.64);
// ordinal 1 = #000000 lower — passes BOTH (21 and 4.62).
// The joint re-solve returns candidate 1, re-verified across the whole set,
// and the set-breaching candidate 0 is NEVER returned as feasible.
let both_samples = || {
observation(
2,
vec![JROOT],
vec![
scenario(1, [(JROOT, [255, 255, 255])]),
scenario(2, [(JROOT, [118, 118, 118])]),
],
)
};

let candidates = JointCandidateSetV1::new(vec![
JointCandidateTupleV1::new(
CandidateOrdinalV1::new(0),
joint_lower([85, 85, 85]),
joint_upper(),
),
JointCandidateTupleV1::new(
CandidateOrdinalV1::new(1),
joint_lower([0, 0, 0]),
joint_upper(),
),
])
.unwrap();

let resolution = resolve_across_all_samples(
&readability_joint_program(),
candidates,
both_samples(),
vec![CandidateOrdinalV1::new(0), CandidateOrdinalV1::new(1)],
)
.unwrap();

let JointReadabilityResolutionV1::Feasible(verified) = resolution else {
panic!("the black candidate is jointly feasible across both samples");
};
// The set-breaching #555555 (ordinal 0) is never selected; the all-passing
// #000000 (ordinal 1) is, and every fresh re-verify cell passes.
assert_eq!(verified.ordinal(), CandidateOrdinalV1::new(1));
assert_eq!(verified.fresh_cells().len(), 2);
assert!(
verified
.fresh_cells()
.iter()
.all(|cell| cell.decision().is_pass())
);

// When ONLY the set-breaching candidate is offered, the resolve is a typed
// Indeterminate — a breaching candidate is never dressed up as feasible.
let only_breaching = JointCandidateSetV1::new(vec![JointCandidateTupleV1::new(
CandidateOrdinalV1::new(0),
joint_lower([85, 85, 85]),
joint_upper(),
)])
.unwrap();
let resolution = resolve_across_all_samples(
&readability_joint_program(),
only_breaching,
both_samples(),
vec![CandidateOrdinalV1::new(0)],
)
.unwrap();
assert!(matches!(
resolution,
JointReadabilityResolutionV1::Indeterminate(_)
));
}
Loading