Skip to content

Commit

Permalink
feat: refine capabilities (#4406)
Browse files Browse the repository at this point in the history
Improved capability system, introducing a synchronous (`system`) capability.

The `actor` initialisation body, `pre`/`postupgrade` hooks, `async` function bodies (and
blocks) possess this capability. Functions (and classes) can demand it by prepending `system`
to the type argument list. The capability can be forwarded in calls by mentioning `<system, …>`
in the instantiation parameter list.
  • Loading branch information
ggreif authored Mar 5, 2024
1 parent 01efc2a commit c30c898
Show file tree
Hide file tree
Showing 59 changed files with 581 additions and 242 deletions.
13 changes: 12 additions & 1 deletion Changelog.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,20 @@

**Limitations**: recursive and mutually recursive definitions are considered used,
even if never referenced outside the recursive definition.

* Remove `__get_candid_interface_tmp_hack` endpoint. Candid interface is already stored as canister metadata, this temporary endpoint is redundant, thus removed. (#4386)

* Improved capability system, introducing a synchronous (`system`) capability (#4406).

`actor` initialisation body, `pre`/`postupgrade` hooks, `async` function bodies (and
blocks) possess this capability. Functions (and classes) can demand it by prepending `system`
to the type argument list. The capability can be forwarded in calls by mentioning `<system, …>`
in the instantiation parameter list.

BREAKING CHANGE (Minor): A few built-in functions have been marked with demand
for the `system` capability. In order to call these, the full call hierarchy needs to be
adapted to pass the `system` capability.

## 0.10.4 (2024-01-10)

* motoko (`moc`)
Expand Down
14 changes: 6 additions & 8 deletions doc/md/base/List.md
Original file line number Diff line number Diff line change
Expand Up @@ -162,9 +162,7 @@ sum // => 3

Runtime: O(size)

Space: O(size)

*Runtime and space assumes that `f` runs in O(1) time and space.
Space: O(1)

## Function `map`
``` motoko no-repl
Expand Down Expand Up @@ -221,8 +219,6 @@ Runtime: O(size)

Space: O(size)

*Runtime and space assumes that `f` runs in O(1) time and space.

## Function `mapFilter`
``` motoko no-repl
func mapFilter<T, U>(l : List<T>, f : T -> ?U) : List<U>
Expand All @@ -249,8 +245,6 @@ Runtime: O(size)

Space: O(size)

*Runtime and space assumes that `f` runs in O(1) time and space.

## Function `mapResult`
``` motoko no-repl
func mapResult<T, R, E>(xs : List<T>, f : T -> Result.Result<R, E>) : Result.Result<List<R>, E>
Expand Down Expand Up @@ -660,7 +654,7 @@ Runtime: O(min(size(xs), size(ys)))

Space: O(min(size(xs), size(ys)))

*Runtime and space assumes that `f` runs in O(1) time and space.
*Runtime and space assumes that `zip` runs in O(1) time and space.

## Function `split`
``` motoko no-repl
Expand All @@ -681,6 +675,8 @@ Runtime: O(n)

Space: O(n)

*Runtime and space assumes that `zip` runs in O(1) time and space.

## Function `chunks`
``` motoko no-repl
func chunks<T>(n : Nat, xs : List<T>) : List<List<T>>
Expand All @@ -707,6 +703,8 @@ Runtime: O(size)

Space: O(size)

*Runtime and space assumes that `zip` runs in O(1) time and space.

## Function `fromArray`
``` motoko no-repl
func fromArray<T>(xs : [T]) : List<T>
Expand Down
7 changes: 0 additions & 7 deletions doc/md/base/Option.md
Original file line number Diff line number Diff line change
Expand Up @@ -124,13 +124,6 @@ func isNull(x : ?Any) : Bool

Returns true if the argument is `null`, otherwise returns false.

## Function `equal`
``` motoko no-repl
func equal<A>(x : ?A, y : ?A, eq : (A, A) -> Bool) : Bool
```

Returns true if the optional arguments are equal according to the equality function provided, otherwise returns false.

## Function `assertSome`
``` motoko no-repl
func assertSome(x : ?Any)
Expand Down
4 changes: 2 additions & 2 deletions doc/md/base/Trie.md
Original file line number Diff line number Diff line change
Expand Up @@ -546,7 +546,7 @@ Build sequence of two sub-builds

### Function `prod`
``` motoko no-repl
func prod<K1, V1, K2, V2, K3, V3>(tl : Trie<K1, V1>, tr : Trie<K2, V2>, op : (K1, V1, K2, V2) -> ?(K3, V3), _k3_eq : (K3, K3) -> Bool) : Build<K3, V3>
func prod<K1, V1, K2, V2, K3, V3>(tl : Trie<K1, V1>, tr : Trie<K2, V2>, op : (K1, V1, K2, V2) -> ?(K3, V3), k3_eq : (K3, K3) -> Bool) : Build<K3, V3>
```

Like [`prod`](#prod), except do not actually do the put calls, just
Expand Down Expand Up @@ -920,7 +920,7 @@ new trie, and the prior value, if any.

## Function `mergeDisjoint2D`
``` motoko no-repl
func mergeDisjoint2D<K1, K2, V>(t : Trie2D<K1, K2, V>, _k1_eq : (K1, K1) -> Bool, k2_eq : (K2, K2) -> Bool) : Trie<K2, V>
func mergeDisjoint2D<K1, K2, V>(t : Trie2D<K1, K2, V>, k1_eq : (K1, K1) -> Bool, k2_eq : (K2, K2) -> Bool) : Trie<K2, V>
```

Like [`mergeDisjoint`](#mergedisjoint), except instead of merging a
Expand Down
8 changes: 4 additions & 4 deletions doc/md/examples/Alice.mo
Original file line number Diff line number Diff line change
Expand Up @@ -5,12 +5,12 @@ actor Alice {

public func test() : async () {

Cycles.add(10_000_000_000_000);
Cycles.add<system>(10_000_000_000_000);
let porky = await Lib.PiggyBank(Alice.credit, 1_000_000_000);

assert (0 == (await porky.getSavings()));

Cycles.add(1_000_000);
Cycles.add<system>(1_000_000);
await porky.deposit();
assert (1_000_000 == (await porky.getSavings()));

Expand All @@ -20,7 +20,7 @@ actor Alice {
await porky.withdraw(500_000);
assert (0 == (await porky.getSavings()));

Cycles.add(2_000_000_000);
Cycles.add<system>(2_000_000_000);
await porky.deposit();
let refund = Cycles.refunded();
assert (1_000_000_000 == refund);
Expand All @@ -31,7 +31,7 @@ actor Alice {
// Callback for accepting cycles from PiggyBank
public func credit() : async () {
let available = Cycles.available();
let accepted = Cycles.accept(available);
let accepted = Cycles.accept<system>(available);
assert (accepted == available);
}

Expand Down
4 changes: 2 additions & 2 deletions doc/md/examples/PiggyBank.mo
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ shared(msg) actor class PiggyBank(
let acceptable =
if (amount <= limit) amount
else limit;
let accepted = Cycles.accept(acceptable);
let accepted = Cycles.accept<system>(acceptable);
assert (accepted == acceptable);
savings += acceptable;
};
Expand All @@ -29,7 +29,7 @@ shared(msg) actor class PiggyBank(
: async () {
assert (msg.caller == owner);
assert (amount <= savings);
Cycles.add(amount);
Cycles.add<system>(amount);
await benefit();
let refund = Cycles.refunded();
savings -= amount - refund;
Expand Down
4 changes: 2 additions & 2 deletions doc/md/examples/Reminder.mo
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,9 @@ actor Reminder {
print("Happy New Year!");
};

ignore setTimer(#seconds (solarYearSeconds - abs(now() / 1_000_000_000) % solarYearSeconds),
ignore setTimer<system>(#seconds (solarYearSeconds - abs(now() / 1_000_000_000) % solarYearSeconds),
func () : async () {
ignore recurringTimer(#seconds solarYearSeconds, remind);
ignore recurringTimer<system>(#seconds solarYearSeconds, remind);
await remind();
});
}
19 changes: 14 additions & 5 deletions doc/md/examples/grammar.txt
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@

<typ_nobin> ::=
<typ_pre>
<func_sort_opt> ('<' <list(<typ_bind>, ',')> '>')? <typ_un> '->' <typ_nobin>
<func_sort_opt> <typ_params_opt> <typ_un> '->' <typ_nobin>

<typ> ::=
<typ_nobin>
Expand All @@ -66,10 +66,19 @@
<typ_args> ::=
'<' <list(<typ>, ',')> '>'

<inst> ::=
<empty>
'<' <list(<typ>, ',')> '>'
'<' 'system' (',' <typ>)* '>'

<typ_params_opt> ::=
('<' <list(<typ_bind>, ',')> '>')?
'<' 'system' (',' <typ_bind>)* '>'

<typ_field> ::=
'type' <id> ('<' <list(<typ_bind>, ',')> '>')? '=' <typ>
'var'? <id> ':' <typ>
<id> ('<' <list(<typ_bind>, ',')> '>')? <typ_nullary> ':' <typ>
<id> <typ_params_opt> <typ_nullary> ':' <typ>

<typ_tag> ::=
'#' <id> (':' <typ>)?
Expand Down Expand Up @@ -165,7 +174,7 @@
<exp_post> '[' <exp> ']'
<exp_post> '.'<nat>
<exp_post> '.' <id>
<exp_post> ('<' <list(<typ>, ',')> '>')? <exp_nullary>
<exp_post> <inst> <exp_nullary>
<exp_post> '!'
'(' 'system' <exp_post> '.' <id> ')'

Expand Down Expand Up @@ -293,8 +302,8 @@
'let' <pat> '=' <exp>
'type' <id> ('<' <list(<typ_bind>, ',')> '>')? '=' <typ>
<obj_sort> <id>? (':' <typ>)? '='? <obj_body>
<shared_pat_opt> 'func' <id>? ('<' <list(<typ_bind>, ',')> '>')? <pat_plain> (':' <typ>)? <func_body>
<shared_pat_opt> <obj_sort>? 'class' <id>? ('<' <list(<typ_bind>, ',')> '>')? <pat_plain> (':' <typ>)? <class_body>
<shared_pat_opt> 'func' <id>? <typ_params_opt> <pat_plain> (':' <typ>)? <func_body>
<shared_pat_opt> <obj_sort>? 'class' <id>? <typ_params_opt> <pat_plain> (':' <typ>)? <class_body>

<dec> ::=
<dec_var>
Expand Down
67 changes: 54 additions & 13 deletions doc/md/language-manual.md
Original file line number Diff line number Diff line change
Expand Up @@ -398,7 +398,7 @@ The syntax of a *declaration* is as follows:
var <id> (: <typ>)? = <exp> mutable
<sort> <id>? (: <typ>)? =? <obj-body> object
<shared-pat>? func <id>? <typ-params>? <pat> (: <typ>)? =? <exp> function
type <id> <typ-params>? = <typ> type
type <id> <type-typ-params>? = <typ> type
<shared-pat>? <sort>? class class
<id>? <typ-params>? <pat> (: <typ>)? <class-body>
Expand Down Expand Up @@ -556,7 +556,7 @@ Type expressions are used to specify the types of arguments, constraints (a.k.a

``` bnf
<typ> ::= type expressions
<path> <typ-args>? constructor
<path> <type-typ-args>? constructor
<sort>? { <typ-field>;* } object
{ <typ-tag>;* } variant
{ # } empty variant
Expand Down Expand Up @@ -758,7 +758,7 @@ See [Stable Regions](stable-regions.md) and library [Region](./base/Region.md) f

### Constructed types

`<path> <typ-args>?` is the application of a type identifier or path, either built-in (i.e. `Int`) or user defined, to zero or more type **arguments**. The type arguments must satisfy the bounds, if any, expected by the type constructor’s type parameters (see [Well-formed types](#well-formed-types)).
`<path> <type-typ-args>?` is the application of a type identifier or path, either built-in (i.e. `Int`) or user defined, to zero or more type **arguments**. The type arguments must satisfy the bounds, if any, expected by the type constructor’s type parameters (see [Well-formed types](#well-formed-types)).

Though typically a type identifier, more generally, `<path>` may be a `.`-separated sequence of actor, object or module identifiers ending in an identifier accessing a type component of a value (for example, `Acme.Collections.List`).

Expand Down Expand Up @@ -867,7 +867,7 @@ In all other positions, `( <typ> )` has the same meaning as `<typ>`.
<id> : <typ> immutable value
var <id> : <typ> mutable value
<id> <typ-params>? <typ1> : <typ2> function value (short-hand)
type <id> <typ-params>? = <typ> type component
type <id> <type-typ-params>? = <typ> type component
```

A type field specifies the name and type of a value field of an object, or the name and definition of a type component of an object. The value field names within a single object type must be distinct and have non-colliding hashes. The type component names within a single object type must also be distinct and have non-colliding hashes. Value fields and type components reside in separate name spaces and thus may have names in common.
Expand All @@ -876,7 +876,7 @@ A type field specifies the name and type of a value field of an object, or the n

`var <id> : <typ>` specifies a *mutable* field, named `<id>` of type `<typ>`.

`type <id> <typ-params>? = <typ>` specifies a *type* component, with field name `<id>`, abbreviating (parameterized) type `<typ>`.
`type <id> <type-typ-params>? = <typ>` specifies a *type* component, with field name `<id>`, abbreviating (parameterized) type `<typ>`.

Unlike type declarations, a type component is not, in itself, recursive (though it may abbreviate an existing recursive type).
In particular, the name `<id>` is not bound in `<typ>` nor in any other fields of the enclosing object type. The name `<id>` only determines the label to use when accessing the definition through a record of this type (using the dot notation).
Expand Down Expand Up @@ -910,7 +910,24 @@ When enclosed by a non-`actor` object type, `<id> <typ-params>? <typ1> : <typ2>`
<id> unconstrained type parameter
```

A type constructors, function value or function type may be parameterised by a vector of comma-separated, optionally constrained, type parameters.
``` bnf
<type-typ-params> ::= type parameters to type constructors
< typ-param,* >
<typ-params> ::= function type parameters
< typ-param,* > type parameters
< system (, <typ-param>*)) > system capability prefixed type parameters
<typ-param>
<id> <: <typ> constrained type parameter
<id> unconstrained type parameter
```

A type constructor may be parameterised by a vector of comma-separated, optionally constrained, type parameters.

A function, class constructor or function type may be parameterised by a vector of comma-separated, optionally constrained, type parameters.
The first of these may be the special, pseudo type parameter `system`.

`<id> <: <typ>` declares a type parameter with constraint `<typ>`. Any instantiation of `<id>` must subtype `<typ>` (at that same instantiation).

Expand All @@ -920,11 +937,20 @@ The names of type parameters in a vector must be distinct.

All type parameters declared in a vector are in scope within its bounds.

The `system` pseudo-type parameter on function types indicates that a value of that type
requires `system` capability in order to be called and may itself call functions requiring `system` capability during its execution.

### Type arguments

``` bnf
<typ-args> ::= type arguments
<type-typ-args> ::= type arguments to type constructors
< <typ>,* >
<typ-args> ::= type arguments to functions
< <typ>,* > plain type arguments
< system (, <typ>*) > system capability prefixed type arguments
```

Type constructors and functions may take type arguments.
Expand All @@ -935,6 +961,20 @@ For a function, the number of type arguments, when provided, must agree with the

Given a vector of type arguments instantiating a vector of type parameters, each type argument must satisfy the instantiated bounds of the corresponding type parameter.

In function calls, supplying the `system` pseudo type argument grants system capability to the function that requires it.

System capability is available only in the following syntactic contexts:

- in the body of an actor expression or actor class;
- in the body of a (non-`query`) `shared` function, asynchronous function, `async` expression or `async*` expression;
- in the body of a function or class that is declared with `system` pseudo type parameter;
- in system functions `preupgrade` and `postupgrade`.

No other context provides `system` capabilities, including `query` and `composite query` methods.

The `<system>` type parameters of shared and asynchronous functions need not be declared.


### Well-formed types

A type `T` is well-formed only if (recursively) its constituent types are well-formed, and:
Expand Down Expand Up @@ -1265,8 +1305,8 @@ The declaration `<dec>` of a `system` field must be a manifest `func` declaratio
| `heartbeat` | `() -> async ()` | heartbeat action |
| `timer` | `(Nat64 -> ()) -> async ()` | timer action |
| `inspect` | `{ caller : Principal; msg : <Variant>; arg : Blob } -> Bool` | message predicate |
| `preupgrade` | `() -> ()` | pre upgrade action |
| `postupgrade` | `() -> ()` | post upgrade action |
| `preupgrade` | `<system>() -> ()` | pre upgrade action |
| `postupgrade` | `<system>() -> ()` | post upgrade action |

- `heartbeat`, when declared, is called on every Internet Computer subnet **heartbeat**, scheduling an asynchronous call to the `heartbeat` function. Due to its `async` return type, a heartbeat function may send messages and await results. The result of a heartbeat call, including any trap or thrown error, is ignored. The implicit context switch means that the time the heartbeat body is executed may be later than the time the heartbeat was issued by the subnet.

Expand All @@ -1275,8 +1315,9 @@ The declaration `<dec>` of a `system` field must be a manifest `func` declaratio
- `inspect`, when declared, is called as a predicate on every Internet Computer ingress message (with the exception of HTTP query calls). The return value, a `Bool`, indicates whether to accept or decline the given message. The argument type depends on the interface of the enclosing actor (see [Inspect](#inspect)).

- `preupgrade`, when declared, is called during an upgrade, immediately *before* the (current) values of the (retired) actor’s stable variables are transferred to the replacement actor.
Its `<system>` type parameter is implicitly assumed and need not be declared.

- `postupgrade`, when declared, is called during an upgrade, immediately *after* the (replacement) actor body has initialized its fields (inheriting values of the retired actors' stable variables), and before its first message is processed.
- `postupgrade`, when declared, is called during an upgrade, immediately *after* the (replacement) actor body has initialized its fields (inheriting values of the retired actors' stable variables), and before its first message is processed. Its `<system>` type parameter is implicitly assumed and need not be declared.

These `preupgrade` and `postupgrade` system methods provide the opportunity to save and restore in-flight data structures (e.g. caches) that are better represented using non-stable types.

Expand Down Expand Up @@ -1481,7 +1522,7 @@ Evaluation of `var <id> (: <typ>)? = <exp>` proceeds by evaluating `<exp>` to a

### Type declaration

The declaration `type <id> <typ-params>? = <typ>` declares a new type constructor `<id>`, with optional type parameters `<typ-params>` and definition `<typ>`.
The declaration `type <id> <type-typ-params>? = <typ>` declares a new type constructor `<id>`, with optional type parameters `<type-typ-params>` and definition `<typ>`.

The declaration `type C< X0 <: T0, …​, Xn <: Tn > = U` is well-formed provided:

Expand Down Expand Up @@ -1698,7 +1739,7 @@ The *class* declaration `<shared-pat>? <sort>? class <id>? <typ-params>? <pat> (

``` bnf
<shared-pat>? <sort>? class <id> <typ-params>? <pat> (: <typ>)? <class-body> :=
type <id> <typ-params> = <sort> { <typ-field>;* };
type <id> <type-typ-params>? = <sort> { <typ-field>;* };
<shared-pat>? func <id> <typ-params>? <pat> : async? <id> <typ-args> =
async? <sort> <id_this>? <obj-body>
```
Expand All @@ -1707,7 +1748,7 @@ where:

- `<shared-pat>?`, when present, requires `<sort>` == `actor`, and provides access to the `caller` of an `actor` constructor, and

- `<typ-args>?` is the sequence of type identifiers bound by `<typ-params>?` (if any), and
- `<typ-args>?` and `<type-typ-params>?` is the sequence of type identifiers bound by `<typ-params>?` (if any), and

- `<typ-field>;*` is the set of public field types inferred from `<dec-field>;*`.

Expand Down
6 changes: 3 additions & 3 deletions nix/sources.json
Original file line number Diff line number Diff line change
Expand Up @@ -75,10 +75,10 @@
"homepage": null,
"owner": "dfinity",
"repo": "motoko-base",
"rev": "712d0587b0c8d2958adf450bd2e1554f2b0ff258",
"sha256": "17ghrfgzwlz7hbapy4sq9wbckxqy4xmcj8jpqv68bng9s83zvvvn",
"rev": "c7774995a5e271339dff11e16474ece959cc4b60",
"sha256": "10zfybm940bdbx1a1z614127r8bnjrxyq3qm6d3zn27l32y248k4",
"type": "tarball",
"url": "https://github.com/dfinity/motoko-base/archive/712d0587b0c8d2958adf450bd2e1554f2b0ff258.tar.gz",
"url": "https://github.com/dfinity/motoko-base/archive/c7774995a5e271339dff11e16474ece959cc4b60.tar.gz",
"url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
},
"motoko-matchers": {
Expand Down
Loading

0 comments on commit c30c898

Please sign in to comment.