Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Celestial #272

Open
wants to merge 66 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
66 commits
Select commit Hold shift + click to select a range
15e89de
celestial: initial commit
Sep 20, 2020
c68bbca
Add support built-in crypto functions
samvid25 Sep 22, 2020
6a9f8a3
Add support for tx.origin
samvid25 Sep 22, 2020
7f3b310
Add support for block level functions, deprecate 'now', fix bug with …
samvid25 Sep 24, 2020
7a0bb93
Update Makefile for the new repo
samvid25 Sep 25, 2020
9a61372
Change event send syntax to 'emit', fix bugs
samvid25 Sep 25, 2020
d193278
Add number of event payloads check
samvid25 Sep 25, 2020
80d037a
Fix bug - remove extra address payload in generated Solidity
samvid25 Sep 25, 2020
7014132
Update examples
samvid25 Sep 25, 2020
e1c59e3
Merge pull request #1 from suvamM/change_event_syntax
samvid25 Sep 25, 2020
d42c506
adding BinanceCoin Sample
chandrikabhardwaj Sep 29, 2020
8558989
cleaning comments in BNB
chandrikabhardwaj Sep 29, 2020
3c04640
Update BinanceCoin.cel
chandrikabhardwaj Sep 29, 2020
a205b1b
Update BinanceCoin.cel
chandrikabhardwaj Sep 29, 2020
e703659
updating makefile for BNB
chandrikabhardwaj Sep 29, 2020
c1699b4
Merge branch 'celestial' of https://github.com/suvamM/verisol into ce…
chandrikabhardwaj Sep 29, 2020
89a8b08
BNB fstar
chandrikabhardwaj Sep 29, 2020
e4b1813
BNB acc to new compiler changes
chandrikabhardwaj Sep 29, 2020
327819e
Remove automatically adding locks, add re-entrancy reverts condition …
samvid25 Sep 29, 2020
4bff36f
Update examples
samvid25 Sep 29, 2020
5a0ea4b
Fix bug with r_reverts
samvid25 Sep 29, 2020
924a10c
Update EtherDelta
samvid25 Sep 29, 2020
c850aff
Merge pull request #2 from suvamM/add_re-ent_reverts
samvid25 Sep 29, 2020
241ae70
fixes to samples
suvamM Sep 29, 2020
a5d34da
merging
suvamM Sep 29, 2020
077deca
BNB updated
chandrikabhardwaj Sep 29, 2020
3aee538
Update Ether transfer function to .transfer()
samvid25 Sep 30, 2020
f6024b1
Update experiments
samvid25 Sep 30, 2020
4eeae29
Update SimpleAuction sample
samvid25 Sep 30, 2020
1e39300
Update BinanceCoin.cel
chandrikabhardwaj Sep 30, 2020
d320330
Update BinanceCoin.cel
chandrikabhardwaj Sep 30, 2020
94cf3c5
Change transfer semantics, add fallback support, add abi encode funct…
samvid25 Oct 1, 2020
530fc4d
Merge pull request #3 from suvamM/more_solidity_features
samvid25 Oct 1, 2020
3c9ffcd
Add Ether transfer check (changed transfer semantics)
samvid25 Oct 1, 2020
3a0ee7e
Add remaining functions in EtherDelta (WIP)
samvid25 Oct 1, 2020
3800bb0
Add missing function in OZ ERC20 (WIP)
samvid25 Oct 1, 2020
3daf2b2
Change balance decrease check
samvid25 Oct 1, 2020
3c43f52
Update examples
samvid25 Oct 1, 2020
2c39065
Update lib
samvid25 Oct 3, 2020
d8e6401
Support 'using', 'pragma' and 'call' wrapper functions
samvid25 Oct 10, 2020
57b9fc2
Update Samples
samvid25 Oct 10, 2020
ae95b63
Bug fix
samvid25 Oct 10, 2020
30748dd
wip:VeriSol-Integration
chandrikabhardwaj Oct 10, 2020
a7cf716
wip:fallbackVsReceive
chandrikabhardwaj Oct 15, 2020
51fe210
minorfix
chandrikabhardwaj Oct 15, 2020
205d6a8
updated Readme
chandrikabhardwaj Oct 15, 2020
4de9b86
update readme
chandrikabhardwaj Oct 15, 2020
7fa4f7d
update readmes
chandrikabhardwaj Oct 15, 2020
e831485
update readme
chandrikabhardwaj Oct 15, 2020
64f0241
minor fix
chandrikabhardwaj Oct 15, 2020
2374e4e
minor fix
chandrikabhardwaj Oct 15, 2020
d772b78
minor fix
chandrikabhardwaj Oct 15, 2020
af5bede
wip:readme license
chandrikabhardwaj Oct 15, 2020
a464687
wip:readme case for CELESTIAL
chandrikabhardwaj Oct 15, 2020
715a190
wip:readme lowercase for CELESTIAL
chandrikabhardwaj Oct 15, 2020
c3482fb
payable not allowed for VeriSol
chandrikabhardwaj Oct 15, 2020
ef57563
moving Celestial folder up
chandrikabhardwaj Oct 30, 2020
784b2e3
Update Overview
samvid25 May 21, 2021
6b93637
Add Celestial language documentation
samvid25 May 21, 2021
bc410f8
Update Celestial language documentation
samvid25 May 21, 2021
97b6978
Update Celestial README
samvid25 May 21, 2021
8f082b1
Update Celestial README
samvid25 May 21, 2021
d2d35ba
Update Samples/README.md and create README for each experiment and up…
samvid25 May 21, 2021
1d217da
Update Overview contract
samvid25 May 21, 2021
efaaa24
Remove original Solidity versions and some comments in the contract c…
samvid25 May 21, 2021
52c6071
Updates
samvid25 May 21, 2021
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file added Celestial/CelestialArchitecture.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
5 changes: 5 additions & 0 deletions Celestial/Compiler/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
.vscode/*

.antlr/*

__pycache__/*
168 changes: 168 additions & 0 deletions Celestial/Compiler/CelestialLexer.g4
Original file line number Diff line number Diff line change
@@ -0,0 +1,168 @@
lexer grammar CelestialLexer;

options {language=Python3;}

// Type names

ADDR : 'address' ;
BOOL : 'bool' ;
ENUM : 'enum' ;
EVENT : 'event' ;
EVENTLOG : 'eventlog' ;
UINT : 'uint' ;
UINT8 : 'uint8' ;
INSTMAP : 'inst_map' ;
INT : 'int' ;
STRING : 'string' ;
CONTRACT : 'contract' ;
MAP : 'mapping' ;
BYTES : 'bytes' ;
BYTES20 : 'bytes20' ;
BYTES32 : 'bytes32' ;

// Keywords

ADD : 'add' ;
AS : 'as' ;
ASSERT : 'assert' ;
BALANCE : 'balance' ;
BCOINBASE : 'block.coinbase' ;
BDIFF : 'block.difficulty' ;
BGASLIMIT : 'block.gaslimit' ;
BNUMBER : 'block.number' ;
BTIMESTAMP: 'block.timestamp' ;
CALL : 'call' ;
CALLBOOL : 'call_bool' ;
CALLUINT : 'call_uint' ;
CONSTANT : 'constant' ;
CONSTR : 'constructor' ;
CONTAINS : 'contains' ;
CREDIT : 'credit' ;
DEBIT : 'debit' ;
DEFAULT : 'default' ;
DELETE : 'delete' ;
ELSE : 'else' ;
EMIT : 'emit' ;
ETRANSFER : 'eTransfer' ;
EXISTS : 'exists' ;
FALLBACK : 'fallback' ;
FOR : 'for' ;
FORALL : 'forall';
FROM : 'from' ;
FUNCTION : 'function' ;
IF : 'if' ;
IMPORT : 'import' ;
IN : 'in' ;
INT_MIN : 'int_min' ;
INT_MAX : 'int_max' ;
ITE : 'ite' ;
INVARIANT : 'invariant' ;
KEYS : 'keys' ;
LEMMA : 'lemma' ;
LENGTH : 'length' ;
LOG : 'log' ;
MODIFIES : 'modifies' ;
MODIFIESA : 'modifies_addresses' ;
NEW : 'new' ;
PAYABLE : 'payable' ;
POP : 'pop' ;
POST : 'post' ;
PRAGMA : 'pragma' ;
PRE : 'pre' ;
PRINT : 'print' ;
PRIVATE : 'private' ;
PUBLIC : 'public' ;
PURE : 'pure' ;
PUSH : 'push' ;
RECEIVE : 'receive';
RETURN : 'return' ;
RETURNS : 'returns' ;
REVERT : 'revert' ;
RREVERTS : 'r_reverts' ;
SAFEADD : 'safe_add' ;
SAFEDIV : 'safe_div' ;
SAFEMOD : 'safe_mod' ;
SAFEMUL : 'safe_mul' ;
SAFESUB : 'safe_sub' ;
SEND : 'send' ;
SENDER : 'sender' ;
SPEC : 'spec' ;
STRUCT : 'struct' ;
// SUMEQ : 'sumEquals' ;
THIS : 'this' ;
TRANSFER : 'transfer' ;
TXREVERTS : 'tx_reverts' ;
TXGASPRICE: 'tx.gasprice' ;
TXORIGIN : 'tx.origin' ;
UINT_MAX : 'uint_max' ;
USING : 'using' ;
VALUE : 'value' ;
VIEW : 'view' ;

// Literals

BoolLiteral : 'true' | 'false' ;

IntLiteral : [0-9]+ ;

NullLiteral : 'null';

StringLiteral : '"' StringCharacters? '"' ;
fragment StringCharacters : StringCharacter+ ;
fragment StringCharacter : ~["\\] | EscapeSequence ;
fragment EscapeSequence : '\\' . ;

VersionLiteral : [0-9]+ '.' [0-9]+ ('.' [0-9]+)? ;

// Symbols

LNOT : '!' ;
LAND : '&&' ;
LOR : '||' ;
MAPUPD : '=>' ;
IMPL : '==>' ;
BIMPL : '<==>' ;

EQ : '==' ;
NE : '!=' ;
LE : '<=' ;
GE : '>=' ;
LT : '<' ;
GT : '>' ;
RARROW : '->' ;

ASSIGN : '=' ;
INSERT : '+=' ;
REMOVE : '-=' ;

PLUS : '+' ;
SUB : '-' ;
MUL : '*' ;
DIV : '/' ;
MOD : '%' ;

CARET : '^' ;
BNOT : '~' ;

LBRACE : '{' ;
RBRACE : '}' ;
LBRACK : '[' ;
RBRACK : ']' ;
LPAREN : '(' ;
RPAREN : ')' ;
SEMI : ';' ;
COMMA : ',' ;
DOT : '.' ;
COLON : ':' ;

// Identifiers

Iden : PLetter PLetterOrDigit* ;
fragment PLetter : [a-zA-Z_] ;
fragment PLetterOrDigit : [a-zA-Z0-9_] ;

// Non-code regions

Whitespace : [ \t\r\n\f]+ -> skip ;
BlockComment : '/*' .*? '*/' -> channel(HIDDEN) ;
LineComment : '//' ~[\r\n]* -> channel(HIDDEN) ;
Loading