Run Phil in your browser

Show the introduction again

What this is

A browser playground for Phil, a systems language where architecture is executable and implementation is replaceable. The editor checks your code against Phil's official Grammar v1 as you type, using the same checker as the Phil VS Code extension.

Built by the Philcoin community

This playground is a community tool. It is not part of, or endorsed by, the Phil project or its authors.

The simulator is unofficial

Phil's own compiler cannot run real programs yet, so Run uses an experimental interpreter built from the Phil tour and design documents. Where Phil proves things at compile time, the simulator checks them while the program runs:

• Ownership: linear values must be used exactly once, affine values at most once. Protocol endpoints are linear.
• Protocols: every send, receive, select, offer and close must match the next step of the role's protocol.
• Contracts: requires before each call, ensures after it, refinement types when values are bound, loop and join invariants, and prove(...).
• Arithmetic: fixed-width integers never wrap. Overflow, underflow and division by zero stop the program.
• Processes declared in an architecture run concurrently with synchronous messages. If nobody can move, that is reported as a deadlock.

A program the simulator runs can still be rejected by the real Phil checker, and the other way round.

Simulator choices that are not Phil

Ordinary Phil expressions have no comparison operators, so the simulator provides these host operations:

• Inside an offer arm, the offered endpoint's name refers to its next state.
• A role marked external is played by an automatic peer that sends default values and picks the first branch.
• Effects, authority, providers, generics and byte-level operations (recognize, validate, receive_exact…) are accepted by the checker but not executed.

Hunt, Design and puzzles

• Hunt tries boundary values for every entry, several process orders and several strategies for external peers. With no runnable program it calls each function on generated arguments. Finding nothing is not a proof.
• Design generates a full program from a list of messages.
• Puzzles (in the example menu) are broken programs. One is solved when it runs to completion and a hunt finds nothing.
• Under the sequence diagram, each process shows the linear and affine values it owns at the current replay step.

Keyboard

• Ctrl/⌘ + Enter run · Ctrl/⌘ + / toggle comment · Tab / Shift + Tab indent · Shift + Alt + F format

Your code

Edits are kept in this browser for each example. Reset restores the original. Open file loads a .phil file into the scratch pad.