Skip to content

Instantly share code, notes, and snippets.

View nrryuya's full-sized avatar

Ryuya Nakamura nrryuya

57 followers · 0 following
View GitHub Profile
@nrryuya
nrryuya / cbc_casper.py
Created January 29, 2019 01:49
from itertools import chain, combinations, product
import pprint
def powerset(iterable):
"powerset([1,2,3]) --> () (1,) (2,) (3,) (1,2) (1,3) (2,3) (1,2,3)"
s = list(iterable)
return chain.from_iterable(combinations(s, r) for r in range(len(s)+1))
class CBCCasper:
@nrryuya
nrryuya / RSAAccumulator.sol assembly
Last active January 5, 2019 07:53
.code
PUSH 80 contract RSAAccumulator {\n ...
PUSH 40 contract RSAAccumulator {\n ...
MSTORE contract RSAAccumulator {\n ...
CALLVALUE constructor(bytes modulus) pub...
DUP1 olidity ^
ISZERO a
PUSH [tag] 1 a
JUMPI a
PUSH 0 r
@nrryuya
nrryuya / LLL of RSAAccumulator
Last active January 5, 2019 07:46
[seq,
[mstore, 28, [calldataload, 0]],
[mstore, 32, 1461501637330902918203684832716283019655932542976],
[mstore, 64, 170141183460469231731687303715884105727],
[mstore, 96, -170141183460469231731687303715884105728],
[mstore, 128, 1701411834604692317316873037158841057270000000000],
[mstore, 160, -1701411834604692317316873037158841057280000000000],
# Line 179
[codecopy, 320, ~codelen, 256],
[assert, [iszero, callvalue]],
@nrryuya
nrryuya / RSAAccumulator.sol
Last active January 5, 2019 07:02
With my personal comments
pragma solidity ^0.4.25;
import {PrimeTester} from "./PrimeTester.sol";
contract RSAAccumulator {
// all arithmetics is modulo N
uint256 constant public NlengthIn32ByteLimbs = 8; // 1024 bits for factors, 2048 for modulus
uint256 constant public NlengthInBytes = 32 * NlengthIn32ByteLimbs;
uint256 constant public NLength = NlengthIn32ByteLimbs * 8 * 32;
@nrryuya
nrryuya / simpleOR-spec.k(with split)
Last active December 20, 2018 15:07
requires "abstract-semantics.k"
requires "verification.k"
module SIMPLEOR-SPEC
imports ETHEREUM-SIMULATION
imports ABSTRACT-SEMANTICS
imports VERIFICATION
rule
// <k> (split(A ==Int 1) ~> split(B ==Int 1) => .) ~> (#execute => #halt) ~> _ </k>
@nrryuya
nrryuya / test-spec.k(setZero.sol)
Created December 20, 2018 02:10
requires "abstract-semantics.k"
requires "verification.k"
module TEST-SPEC
imports ETHEREUM-SIMULATION
imports ABSTRACT-SEMANTICS
imports VERIFICATION
// transferFrom-success-1
rule
@nrryuya
nrryuya / simpleOR-sol-spec.k(v0.5.0, #True)
Last active December 19, 2018 02:23
requires "abstract-semantics.k"
requires "verification.k"
module SIMPLEOR-SOL-SPEC
imports ETHEREUM-SIMULATION
imports ABSTRACT-SEMANTICS
imports VERIFICATION
rule
<k> #execute => #halt </k>
@nrryuya
nrryuya / simpleOR-spec.k
Last active December 19, 2018 02:23
requires "abstract-semantics.k"
requires "verification.k"
module SIMPLEOR-SPEC
imports ETHEREUM-SIMULATION
imports ABSTRACT-SEMANTICS
imports VERIFICATION
rule
<k> #execute => #halt </k>
@nrryuya
nrryuya / [ERC721]transfer-success-1(--log)
Last active December 18, 2018 08:37
BYZANTIUM
STEP 12604 v1 : 333.542 s, 1856 MB
===================
<k>(#KSequence(Int(#"0"), #deductGas_EVM(.KList), STOP_EVM(.KList), #pc[_]_EVM(STOP_EVM(.KList)), #execute_EVM(.KList)))
<output>(_1201_1379:WordStack)
<statusCode>(_1203_1381:StatusCode)
<localMem>
...
</localMem>
<pc>(Int(#"1963"))
<gas>(#if_#then_#else_#fi_K-EQUAL(_andBool_(_==K_(TO_BAL_1371:Int,, Int(#"0")),, notBool_(_==K_(_+Int_(TO_BAL_1371:Int,, Int(#"1")),, Int(#"0")))),, Int(#"37710"),, Int(#"52710")))
@nrryuya
nrryuya / [ERC721]transfer-success-2(--log)
Last active December 18, 2018 06:58
BYZANTIUM
STEP 8414 v1 : 181.023 s, 1096 MB
===================
<k>(#KSequence(Map:lookup(hash2(Int(#"0"),, TOKEN_ID_1384:Int) |-> Int(#"0") hash2(hash2(Int(#"3"),, TO_ID_1386:Int),, CALLER_ID_1433:Int) |-> ISAPPROVED_1432:Int hash2(Int(#"1"),, TOKEN_ID_1384:Int) |-> Int(#"0") _1239_1425:Map,, hash2(Int(#"2"),, TO_ID_1386:Int)), #push_EVM(.KList), #pc[_]_EVM(SLOAD_EVM(.KList)), #execute_EVM(.KList)))
<output>(_1201_1387:WordStack)
<statusCode>(_1203_1389:StatusCode)
<localMem>
...
</localMem>
<pc>(Int(#"953"))
<gas>(Int(#"91519"))