jessie-check contracts #5497

turadg · 2022-06-02T13:09:05Z

Description

A discussion on #4770 suggested we should be using @jessie-check in all our contracts. This PR attempts that.

TODO

solve new Uint8Array
solve do/while statements are not allowed in Jessie (why is this a rule?)
solve generators are not allowed in Jessie. Would it suffice to pull this out of the contract? there'd still be processTranches
solve Unexpected await expression (not top of function body) without changing semantics (several in liquidateIncrementally)
reconsider the curly rule. Why is this in Jessie?

Security Considerations

Documentation Considerations

Testing Considerations

dckc

some of these changes are not semantics-preserving:

Adding + in rec[+kwd] coerces kwd to a number.
new Error(...) -> assert.fail(...) changes control flow.

dckc · 2022-06-02T14:01:24Z

packages/run-protocol/src/reserve/assetReserve.js

-        collateralSeat.getCurrentAllocation()[collateralKeyword],
+        collateralSeat.getCurrentAllocation()[+collateralKeyword],


+ coerces to a number. I don't think this can work. Does it pass tests?

I suggest an extractFieldFromKeywordRecord(record, key) library function imported from a module with keyword record helpers. Perhaps with a more concise name. Or perhaps there's some Object.getProperty standard JS function that would work?

I was (intentionally) blindly following what the rule said to do,

106:9 error arbitrary computed property names are not allowed in Jessie; use leading '+' no-restricted-syntax

what should it say instead?

splitting out into a helper function would still be running the computed property name, right?

The helper function would not be in a @jessie-check file. Just like makeSet and such.

what should it say instead?

Maybe "if you're trying to do numeric indexing, prefix the index with a +". I agree that diagnostic is misleading.

The helper function would not be in a @jessie-check file. Just like makeSet and such.

Sure. But won't it still run in a Jessie environment? I thought jessie-check was for ensuring that something can safely run in a Jessie environment. Below you show that curlies can't run at all. Is the arbitrarily computed property rule the same? If so, won't the imported module have the same problem?

But won't it still run in a Jessie environment?

No. Again, just like makeSet.

Jessie has 2 purposes:

Reduce hazards in writing contracts

Ease language implementation burden

In our system as a whole, we don't use Jessie in our contracts for the 2nd purpose. We support the whole (hardened) JS language at runtime.

Someone else might, for example, build a Jessie interpreter targeting WASM for use on some other platform. They could use the @jessie-check modules without modification. But they would have to do something platform-specific for makeSet and getFieldFromKeywordRecord. For the latter, perhaps makeMap(Object.entries(rec)).get(kw). We don't want to do that because it's O(n). But it's worth putting it in a library module that's reviewed with different expectations.

Yes, the primary purpose of Jessie, and the only purpose for which we are currently using it, is to help us write more reliable and analyzable code. To be fully pedantic, the // @jessie-check enforces only Tiny-SES rather than Jessie, where the difference is the primordials the code is allowed to assume exists. Aside from the primordials the code can assume exists, Jessie and Tiny-SES are identical.

In practice that was one too many distinctions so we use Jessie to describe both. In practice, when we say we're writing most of our code in Jessie, we do not generally mean to imply that the code cannot assume the presence of, for example Reflect, which is part of SES but not Jessie.

We eventually intend to support Jessie as a std for universal mobile code, where a Jessie interpreter can be implemented simply in any normal imperative language. For that purpose, this difference will matter, as that implementation can only be simple if it omits many of the SES primordials including Reflect.

The purpose of the square bracket indexing rules is to make code that is using computed property lookup to index into arrays not be able to be tricked into looking up, for example, inherited method properties. In general, we want code that is using [] safely to index into a collection of some sort safely to be analyzably safe. Zoe introduced the notion of keywords for exactly the same reason, noting that at least all the primordial method names begin with a lowercase character, and so cannot be mistaken for keywords.

If we were willing to have Jessie understand that keywords are safe computed indexes, we could similarly enable syntax that enforced that the index expression evaluated to a keyword. We have not bothered to do that, and have instead just tried to use [] safely by feeding it only keywords, which a static or dynamic check ensuring this.

