Effects, witnesses, parameters and purity

In this post I talked about a new quote operator that would be used to transform a Simplicity expression into a new expression which computes the CMR of the original expression. In such expressions witness nodes all turn into the constant witness CMR, and parameters turn into inputs. However, unlike inputs to functions, these are identified by name rather than position.

Relatedly, in this post Mike asks why only main can have witnesses, and speculates that it would cause action-at-a-distance (and maybe enable some kinds of backdoors) if witnesses or parameters were implicitly accessible to imported library code. However, it would be useful for libraries to be parameterizable and also for them to take witnesses (e.g. you could imagine a factorization method that just takes the factors as witnesses and verifies they multiply to the target … obviously much much more efficient than one that attempts to do the factorization on-chain). The issue here is that while in Simplicity, witnesses are pure (they differ from constants only in their encoding and their commitment structure), in SimplicityHL they are side-effects (global variable accesses).

Also relatedly, in this Github post Seth complains that you need to setup a full transaction environment to test SimplicityHL code, and write some sort of test harness that will compile as a blockchain program, even for pure or witness-only functions.

All of these things suggest that we want some sort of language support for listing effects. In particular, we should list all the parameters and witnesses that a module (or function, or expression) accesses. I think we should also add some sort of syntax to indicate whether a module/function/expression access the transaction context or not. For functions that don’t access transaction context, we should have access to much simpler unit testing infrastructure.

There are some open questions here:

  • When should these annotations be required?
  • How should they inherit?

My proposal is as follows:

  • For all functions except main, and all modules, it is required to list all parameters and witnesses it accesses. When importing modules, it is required to list and re-assign all witnesses. (e.g. a module which uses witness::PUBLIC_KEY would be imported as use { witness::PUBLIC_KEY = witness::ALICE_PUBLIC_KEY } my_module or something.
  • Functions/modules are only allowed to access witnesses/parameters that their containing module(s) declare.
  • You can declare a function as notxenv to indicate that it does not access the transaction environment. If a module is notxenv then every function and submodule is also notxenv whether or not it declares itself to be.

I am not married to any particular syntax or set of keywords or whatever.

I think I prefer the rule that witnesses are only declared in the main function. I originally created the mentioned post after listening to @tvolk131 ask about it in an office hours, so perhaps he has a stronger preference.

Parameters however, I think should be allowed in modules and in that case, I think it’s a good idea to either expose them using a syntax like you described, or potentially disallow them. It’s worth noting that parameters are currently supported in imported modules already. This might need to change if we are planning on moving towards a canonical CMR approach.

Regarding the environment and transaction reading, I have a work-in-progress effects analyser, which basically does two things: determine the parts of the environment read, and determine if all paths through the program have at least one failure case.

The only way to read anything in Simplicity is through jets, so I added a method that returns the transaction fields that each jet reads. This should be generated for rust-simplicity along with the other generators. I was using it to determine whether any fields were left out of being read, which would be an indication of malleability. I paused this because there were a lot of changes happening in rust-simplicity at the time. I plan to pick this up again now that this has stablized.

Off topic is the failure (aka write) effects. I did get quite far with this, but it is harder to determine when the failure comes from a SimplicityHL match + panic pair.

Coming back to your proposal, if we implement the reader effect at least, I don’t think we need notxenv. It may be useful for functions to specify with environments (Core, Bitcoin, Elements) they can be compiled for, with Core being the equivalent of notxenv.

So, after discussion this on the phone with you, I think there’s a more straightforward solution:

  1. We leave the existing witnesses and parameters as-is; can only be used in main() and in the file that contains main(). But we soft-deprecated them in favor of…
  2. …we add new function argument syntax, like fn myfunc(param ALICE_PUBKEY: \[u8; 33\], witness ALICE_SIGNATURE: \[u8; 65\], ordinary_arg: bool) -> whatever. (I don’t care about the particular syntax, but I recall in early Rust that had a ton of sigils that users complained about this endlessly, compared the language to Perl, etc., so I suspect we should prefer adding keywords over adding sigils.)
  3. We also add module syntax mod mymodule(param ALICE_PUBKEY, witness ALICE_SIGNATURE)
  4. Also some sort of corresponding syntax for modules that are implicitly defined by mod.simf files, and corresponding syntax when importing these modules that requires the user to explicitly list the params/witnesses and rename them if necessary.

So now each function declares upfront what parameters and witnesses it has access to, but does so in basically the same way that it declares what ordinary arguments it has access to. Internally, the compiler turns param args into inline constants and witness args into ordinary arguments (that it populates internally at every callsite). We should add a few rules:

  1. (Lint only) params and witnesses should be ALL CAPS
  2. Params must come first, then witnesses, then ordinary arguments
  3. Functions/modules can only access params/witnesses that their parents have access to

Then the quote operator can be used on function names, in which case the signature of the quoted expression is the same as the function’s signature except that the param arguments become regular arguments and the other kinds of arguments are removed. We should also support quoting bare expressions that don’t use any parameters. If you quote an expression that uses a parameter, the compiler should tell you to wrap it in a function.

The resulting quote semantics are then non-magical and clear to a user who understands the language, as are the semantics of witnesses (that they are effectively function arguments, rather than lookups into some magic global table, or inline constants, or Simplicity witness nodes, or something else).

Well, the question becomes, “do we make users annotate every function with the txenv-reading effects it has (so notxenv is the default and we don’t need a keyword, but existing code will stop working), or do we assume that an unannotated function might access the transaction environment (then we need a notxenv to opt out)”.

1 Like

Yeah, I’m quite happy with this plan. I think let’s leave the notxenv discussion for another time, unless it cleanly fits into your plan