Virtual hidden nodes by uncomputable · Pull Request #264 · BlockstreamResearch/rust-simplicity

uncomputable · 2025-02-06T14:05:29Z

This PR adds the wrapper type Hiding<N> which allows the use of hidden nodes during the construction of a program. The hidden nodes exist only in the wrapper and the Inner struct remains untouched (therefore "virtual hidden nodes").

We use Hiding<N> to simplify the policy satisfier and to represent missing assembly fragments, which removes one error path.

uncomputable · 2025-02-06T14:08:45Z

CI fails because of outdated github actions which are updated in #261

src/merkle/mod.rs

src/node/mod.rs

src/node/hiding.rs

Take some of the changes from BlockstreamResearch#261 to make fuzzing CI work again.

This trait helps dealing with CMRs in generic contexts.

uncomputable · 2025-02-07T11:43:41Z

Made fuzzing CI work again and addressed the comments.

apoelstra · 2025-02-07T16:22:47Z

Ok, after thinking about this more, I think that the type inference story in this PR is correct. But let me write out some thoughts.

In this PR there are three ways to construct a Hiding node:

Calling Hiding::hidden and explicitly passing a CMR and a type inference context, which is unused except as an accessor
Calling Hiding::from on some CoreConstructible node, which simply wraps the node and stores a copy of its inference context arc.
Doing the same but then calling hide, which drops the original node, keeping its CMR and the handle to its inference context.

When we construct programs/expressions, we always do so in post-order. This is enforced by our API which simply doesn't let you create nodes until their children exist, which in turn means that when you create a new node, its children "haven't seen each other" until the moment of creation. What I mean by this is that the children's sets of type inference variables will be disjoint, and during creation of the new node, bounds may be created that entangle them. (Sharing complicates this a bit but let's ignore that for now.)

The rule for type inference is that hidden nodes do not have type variables. So when you put a hidden node into a combinator with anything else, there are no new type bounds and the other child's type variables are unaffected. In fact, they are not just unaffected but they are hidden -- the new node will be hidden, and therefore also have "no type inference variables", and any variables that its children might've had before being hidden are effectively gone. (Again, with sharing maybe these variables are still accessible elsewhere, but we can ignore that.)

This code is correct in that when you, for example, create a new comp combinator, if either child is hidden we manually combine their CMRs, preserve the type inference engine, and do nothing else. And only if neither child is hidden, then we pass through to CoreConstructible::comp on the two children, which will add bounds between the children's type inference variables.

However, it makes me a little nervous that in the hiding case, we carefully preserve the type inference variables/bounds/arrows/etc of the children by preserving the type inference context. I wish there was a way that we could say "hidden node, no types to see here".

apoelstra · 2025-02-07T16:25:52Z

API-wise I don't see any good way to do what I'm describing -- we could drop the ctx member of Hiding at the expense of adding a types::Context::new_dummy constuctor and updating the context-consistency checks to say that a dummy is "the same context" as any other one, and so on, but the result would be a lot of extra complicated code which might even be more confusing than what you've got here.

Could you put my above comment, or maybe some subset of it, as a block comment in the hiding.rs file? Maybe as a doccomment on the private ctx field?

apoelstra · 2025-02-07T16:27:17Z

0b2ae76 looks good other than my above comments, which are exclusively "can you add more comments".

uncomputable · 2025-02-07T20:45:42Z

In the end, the hidden nodes in this PR are simulated and the rule that they must not have type inference variables does not apply. We do throw away expressions and their types when we hide them, but that should not be a problem.

I agree that it is confusing that hidden nodes (even if they are simulated) have a type inference context. However, as long as CoreConstructible::inference_context exists, no one knows how this method will be called. For soundness, the same context should be returned for all nodes of the same program.

uncomputable · 2025-02-09T12:34:46Z

I updated the documentation of Hiding and added comments that explain soundness.

apoelstra · 2025-02-09T18:16:53Z

src/node/hiding.rs

+///
+/// A node can be wrapped via [`Hidden::from`] to add hiding support.
+/// A wrapped node can be converted into a "hidden" node via [`Hidden::hide`].
+/// Finally, a "hidden" node can be manually created via [`Hidden::hidden`].


In 8bc68ac:

In several places in these docs you say Hidden but the type is called Hiding.

Good catch. Thanks for pointing out the typo.

The policy satisfier needs to produce a Simplicity program that matches a given CMR. When an assembly fragment is missing, then we can use hidden nodes to represent it. Hidden<N> simulates this behavior by propagating hidden nodes upwards towards the next case node. If the root node becomes hidden, then the entire program is unsatisfiable.

Use hidden nodes to signify unsatisfiability of sub-expressions. When a sub-expression is unsatisfiable, then it makes no sense to execute it. We can just as well keep its CMR in a hidden node. This simplifies the code and it solves a potential problem of the previous design: a hidden node could be marked as satisfiable.

This error was thrown when a disconnected branch is populated during construction of a CommitNode. The error was intended to inform users that the disconnected branches are thrown away, but this information is not useful. It is a general fact that CommitNode omits disconnected branches. We don't need to throw a runtime error in case a disconnected branch exists. Removing Error::DisconnectedCommitTime eliminates a useless runtime error path.

apoelstra

ACK 29dd9ea; successfully ran local tests; awesome, thanks!