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

Update UIP-0123.md #52

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
15 changes: 7 additions & 8 deletions UIPS/UIP-0123.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,27 +17,26 @@ Implementing this hint would remove the need to manually implement such checks w

## Motivation

Some Nock programs such as the Hoon compiler must run complex recursive functions over arbitrary user input. Algorithms which rely on memoization to be feasible can leverage the `%memo` hint supported by both Vere and Ares.
The `%memo` hint, supported by both Vere and Ares, allows algorithms to improve performance using memoization. The underlying cache for the hint is, in general, a map from subject-formula pair to result.

However, if it is necessary to deduce non-termination and crash with an error, the necessary state in the subject prevents the use of the %memo hint. While this is not the only reason for custom memoizing jets in the Hoon compiler, it is a major contributor. Non-termination and crashes are equivalent in Nock, and an interpreter choosing to report a crash is reporting that the computation would not terminate if continued.
Some Nock programs, such as the Hoon compiler, must run complex recursive functions over arbitrary user input. These programs need memoization to be feasible. However, they also need to crash with an error when they detect non-termination. Since the programs store the state used to deduce non-termination in the subject, they're unable to use the `%memo` hint. This is a major contributor to the custom memoization jets for the Hoon compiler functions, which manually punch out holes in the subject before caching.
ashelkovnykov marked this conversation as resolved.
Show resolved Hide resolved

Thus, if the interpreter makes this determination, it is correct for it to crash with a stack trace. However, we do not want to check every subject-formula pair against all prior pairs in the call stack at every evaluation site (Nock 2 or Nock 9).
Non-termination and crashes are equivalent in Nock, and an interpreter choosing to report a crash is reporting that the computation would not terminate if continued. Thus, if the interpreter makes this determination, it is correct for it to crash with a stack trace. However, we do not want to check every subject-formula pair against all prior pairs in the call stack at every evaluation site (Nock 2 or Nock 9).

## Specification

Nock interpreters SHOULD recognize the `%loop` static hint as follows (or extensionally equivalent behavior):
Nock interpreters SHOULD recognize the `%loop` static hint using the following (or extensionally equivalent) behavior:

- Maintain a stack of subject and formula pairs
- On entry into the hinted computation
- On entry into a `%loop` hinted computation:
- check whether the current subject and hinted formula are already on the stack
- if so, crash
- if not, push the current subject and formula onto the stack
- On exit from the hinted computation, pop the stack.

- On exit from the hinted computation, pop the stack

## Rationale

Any algorithm which maintains a stack-like structure in order to catch input on which it would naively nonterminate can simply be hinted by `%loop` instead. This removes state from the subject and allows such algorithms to also leverage the `%memo` hint.
An interpreter that handles the `%loop` hint allows non-termination detection state to be removed from the subject and instead stored in an interpreter cache. Any algorithm that currently maintains a stack-like structure in order to catch input for which it would naively not terminate can simply be hinted `%loop` instead, and can also leverage `%memo` as well.

## Backwards Compatibility

Expand Down