OpenSC

A toy project of programming language for smart contract written in Ocaml. This is final project for COMS W4115 programming language & translator @ Columbia.

Introduction

OpenSC is a functional programming language which has similar functionality compared to Scilla and Pact. It is statically typed and will support several features. It is a high-level language that will be primarily used to implement smart contracts, which are programs that provide protocol for handling account behavior in Ethereum.

Compared to other languages, we model contracts as some simple transition systems, with the transitions being pure functions of the contract state. These functions are expressed from one state to another state in a list of storage mutations.

Inspired by the MiniC language, part of the DeepSEA compiler, we aim to develop a language which allows interactive formal verification of smart contracts with security guarantees. From a specific input program, the compiler generates executable bytecode, as well as a model of the program that can be loaded into the Coq proof assistant. Our eventual goal is that smart contracts like storage, auction and token can be written by OpenSC, and that these contracts can be compiled via the translator into binary codes that can be executed on EVM.

Structure

Translator Architecture

Translate Details

Code Structure

• src/opensc.ml is the top-level program of the compiler
• A src/Makefile is included to automate the compilation of the compiler

Usage

Environment Dependencies

• Install ocaml, which is what our translator is written in.
• Install opam, the ocaml package manager
• opam install cryptokit, which is used in the Minic (IR code) generation phase of the compiler front-end for cryptographic hashing

Synopsis

# at root directory of OpenSC
cd src && Make
./opensc.native [source.sc] [mode]

Modes

• ast
  • generate raw AST and print its structure
• sast
  • generate SAST (semantically checked AST) and print its structure
• minic
  • generate Minic AST (the IR code) and print its structure
• bytecode
  • generate EVM bytecode and print it

How to test

command

# at root directory of OpenSC
% cd src
# compile opensc
% make
ocamlbuild -pkg cryptokit -I backend opensc.native
# run opensc
% ./opensc.native [path to source.sc] [mode] 
# mode : ast | sast | minic | bytecode

example program sources for test

• example_contract/simpleStorage.sc
• example_contract/simpleToken.sc

run bytecode on EVM

install dependencies

• install and use node 12
• install ganache-cli, ethers
• open ganache-cli

run bytecode on EVM

# at root directory of OpenSC
% cd src/example_contract
./test-simpleStorage.js simpleStorage.bytecode
./test-simpleToken.js simpleToken.bytecode

Reference Manual

Check our Language Reference Manual for detailed usage

WARNING: We are not supporting multi-key mapping, events and log functions.

TODO

• Constructor
• Ethernum Event and log
• Guard statement
• Single-key mapping
• Multi-key mapping
• Multiple objects
• Control flow statement (if, for statement)

Presentation

• Proposal: proposal pdf
• Report: report pdf
• Language Reference Manual: LRM
• Presentation: presetation slides

Contribution

• scanner: Linghan Kong, Chong Hu
• parser: Linghan Kong, Chong Hu, Jun Sha
• AST design: Linghan Kong, Ruibin Ma, Chong Hu
• SAST design：: Linghan Kong, Ruibin Ma, Chong Hu
• semantic analysis： Chong Hu, Linghan Kong, Ruibin Ma, Jun Sha
• translate MiniC: Ruibin Ma, Linghan Kong, Chong Hu, Jun sha

Acknowledgements

Thanks to Professor Ronghui Gu, the instructor of our course, who brought us to the PLT world and let us realize the charm of functional programming and formal verification, both of which are what our project is based on.

Thanks to River Dillon Keefer and Amanda Liu, TAs of our course, who introduced the DeepSEA project to us and provided very inspiring and helpful ideas on the OpenSC language syntax among other project details.

Thanks to Vilhelm Sjöberg, our project advisor, researcher at Yale and the primary creator of the DeepSEA project, who provided us with great information on everything about the DeepSEA project, and answered our many questions, which has been super helpful.

Contact

• Jun Sha js5506: email
• Linghan Kong lk2811: email
• Ruibin Ma rm3708: email
• Chong Hu ch3467: email

License

Copyright (c) 2020, OpenSC. All rights reserved.

The code is distributed under a MIT license. See LICENSE for information.