WIP: this gist is being updated as it is being written.
This describes the design for a system to ease building/downloading and installing HOL4 and working with HOL theories. The hoped for advantages are:
| import { ethers } from 'ethers' | |
| // tested using a fork of mainnet (where we can impersonate the signers) | |
| // e.g. anvil -f http://localhost:8545@20143000 -p 8549 | |
| const provider = new ethers.JsonRpcProvider('http://localhost:8549') | |
| const rocketStorage = new ethers.Contract('rocketstorage.eth', | |
| [ | |
| 'function getAddress(bytes32) view returns (address)', |
| # @version ^0.3.7 | |
| # mental poker deck protocol | |
| # | |
| # Implements the paper | |
| # A Fast Mental Poker Protocol by Tzer-Jen Wei & Lih-Chung Wang | |
| # https://ia.cr/2009/439 | |
| # using the alt-bn128's G1 (https://neuromancer.sk/std/bn/bn254) for G | |
| # | |
| # For discrete log equality non-interactive ZK proofs, we use the scheme | |
| # described in Wallet Databases with Observers by David Chaum & Torben Pryds Pederson |
| Started Go-Ethereum Daemon on mainnet. | |
| INFO [06-24|13:01:27.632] Starting Geth on Ethereum mainnet... | |
| INFO [06-24|13:01:27.633] Bumping default cache on mainnet provided=1024 updated=4096 | |
| INFO [06-24|13:01:27.635] Maximum peer count ETH=50 LES=0 total=50 | |
| INFO [06-24|13:01:27.636] Smartcard socket not found, disabling err="stat /run/pcscd/pcscd.comm: no such file or directory" | |
| WARN [06-24|13:01:27.637] Sanitizing cache to Go's GC limits provided=4096 updated=2651 | |
| INFO [06-24|13:01:27.637] Set global gas cap cap=50,000,000 | |
| INFO [06-24|13:01:27.653] Allocated trie memory caches clean=397.00MiB dirty=662.00MiB | |
| INFO [06-24|13:01:27.653] Allocated cache and file handles database=/var/lib/gethmainnet/geth/chaindata cache=1.29GiB handles=262,144 | |
| INFO [06-24|13:01:27.724] Opened ancient database database=/var/lib/gethmainnet/geth/chaindata/ancient readonly=false |
| Started Go-Ethereum Daemon on mainnet. | |
| INFO [06-24|13:01:27.632] Starting Geth on Ethereum mainnet... | |
| INFO [06-24|13:01:27.633] Bumping default cache on mainnet provided=1024 updated=4096 | |
| INFO [06-24|13:01:27.635] Maximum peer count ETH=50 LES=0 total=50 | |
| INFO [06-24|13:01:27.636] Smartcard socket not found, disabling err="stat /run/pcscd/pcscd.comm: no such file or directory" | |
| WARN [06-24|13:01:27.637] Sanitizing cache to Go's GC limits provided=4096 updated=2651 | |
| INFO [06-24|13:01:27.637] Set global gas cap cap=50,000,000 | |
| INFO [06-24|13:01:27.653] Allocated trie memory caches clean=397.00MiB dirty=662.00MiB | |
| INFO [06-24|13:01:27.653] Allocated cache and file handles database=/var/lib/gethmainnet/geth/chaindata cache=1.29GiB handles=262,144 | |
| INFO [06-24|13:01:27.724] Opened ancient database database=/var/lib/gethmainnet/geth/chaindata/ancient readonly=false |
| open preamble basis | |
| val _ = translation_extends "basisProg"; | |
| val ex2 = process_topdecs` | |
| fun ex2 x r = let val r' = ref r in r := x; !r' end`; | |
| val () = append_prog ex2; | |
| val st2 = get_ml_prog_state(); |
| synonyms: | |
| >> | |
| \\ | |
| THEN | |
| ( means ";" in Isar ) | |
| meaning: | |
| tac1 \\ tac2 | |
| means apply tac1 to the current proof state | |
| then apply tac2 to all the resulting subgoals |