Behavioral types for rholang

[leithaus]

Description: Implement Spatial-Behavioral types for Rholang

Motivation/Impact/Importance: offers compile-time correctness for a broad range of safety, liveness, and security properties. Completion/Success Criteria: Type check code after parsing, but before interpreting, report typing errors if encountered and prevent deployment, otherwise allow deployment. Bonus points: 1. Provide line-number info. Link to specs and additional info : Namespace logic paper. Rhocaml implementation. Spatial logic model checker.

Current Interpreter code https://github.com/rchain/rchain/tree/dev/rholang/src/main/scala/coop/rchain/rholang https://github.com/rchain/rchain/tree/dev/rholang (The read.me needs a review and may be old)

Mentors : @leithaus

Team :

Skills : Scala required, Rholang knowledge helps. Interest in implementing translators, interpreters, compilers etc.

Judgment criteria :

Rchain Priority :

[dckc]

A type checker that only integrates with dev tools and not rnode would still be useful, to me. I started on something in https://github.com/rchain-community/behavr ... it's not at all clear to me how to integrate modal operators into rhocaml. Is that published anywhere?

In fact, a simple HM type checker that would find problems with strings passed where integers are expected would be useful.

e.g. https://gist.github.com/oxyflour/f98432aa400daa225d04 https://gist.github.com/dckc/30cdcfde271cf7f02f2e1e13984f7b30

[dckc]

Another chunk of work that might fit in a small amount of time is doing a somewhat manual typecheck of some existing contracts. For example, RevVault.rho or NonNegativeNumber.rho.

Proving that methods such as .hexToBytes() are called with correct arguments seems tricky. Using SMT solvers is the only technique I know for handling that sort of thing.

[dckc]

notes...

just use the pattern matcher for type checking, for a bounded scope

---

DC: suppose T is that type for a live server... do we have syntax yet? or would it be contract abc(x : T) = { ... }

@leithaus not yet; we'd enhance the syntax. I sketched a syntax in a 2016 draft:

• Contracts, composition, and scaling The rholang 0.1 specification 3 Aug 2016 Lucius Gregory Meredith, Jack Pettersson, Ed Eykholt, Gary Stephenson

<property> ::= property <name> ( <var> [, <var>]* ) = <type>
<type> ::= true
    | ~<type>
        ...

DC: is that like a construct from SLMC? LGM: a little. in SLMC, you make assertions. Here we decorate things such as contracts. DC: I'm starting to see; a few concrete examples would help. LGM: sure; I can do that.