So we have choices wrt these uses of record[keyword] in what would otherwise be Jessie code:

Have Jessie drop the [] restrictions. Yes, we should consider this.

Rewrite such code to Reflect.get(record, keyword) which means the same thing given the availability of Reflect which is technically part of SES and Tiny-SES but not Jessie.

Introduce a keyword enforcing helper function, upgrade Jessie to allow it, and use it for keyword lookup in the same way we use + for array lookup.

Do we have a // @jessie-expect-error directive analogous to // @ts-expect-error? If so, you could use it to allow expressions you know to be safe -- perhaps even adding to the comment directive an explanation of why you believe it to be safe.

The path of least resistance for now is probably rewriting to Reflect.get(record, keyword). That's what I'd do, but feel free to consider the other alternatives.

dckc · 2022-06-02T14:02:26Z

packages/run-protocol/src/reserve/assetReserve.js

-      throw new Error('insufficient reserves for that transaction');
+      throw assert.fail('insufficient reserves for that transaction');


throw is redundant with assert.fail, yes? I think we have an assert.error constructor.

Yes, the throw assert.fail should normally be just assert.fail. Because assert.fail @returns {never} the two should also be equivalent to typescript.

I have encountered rare circumstances where the throw was still necessary to inform some static check (probably es-lint) that control flow would not proceed normally past that point. Hope that you don't run into that.

dckc · 2022-06-02T14:07:18Z

packages/zoe/src/contracts/priceAggregatorChainlink.js

-    if (_roundId <= add(lastStarted, restartDelay) && lastStarted !== 0n)
+    if (_roundId <= add(lastStarted, restartDelay) && lastStarted !== 0n) {
      return;
+    }


This fixes a hazard that motivates the curly rule. (The other motivation is simplifying the Jessie grammar, I think.)

I would hope that 'jessie-check' checks what's known to fail and doesn't get into style decisions.

in the absence of curlies does Jessie fail to parse?

yes:

In Jessie, only blocks are accepted as arms

https://github.com/agoric-labs/jessica/blob/e8ab6f70065360e201d5230824796b1ce6557cb7/lib/quasi-jessie.js.ts#L141

The motivation is writing reliable code. Before I religiously followed this style I would occasionally screw up by adding a statement to an indented block, not noticing that the indented block was not delimited by curlies.

There are also some strange language edge cases associated with curly-less control-flow arms. For example, what if it brings a variable into scope? What is the scope of the variable? What looks like the scope of the variable? Bad for these two answers to disagree.

dckc · 2022-06-02T14:09:39Z

packages/zoe/src/contracts/sellItems.js

-      throw buyerSeat.fail(new Error(rejectMsg));
+      throw buyerSeat.fail(assert.fail(rejectMsg));


assert.fail throws. It's not a replacement for new Error.

I suggest just taking out new. Error(...) and new Error(...) mean the same thing.

Better would be assert.error. Like Error(...) it makes and returns an error. Like the other assert methods, you can use an

X`literal stuff ${redacted value}`

for better diagnostics. Also, all the assert methods create the error object at the same line of code that becomes a useful place to put a breakpoint.

dckc · 2022-06-02T14:10:49Z

packages/zoe/src/contracts/simpleExchange.js

-      new Error(`The proposal did not match either a buy or sell order.`),
+      assert.fail(`The proposal did not match either a buy or sell order.`),


again, this is not semantics-preserving.

