Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

SAWCore maxNat has the wrong definition #1502

Closed
robdockins opened this issue Nov 9, 2021 · 1 comment
Closed

SAWCore maxNat has the wrong definition #1502

robdockins opened this issue Nov 9, 2021 · 1 comment
Labels
subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem

Comments

@robdockins
Copy link
Contributor

maxNat : Nat -> Nat -> Nat;
maxNat x y =
Nat_cases2 Nat (\ (x':Nat) -> x')
(\ (y':Nat) -> Succ y')
(\ (y':Nat) -> \ (x':Nat) -> \ (sub_xy:Nat) -> sub_xy) y x;

This defines the incorrect function. The final case should actually be (Succ sub_xy). The naming makes me suspect this is a copy-paste error from the prior definition of subNat. We mostly haven't noticed this problem because maxNat is overridden in the simulators with a correct definition. However, for Coq extraction, we are directly translating this recursive definition and computing the wrong answers.

@robdockins robdockins added the subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem label Nov 9, 2021
@robdockins
Copy link
Contributor Author

This definition seems like it came in when we refactored SAWCore to use recursors. CF c37aa45

robdockins added a commit that referenced this issue Nov 10, 2021
@mergify mergify bot closed this as completed in 4fc5ddd Nov 10, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem
Projects
None yet
Development

No branches or pull requests

1 participant