xrchz

# @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

xrchz

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

xrchz

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

xrchz

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();

xrchz

synonyms:
   >>
   \\
   THEN
   ( means ";" in Isar )
  meaning:
    tac1 \\ tac2
    means apply tac1 to the current proof state
    then apply tac2 to all the resulting subgoals