I suggest just changing new Error( to Error(

Or assert.error

erights

LGTM AWESOME! I've been looking forward to this day for years. I am astonished how close so much of our code already was to Jessie prior to any automated checking!

Thanks for doing this!!

erights · 2022-06-03T02:13:13Z

packages/run-protocol/src/reserve/assetReserve.js

-        collateralSeat.getCurrentAllocation()[collateralKeyword],
+        collateralSeat.getCurrentAllocation()[+collateralKeyword],


Yes, the primary purpose of Jessie, and the only purpose for which we are currently using it, is to help us write more reliable and analyzable code. To be fully pedantic, the // @jessie-check enforces only Tiny-SES rather than Jessie, where the difference is the primordials the code is allowed to assume exists. Aside from the primordials the code can assume exists, Jessie and Tiny-SES are identical.

In practice that was one too many distinctions so we use Jessie to describe both. In practice, when we say we're writing most of our code in Jessie, we do not generally mean to imply that the code cannot assume the presence of, for example Reflect, which is part of SES but not Jessie.

We eventually intend to support Jessie as a std for universal mobile code, where a Jessie interpreter can be implemented simply in any normal imperative language. For that purpose, this difference will matter, as that implementation can only be simple if it omits many of the SES primordials including Reflect.

erights · 2022-06-03T02:30:54Z

packages/run-protocol/src/reserve/assetReserve.js

-        collateralSeat.getCurrentAllocation()[collateralKeyword],
+        collateralSeat.getCurrentAllocation()[+collateralKeyword],


The purpose of the square bracket indexing rules is to make code that is using computed property lookup to index into arrays not be able to be tricked into looking up, for example, inherited method properties. In general, we want code that is using [] safely to index into a collection of some sort safely to be analyzably safe. Zoe introduced the notion of keywords for exactly the same reason, noting that at least all the primordial method names begin with a lowercase character, and so cannot be mistaken for keywords.

If we were willing to have Jessie understand that keywords are safe computed indexes, we could similarly enable syntax that enforced that the index expression evaluated to a keyword. We have not bothered to do that, and have instead just tried to use [] safely by feeding it only keywords, which a static or dynamic check ensuring this.

So we have choices wrt these uses of record[keyword] in what would otherwise be Jessie code:

Have Jessie drop the [] restrictions. Yes, we should consider this.

Rewrite such code to Reflect.get(record, keyword) which means the same thing given the availability of Reflect which is technically part of SES and Tiny-SES but not Jessie.

Introduce a keyword enforcing helper function, upgrade Jessie to allow it, and use it for keyword lookup in the same way we use + for array lookup.

Do we have a // @jessie-expect-error directive analogous to // @ts-expect-error? If so, you could use it to allow expressions you know to be safe -- perhaps even adding to the comment directive an explanation of why you believe it to be safe.

The path of least resistance for now is probably rewriting to Reflect.get(record, keyword). That's what I'd do, but feel free to consider the other alternatives.

erights · 2022-06-03T02:33:45Z

packages/run-protocol/src/reserve/assetReserve.js

-      throw new Error('insufficient reserves for that transaction');
+      throw assert.fail('insufficient reserves for that transaction');


Yes, the throw assert.fail should normally be just assert.fail. Because assert.fail @returns {never} the two should also be equivalent to typescript.

I have encountered rare circumstances where the throw was still necessary to inform some static check (probably es-lint) that control flow would not proceed normally past that point. Hope that you don't run into that.

erights · 2022-06-03T02:35:13Z

packages/zoe/src/contracts/autoswap.js


 import { Far } from '@endo/marshal';
 import { assert } from '@agoric/assert';
 import { AmountMath, isNatValue } from '@agoric/ertp';
+import { makeMap } from 'jessie.js';


@michaelfig is that the right way to import from the Jessie std library? No @something/something ?

Yes, absolutely! 'jessie.js' is the stdlib package.

erights · 2022-06-03T02:40:00Z

packages/zoe/src/contracts/priceAggregatorChainlink.js

-    if (_roundId <= add(lastStarted, restartDelay) && lastStarted !== 0n)
+    if (_roundId <= add(lastStarted, restartDelay) && lastStarted !== 0n) {
      return;
+    }


The motivation is writing reliable code. Before I religiously followed this style I would occasionally screw up by adding a statement to an indented block, not noticing that the indented block was not delimited by curlies.

There are also some strange language edge cases associated with curly-less control-flow arms. For example, what if it brings a variable into scope? What is the scope of the variable? What looks like the scope of the variable? Bad for these two answers to disagree.

erights · 2022-06-03T02:41:04Z

packages/zoe/src/contracts/priceAggregatorChainlink.js

+    if (startingRound > _roundId) {
+      return 'not yet enabled oracle';
+    }
+    if (oracleStatuses.get(_oracle).endingRound < _roundId) {
      return 'no longer allowed oracle';


The code before your change here is an example of the case that scares me: where the arm is on its own line and indented.

erights · 2022-06-03T02:48:01Z

packages/zoe/src/contracts/sellItems.js

-      throw buyerSeat.fail(new Error(rejectMsg));
+      throw buyerSeat.fail(assert.fail(rejectMsg));


Better would be assert.error. Like Error(...) it makes and returns an error. Like the other assert methods, you can use an

X`literal stuff ${redacted value}`

for better diagnostics. Also, all the assert methods create the error object at the same line of code that becomes a useful place to put a breakpoint.

erights · 2022-06-03T02:48:36Z

packages/zoe/src/contracts/simpleExchange.js

-      new Error(`The proposal did not match either a buy or sell order.`),
+      assert.fail(`The proposal did not match either a buy or sell order.`),


Or assert.error

erights · 2022-06-11T19:31:22Z

What is the status of this? Is there at least an easy subset that could move forward quickly?

turadg · 2022-06-12T00:45:38Z

What is the status of this?

It's a draft PR that passes 5 out of 30 CI checks. It doesn't have a ticket and if it did I don't think it would be required for MN-1, so it's prioritized behind MN-1 release.

Is there at least an easy subset that could move forward quickly?

Probably the jessie.js update. Any files that had @jessie-check added and aren't erroring.

Again, TMK it's not required for MN-1 but if it is let's prioritize it.

erights · 2022-06-12T00:50:05Z

It's not

turadg added 3 commits June 2, 2022 05:44

jessie-check all contracts

d54393a

chore: bump @jessie.js/eslint-plugin

0d79bf5

chore: jessie-check fixes

3480754

turadg requested review from dckc and erights June 2, 2022 13:09

dckc requested changes Jun 2, 2022

View reviewed changes

erights approved these changes Jun 3, 2022

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

jessie-check contracts #5497

jessie-check contracts #5497

turadg commented Jun 2, 2022

dckc left a comment

dckc Jun 2, 2022

turadg Jun 2, 2022

dckc Jun 2, 2022

turadg Jun 2, 2022 •

edited

Loading

dckc Jun 2, 2022

erights Jun 3, 2022

erights Jun 3, 2022

dckc Jun 2, 2022

erights Jun 3, 2022

dckc Jun 2, 2022

turadg Jun 2, 2022

dckc Jun 2, 2022

erights Jun 3, 2022

dckc Jun 2, 2022

erights Jun 3, 2022

dckc Jun 2, 2022

erights Jun 3, 2022

erights left a comment

erights Jun 3, 2022

erights Jun 3, 2022

erights Jun 3, 2022

erights Jun 3, 2022

michaelfig Jun 3, 2022

erights Jun 3, 2022

erights Jun 3, 2022 •

edited

Loading

erights Jun 3, 2022

erights Jun 3, 2022

erights commented Jun 11, 2022

turadg commented Jun 12, 2022

erights commented Jun 12, 2022

		collateralSeat.getCurrentAllocation()[collateralKeyword],
		collateralSeat.getCurrentAllocation()[+collateralKeyword],

		throw new Error('insufficient reserves for that transaction');
		throw assert.fail('insufficient reserves for that transaction');

		throw buyerSeat.fail(new Error(rejectMsg));
		throw buyerSeat.fail(assert.fail(rejectMsg));

		new Error(`The proposal did not match either a buy or sell order.`),
		assert.fail(`The proposal did not match either a buy or sell order.`),

jessie-check contracts #5497

Are you sure you want to change the base?

jessie-check contracts #5497

Conversation

turadg commented Jun 2, 2022

Description

Security Considerations

Documentation Considerations

Testing Considerations

dckc left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

turadg Jun 2, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

erights left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

erights Jun 3, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

erights commented Jun 11, 2022

turadg commented Jun 12, 2022

erights commented Jun 12, 2022

turadg Jun 2, 2022 •

edited

Loading

erights Jun 3, 2022 •

edited

Loading