UIP-0123 %loop hint crash determinism question

[belisarius222]

The UIP suggests that the interpreter should produce a deterministic error (bail: exit) when the %loop hint triggers. While this does not violate the Nock spec, @joemfb, @frodwith, and I all had the same gut feeling that it would be more conservative to fail nondeterministically (bail:fail), since that would preserve the existing behavior, i.e. an infinite loop could only ever result in a nondeterministic error in any interpreter that doesn't support the %loop hint.

@eamsden Do you have a specific use case in mind that would benefit from this error being catchable? If not, we are leaning toward making this a bail:fail.

[eamsden]

Yes the case is precisely where you would otherwise keep a set of some sort in your subject to track if you are recurring on some already seen part of . The goal of the hint isn't just to turn otherwise-infinitely-looping nock into a crash, but to allow the removal of explicit checks in hoon while retaining the ability to crash deterministically instead of infinite-looping.

@joemfb there is state in the Hoon compiler like this, right?

[dozreg-toplud]

@belisarius222 @joemfb @frodwith your gut feeling was correct: implementation of %loop hint proposal in its current form would lead to +mink jet mismatch.

It is true that in Nock proper both !! and |-($) are similarly uncomputable: both produce an infinite loop of reductions according to the specification. Virtual Nock (or Mock), however, is different: in +mink !! is computable (%2 case with a trace) and |-($) is not, since it would lead to an infinite loop of reductions of Mock.

Consider having to compute or |-($) in kernelspace Nock in Arvo. No matter how this computation is handled (processed as a deterministic crash or aborted non-deterministically) it would lead to the same result - an event that caused such computation to occur would not be added to the event log, keeping the event log replayable across all instances of valid Nock interpreters.

Consider now computing that expression virtually with a %loop hint (e.g. (mole |.(~>(%loop |-($))))). Now, a Nock interpreter that faithfully implements the Nock spec would not be able to compute that expression, leading to a non-deterministic crash and an event not being added to the event log. But with %loop proposal implemented as it is currently described, the expession would return ~, and the event would be added to the event log, corrupting the event log by making it non-replayable.

This proposal would bring a jet mismatch in +mink and friends, similar to the one in current +dec jet implementation: it crashes deterministically on the sample being a cell, breaking the interpreter and potential event log replay in the case of virtualized execution.

Therefore,

Either the proposal must make the crash non-recoverable,

Or +mink implementation in Hoon must be updated to handle %loop hint.

I would prefer the latter as it would make it simpler to catch Hoon compilation errors in userspace without having to catch the error via +on-error of a Gall agent or alternative ways in Spider threads.