Date: 2026-08-31
Block: 115260 (glamsterdam-devnet-7, chainId 7082904758)
Emulator: ZisK ziskemu v1.1.0-alpha (9a5a1ac, 2026-08-18)
Yoichi Hirai pirapira
pirapira
/ gist:2c5418c6eab7a66a061b01187bc9fe6a
Created
August 31, 2026 21:53
evm-asm-bench-20260831.md
pirapira
/ gist:80bc4747f560f3b9d9fa430d5db0ce20
Last active
August 9, 2026 21:34
evm-sail rejects 67 nibbles in mpt leaf path
Text generated by Claude Code. I tried the command in "Run" section and saw the output.
Answer: no. evm-sail's trie-node decoder rejects a leaf whose remaining key
exceeds 64 nibbles with fatal_error(RlpDecode), both by a decode-time length
check and by the type of TriePath itself. Caveats about whether the decoder is
reached for that particular fixture are in §5.
Everything below is self-contained: starting from an empty directory, the steps
pirapira
/ gist:08e0a9dce64bf2a082900c4755ea7edb
Last active
August 9, 2026 21:29
evm-sail rejects 67 nibbles in mpt leaf path
Text generated by Claude Code.
Answer: no. evm-sail's trie-node decoder rejects a leaf whose remaining key
exceeds 64 nibbles with fatal_error(RlpDecode), both by a decode-time length
check and by the type of TriePath itself. Caveats about whether the decoder is
reached for that particular fixture are in §5.
Everything below is self-contained: starting from an empty directory, the steps
pirapira
/ refinement.lean
Created
November 13, 2025 20:02
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- Distributed under MIT License available at https://github.com/Verified-zkEVM/clean/blob/883ac93d22397edbdef3876623749e73425d571a/LICENSE | |
| -- Copyright (c) 2025 zkSecurity, LLC | |
| namespace High | |
| axiom ProverInput : Type | |
| axiom Witness : Type | |
| axiom compute : ProverInput → Option Witness |
pirapira
/ gist:737f0b8ba2e3e94ba85c8d1f67bdbd0d
Created
August 4, 2020 13:03
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| privat@yoichi-MS-7A93:~/shared/cpp2v$ coq --version | |
| Command 'coq' not found, did you mean: | |
| command 'oq' from snap oq (1.1.2) | |
| command 'coz' from deb coz-profiler (0.1.0-2ubuntu3) | |
| command 'cow' from deb fl-cow (0.6-4.2) | |
| command 'cnq' from deb cplay (1.50-2) | |
| command 'col' from deb bsdmainutils (11.1.2ubuntu3) | |
| command 'coqc' from deb coq (8.11.0-1) |
pirapira
/ ClockworkBase32.thy
Last active
July 31, 2020 19:56
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* This file is to be opened in Isabelle2020 available from | |
| https://isabelle.in.tum.de/ | |
| Lots of symbols look nicer there. Instead of ↦, you'll see an arrow. | |
| Moreover, Isabelle checks definitions are definitions and theorems are theorems. | |
| *) | |
| text ‹ | |
| Copyright 2020 Yoichi Hirai | |
| Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: | |
| The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| yh@14h:~/src/k-dss$ make | |
| dapp --version | |
| dapp 0.26.0 | |
| solc, the solidity compiler commandline interface | |
| Version: 0.5.15+commit.6a57276f.Linux.g++ | |
| hevm 0.36 | |
| git submodule update --init --recursive | |
| Submodule 'dss' (https://github.com/makerdao/dss.git) registered for path 'dss' | |
| Cloning into '/home/yh/src/k-dss/dss'... | |
| Submodule path 'dss': checked out 'b5e9bc0717defffae73cd4f4e7f30fb84843c200' |
pirapira
/ raiden-debug_2019-07-25T09:40:33.055353.log
Created
August 30, 2019 12:54
raiden-debug_2019-07-25T09:40:33.055353.log
This file has been truncated, but you can view the full file.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {"raiden": "0.100.5.dev113+g2ba85cbee", "raiden_db_version": 23, "python_implementation": "CPython", "python_version": "3.7.4", "system": "Linux 64bit_ELF 5.0.0-21-generic", "architecture": "x86_64", "distribution": "bundled", "event": "Starting Raiden", "logger": "raiden.ui.runners", "level": "info", "timestamp": "2019-07-25 09:40:33.074475"} | |
| {"config_file": "/home/yoichi/.local/share/raiden/config-16fa85f3a477b95c7180209b25ef0291ade95e3f-goerli.toml", "event": "Using config file", "logger": "raiden.ui.runners", "level": "debug", "timestamp": "2019-07-25 09:40:33.075235"} | |
| {"node": "0x16Fa85F3a477B95c7180209B25ef0291ade95e3F", "available_nonce": 3, "client": "Geth/v1.8.23-omnibus-2ad89aaa/linux-amd64/go1.11.1", "event": "JSONRPCClient created", "logger": "raiden.network.rpc.client", "level": "debug", "timestamp": "2019-07-25 09:40:34.502762"} | |
| {"pfs_info": "PFSInfo(url='https://pfs-goerli-with-fee.services-dev.raiden.network', price=100, chain_id=5, token_network_registry_address=b'\\xb3\\x86\\xe8~S\\xfbu/`\\x |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| export GOERLI=http://geth.goerli.ethnodes.brainbot.com:8545 | |
| export GOERLIPRIV=/home/yoichi/.ethereum/goerli/keystore/UTC--2019-02-18T14-56-34.781524237Z--6c5c227036a1d159c19f17316e5d0f0a52d84d5c | |
| export MAX_UINT256=115792089237316195423570985008687907853269984665640564039457584007913129639935 | |
| let "seconds_per_day=60*60*24" | |
| let "decay=200*$seconds_per_day" | |
| let "duration=200*$seconds_per_day" | |
| export Deposit=2000000000000000000000 | |
| python -m raiden_contracts.deploy raiden --rpc-provider $GOERLI --private-key $GOERLIPRIV --gas-price 20 --gas-limit 6000000 --max-token-networks $MAX_UINT256 --secret-registry-from-deployment-file raiden_contracts/data_0.21.0/deployment_goerli.json |
NewerOlder