prelim.tex

\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}

\usepackage{amsmath,amssymb,amsthm}
  \allowdisplaybreaks % allow page breaks inside displayed equations
\usepackage[ruled,linesnumbered]{algorithm2e}
\usepackage{booktabs}
\usepackage{comment}
\usepackage{hyperref,cleveref}
\usepackage{mathtools}
\usepackage{prftree}
\usepackage{stmaryrd}
\usepackage{xspace}

\theoremstyle{definition}
  \newtheorem{definition}{Definition}
\theoremstyle{theorem}
  \newtheorem{theorem}{Theorem}

% algorithm2e
\SetKwInput{KwParam}{Parameters}
\SetKwInput{KwDescr}{Description}

\newcommand{\K}{\ensuremath{\mathbb{K}}\xspace}
\newcommand{\imp}{\to} % implication (logic)
\newcommand{\dimp}{\leftrightarrow} % iff (logic)
\newcommand{\xto}[1]{\xrightarrow{\text{#1}}} % rightarrow with text above
\newcommand{\prule}[1]{(\textsc{#1})\xspace} % proof rule names
  \newcommand{\pruleLuk}{\prule{Łukasiewicz}}
  \newcommand{\pruleMP}{\prule{Modus Ponens}}
  \newcommand{\pruleQ}{\prule{Quantifier}}
  \newcommand{\pruleG}{\prule{Generalization}}
  \newcommand{\prulePOR}{\prule{Propagation$_{\lor}$}}
  \newcommand{\prulePORL}{\prule{Propagation$_{\lor,\textnormal{left}}$}}
  \newcommand{\prulePORR}{\prule{Propagation$_{\lor,\textnormal{right}}$}}
  \newcommand{\prulePORN}{\prule{Propagation$_{\lor,\textnormal{nested}}$}}
  \newcommand{\prulePEX}{\prule{Propagation$_{\exists}$}}
  \newcommand{\prulePEXL}{\prule{Propagation$_{\exists,\textnormal{left}}$}}
  \newcommand{\prulePEXR}{\prule{Propagation$_{\exists,\textnormal{right}}$}}
  \newcommand{\prulePEXN}{\prule{Propagation$_{\exists,\textnormal{nested}}$}}
  \newcommand{\pruleFrame}{\prule{Frame}}
  \newcommand{\pruleFrameN}{\prule{Frame$_{\textnormal{nested}}$}}
  \newcommand{\pruleFrameL}{\prule{Frame$_{\textnormal{left}}$}}
  \newcommand{\pruleFrameR}{\prule{Frame$_{\textnormal{right}}$}}
  \newcommand{\pruleSubst}{\prule{Substitution}}
  \newcommand{\pruleKT}{\prule{Knaster Tarski}}
  \newcommand{\prulePFix}{\prule{Pre-Fixpoint}}
  \newcommand{\pruleEX}{\prule{Existence}}
  \newcommand{\pruleSingleV}{\prule{Singleton Variable}}
\newcommand{\EV}{EV} % element variable set
\newcommand{\SV}{SV} % set variable set
\newcommand{\ld}{\,.\,} % used in exists x . phi and similar situations
\newcommand{\Slash}{/\!/\xspace} % //, used to begin a line comment
\newcommand{\FV}[1]{FV(#1)} % free variables
\newcommand{\mkappC}[2]{#1[#2]} % make an application context
  \newcommand{\appC}[1]{\mkappC{C}{#1}}    % C[...]
  \newcommand{\appCa}[1]{\mkappC{C_1}{#1}} % C1[...]
  \newcommand{\appCb}[1]{\mkappC{C_2}{#1}} % C2[...]
\newcommand{\hole}{\square} % the hole variable
\newcommand{\pr}[1]{\left\langle #1 \right\rangle} % <...>
\newcommand{\code}[1]{\textnormal{\texttt{#1}}} % code
  \newcommand{\cdpc}{\code{pc}} % proof checker program
  \newcommand{\cdsucc}{\code{success}} % success flag
  \newcommand{\cdfail}{\code{failure}} % failure flag
  \newcommand{\cdacc}{\code{accept}}   % accept flag
  \newcommand{\cdrej}{\code{reject}}   % reject flag
  \newcommand{\cdsum}{\code{sum.imp}\xspace} % sum program
  \newcommand{\cdassump}{\code{assump}}
  \newcommand{\cdax}{\code{ax}}
  \newcommand{\cdmp}{\code{mp}}
  \newcommand{\cdother}{\code{other}}
\newcommand{\mkth}[1]{\Gamma^{\mathsf{#1}}} % make a logical theory
  \newcommand{\GammaIMP}{\mkth{IMP}}
\newcommand{\ceil}[1]{\left\lceil #1 \right\rceil}
\newcommand{\floor}[1]{\left\lfloor #1 \right\rfloor}
% useful formulas with sub/super-scripts
\newcommand{\varphisum}{\varphi_\cdsum} % \varphi_sum
% mathcal
\newcommand{\AAc}{\mathcal{A}}
\newcommand{\CC}{\mathcal{C}}
\newcommand{\DD}{\mathcal{D}}
\newcommand{\II}{\mathcal{I}}
\newcommand{\OO}{\mathcal{O}}
\newcommand{\PP}{\mathcal{P}}
\newcommand{\VV}{\mathcal{V}}
\newcommand{\TT}{\mathcal{T}}
\newcommand{\MM}{\mathcal{M}}
\newcommand{\NN}{\mathcal{N}}
% mathbb
\newcommand{\NNN}{\mathbb{N}}
% mathbb

% ZK
\newcommand{\ZKprover}{\PP}
  \newcommand{\PPbasic}{\PP_\code{basic}}
\newcommand{\ZKverifier}{\VV}
  \newcommand{\VVbasic}{\VV_\code{basic}}
\newcommand{\pibasic}{\pi_\code{basic}}
\newcommand{\pibn}[1]{\pi_{\code{basic},#1}}
\newcommand{\MT}{\TT}
\newcommand{\MTGamma}{\TT_\Gamma}
\newcommand{\MTPi}{\TT_\Pi}
\newcommand{\cMT}{c_\MT}
\newcommand{\cPi}{c_\Pi}
\newcommand{\oPi}{o_\Pi}
\newcommand{\cGamma}{c_\Gamma}
\newcommand{\oGamma}{o_\Gamma}
% nonlogical symbols
\newcommand{\nlsymbol}[1]{\mathsf{#1}}
  \newcommand{\nlzero}{\nlsymbol{zero}}
  \newcommand{\nlsucc}{\nlsymbol{succ}}
% concrete (non-meta) variables
\newcommand{\cv}[1]{\mathsf{#1}}
  \newcommand{\cvx}{\cv{x}}
  \newcommand{\cvy}{\cv{y}}
  \newcommand{\cvX}{\cv{X}}
% basic proof checking procedures
\newcommand{\bp}[1]{\code{basic\_prove}_\code{#1}}
  \newcommand{\bpassump}{\bp{assump}}
  \newcommand{\bpax}{\bp{ax}}
  \newcommand{\bpmp}{\bp{mp}}
  \newcommand{\bpgen}{\bp{gen}}
  \newcommand{\bpframe}{\bp{frame}}
  \newcommand{\bpsubst}{\bp{subst}}
  \newcommand{\bpkt}{\bp{kt}}
  \newcommand{\bptop}{\code{basic\_prove}}
% encoding
\newcommand{\en}[1]{\left\llbracket #1 \right\rrbracket}
  \newcommand{\enGamma}{\en{\Gamma}}
  \newcommand{\enGamman}[1]{\en{\Gamma_{#1}}}
  \newcommand{\envarphi}{\en{\varphi}}
  \newcommand{\envarphin}[1]{\en{\varphi_{#1}}}
  \newcommand{\enpsi}{\en{\psi}}
  \newcommand{\enpsin}[1]{\en{\psi_{#1}}}
  \newcommand{\enDelta}{\en{\Delta}}
  \newcommand{\enDeltan}[1]{\en{\Delta_{#1}}}
% hash and commitment
\newcommand{\hof}[1]{h(#1)}
\newcommand{\Com}{\code{Com}}
\newcommand{\CSCommit}{\code{CS.Commit}}
\newcommand{\CSVerCommit}{\code{CS.VerCommit}}
\newcommand{\CSSetup}{\code{CS.Setup}}
\newcommand{\VCCommit}{\code{VC.Commit}}
\newcommand{\VCVerCommit}{\code{VC.VerCommit}}
\newcommand{\VCSetup}{\code{VC.Setup}}
\newcommand{\ck}{\mathit{ck}}
  \newcommand{\ckGamma}{\ck_\Gamma}
  \newcommand{\ckPi}{\ck_\Pi}
\newcommand{\Ispace}{\II}
\newcommand{\Ospace}{\OO}
\newcommand{\Cspace}{\CC}
\newcommand{\Adversary}{\AAc}
\newcommand{\negl}{\code{negl}}
% data space
\newcommand{\Data}{\DD}
\newcommand{\Dpattern}{\DD_\textit{pattern}}
\newcommand{\Dtheory}{\DD_\textit{theory}}
% proof network
\newcommand{\PNet}{\NN}
\newcommand{\Ninit}{\mathit{IN}}
\newcommand{\Naggr}{\mathit{AN}}
\newcommand{\Npr}{\mathit{PN}}
  \newcommand{\Nprn}[1]{\Npr_{#1}}
% vectors
\newcommand{\vecu}{\vec{u}}