Skip to content

Raise explicit range error for unmatched stack segments#1129

Open
brik64-admin wants to merge 1 commit intoskyfielders:masterfrom
brik64-admin:codex/brik64-skyfield-1125-stack-no-match
Open

Raise explicit range error for unmatched stack segments#1129
brik64-admin wants to merge 1 commit intoskyfielders:masterfrom
brik64-admin:codex/brik64-skyfield-1125-stack-no-match

Conversation

@brik64-admin
Copy link
Copy Markdown

@brik64-admin brik64-admin commented May 10, 2026

BRIK64 Proof

Summary

  • make scalar Stack._at() return immediately when a matching segment is found
  • raise an explicit EphemerisRangeError when no segment covers the requested scalar date
  • add a regression test that verifies the no-match case does not fall through to the wrong segment

Closes #1125.

BRIK64 verification credit

This bounded scalar segment-selection branch was prepared with BRIK64, a verification ecosystem that models critical logic as bounded circuits and checks the resulting scope with generated regression fixtures.

For this PR, BRIK64 was used to lift and compare the scalar Stack._at() path behind segment matching and the no-match fail-closed invariant. The submitted code remains ordinary Python and requires no BRIK64 dependency.

The certificate covers only this bounded segment-selection scope; it does not certify the full repository, ephemeris source authority, security, deployment behavior, generated tests, or future changes.

Tests

  • ./.venv/bin/python -m pytest skyfield/tests/test_jpllib.py::test_stack_scalar_no_matching_segment_raises_without_fallthrough -q - passed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Stack._at() out-of-range exception only mentions final segment checked, instead of all segments available

1 participant