types for Correct-by-Construction contracts

[golovach-ivan]

This is a general task for combining other tasks and tracking their status.

The main objective

Develop software that is able to test the basic properties (written as Namespace Logic formulas) for basic contracts written in RHO-Lang.

Stages

• [ ] Step I: checking Hennessy-Milner Logic formulas for CCS Processes (DONE: 50%)
• [ ] Step II: checking Spatial Logic formulas for Pi-Calculi Processes
• [ ] Step III: checking Namespace Logic formulas for RHO-Calculi Processes
• [ ] Step IV: checking "Typed Namespace" Logic formulas for RHO-Lang Processes OR Namespace Logic formulas and RHO-lang translation to RHO-Calculi

[golovach-ivan]

Add sources Correct-by-Construction

[deannald]

Hi Ivan, what are you hoping to get out of this particular issue (and the individual Steps listed above)? How do you see this work being of value to the rest of the community? Or is there a Core Dev task that this links to?

[David405]

@golovach-ivan please see my comment in #836

[dckc]

@deannald this looks to me like a big part of the RChain value proposition: the ability to typecheck contracts for basic properties such as "doesn't leak this unforgeable name" or "has no races" (cf. DAO hack). (IOU references to details). I tweaked the title to clarify. I hope that's consistent with what you had in mind, @golovach-ivan .

I suppose it depends on a lot of work that the core dev team is yet to do, but I see no problem getting a head start.

[dckc]

I encourage progress on this issue, but at least for July, the work was done in sub-issue #836. So I put $0 in July budget votes for this issue to keep it off the overdue task approval audit.

[golovach-ivan]

The main goal of this issue - create tool (command-line + web interfaces) that can formally verify RhoLang contracts. It means check satisfaction of RhoLang contract to Namespace Logic formulae.

Facts:

• RhoLang is extension of RhoCalculi
• RhoCalculi is extension of Pi-calculi
• Pi-calculi is extension of CCS
• Namespace Logic is extension of Caires/Cardelli Logic
• Caires/Cardelli Logic is extension of Hennessy-Milner Logic

So work can be done in 6 Milestones:

1. Implement checking CCS Process satisfaction to Hennessy-Milner Logic formulae
2. Implement checking Pi-Calculi Process satisfaction to Caires/Cardelli Logic formulae
3. Implement checking Rho-Calculi Process satisfaction to Namespace Logic formulae
4. Implement checking RhoLang Contract satisfaction to Namespace Logic formulae
5. Create Commant-line tool
6. Create Web-interface