Skip to content

Formally prove totality and determinism of numeric casts#85

Open
zimri-leisher wants to merge 5 commits into
develfrom
math-proof
Open

Formally prove totality and determinism of numeric casts#85
zimri-leisher wants to merge 5 commits into
develfrom
math-proof

Conversation

@zimri-leisher

Copy link
Copy Markdown
Collaborator
Related Issue(s)
Has Unit Tests (y/n) y
Documentation Included (y/n)

Change Description

A description of the changes contained in the PR.

Rationale

A rationale for this change. e.g. fixes bug, or most projects need XYZ feature.

Testing/Review Recommendations

Fill in testing procedures, specific items to focus on for review, or other info to help the team verify these changes are flight-quality.

Future Work

Note any additional work that will be done relating to this issue.

@zimri-leisher zimri-leisher changed the base branch from main to devel July 5, 2026 16:10
Comment thread test/fpy/test_model.py
model.push(0.0)
result = model.dispatch(FloatModuloDirective())
assert result is None or result == DirectiveErrorCode.NO_ERROR
assert math.isnan(model.pop(type=float))
Comment thread test/fpy/test_model.py
model.push(2.0)
result = model.dispatch(FloatModuloDirective())
assert result is None or result == DirectiveErrorCode.NO_ERROR
assert math.isnan(model.pop(type=float))
Comment thread test/fpy/test_model.py
model.push(2.0)
result = model.dispatch(FloatModuloDirective())
assert result is None or result == DirectiveErrorCode.NO_ERROR
assert model.pop(type=float) == 0.5

bad = []
n = 0
for op in BinaryStackOp:
bad.append(
f"{t1.name} {op.value} {t2.name}: compiler={got} spec={want}"
)
for op in UnaryStackOp:

bad = []
n = 0
for op in BinaryStackOp:
v.eq(x) or v.eq(y) or v.decl().name() == "fpy_pow" for v in fv
):
bad.append(f"{t1.name} {op.value} {t2.name}: free vars {fv}")
for op in UnaryStackOp:
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.

2 participants