improve static typing of contract start terms

[turadg]

Description

Work around endojs/endo#1257 by defining a local deeplyFulfilledObject.

Use it in contract starts to restore type safety (see #5930 (comment) )

Security Considerations

--

Documentation Considerations

This may not be something we want to include in the API backwards compatibility. Once Endo has better type annotations this won't be necessary.

Testing Considerations

No change in code. Tested types manually:

[Chris-Hibbert]

I don't understand the necessity, but if it's required to support typing, I'm fine with it.

[erights]

I would expect "more constrained" to mean that it imposes constraints that the original does not. I see here that it is just a renaming of the original, which is great! It is only better typed. Its runtime behavior is identical.

Wonderful that you could get the types to reflect even some of the recursion! Do you think it is possible to recur into promise types as well? No priority to do so now. I'm just wondering what we know about what's possible in TS.

On the renaming, deeplyFulfilledObject sounds like it applies only to objects, not to primitive values. But this is only a renaming, and the original also applies to primitive values.

[turadg]

On the renaming, deeplyFulfilledObject sounds like it applies only to objects, not to primitive values.

Correct. That's what the types denote.

I would expect "more constrained" to mean that it imposes constraints that the original does not.

It in the sense you describe: it accepts only objects.

But this is only a renaming, and the original also applies to primitive values

It's an encapsulation. That deeplyFulfilledObjects uses deeplyFulfilled is an implementation detail. Callers of deeplyFulfilledObjects should not expect that behavior and will get a static type error if they try to use it more generally.

It is only better typed. … Wonderful that you could get the types to reflect even some of the recursion!

Restricting to object types is part of what achieved this. We could to more work to support all the domain of deeplyFulfilled but I think that's Endo work and it's scope creep for solving type safety for contract terms.

Do you think it is possible to recur into promise types as well?

It goes one level deep into the resolving Promise types (with Awaited):

agoric-sdk/packages/zoe/src/contractSupport/zoeHelpers.js

Line 410 in 4f51b41

* @typedef {T extends PromiseLike ? Awaited<T> : T extends {} ? DeeplyAwaitedObject<T> : Awaited<T>} DeeplyAwaited

That's all that is needed for the terms validation. It should be possible to go arbitrarily deep. Just as ReadonlyDeep does, but it'll take some more supporting types like Primitive. I think solving this fully should be done in Endo. Agoric-SDK is just temporarily working around Endo's poor type definitions. E.g. endojs/endo#1257

[erights]

Not a comment on the code of the PR, but just a note about our curious divergence in terminology I see in your comments above:

It in the sense you describe: it accepts only objects.

But it doesn't accept only objects. The runtime behavior is unchanged. deeplyFulfilledObjects still accepts primitive values. It is only the types describing only the subset of its behavior in which only objects are provided. The reason I call attention to these terminology issues is that we need to maintain clarity about what the runtime behavior of the code actually enforces. Any further restrictions implied by the erased type system are a fiction that, if taken seriously, can lead to a false sense of security and to missing the possibility of an attack, merely because the attack is outside what the types describe.

It's an encapsulation. That deeplyFulfilledObjects uses deeplyFulfilled is an implementation detail. Callers of deeplyFulfilledObjects should not expect that behavior and will get a static type error if they try to use it more generally.

That's only true if we take the specification of deeplyFulfilledObjects to cover only the case where the inputs are well typed. This is the underspecification sin of the "unspecified behavior" that non-secure languages practice, that is incompat with secure languages.

What would be an encapsulation:

const deeplyFulfilledObjects = specimen => {
  assert(isObject(specimen));
  return deeplyFulfilled(specimen);
};

This successfully encapsulates the behavior of deeplyFulfilled on primitive values in the sense that this behavior is no longer reachable.

We need alignment on how we describe such things, because confusion between us about what is actually enforced could be fatal.

[erights]

Likewise in the PR comment

Once Endo has type safety

Hard to imagine that Endo will have type safety before TypeScript does.

[erights]

I'm leaving this one unresolved until I review the comments in the code itself, which may or may not have the same issue as the text in these PR conversations.

[erights]

all bets are off.

"all bets are off" is exactly right. This is programming with preconditions, where a precondition violation waives all specified properties and instead allow "undefined behavior". This is the opposite of defensive consistency (see my thesis), and presents a golden opportunity to an attacker who can cause preconditions to be violated. Defensive consistency starts by generally replacing preconditions with input validation.

Since we're building a platform for mutually suspicious parties to interact via smart contracts, including those representing prediction markets, "all bets are off" is an elegant summary of why we cannot allow such situations ;)

In my experience as a JS developer, I don't expect the function to check all my arguments and tell me which aren't valid.

How much of that experience is in a fine-grain adversarial context, where you have direct contact between mutually suspicious objects, each responsible for defending its invariants from its immediate clients?

Defensive consistency does not require a function to do full input validation. But it does require stated bounds on the misbehavior that any input can cause, and confidence that the implementation succeeds at enforcing these bounds.

Java is relatively sound but still has NullPointerException

On a program that statically type checks, Java makes some hard soundness guarantees about what absolutely cannot happen at runtime. NullPointerException is not one of them. Generic (i.e., parameterized) types are also not sound. Java generics did originally claim that a whole program that passed the type checker with no warnings was type safe wrt generics, but that was shown to be untrue. So Java is only type safe wrt outer (non-type-parameter) types under the interpretation that all object types are nullable types. But within that narrow constraint, AFAIK, Java is absolutely type safe. I have certainly written Joe-E code whose security depends on such guarantees. (Joe-E is an ocap subset of Java, enforced by putting additional static checks in from of the Java compiler.)

AFAIK, a TS program passing its type check with no warnings does not guarantee any runtime invariant whatsoever. I would like to be wrong about this.

[erights]

Partially in reaction to Java generics, C# parameterized types are sound.

[erights]

Here's an interesting riddle (from the Joe-E work) for understanding the difference between Java and JVM soundness. Does the following Java function always return true? (I've forgotten my Java syntax, so please let me know if it not clear what syntactically valid Java program I mean)

boolean isAByte(byte b) {
  return -128 <= b && b <= 255;
}

May a Java compiler validly optimize this function to

boolean isAByte(byte b) {
  return true;
}

?

[erights]

I forgot at first that Java bytes are signed, so I changed the lower bound above. I left the overly generous upper bound since it does not effect the riddle.

[erights]

Spoiler alert

For a hypothetical Java language as specified and implemented independent of the JVM semantics, I imagine that it could validly optimize the body to return true;. But, AFAIK, such a hypothetical JVM-independent Java semantics does not exist.

For actual Java, a Java function may be called from a JVM function that could not have been written in Java. The JVM type rules recognizes integral typed words (32 bits? 64 bits? I forget) but does not recognize or validate typing rules restricting numeric ranges to smaller than a word. So the Java function above, linked with a valid JVM caller that passes the JVM bytecode verifier, can return false, and therefore cannot be optimized to return true;. This divergence between what's possible in Java vs JVM is known (bizarrely IMO) as a "failure of full abstraction".

[erights]

The misleading comment text (with the accurate but disappearing qualifier) is the only remaining hard issue. Terminology about unsound types must never be misunderstood as implying enforcement.

[erights]

LGTM, thanks.