Backend-selection reports

Inspectable explanations of deterministic selector decisions. Reports are intended for development tools and calibration; executable arithmetic does not construct them.

inductive FloatLib.Floats.ExecFloat.Backend.AssessmentStatus : Type

Why one candidate appears in a selector decision report.

• selected : AssessmentStatus
• rejectedResidentMemory (required limit : Nat) : AssessmentStatus
• rejectedTemporaryMemory (required limit : Nat) : AssessmentStatus
• notPreferred : AssessmentStatus

def FloatLib.Floats.ExecFloat.Backend.instDecidableEqAssessmentStatus.decEq (x✝ x✝¹ : AssessmentStatus) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instDecidableEqAssessmentStatus : DecidableEq AssessmentStatus

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instReprAssessmentStatus : Repr AssessmentStatus

def FloatLib.Floats.ExecFloat.Backend.instReprAssessmentStatus.repr : AssessmentStatus → Nat → Std.Format

structure FloatLib.Floats.ExecFloat.Backend.Assessment : Type

Disposition of one candidate in a selector report.

• candidate : Candidate

  Candidate whose disposition is reported.

• status : AssessmentStatus

  Reason the candidate was selected or rejected.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instDecidableEqAssessment : DecidableEq Assessment

def FloatLib.Floats.ExecFloat.Backend.instDecidableEqAssessment.decEq (x✝ x✝¹ : Assessment) : Decidable (x✝ = x✝¹)

def FloatLib.Floats.ExecFloat.Backend.instReprAssessment.repr : Assessment → Nat → Std.Format

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instReprAssessment : Repr Assessment

def FloatLib.Floats.ExecFloat.Backend.Candidate.assess (policy : Policy) (selectedIndex index : Nat) (candidate : Candidate) : Assessment

Explain the candidate at position index of a candidate list whose selected member is at position selectedIndex.

Candidates are identified by position rather than by comparing estimates, so identical estimates do not create multiple selected assessments. The selected index takes precedence over memory limits: the mandatory baseline may be selected even when it exceeds either cap. Memory rejection describes only unselected candidates.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.Candidate.assess_selected (policy : Policy) (index : Nat) (candidate : Candidate) : (assess policy index index candidate).status = AssessmentStatus.selected

The selected candidate is reported as selected, regardless of the policy's memory limits.

def FloatLib.Floats.ExecFloat.Backend.selectCandidateIndexed (policy : Policy) (candidates : CandidateSet Candidate) : Candidate × Nat

Run the selection fold while tracking the position of the incumbent in candidates.toList.

Alternatives occupy positions 0 through alternatives.length - 1 and the baseline occupies position alternatives.length, matching CandidateSet.toList.

def FloatLib.Floats.ExecFloat.Backend.selectedIndex (policy : Policy) (candidates : CandidateSet Candidate) : Nat

Position in candidates.toList of the candidate returned by selectCandidate.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.selectCandidateIndexed_fst (policy : Policy) (candidates : CandidateSet Candidate) : (selectCandidateIndexed policy candidates).fst = selectCandidate policy candidates

The tracked fold selects the same candidate as selectCandidate.

structure FloatLib.Floats.ExecFloat.Backend.SelectionReport : Type

Inspectable explanation of one static selection calculation.

• policy : Policy

  Policy under which all estimates were evaluated.

• selected : Candidate

  Candidate chosen from the mandatory baseline and admissible alternatives.

• assessments : List Assessment

  Assessment of every alternative followed by the mandatory baseline.

def FloatLib.Floats.ExecFloat.Backend.instDecidableEqSelectionReport.decEq (x✝ x✝¹ : SelectionReport) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instDecidableEqSelectionReport : DecidableEq SelectionReport

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instReprSelectionReport : Repr SelectionReport

def FloatLib.Floats.ExecFloat.Backend.instReprSelectionReport.repr : SelectionReport → Nat → Std.Format

def FloatLib.Floats.ExecFloat.Backend.selectionReport (policy : Policy) (candidates : CandidateSet Candidate) : SelectionReport

Compute the same result as selectCandidate together with every accepted or rejected alternative.

This is for inspection and calibration; arithmetic projects the stored Certified implementation and never constructs a report on the hot path.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.selectionReport_selected (policy : Policy) (candidates : CandidateSet Candidate) : (selectionReport policy candidates).selected = selectCandidate policy candidates

The reported winner is the candidate chosen by selectCandidate.