diff --git a/docs/general/flake.lock b/docs/general/flake.lock new file mode 100644 index 0000000..0cf18d8 --- /dev/null +++ b/docs/general/flake.lock @@ -0,0 +1,61 @@ +{ + "nodes": { + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1705309234, + "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1704290814, + "narHash": "sha256-LWvKHp7kGxk/GEtlrGYV68qIvPHkU9iToomNFGagixU=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "70bdadeb94ffc8806c0570eb5c2695ad29f0e421", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-23.05", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/docs/general/flake.nix b/docs/general/flake.nix new file mode 100644 index 0000000..d146b54 --- /dev/null +++ b/docs/general/flake.nix @@ -0,0 +1,54 @@ +{ + description = "Flake"; + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixos-23.05"; + flake-utils.url = "github:numtide/flake-utils"; + }; + outputs = { self, nixpkgs, flake-utils }: + with flake-utils.lib; eachSystem allSystems (system: + let + pkgs = nixpkgs.legacyPackages.${system}; + lib = pkgs.lib; + tex = pkgs.texlive.combine { + inherit (pkgs.texlive) scheme-full + biber + biblatex + cleveref + dashbox + environ + gentium-tug + ifmtarg + iftex + pbox + scalerel + totpages + xifthen + xstring; + }; + in { + packages = { + latex-artifact = pkgs.stdenvNoCC.mkDerivation rec { + name = "latex-artifact"; + src = ./src; + buildInputs = [ pkgs.coreutils tex ]; + phases = ["unpackPhase" "buildPhase" "installPhase"]; + buildPhase = '' + export PATH="${lib.makeBinPath buildInputs}"; + mkdir -p .cache/texmf-var + env TEXMFHOME=.cache TEXMFVAR=.cache/texmf-var \ + latexmk -interaction=nonstopmode -pdf -pdflatex \ + main.tex + ''; + installPhase = '' + mkdir -p $out + cp main.pdf $out/ + ''; + }; + }; + devShell = pkgs.mkShell { + buildInputs = [ + tex + ]; + }; + }); +} diff --git a/docs/general/src/iris.sty b/docs/general/src/iris.sty new file mode 100644 index 0000000..ce1787c --- /dev/null +++ b/docs/general/src/iris.sty @@ -0,0 +1,637 @@ +\NeedsTeXFormat{LaTeX2e}[1999/12/01] +\ProvidesPackage{iris} + +\RequirePackage{tikz} +\RequirePackage{scalerel} +\RequirePackage{array} +\RequirePackage{dashbox} +\RequirePackage{tensor} +\RequirePackage{xparse} +\RequirePackage{xstring} +\RequirePackage{mathtools} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% SETUP +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +\usetikzlibrary{shapes} +%\usetikzlibrary{snakes} +\usetikzlibrary{arrows} +\usetikzlibrary{calc} +\usetikzlibrary{arrows.meta} +\tikzstyle{state}=[circle, draw, minimum size=1.2cm, align=center] +\tikzstyle{trans}=[arrows={->[scale=1.4]}] + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% MATH SYMBOLS & NOTATION & IDENTIFIERS +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\nat}{\mathbb{N}} + +\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}} +\newcommand*{\disj}[1][]{\mathrel{\#_{#1}}} +\newcommand\pord{\sqsubseteq} +\newcommand\dplus{\mathbin{+\kern-1.0ex+}} +\newcommand{\upclose}{\mathord{\uparrow}} +\newcommand{\ALT}{\ |\ } + +\newcommand{\spac}{\,} % a space + +\def\All #1.{\forall #1.\spac}% +\def\Exists #1.{\exists #1.\spac}% +\def\Ret #1.{#1.\spac}% + +\newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}% + +\newcommand{\judgment}[2][]{\paragraph{#1}\hspace{\stretch{1}}\fbox{$#2$}} + +\newcommand{\pfn}{\rightharpoonup} +\newcommand\fpfn{\xrightharpoonup{\kern-0.25ex\textrm{fin}\kern-0.25ex}} +\newcommand{\la}{\leftarrow} +\newcommand{\ra}{\rightarrow} +\newcommand{\Ra}{\Rightarrow} +\newcommand{\Lra}{\Leftrightarrow} +\newcommand\monra{\xrightarrow{\kern-0.15ex\textrm{mon}\kern-0.05ex}} +\newcommand\nfn{\xrightarrow{\kern-0.15ex\textrm{ne}\kern-0.05ex}} +\newcommand{\eqdef}{\triangleq} +\newcommand{\bnfdef}{\vcentcolon\vcentcolon=} + +\newcommand*\setComp[2]{\left\{#1\spac\middle|\spac#2\right\}} +\newcommand*\set[1]{\left\{#1\right\}} +\newcommand*\record[1]{\left\{\spac#1\spac\right\}} +\newcommand*\recordComp[2]{\left\{\spac#1\spac\middle|\spac#2\spac\right\}} + +\newenvironment{inbox}[1][]{ + \begin{array}[#1]{@{}l@{}} +}{ + \end{array} +} + +\newcommand{\dom}{\mathrm{dom}} +\newcommand{\cod}{\mathrm{cod}} +\newcommand{\chain}{\mathrm{chain}} + +\newcommand{\pset}[1]{\wp(#1)} % Powerset +\newcommand{\psetdown}[1]{\wp^\downarrow(#1)} +\newcommand{\finpset}[1]{\wp^\mathrm{fin}(#1)} + +\newcommand{\Func}{F} % functor + +\newcommand{\subst}[3]{{#1}[{#3} / {#2}]} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newcommand{\textdom}[1]{\textit{#1}} + +\newcommand{\wIso}{\xi} + +\newcommand{\rs}{r} +\newcommand{\rsB}{s} +\newcommand{\rss}{R} + +\newcommand{\pres}{\pi} +\newcommand{\wld}{w} +\newcommand{\ghostRes}{g} + +%% Various pieces of syntax +\newcommand{\wsat}[3]{#1 \models_{#2} #3} +\newcommand{\wsatpre}{\textdom{pre-wsat}} + +\newcommand{\wtt}[2]{#1 : #2} % well-typed term + +% \newcommand{\nequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{=}}}} +\newcommand{\notnequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{\neq}}}} +\newcommand{\nequivset}[2]{\ensuremath{\mathrel{\stackrel{#1}{=}_{#2}}}} +\newcommand{\nequivB}[1]{\ensuremath{\mathrel{\stackrel{#1}{\equiv}}}} +\newcommand{\latert}{\mathord{\blacktriangleright}} +\newcommand{\latertinj}{\textlog{next}} + +\newcommand{\Sem}[1]{\llbracket #1 \rrbracket} + +\newcommand{\sembox}[1]{\hfill \normalfont \mbox{\fbox{\(#1\)}}} +\newcommand{\typedsection}[2]{\subsubsection*{\rm\em #1 \sembox{#2}}} + + +%% Some commonly used identifiers +\newcommand{\SProp}{\textdom{SProp}} +\newcommand{\UPred}{\textdom{UPred}} +\newcommand{\mProp}{\textdom{Prop}} % meta-level prop +\newcommand{\iProp}{\textdom{iProp}} +\newcommand{\iPreProp}{\textdom{iPreProp}} +\newcommand{\Wld}{\textdom{Wld}} +\newcommand{\Res}{\textdom{Res}} +\newcommand{\State}{\textdom{State}} +\newcommand{\Val}{\textdom{Val}} +\newcommand{\Var}{\textdom{Var}} +\newcommand{\Ectx}{\textdom{Ectx}} +\newcommand{\Loc}{\textdom{Loc}} + +\newcommand{\cofe}{T} +\newcommand{\cofeB}{U} +\newcommand{\COFEs}{\mathcal{COFE}} % category of COFEs +\newcommand{\iFunc}{\Sigma} +\newcommand{\fix}{\textdom{fix}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newcommand{\textmon}[1]{\textsc{#1}} + +\newcommand{\monoid}{M} +\newcommand{\mval}{\mathcal{V}} + +\newcommand{\melt}{a} +\newcommand{\meltB}{b} +\newcommand{\meltC}{c} +\newcommand{\melts}{A} +\newcommand{\meltsB}{B} + +\newcommand{\f}{\mathrm{f}} % for "frame" + +\newcommand{\mcar}[1]{|#1|} +\newcommand{\mcarp}[1]{\mcar{#1}^{+}} +\newcommand{\munit}{\varepsilon} +\newcommand{\mcore}[1]{\llparenthesis#1\rrparenthesis} +\newcommand{\mtimes}{\mathbin{\cdot}} + +\newcommand{\mupd}{\rightsquigarrow} +\newcommand{\mincl}[1][]{\ensuremath{\mathrel{\stackrel{#1}{\preccurlyeq}}}} + +\newcommand{\CMRAs}{\mathcal{CMRA}} % category of CMRAs + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% LOGIC SYMBOLS & NOTATION & IDENTIFIERS +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newcommand{\textlog}[1]{\textsf{#1}} + +\newcommand{\Sig}{\mathcal{S}} +\newcommand{\SigType}{\mathcal{T}} +\newcommand{\SigFn}{\mathcal{F}} +\newcommand{\SigAx}{\mathcal{A}} +\newcommand{\sigtype}{T} +\newcommand{\sigfn}{F} +\newcommand{\sigax}{A} + +\newcommand{\type}{\tau} +\newcommand{\typeB}{\sigma} + +\newcommand{\var}{x} +\newcommand{\varB}{y} +\newcommand{\varC}{z} + +\newcommand{\term}{t} +\newcommand{\termB}{u} + +\newcommand{\vctx}{\Gamma} +\newcommand{\pfctx}{\Theta} + +\newcommand{\prop}{P} +\newcommand{\propB}{Q} +\newcommand{\propC}{R} + +% pure propositions +\newcommand{\pprop}{\phi} +\newcommand{\ppropB}{\psi} + +\newcommand{\pred}{\varPhi} +\newcommand{\predB}{\Psi} +\newcommand{\predC}{\Zeta} + +\newcommand{\gname}{\gamma} +\newcommand{\iname}{\iota} + +\newcommand{\mask}{\mathcal{E}} +\newcommand{\namesp}{\mathcal{N}} +\newcommand{\namecl}[1]{{#1^{\kern0.2ex\uparrow}}} + +%% various pieces of Syntax +\def\MU #1.{\mu #1.\spac}% +\def\Lam #1.{\lambda #1.\spac}% + +\newcommand{\proves}{\vdash} +\newcommand{\provesCoq}{\mathrel{\vdash_{\mbox{\!\includegraphics[width=0.7em]{rooster.jpg}}}}} +\newcommand{\provesIff}{\mathrel{\dashv\vdash}} + +\newcommand{\wand}{\mathrel{-\!\!*}} + +% oh my... I have to wrap the "-" in a \mathrm, otherwise all hell breaks lose... +\newcommand{\fmapsto}[1][]{\xmapsto{#1}} +\newcommand{\gmapsto}{\hookrightarrow}% +\newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}% + +\NewDocumentCommand\wpre{m O{} m}% + {\textlog{wp}_{#2}\spac#1\spac{\big\{#3\big\}}} +\newcommand{\wbwprename}{\textlog{wbwp}} +\NewDocumentCommand\wbwpre{m O{} m O{}}% + {\textlog{wbwp}_{#2}\spac#1\spac\bagbracket{#3}^{#4}} + +\newcommand{\later}{\mathop{\triangleright}} +\newcommand{\always}{\mathop{\Box}} +\newcommand{\pure}{\mathop{\blacksquare}} + +%% Invariants and Ghost ownership +% PDS: Was 0pt inner, 2pt outer. +% \boxedassert [tikzoptions] contents [name] +\tikzstyle{boxedassert_border} = [sharp corners,line width=0.2pt] +\NewDocumentCommand \boxedassert {O{} m o}{% + \tikz[baseline=(m.base)]{ + % \node[rectangle, draw,inner sep=0.8pt,anchor=base,#1] (m) {${#2}\mathstrut$}; + \node[rectangle,inner sep=0.8pt,outer sep=0.2pt,anchor=base] (m) {${#2}\mathstrut$}; + \draw[#1,boxedassert_border] ($(m.south west) + (0,0.65pt)$) rectangle ($(m.north east) + (0, 0.7pt)$); + }\IfNoValueF{#3}{^{\,#3}}% +} +\newcommand*{\knowInv}[2]{\boxedassert{#2}[#1]} +\newcommand*{\ownGhost}[2]{\boxedassert[densely dashed]{#2}[#1]} +\newcommand*{\ownGGhost}[1]{\boxedassert[densely dashed]{#1}} +\newcommand{\ownM}[1]{\textlog{Own}(#1)} +\newcommand{\ownPhys}[1]{\lfloor\, #1\, \rfloor} + +\newcommand{\raop}{\cdot} +\newcommand{\raset}{M} +\newcommand{\rael}{m} + +%% View Shifts +\NewDocumentCommand \vsGen {O{} m O{}}% + {\mathrel{% + \ifthenelse{\equal{#3}{}}{% + % Just one mask, or none + {#2}_{#1}% + }{% + % Two masks + \tensor*[^{#1}]{#2}{^{#3}} + }% + }}% +\NewDocumentCommand \vs {O{} O{}} {\kern-0.5ex\vsGen[#1]{\Rrightarrow}[#2]} +\NewDocumentCommand \vsL {O{} O{}} {\kern-0.5ex\vsGen[#1]{\Lleftarrow}[#2]} +\NewDocumentCommand \vsE {O{} O{}} % + {\kern-0.5ex\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]} +\NewDocumentCommand \pvs {O{} O{}} {\mathord{\vsGen[#1]{{\mid\kern-0.5ex\Rrightarrow\kern-0.25ex}}[#2]\kern0.2ex}} + +\newcommand\vsWand{{\displaystyle\equiv\kern-1.1ex\smash{\raisebox{-0.2ex}{\scalerel*{\vphantom-\ast}{4}}}\kern-0.2ex}} +\NewDocumentCommand \vsW {O{} O{}}{\vsGen[#1]{\vsWand}[#2]} + +\NewDocumentCommand \upd {} {\mathop{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}} + +%% Hoare Triples +\newcommand*{\hoaresizebox}[1]{% + \hbox{$\mathsurround=0pt{#1}\mathstrut$}} +\newcommand*{\hoarescalebox}[2]{% + \hbox{\scalerel*[1ex]{#1}{#2}}} +\newcommand{\triple}[5]{% + \setbox0=\hoaresizebox{{#3}{#5}}% + \setbox1=\hoarescalebox{#1}{\copy0}% + \setbox2=\hoarescalebox{#2}{\copy0}% + \copy1{#3}\copy2% + \; #4 \;% + \copy1{#5}\copy2} + +\newcommand{\bracket}[4][]{% + \setbox0=\hbox{$\mathsurround=0pt{#1}{#4}\mathstrut$}% + \scalerel*[1ex]{#2}{\copy0}% + {#4}% + \scalerel*[1ex]{#3}{\copy0}} +% \curlybracket[other] x +\newcommand{\curlybracket}[2][]{\bracket[{#1}]\{\}{#2}} +\newcommand{\anglebracket}[2][]{\bracket[{#1}]\langle\rangle{#2}} + +\newcommand{\bagbracket}[2][]{\bracket[{#1}]\llparenthesis\rrparenthesis{#2}} + +\NewDocumentCommand \hoare {m m m O{}}{ + \curlybracket{#1}\spac #2 \spac \curlybracket{#3}_{#4}% +} + +% \NewDocumentCommand \wbhoare {m m m O{} O{}}{ +% {\curlybracket{#1}}^{\textlog{wb}}\spac #2 \spac \curlybracket{#3}_{#5}^{#4}% +% } + +\NewDocumentCommand \wbhoare {m m m O{} O{}}{ + \bagbracket{#1}\spac #2 \spac \bagbracket{#3}_{#5}^{#4}% +} + + +% \hoareV[t] pre c post [mask] +\NewDocumentCommand \hoareV {O{c} m m m O{}}{ + {\begin{aligned}[#1] + &\curlybracket{#2} \\ + &\quad{#3} \\ + &{\curlybracket{#4}}_{#5} + \end{aligned}}% +} +% \hoareHV[t] pre c post [mask] +\NewDocumentCommand \hoareHV {O{c} m m m O{}}{ + {\begin{aligned}[#1] + &\curlybracket{#2} \; {#3} \\ + &{\curlybracket{#4}}_{#5} + \end{aligned}}% +} + + +% \wbhoareV[t] pre c post [mask] +\NewDocumentCommand \wbhoareV {O{c} m m m O{} O{}}{ + {\begin{aligned}[#1] + &\bagbracket{#2} \\ + &\quad{#3} \\ + &{\bagbracket{#4}}_{#6}^{#5} + \end{aligned}}% +} +% \wbhoareHV[t] pre c post [mask] +\NewDocumentCommand \wbhoareHV {O{c} m m m O{} O{}}{ + {\begin{aligned}[#1] + &\bagbracket{#2} \; {#3} \\ + &{\bagbracket{#4}}_{#6}^{#5} + \end{aligned}}% +} + +% \wbhoareHV[t] pre c post [mask] +\NewDocumentCommand \wbhoareVH {O{c} m m m O{} O{}}{ + {\begin{aligned}[#1] + &\bagbracket{#2} \\ + &{#3}\; {\bagbracket{#4}}_{#6}^{#5} + \end{aligned}}% +} + +% % \wbhoareV[t] pre c post [mask] +% \NewDocumentCommand \wbhoareV {O{c} m m m O{} O{}}{ +% {\begin{aligned}[#1] +% &{\curlybracket{#2}}^{\textlog{wb}} \\ +% &\quad{#3} \\ +% &{\curlybracket{#4}}_{#6}^{#5} +% \end{aligned}}% +% } +% % \wbhoareHV[t] pre c post [mask] +% \NewDocumentCommand \wbhoareHV {O{c} m m m O{} O{}}{ +% {\begin{aligned}[#1] +% &{\curlybracket{#2}}^{\textlog{wb}} \; {#3} \\ +% &{\curlybracket{#4}}_{#6}^{#5} +% \end{aligned}}% +% } + +% % \wbhoareHV[t] pre c post [mask] +% \NewDocumentCommand \wbhoareVH {O{c} m m m O{} O{}}{ +% {\begin{aligned}[#1] +% &{\curlybracket{#2}}^{\textlog{wb}} \\ +% &{#3}\; {\curlybracket{#4}}_{#6}^{#5} +% \end{aligned}}% +% } + +\newcommand{\stackmask}{\mathcal{O}} + + +%% Some commonly used identifiers +\newcommand{\timeless}[1]{\textlog{timeless}(#1)} +\newcommand{\persistent}[1]{\textlog{persistent}(#1)} +\newcommand{\physatomic}[1]{\textlog{atomic}($#1$)} +\newcommand{\infinite}{\textlog{infinite}} + +%\newcommand{\Prop}{\textlog{Prop}} +\newcommand{\Prop}{\textlog{iProp}} +\newcommand{\Pred}{\textlog{Pred}} + +\newcommand{\TRUE}{\textlog{True}} +\newcommand{\FALSE}{\textlog{False}} +\newcommand{\TLam}{\Lambda\spac}% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% GENERIC LANGUAGE SYNTAX AND SEMANTICS +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newcommand{\expr}{e} +\newcommand{\val}{v} +\newcommand{\valB}{w} +\newcommand{\pstate}{\sigma} +\newcommand{\step}{\ra} +\newcommand{\hstep}[1]{\ra_{#1}} +\newcommand{\coopstep}{\ra_{\mathsf{coop}}} +\newcommand{\seqstep}{\ra_{\mathsf{seq}}} +\newcommand{\tpstep}{\ra_{\mathsf{tp}}} +\newcommand{\elctx}{K} +\newcommand{\lctx}{C} +\newcommand{\reduces}{\Downarrow} +\newcommand{\coopreduces}{\Downarrow_{\mathsf{coop}}\ } +\newcommand{\seqreduces}{\Downarrow_{\mathsf{seq}}\ } + +\newcommand{\toval}{\mathrm{expr2val}} +\newcommand{\ofval}{\mathrm{val2expr}} +\newcommand{\atomic}{\mathrm{atomic}} +\newcommand{\red}{\mathrm{red}} +\newcommand{\Lang}{\Lambda} + +\newcommand{\tpool}{T} + +\newcommand{\cfg}{\rho} + +%\def\fill#1[#2]{#1 {[}\, #2\,{]} } +\def\fill#1[#2]{#1 {[} #2{]} } % Lars + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% STANDARD DERIVED CONSTRUCTIONS +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% Option +\newcommand{\option}[1]{#1^?} +\newcommand{\Some}{} +\newcommand{\None}{\textlog{None}} + +% Agreement +\newcommand{\agm}{\ensuremath{\textmon{Ag}}} +\newcommand{\aginj}{\textlog{ag}} + +% Fraction +\newcommand{\fracm}{\ensuremath{\textmon{Frac}}} + +% Exclusive +\newcommand{\exm}{\ensuremath{\textmon{Ex}}} +\newcommand{\exinj}{\textlog{ex}} + +% Finset +\newcommand{\unitm}{\ensuremath{\textmon{Unit}}} +\newcommand{\unitel}{\textlog{unit}} + +%sum +\newcommand{\summ}{\ensuremath{\textmon{Sum}}} +\newcommand{\suminjl}{\textlog{injl}} +\newcommand{\suminjr}{\textlog{injr}} + + +% Finset +\newcommand{\finsetm}{\ensuremath{\textmon{FinSet}}} + +% Auth +\newcommand{\authm}{\textmon{Auth}} +\newcommand{\authfull}{\mathord{\bullet}\,} +\newcommand{\authfrag}{\mathord{\circ}\,} +\newcommand{\authboth}{\mathord{\bullet}\!\mathord{\circ}} +\newcommand{\extord}{\preceq} + +\newcommand{\AuthInv}{\textsf{AuthInv}} +\newcommand{\Auth}{\textsf{Auth}} + +% One-Shot +\newcommand{\oneshotm}{\ensuremath{\textmon{OneShot}}} +\newcommand{\ospending}{\textlog{pending}} +\newcommand{\osshot}{\textlog{shot}} + +% STSs +\newcommand{\STSCtx}{\textlog{StsCtx}} +\newcommand{\STSSt}{\textlog{StsSt}} +\newcommand{\STSclsd}{\textlog{closed}} +\newcommand{\STSauth}{\textlog{auth}} +\newcommand{\STSfrag}{\textlog{frag}} +\newcommand{\STSS}{\mathcal{S}} % states +\newcommand{\STST}{\mathcal{T}} % tokens +\newcommand{\STSL}{\mathcal{L}} % labels +\newcommand{\stsstep}{\ra} +\newcommand{\ststrans}{\ra^{*}}% the relation relevant to the STS rules +\newcommand{\stsfstep}[1]{\xrightarrow{#1}} +\newcommand{\stsftrans}[1]{\stsfstep{#1}^{*}} + +\tikzstyle{sts} = [->,every node/.style={rectangle, rounded corners, draw, minimum size=1.2cm, align=center}] +\tikzstyle{sts_arrows} = [arrows={->[scale=1.5]},every node/.style={font=\sffamily\small}] + +%% Stored Propositions +\newcommand{\mapstoprop}{\mathrel{\kern-0.5ex\tikz[baseline=(m)]{\node at (0,0) (m){}; \draw[line cap=round] (0,0.16) -- (0,-0.004);}\kern-1.5ex\Ra}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% CONCRETE LANGUAGE SYNTAX AND SEMANTICS +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%\newcommand{\textlang}[1]{\texttt{#1}} +\newcommand{\textlang}[1]{\mathsf{#1}} % Lars +%\newcommand{\langkw}[1]{\textlang{\color{blue}\scriptsize #1}} +\newcommand{\langkw}[1]{\textlang{\color{blue} #1}} % Lars +\newcommand{\lvar}[1]{\textit{#1}} % Yes, this makes language-level variables look like logic-level variables. but we still distinguish locally bound variables from global definitions. +\newcommand{\lvarA}{\lvar{\var}} +\newcommand{\lvarB}{\lvar{\varB}} +\newcommand{\lvarC}{\lvar{\varC}} + +\newcommand{\loc}{\ell} + +\def\Let#1=#2in{\langkw{let} \spac #1 \mathrel{=} #2 \spac \langkw{in} \spac} +\newcommand{\JustLet}{\langkw{let} \spac} +\newcommand{\JustIn}{\langkw{in}} +\def\If#1then{\langkw{if} \spac #1 \spac \langkw{then} \spac} +\def\Else{\spac\langkw{else} \spac} +\newcommand{\Alloc}[1]{\langkw{ref}(#1)} +\def\Rec#1 #2={\langkw{rec}\spac{#1}({#2}) \mathrel{=} } +\def\Skip{\langkw{skip}} +\def\Assert{\langkw{assert}} +\newcommand\Inj[1]{\textlang{inj}_{#1}\spac} +\newcommand\Proj[1]{\pi_{#1}\spac} +\def\True{\langkw{true}} +\def\False{\langkw{false}} +\def\Match#1with#2=>#3|#4=>#5end{\langkw{match}\spac#1\spac\langkw{with}\spac#2\Ra#3\mid#4\Ra#5\spac\langkw{end}} +\def\MatchML#1with#2=>#3|#4=>#5end#6{{\arraycolsep=1.4pt\begin{array}[t]{rll}% + \multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\% + &\Ra#3\\|&\Ra#5\\% + \multicolumn{3}{l}{\langkw{end}#6}% + \end{array}}} +\def\MatchMLL#1with#2=>#3|#4=>#5|#6=>#7end#8{{\arraycolsep=1.4pt\begin{array}[t]{rll}% + \multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\% + &\Ra#3\\|&\Ra#5\\|&\Ra#7\\% + \multicolumn{3}{l}{\langkw{end}#8}% + \end{array}}} +\def\MatchS#1with#2=>#3end{ + \langkw{match}\spac#1\spac\langkw{with}\spac#2\Ra#3\spac\langkw{end}} +%\newcommand\CAS{\langkw{CAS}} +\newcommand\CAS{\langkw{cas}} % Lars +\newcommand*\JustFork{\langkw{fork}} +\newcommand*\Fork[1]{\langkw{fork}\set{#1}} +\newcommand*\CFork[1]{\langkw{Cfork}\spac\set{#1}} +\newcommand*\JustCFork{\langkw{Cfork}} +\newcommand*\Yield{\langkw{yield}} +\newcommand\deref{\mathop{!}} +\let\gets\leftarrow + +% \def\cont{\langkw{cont}} +% \def\callcc(#1.{\langkw{call/cc}\spac(#1.\spac} +% \def\throw#1to#2{\langkw{throw}\spac#1\spac\langkw{to}\spac#2} +% \newcommand{\callccop}{\langkw{call/cc}} +% \newcommand{\throwop}{\langkw{throw}} +% %\newcommand{\empctx}{\circledcirc} +% % \newcommand{\empctx}{\ll \gg} +% \newcommand{\empctx}{[\;]} + +\newcommand{\fold}{\langkw{fold}\spac} +\newcommand{\unfold}{\langkw{unfold}\spac} + +\newcommand{\Pack}{\langkw{pack}\spac} +\newcommand{\Unpack}{\langkw{unpack}} + +\newcommand{\op}[1]{\mathrel{#1}} + +\newcommand{\binop}{\circledcirc} +\newcommand{\Plus}{\op{+}} +\newcommand{\Minus}{\op{-}} +\newcommand{\Mult}{\op{*}} +\newcommand{\Eq}{\op{=}} +\newcommand{\Lt}{\op{<}} + +\newcommand{\TT}{()} + +% types +\newcommand{\tvar}{\alpha} +\newcommand{\tvarB}{\beta} +\newcommand{\TVar}{\textdom{Tvar}} +\newcommand{\Expr}{\textdom{Expr}} + +\newcommand{\typ}{\tau} +\newcommand{\typB}{\rho} +\newcommand{\Tunit}{\mathbf{1}} +\newcommand{\Tbool}{\mathbb{B}} +% \newcommand{\Tnat}{\mathbb{N}} +\newcommand{\Tarr}{\ra} +\def\Tall #1.{\forall #1.\spac}% +\def\Texists #1.{\exists #1.\spac}% +\def\Tmu #1.{\mu #1.\spac}% +\def\Tref(#1){\textlang{ref}(#1)} + +\def\Tcont(#1){\textlang{cont}(#1)} + +\newcommand{\Tenv}{\Xi} +\newcommand{\env}{\Gamma} +\newcommand{\typed}[4]{#1 ~|~ #2 \vdash #3 : #4} +\newcommand{\cooptyped}[4]{#1 ~|~ #2 \vdash_{\mathsf{coop}} #3 : #4} +\newcommand{\seqtyped}[4]{#1 ~|~ #2 \vdash_{\mathsf{seq}} #3 : #4} +\newcommand{\coopvdash}{\vdash_{\mathsf{coop}}} +\newcommand{\seqvdash}{\vdash_{\mathsf{seq}}} +\newcommand{\ctxtyped}[7]{#1 : (#2~|~ #3; #4) \leadsto (#5~|~ #6; #7)} +\newcommand{\semtyped}[4]{#1 ~|~ #2 \vDash #3 : #4} + +%context refinement and logical relations +\newcommand{\ctxrefines}{\leq_{\text{ctx}}} +\newcommand{\ctxequiv}{\approx_{\text{ctx}}} +\newcommand{\logrefines}{\leq_{\text{log}}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Proofmode +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newcommand{\ipat}{\mathsf{ipat}} +\newcommand{\IName}[1]{#1} +\newcommand{\IAnom}{?} +\newcommand{\IDrop}{{\_\!\_}} +\newcommand{\IAnomPure}{\%} +\newcommand{\IPersistent}[1]{\#\ #1} +\newcommand{\IFalse}{[\;]} +\newcommand{\IConj}[2]{[\;#1\ #2\;]} +\newcommand{\IDisj}[2]{[\;#1 \mid #2\;]} +\newcommand{\iFrame}{\$} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Lists +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newcommand{\app}{\spac} +\newcommand{\reverse}{\mathsf{reverse}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Logical relations +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\semenv}{\Delta} +\newcommand{\semVtype}[3]{ \llbracket #1 \vdash #2 \rrbracket_{#3} } % #1 \vdash +\newcommand{\semEtype}[3]{ \mathcal{E}\llbracket #1 \vdash #2 \rrbracket_{#3} } % #1 \vdash +\newcommand{\semKtype}[3]{ \mathcal{K}\llbracket #1 \vdash #2 \rrbracket_{#3} } % #1 \vdash +\newcommand{\obrefines}{\mathcal{O}} +\newcommand{\crossobrefines}{\mathcal{O}^\mathsf{cross}} + +\endinput diff --git a/docs/general/src/macro.sty b/docs/general/src/macro.sty new file mode 100644 index 0000000..3cdbb3d --- /dev/null +++ b/docs/general/src/macro.sty @@ -0,0 +1,334 @@ +\def\stackreltwo#1#2{\mathrel{\mathop{#2}\limits^{#1}}} + +\newcommand{\gitree}{GITree\xspace} +\newcommand{\gitrees}{GITrees\xspace} +\newcommand{\IT}{\mathbf{IT}} +\newcommand{\ITv}{\mathbf{IT}^v} +\newcommand{\Ins}{\mathit{Ins}} +\newcommand{\Outs}{\mathit{Outs}} +\newcommand{\Type}{\mathit{Type}} +\newcommand{\Hom}{\mathit{Hom}} + +\newcommand{\foldIT}{\mathit{fold}} +\newcommand{\unfoldIT}{\mathit{unfold}} + +\newcommand{\Next}{\latertinj} +% IT constructors +\newcommand{\Error}{\mathtt{Error}} +\newcommand{\RunTime}{\mathit{RunTime}} +\newcommand{\Rret}{\mathsf{Ret}} +\newcommand{\Err}{\mathsf{Err}} +\newcommand{\Fun}{\mathsf{Fun}} +\newcommand{\Tau}{\mathsf{Tau}} +\newcommand{\Tick}{\mathsf{Tick}} +\newcommand{\Vis}{\mathsf{Vis}} +\newcommand{\idfun}{\mathsf{id}} + +\newcommand{\idx}{{\mathtt i}} + +\newcommand{\getfun}{\mathsf{get\_fun}} +\newcommand{\getval}{\mathsf{get\_val}} +\newcommand{\getnat}{\mathsf{get\_nat}} +\newcommand{\getret}{\mathsf{get\_ret}} + +\newcommand{\inl}{\textlog{inl}} +\newcommand{\inr}{\textlog{inr}} +\newcommand{\inj}{\textlog{inj}} + +% programming +\newcommand{\APPl}{\mathsf{App}_l} +\newcommand{\APPs}[2]{#1 \mathrel{\bullet} #2} +\newcommand{\APPsl}[2]{#1 \mathrel{(\latert\bullet)} #2} +\newcommand{\IF}{\mathsf{If}} +\newcommand{\NATOP}{\mathsf{NatOp}} +\newcommand{\SEQ}{\mathrel{;}} +\def\LET#1=#2IN{\mathsf{Let} \spac #1 \mathrel{=} #2 \spac \mathsf{in} \spac} +\newcommand{\WHILE}[2]{\mathsf{While} \spac #1 \spac \mathsf{do} \spac #2} + +% effects +\newcommand{\INPUT}{\mathsf{Input}} +\newcommand{\OUTPUT}{\mathsf{Output}} + +\newcommand{\ALLOC}{\mathsf{Alloc}} +\newcommand{\DEALLOC}{\mathsf{Dealloc}} +\newcommand{\READ}{\mathsf{Read}} +\newcommand{\WRITE}{\mathsf{Write}} +\newcommand{\callccEff}{\mathsf{CALLCC}} +\newcommand{\throwEff}{\mathsf{THROW}} + +\newcommand{\callccGT}{\mathrm{Callcc}} +\newcommand{\throwGT}{\mathrm{Throw}} + +% reification +\newcommand{\stateO}{\mathit{State}} +\newcommand{\optionO}{\mathit{option}} +\newcommand{\reify}{\mathsf{reify}} +\renewcommand{\Some}{\mathsf{Some}} + +\newcommand{\istep}{\rightsquigarrow} + +% object languages +\newcommand{\iocclang}{\lambda_{\mathsf{rec},\mathsf{io,callcc}}} +\newcommand{\iolang}{\lambda_{\mathsf{rec},\mathsf{io}}} +\newcommand{\Input}{\langkw{input}} +\newcommand{\Output}{\langkw{output} \spac} +\newcommand\bigcdot{\mathrel{\raisebox{1pt}{$\scriptscriptstyle\bullet$}}} +\newcommand\holed[1]{[\,#1\,]} +\newcommand\ctxhole{\holed\bigcdot} +\newcommand{\Tnat}{\mathsf{Nat}} +\newcommand{\scope}{\mathsf{scope}} +\newcommand{\fv}{\mathsf{fv}} + +% affine lang + +\newcommand{\afflang}{\lambda_{\mathsf{\multimap},\mathsf{ref}}} +\newcommand{\lolli}{{\color{orange}\multimap}} +\newcommand{\atensor}{{\color{orange}\otimes}} +\newcommand{\avar}{{\color{orange}a}} +\newcommand{\typeAff}{{\color{orange}\tau}} +\newcommand{\langkwa}[1]{\textlang{\color{orange} #1}} % Lars +\newcommand{\tBool}{\langkwa{Bool}} +\newcommand{\tNat}{\langkwa{Nat}} +\newcommand{\tUnit}{\langkwa{Unit}} +\newcommand{\tRef}[1]{{\langkwa{ref}\ #1}} +\newcommand{\unittt}{()} +\def\LamA #1.{{\color{orange}\lambda} #1.\spac}% +\newcommand{\aPair}[2]{{\color{orange}(}#1{\color{orange},}#2{\color{orange})}} +\def\LetA#1=#2in{\langkwa{let} \spac #1 \mathrel{{\color{orange}=}} #2 \spac \langkwa{in} \spac} +\newcommand{\aAlloc}{\langkwa{alloc}} +\newcommand{\aDealloc}{\langkwa{dealloc}} +\newcommand{\aReplace}{\langkwa{replace}} +\newcommand{\aCtx}{{\color{orange}\Omega}} +\newcommand{\provesAff}{\mathrel{{\color{orange}\proves}}} +\newcommand{\modelsAff}{\mathrel{{\color{orange}\models}}} +\newcommand{\aEmbed}[1]{{\color{orange}\llparenthesis} #1 {\color{orange}\rrparenthesis}} +\newcommand{\tyconv}[2]{#1 \sim {\color{orange}#2}} + + + +\newcommand{\Force}{\mathsf{Force}} +\newcommand{\Thunk}{\mathsf{Thunk}} +\newcommand{\protec}{\mathsf{protected}} + +% program logic +\newcommand{\hasstate}{\mathsf{has\_state}} +\newcommand{\heapctx}{\mathsf{heap\_ctx}} + +\newcommand{\AffSem}[1]{\mathit{Aff}\Sem{#1}} +\newcommand{\IOSem}[1]{\mathit{IO}\Sem{#1}} +\newcommand{\fromAff}{C} +\newcommand{\toAff}{{\color{orange}C}} + +% logical relation +\newcommand{\refines}{\precsim} +\newcommand{\EE}[1]{\mathcal{E}\Sem{#1}} +\newcommand{\AEE}[1]{{\color{orange}\mathcal{E}}\Sem{{\color{orange}#1}}} +\newcommand{\EK}[3]{\mathcal{E}^{#2}_{#1}(#3)} +\newcommand{\VV}[1]{\mathcal{V}\Sem{#1}} +\newcommand{\AVV}[1]{{\color{orange}\mathcal{V}}\Sem{{\color{orange}#1}}} +\newcommand{\VVCtx}[1]{\mathcal{V}^{\ast}\Sem{#1}} +\newcommand{\AVVCtx}[1]{{\color{orange}\mathcal{V}^{\ast}}\Sem{#1}} + +% subeffects/subreifiers +\newcommand{\subEff}[2]{#1 \rightarrowtail #2} +\newcommand{\subRet}[2]{#1 \rightharpoondown #2} + + +\makeatletter +\def\rightarrowtailfill@{\arrowfill@{\Yright\joinrel\relbar}\relbar\rightarrow} +\newcommand\xrightarrowtail[2][]{\ext@arrow 0055{\rightarrowtailfill@}{#1}{#2}} +\makeatother + +\newcommand{\subReifier}[3][]{#2 \xrightarrowtail[#1]{} #3} + + +%%%%% example programs and stuff +\newcommand{\factbody}{\mathsf{factBody}} +\newcommand{\fact}{\mathsf{fact}} +\newcommand{\acc}{{\mathit acc}} + +\newcommand{\sem}[1]{\llbracket{#1}\rrbracket} + +% Categories +% category +\newcommand{\cat}[1]{\mathscr{#1}} % Arbitrary category +\newcommand{\scat}[1]{\mathbf{#1}} % Arbitrary small category +\newcommand{\fcat}[1]{\mathbf{#1}} % Typeface for fixed categories + +\newcommand{\ovln}[1]{\overline{#1}} +\newcommand{\lwr}[1]{\mathbf{#1}} % \lwr{n} denotes n-element set +\newcommand{\rreg}[1]{\underline{#1}} % Regular representation +\newcommand{\ynt}[1]{\tilde{#1}} % Nat transf in Yoneda lemma +\newcommand{\yel}[1]{\hat{#1}} % Element in Yoneda lemma +\newcommand{\wideyel}[1]{\widehat{#1}} % Wide version of \yel + +\newcommand{\epsln}{\varepsilon} % \epsilon is not used anywhere + +\newcommand{\integers}{\mathbb{Z}} +\newcommand{\rationals}{\mathbb{Q}} +\newcommand{\reals}{\mathbb{R}} +\newcommand{\complexes}{\mathbb{C}} + +\DeclareMathOperator{\cset}{\cat{C}} % Set of closed subsets +\DeclareMathOperator{\Cl}{Cl} % Closure +\DeclareMathOperator{\Cone}{Cone} % Cones (in limit sense) +\DeclareMathOperator{\End}{\fcat{End}} % Endomorphisms +\DeclareMathOperator{\EqCat}{Eq} % Equalizer +\DeclareMathOperator{\ev}{ev} % Evaluation +\DeclareMathOperator{\HomCat}{Hom} % Hom-set/functor +\DeclareMathOperator{\HOM}{\fcat{Hom}} % Homs between vector spaces +\DeclareMathOperator{\im}{im} % Image +\DeclareMathOperator{\Lan}{Lan} % Left Kan extension +\DeclareMathOperator{\ob}{ob} % Object-set +\DeclareMathOperator{\oset}{\cat{O}} % Set of open subsets +\DeclareMathOperator{\pr}{pr} % Projection +\DeclareMathOperator{\psetCat}{\cat{P}} % Power set +\DeclareMathOperator{\Sub}{Sub} % Set of subobjects + +\newcommand{\h}{H} % Homs (e.g. \h_A means Hom(-, A)) +\newcommand{\opCat}{\mathrm{op}} % Opposite category +\newcommand{\true}{\texttt{true}} % Truth value "true" +\newcommand{\false}{\texttt{false}} % Truth value "false" + +\newcommand{\One}{\mathbf{1}} % Terminal category +\newcommand{\Two}{\mathbf{2}} % Single-arrow category +\newcommand{\Ab}{\fcat{Ab}} % Abelian groups +\newcommand{\Bilin}{\fcat{Bilin}} % Bilinear maps +\newcommand{\Cat}{\fcat{Cat}} % Small categories +\newcommand{\CAT}{\fcat{CAT}} % All categories +\newcommand{\CptHff}{\fcat{CptHff}} % Compact Hausdorff spaces +\newcommand{\CRing}{\fcat{CRing}} % Commutative rings +\newcommand{\FDVect}{\fcat{FDVect}} % Fin-dim vector spaces +\newcommand{\Field}{\fcat{Field}} % Fields +\newcommand{\FinSet}{\fcat{FinSet}} % Finite sets +\newcommand{\Fix}{\fcat{Fix}} % Fixed-point category +\newcommand{\Grp}{\fcat{Grp}} % Groups +\newcommand{\Mt}{\fcat{Mat}} % Matrices +\newcommand{\Mon}{\fcat{Mon}} % Monoids +\newcommand{\Ord}{\fcat{Ord}} % Total orders +\newcommand{\Ring}{\fcat{Ring}} % Rings +\newcommand{\Set}{\fcat{Set}} % Sets +\newcommand{\Sym}{\fcat{Sym}} % Permutations +\newcommand{\Tp}{\fcat{Top}} % Topological spaces +\newcommand{\Toph}{\fcat{Toph}} % Topo spaces + hty classes of maps +\newcommand{\Vect}{\fcat{Vect}} % Vector spaces + + +% CONSTANT SYMBOLS + + +\newcommand{\such}{\mathrel{|}} % Separator in set-builder notation +\newcommand{\Bigsuch}{\mathrel{\big|}} % Big version of \such +\newcommand{\without}{\setminus} % Set complement + +\newcommand{\emptybk}{\hspace*{.5em}} % Empty space used as blank +\newcommand{\blank}{(\emptybk)} % Generic blank +\newcommand{\dashbk}{-} % Dash used as blank +\newcommand{\bl}{\bullet} % Bullet used as blank + +\newcommand{\from}{{\colon}\linebreak[0]} % Colon for f: A --> B + +\newcommand{\iso}{\cong} % Isomorphism +\newcommand{\eqv}{\simeq} % Equivalence +\newcommand{\sub}{\subseteq} % Subset (possibly not proper) +\newcommand{\ladj}{\dashv} % Left adjoint +\newcommand{\divides}{\mathbin{\mid}} % For divisibility of integers +\newcommand{\of}{\mathbin{\circ}} % Composition + +\newcommand{\meet}{\wedge} % Joins and meets in ordered sets +\newcommand{\Meet}{\bigwedge} +\newcommand{\join}{\vee} +\renewcommand{\Join}{\bigvee} + +% MATHEMATICAL EXPRESSIONS TAKING ARGUMENTS + + +\newcommand{\ftrcat}[2]{[#1,#2]} % Functor category +\newcommand{\pshf}[1]{\ftrcat{#1^\op}{\Set}} % Presheaf category +\newcommand{\psh}[1]{\hat{#1}} % Alternative pshf cat + +\newcommand{\elt}[1]{\scat{E}(#1)} % Category of elements + +\newcommand{\colt}[1]{\lim\limits_{\rightarrow #1}} % Colimit +\newcommand{\lt}[1]{\lim\limits_{\leftarrow #1}} % Limit + +\newcommand{\abel}[1]{#1_{\mathrm{ab}}} % Abelianization +\newcommand{\comma}[2]{(#1 \mathbin{\Rightarrow} #2)} % Comma cat +\newcommand{\qer}[2]{#1/\mathord{#2}} % Eq reln for use after slash +\newcommand{\crd}[1]{\left|#1\right|} % Cardinality + + +% ARROWS + + +\newcommand{\oppairu}{\rightleftarrows} % Unlabelled opposing pair +\newcommand{\oppairua}{\leftrightarrows} % Same, but reversed +\newcommand{\parpairu}{\rightrightarrows} % Unlabelled parallel pair +\newcommand{\ot}{\leftarrow} % Left-pointing arrow +\newcommand{\toby}[1]{\stackrel{#1}{\longrightarrow}} % Labelled arrow +\newcommand{\otby}[1]{\stackrel{#1}{\longleftarrow}} % Left lblld arrow +\newcommand{\longto}{\longrightarrow} % Long labelled arrow +\newcommand{\toiso}{\toby{\textstyle{}_\sim}} % Isomorphism arrow +\newcommand{\incl}{\hookrightarrow} % Inclusion arrow +\newcommand{\mapsfromCat}{\mathrel{\reflectbox{\ensuremath{\mapsto}}}} +% Left-pointing \mapsto +\newcommand{\textiff}{\Longleftrightarrow} % Iff arrow for use in text +\newcommand{\textif}{\Longleftarrow} % If arrow for use in text +\newcommand{\textonlyif}{\Longrightarrow} % Only if arrow for text + + +\newcommand{\nent}{\rotatebox{45}{$\Rightarrow$}} +% North-east-pointing arrow for natural transformations +\newcommand{\nwnt}{\rotatebox{-45}{$\Leftarrow$}} % North-west +\newcommand{\swnt}{\rotatebox{45}{$\Leftarrow$}} % South-west +\newcommand{\sent}{\rotatebox{-45}{$\Rightarrow$}} % South-east +\newcommand{\neeq}{\rotatebox{45}{$=$}} + +\newcommand{\oppair}[4]{% + \xymatrix{% + #1 \ar@<.5ex>[r]^-{#3} &{#2}\ar@<.5ex>[l]^-{#4}% + }} +% Opposite-pointing pair of arrows, with arguments, for use in displays + +\newcommand{\oppairi}[4]{% + \xymatrix@1{% + #1 \ar@<.5ex>[r]^{#3} &{#2}\ar@<.5ex>[l]^{#4}% + }} +% Opposite-pointing pair of arrows, with arguments, for use in text + +\newcommand{\parpair}[4]{% + \xymatrix{% + #1 \ar@<.5ex>[r]^{#3} \ar@<-.5ex>[r]_{#4} % + }} +% Parallel pair of arrows, with arguments, for use in displays + +\newcommand{\parpairi}[4]{% + \xymatrix@1{% + #1 \ar@<.5ex>[r]^{#3} \ar@<-.5ex>[r]_{#4} % + }} +% Parallel pair of arrows, with arguments, for use in text + +\newcommand{\adjn}[4]{% + \xymatrix{ + #1 \ar@{}[d]|\ladj \ar@<1ex>[d]^{#4} \\ + #2 \ar@<1ex>[u]^{#3} + }} +% Adjunction, with arguments, for use in displays + +\newcommand{\hadjnli}[4]{% + \xymatrix@1{ + #1 \ar@<1.1ex>[r]^-{#3} \ar@{}[r]|-\bot  \ar@<1.1ex>[l]^-{#4}}} +% Adjunction, with arguments, for use in text (left adjt on top) + +\newcommand{\hadjnri}[4]{% + \xymatrix@1{ + #1 \ar@<1.1ex>[r]^-{#3} \ar@{}[r]|-\top  \ar@<1.1ex>[l]^-{#4}}} +% Adjunction, with arguments, for use in text (left adjt on bottom) + +\newcommand{\searrows}{\makebox[1em]{$\downarrow$% + \hspace*{-.2em}\raisebox{-1ex}{$\rightarrow$}}} +% Little diagram of anticlockwise path around a commutative square + +\newcommand{\esarrows}{\makebox[1em]{% + \raisebox{1ex}{$\rightarrow$}\hspace*{-.2em}$\downarrow$}} +% Little diagram of clockwise path around a commutative square \ No newline at end of file diff --git a/docs/general/src/main.tex b/docs/general/src/main.tex new file mode 100644 index 0000000..df600f5 --- /dev/null +++ b/docs/general/src/main.tex @@ -0,0 +1,143 @@ +\documentclass[a4paper]{article} + +\usepackage[utf8]{inputenc} +\usepackage[margin=1in]{geometry} +\usepackage[square,numbers]{natbib} +\usepackage{hyperref} +\usepackage{listings} +\usepackage{bussproofs} +\usepackage{fancyvrb} +\usepackage{booktabs} +\usepackage{subcaption} +\usepackage{todonotes} +\usepackage{xcolor} +\usepackage{tabularx} +\usepackage{comment} +\usepackage{mathtools} +\usepackage{csquotes} +\usepackage{mathpartir} +\usepackage{stmaryrd} +\usepackage{microtype} +\usepackage{standalone} +\usepackage{import} +\usepackage{multicol} +\usepackage{soul} +\usepackage[capitalize,nameinlink,noabbrev]{cleveref} +\usepackage[inline]{enumitem} +\usepackage{cmll} +\usepackage{amsfonts,amsmath,stmaryrd,amsthm,amssymb} +\usepackage[T1]{fontenc} +\usepackage[all]{xy} +\usepackage{xspace} +\usepackage{latexsym} +\usepackage{bbm} +\usepackage{mathrsfs} +\usepackage{graphicx} +\usepackage{color} +\usepackage[all]{xy} +\usepackage{stackrel} +\usepackage{iris} +\usepackage{syn} +\usepackage{macro} + +\usepackage{tikz} +\usepackage{tikz-cd} +\usetikzlibrary{automata, positioning, arrows} + +\tikzset{ + ->, % makes the edges directed + node distance=3cm, % specifies the minimum distance between two nodes. Change if necessary. + every state/.style={thick, fill=gray!10}, % sets the properties for each ’state’ node + initial text=$ $, % sets the text that appears on the start arrow +} + +\setlength{\columnsep}{0pc} + +\definecolor{dkgreen}{rgb}{0,0.6,0} +\definecolor{ltblue}{rgb}{0,0.4,0.4} +\definecolor{dkviolet}{rgb}{0.3,0,0.5} + +\newtheoremstyle{break} + {\topsep}{\topsep}% + {\itshape}{}% + {\bfseries}{}% + {\newline}{}% + +\lstset{basicstyle=\ttfamily} + +\newcommand{\citets}[1]{\citeauthor{#1}'s~[\citeyear{#1}]} + +\bibliographystyle{abbrvnat} + +\newtheorem{theorem}{Theorem}[section] +\newtheorem{corollary}{Corollary}[theorem] + +\newtheorem{lemma}[theorem]{Lemma} + +\theoremstyle{break} +\newtheorem{definition}{Definition}[section] + +\theoremstyle{remark} +\newtheorem*{remark}{Remark} + +\title{call/cc meets guarded interaction trees (note)} +\author{} +\date{\today} + +\begin{document} + +\maketitle + +\noindent + +\section*{Preface} +Non-trivial control flow operations, such as call/cc, provide immense +control over program execution but also make formal reasoning about +programming languages supporting it more complicated. In this note, we +provide denotational semantics of call/cc, defined in guarded +interaction trees, and prove that this semantics reflects the expected +operational behaviour. +\label{global:sec:preface} + +\tableofcontents + +\clearpage + +\section{Introduction} +\label{global:sec:intro} +\input{sections/intro} + +\section{Guarded interaction trees} +\label{global:sec:gitree} +\input{sections/gitree} + +\section{Language} +\label{global:sec:lang} +\input{sections/lang} + +\section{Reifiers} +\label{global:sec:reifier} +\input{sections/reifier} + +\section{Semantics} +\label{global:sec:sem} +\input{sections/sem} + +% \section{LTS} +% \label{global:sec:lts} +% \input{sections/lts} + +% \section{Gitrees in topos of trees} +% \label{global:sec:tot} +% \input{sections/tot} + +\nocite{*} +\bibliography{refs} + +\end{document} +\endinput + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff --git a/docs/general/src/refs.bib b/docs/general/src/refs.bib new file mode 100644 index 0000000..1650d6f --- /dev/null +++ b/docs/general/src/refs.bib @@ -0,0 +1,356 @@ +@article{DBLP:journals/pacmpl/FruminTB24, + author = {Dan Frumin and + Amin Timany and + Lars Birkedal}, + title = {Modular Denotational Semantics for Effects with Guarded Interaction + Trees}, + journal = {Proc. {ACM} Program. Lang.}, + volume = {8}, + number = {{POPL}}, + pages = {332--361}, + year = {2024}, + url = {https://doi.org/10.1145/3632854}, + doi = {10.1145/3632854}, + timestamp = {Thu, 25 Jan 2024 09:55:47 +0100}, + biburl = {https://dblp.org/rec/journals/pacmpl/FruminTB24.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/pacmpl/TimanyB19, + author = {Amin Timany and + Lars Birkedal}, + title = {Mechanized relational verification of concurrent programs with continuations}, + journal = {Proc. {ACM} Program. Lang.}, + volume = {3}, + number = {{ICFP}}, + pages = {105:1--105:28}, + year = {2019}, + url = {https://doi.org/10.1145/3341709}, + doi = {10.1145/3341709}, + timestamp = {Wed, 17 Feb 2021 08:53:58 +0100}, + biburl = {https://dblp.org/rec/journals/pacmpl/TimanyB19.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/ifip2/FelleisenF87, + author = {Matthias Felleisen and + Daniel P. Friedman}, + editor = {Martin Wirsing}, + title = {Control operators, the SECD-machine, and the {\(\lambda\)}-calculus}, + booktitle = {Formal Description of Programming Concepts - {III:} Proceedings of + the {IFIP} {TC} 2/WG 2.2 Working Conference on Formal Description + of Programming Concepts - III, Ebberup, Denmark, 25-28 August 1986}, + pages = {193--222}, + publisher = {North-Holland}, + year = {1987}, + timestamp = {Thu, 10 Jan 2019 14:38:20 +0100}, + biburl = {https://dblp.org/rec/conf/ifip2/FelleisenF87.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/fsen/Berger09, + author = {Martin Berger}, + editor = {Farhad Arbab and + Marjan Sirjani}, + title = {Program Logics for Sequential Higher-Order Control}, + booktitle = {Fundamentals of Software Engineering, Third {IPM} International Conference, + {FSEN} 2009, Kish Island, Iran, April 15-17, 2009, Revised Selected + Papers}, + series = {Lecture Notes in Computer Science}, + volume = {5961}, + pages = {194--211}, + publisher = {Springer}, + year = {2009}, + url = {https://doi.org/10.1007/978-3-642-11623-0\_11}, + doi = {10.1007/978-3-642-11623-0\_11}, + timestamp = {Tue, 15 Nov 2022 15:22:35 +0100}, + biburl = {https://dblp.org/rec/conf/fsen/Berger09.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/popl/BirkedalRSSTY11, + author = {Lars Birkedal and + Bernhard Reus and + Jan Schwinghammer and + Kristian St{\o}vring and + Jacob Thamsborg and + Hongseok Yang}, + editor = {Thomas Ball and + Mooly Sagiv}, + title = {Step-indexed kripke models over recursive worlds}, + booktitle = {Proceedings of the 38th {ACM} {SIGPLAN-SIGACT} Symposium on Principles + of Programming Languages, {POPL} 2011, Austin, TX, USA, January 26-28, + 2011}, + pages = {119--132}, + publisher = {{ACM}}, + year = {2011}, + url = {https://doi.org/10.1145/1926385.1926401}, + doi = {10.1145/1926385.1926401}, + timestamp = {Thu, 24 Jun 2021 16:19:31 +0200}, + biburl = {https://dblp.org/rec/conf/popl/BirkedalRSSTY11.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/lfp/DanvyF90, + author = {Olivier Danvy and + Andrzej Filinski}, + editor = {Gilles Kahn}, + title = {Abstracting Control}, + booktitle = {Proceedings of the 1990 {ACM} Conference on {LISP} and Functional + Programming, {LFP} 1990, Nice, France, 27-29 June 1990}, + pages = {151--160}, + publisher = {{ACM}}, + year = {1990}, + url = {https://doi.org/10.1145/91556.91622}, + doi = {10.1145/91556.91622}, + timestamp = {Fri, 06 Aug 2021 15:08:55 +0200}, + biburl = {https://dblp.org/rec/conf/lfp/DanvyF90.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/icfp/DelbiancoN13, + author = {Germ{\'{a}}n Andr{\'{e}}s Delbianco and + Aleksandar Nanevski}, + editor = {Greg Morrisett and + Tarmo Uustalu}, + title = {Hoare-style reasoning with (algebraic) continuations}, + booktitle = {{ACM} {SIGPLAN} International Conference on Functional Programming, + ICFP'13, Boston, MA, {USA} - September 25 - 27, 2013}, + pages = {363--376}, + publisher = {{ACM}}, + year = {2013}, + url = {https://doi.org/10.1145/2500365.2500593}, + doi = {10.1145/2500365.2500593}, + timestamp = {Thu, 24 Jun 2021 16:19:30 +0200}, + biburl = {https://dblp.org/rec/conf/icfp/DelbiancoN13.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/popl/Dinsdale-YoungBGPY13, + author = {Thomas Dinsdale{-}Young and + Lars Birkedal and + Philippa Gardner and + Matthew J. Parkinson and + Hongseok Yang}, + editor = {Roberto Giacobazzi and + Radhia Cousot}, + title = {Views: compositional reasoning for concurrent programs}, + booktitle = {The 40th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of + Programming Languages, {POPL} '13, Rome, Italy - January 23 - 25, + 2013}, + pages = {287--300}, + publisher = {{ACM}}, + year = {2013}, + url = {https://doi.org/10.1145/2429069.2429104}, + doi = {10.1145/2429069.2429104}, + timestamp = {Sat, 31 Jul 2021 17:22:15 +0200}, + biburl = {https://dblp.org/rec/conf/popl/Dinsdale-YoungBGPY13.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/corr/abs-1103-0510, + author = {Derek Dreyer and + Amal Ahmed and + Lars Birkedal}, + title = {Logical Step-Indexed Logical Relations}, + journal = {Log. Methods Comput. Sci.}, + volume = {7}, + number = {2}, + year = {2011}, + url = {https://doi.org/10.2168/LMCS-7(2:16)2011}, + doi = {10.2168/LMCS-7(2:16)2011}, + timestamp = {Sun, 16 Apr 2023 20:31:20 +0200}, + biburl = {https://dblp.org/rec/journals/corr/abs-1103-0510.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/jfp/DreyerNB12, + author = {Derek Dreyer and + Georg Neis and + Lars Birkedal}, + title = {The impact of higher-order state and control effects on local relational + reasoning}, + journal = {J. Funct. Program.}, + volume = {22}, + number = {4-5}, + pages = {477--528}, + year = {2012}, + url = {https://doi.org/10.1017/S095679681200024X}, + doi = {10.1017/S095679681200024X}, + timestamp = {Sat, 27 May 2017 14:24:34 +0200}, + biburl = {https://dblp.org/rec/journals/jfp/DreyerNB12.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/popl/Felleisen88, + author = {Matthias Felleisen}, + editor = {Jeanne Ferrante and + Peter Mager}, + title = {The Theory and Practice of First-Class Prompts}, + booktitle = {Conference Record of the Fifteenth Annual {ACM} Symposium on Principles + of Programming Languages, San Diego, California, USA, January 10-13, + 1988}, + pages = {180--190}, + publisher = {{ACM} Press}, + year = {1988}, + url = {https://doi.org/10.1145/73560.73576}, + doi = {10.1145/73560.73576}, + timestamp = {Thu, 16 Sep 2021 11:02:28 +0200}, + biburl = {https://dblp.org/rec/conf/popl/Felleisen88.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/tcs/FelleisenH92, + author = {Matthias Felleisen and + Robert Hieb}, + title = {The Revised Report on the Syntactic Theories of Sequential Control + and State}, + journal = {Theor. Comput. Sci.}, + volume = {103}, + number = {2}, + pages = {235--271}, + year = {1992}, + url = {https://doi.org/10.1016/0304-3975(92)90014-7}, + doi = {10.1016/0304-3975(92)90014-7}, + timestamp = {Wed, 17 Feb 2021 21:58:59 +0100}, + biburl = {https://dblp.org/rec/journals/tcs/FelleisenH92.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/popl/FriedmanH85, + author = {Daniel P. Friedman and + Christopher T. Haynes}, + editor = {Mary S. Van Deusen and + Zvi Galil and + Brian K. Reid}, + title = {Constraining Control}, + booktitle = {Conference Record of the Twelfth Annual {ACM} Symposium on Principles + of Programming Languages, New Orleans, Louisiana, USA, January 1985}, + pages = {245--254}, + publisher = {{ACM} Press}, + year = {1985}, + url = {https://doi.org/10.1145/318593.318654}, + doi = {10.1145/318593.318654}, + timestamp = {Tue, 06 Nov 2018 11:07:43 +0100}, + biburl = {https://dblp.org/rec/conf/popl/FriedmanH85.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/icfp/0002KBD16, + author = {Ralf Jung and + Robbert Krebbers and + Lars Birkedal and + Derek Dreyer}, + editor = {Jacques Garrigue and + Gabriele Keller and + Eijiro Sumii}, + title = {Higher-order ghost state}, + booktitle = {Proceedings of the 21st {ACM} {SIGPLAN} International Conference on + Functional Programming, {ICFP} 2016, Nara, Japan, September 18-22, + 2016}, + pages = {256--269}, + publisher = {{ACM}}, + year = {2016}, + url = {https://doi.org/10.1145/2951913.2951943}, + doi = {10.1145/2951913.2951943}, + timestamp = {Sat, 30 Sep 2023 09:45:14 +0200}, + biburl = {https://dblp.org/rec/conf/icfp/0002KBD16.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/jfp/JungKJBBD18, + author = {Ralf Jung and + Robbert Krebbers and + Jacques{-}Henri Jourdan and + Ales Bizjak and + Lars Birkedal and + Derek Dreyer}, + title = {Iris from the ground up: {A} modular foundation for higher-order concurrent + separation logic}, + journal = {J. Funct. Program.}, + volume = {28}, + pages = {e20}, + year = {2018}, + url = {https://doi.org/10.1017/S0956796818000151}, + doi = {10.1017/S0956796818000151}, + timestamp = {Sat, 30 Sep 2023 10:19:01 +0200}, + biburl = {https://dblp.org/rec/journals/jfp/JungKJBBD18.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/popl/JungSSSTBD15, + author = {Ralf Jung and + David Swasey and + Filip Sieczkowski and + Kasper Svendsen and + Aaron Turon and + Lars Birkedal and + Derek Dreyer}, + editor = {Sriram K. Rajamani and + David Walker}, + title = {Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent + Reasoning}, + booktitle = {Proceedings of the 42nd Annual {ACM} {SIGPLAN-SIGACT} Symposium on + Principles of Programming Languages, {POPL} 2015, Mumbai, India, January + 15-17, 2015}, + pages = {637--650}, + publisher = {{ACM}}, + year = {2015}, + url = {https://doi.org/10.1145/2676726.2676980}, + doi = {10.1145/2676726.2676980}, + timestamp = {Sat, 30 Sep 2023 09:54:52 +0200}, + biburl = {https://dblp.org/rec/conf/popl/JungSSSTBD15.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/esop/Krebbers0BJDB17, + author = {Robbert Krebbers and + Ralf Jung and + Ales Bizjak and + Jacques{-}Henri Jourdan and + Derek Dreyer and + Lars Birkedal}, + editor = {Hongseok Yang}, + title = {The Essence of Higher-Order Concurrent Separation Logic}, + booktitle = {Programming Languages and Systems - 26th European Symposium on Programming, + {ESOP} 2017, Held as Part of the European Joint Conferences on Theory + and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, + 2017, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {10201}, + pages = {696--723}, + publisher = {Springer}, + year = {2017}, + url = {https://doi.org/10.1007/978-3-662-54434-1\_26}, + doi = {10.1007/978-3-662-54434-1\_26}, + timestamp = {Sat, 30 Sep 2023 09:40:24 +0200}, + biburl = {https://dblp.org/rec/conf/esop/Krebbers0BJDB17.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/popl/KrebbersTB17, + author = {Robbert Krebbers and + Amin Timany and + Lars Birkedal}, + editor = {Giuseppe Castagna and + Andrew D. Gordon}, + title = {Interactive proofs in higher-order concurrent separation logic}, + booktitle = {Proceedings of the 44th {ACM} {SIGPLAN} Symposium on Principles of + Programming Languages, {POPL} 2017, Paris, France, January 18-20, + 2017}, + pages = {205--217}, + publisher = {{ACM}}, + year = {2017}, + url = {https://doi.org/10.1145/3009837.3009855}, + doi = {10.1145/3009837.3009855}, + timestamp = {Mon, 28 Aug 2023 21:17:40 +0200}, + biburl = {https://dblp.org/rec/conf/popl/KrebbersTB17.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + + + + + + + diff --git a/docs/general/src/sections/gitree.tex b/docs/general/src/sections/gitree.tex new file mode 100644 index 0000000..5aafa7b --- /dev/null +++ b/docs/general/src/sections/gitree.tex @@ -0,0 +1,108 @@ +Guarded Interaction trees (\gitrees) are constructed as a guarded +recursive type parameterized over two input types: $E$ that provides +an effect signature, which specifies effects that can occur, and their +arity. $A$ specifies a ground type that allows addition of new +primitive values. The type has five constructors: $\Rret$ --- wraps +ground type expressions, $\Fun$ extends the domain to contain +functions, $\Err$ constructor, $\Tau$ constructor that makes \gitrees +into guarded domain, and $\Vis$ that accepts a function from inputs of +some effect (that can involve \gitrees themselves, which allow us to +represent higher-order effects), a function from outputs of the same +effect to gitrees, which represents continuations of effects. + +\gitrees admit an operational semantics given reifiers for all effects +in the signature. A reifier of an effect $i$ is a function of type +shown in~\cref{fig:reifier_sig}. Assuming we have such reifiers for +all effects, we write a function $\reify : \IT \times \stateO \to \IT +\times \stateO$ that satisfies the equations in~\cref{fig:reify_def}. +Note that reifiers don't take continuation into account. Now we can +define a step to be either removing a single $\Tick$ (where $\Tick +\eqdef \Tau \circ \Next$), or reification of the head effect. + +Let us now define a class of homomorphic functions, formally defined +in~\cref{fig:hom}, to be functions that act as identities on errors, +and preserve $\Tick$ and $\Vis$ constructors. + +Now, given $\istep$ representing operational semantics of \gitrees, +and homomorphic functions, representing context of \gitrees. We can +define program logic for a language of \gitrees, including important +wp-bind and wp-reify rules (\cref{fig:wp_rules}), which allow to +modular reasoning about \gitrees and effects respectfully. + +\begin{figure}[t] + \begin{align*} + \mathsf{guarded\ type}\ \IT_E(A) &{}= \Rret : A \to \IT_E\\ + &\ \ALT \Fun : \latert (\IT_E(A) \to \IT_E(A)) \to \IT_E(A)\\ + &\ \ALT \Err : \Error \to \IT_E(A)\\ + &\ \ALT \Tau : \latert \IT_E(A) \to \IT_E(A) \\ + &\ \ALT \Vis : \prod_{\idx \in \mathtt{I}} \big( \Ins_{\idx}(\latert \IT_E(A)) \times (\Outs_{\idx}(\latert \IT_E(A)) \to \latert \IT_E(A))\big) \to \IT_E(A) + \end{align*} + + \caption{Guarded datatype of interaction trees.} + \label{fig:gitrees_def} +\end{figure} + +\begin{figure} + \[ + r : \prod_{\idx \in E} \Ins_{\idx}(\latert \IT_E) \times \stateO \to \optionO(\Outs_{\idx}(\latert\IT_E) \times \stateO). + \] + \caption{Signature of reifiers.} + \label{fig:reifier_sig} +\end{figure} + +\begin{figure} + \begin{mathpar} + \infer + {r_i(x,\sigma) = \Some(y, \sigma') \and k\ y = \Next(\beta)} + {\reify(\Vis_i(x, k), \sigma) = (\Tick(\beta), \sigma')} + \and + \infer + {r_i(x,\sigma) = \None} + {\reify(\Vis_i(x, k), \sigma) = (\Err(\RunTime), \sigma)} + \end{mathpar} + \caption{Reification definition.} + \label{fig:reify_def} +\end{figure} + +\begin{figure} + \[ + (\alpha,\sigma) \istep (\beta,\sigma') \eqdef + \big(\alpha = \Tick(\beta) \wedge \sigma = \sigma' \big) + \vee \big(\Exists i\,x\,k. \alpha = \Vis_i(x,k) + \wedge \reify(\alpha,\sigma) = (\Tick(\beta),\sigma')\big) + \] + \caption{Operational semantics of Guarded interaction trees.} + \label{fig:opsem_gitrees} +\end{figure} + +\begin{figure} + \begin{itemize} + \item $f(\Err(e)) = \Err(e)$; + \item $f(\Tick(\alpha)) = \Tick(f(\alpha))$; + \item $f(\Vis_i(x,k)) = \Vis_i(x, \latert f \circ k)$ + \end{itemize} + \caption{Homomorphisms} + \label{fig:hom} +\end{figure} + +\begin{figure} + \begin{mathpar} + \inferrule[wp-reify] + {\hasstate(\sigma) \and + \reify(\Vis_i(x,k), \sigma) = (\Tick(\beta), \sigma') + \and + \later\big(\hasstate(\sigma') \wand \wpre{\beta}{\Phi} \big)} + {\wpre{\Vis_i(x, k)}{\Phi}} + \and + \inferrule[wp-hom] + {f \in \Hom \and \wpre{\alpha}{\Ret \beta_v. \wpre{f(\beta_v)}{\Phi}}} + {\wpre{f(\alpha)}{\Phi}} + \end{mathpar} + \caption{Selected weakest precondition rules.} + \label{fig:wp_rules} +\end{figure} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../main" +%%% End: diff --git a/docs/general/src/sections/intro.tex b/docs/general/src/sections/intro.tex new file mode 100644 index 0000000..09c5053 --- /dev/null +++ b/docs/general/src/sections/intro.tex @@ -0,0 +1,18 @@ +In this note, we investigate the extension to Guarded Interaction Trees to +support context-dependent effects (e.g., call/cc and throw). + +This note is divided into a few sections. In~\cref{global:sec:gitree} we +recall definition and relevant properties of guarded interaction +trees. In~\cref{global:sec:lang} we describe the calculus with callcc, +which we study in this note. In~\cref{global:sec:reifier} we describe +modifications to guarded interaction trees required to interpret +context-dependent effects. In~\cref{global:sec:sem} we provide a +denotational model for a language with callcc in guarded interaction +trees with modifications and prove soundness and adequacy of the +model. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../main" +%%% TeX-master: "../main" +%%% End: diff --git a/docs/general/src/sections/lang.tex b/docs/general/src/sections/lang.tex new file mode 100644 index 0000000..7056f25 --- /dev/null +++ b/docs/general/src/sections/lang.tex @@ -0,0 +1,151 @@ +In this section we describe our target language, $\iocclang$. + +$\iocclang$, presented in~\cref{fig:syn_lang}, is a lambda calculus +with recursive functions, primitive natural numbers and operations on +them, input/output operations, call/cc, and throw. In addition, it has +first-order evaluation contexts. + +$\callcc{\var}{\expr}$ stands for a computation that takes the current +evaluation context (i.e., the evaluation context, where the term is +being evaluated), and binds it with $\var$ in $\expr$. +$\throw{\expr_1}{\expr_2}$ takes two arguments, the first being any +expression, and the second being an evaluation context. + +$\iocclang$ has a type system, shown in~\cref{fig:stat_sem_lang}, that +includes natural numbers type, function type and a type or +continuations that accept expressions of type $\tau$, represented by +$\tcont{\tau}$. + +Operational semantics on this language is presented +in~\cref{fig:dyn_sem_lang,fig:dyn_global_sem_lang}. It is separated +into two relations. The first relation is for local reductions of +primitive expressions, while the second one accounts for steps lifted +to complete programs. Both relations are parameterized over +configurations that contain expressions and states, where states are +two lists of natural numbers, representing input and output tapes +respectfully. In addition, the local relation is parameterized over +evaluation context, which allows $\callcc{\var}{\expr}$ to capture the +whole evaluation context. + +To give an interpretation of this language we need to provide an +effect signature, and interpretations for all effectful computations +that it exhibits. + +Let us start by the effect signature, shown +in~\cref{fig:eff_sig_lang}. The language contains four different +effects: $\mathtt{input}$, $\mathtt{output}$, $\mathtt{callcc}$, +$\mathtt{throw}$. $\mathtt{input}$ doesn't require any arguments and +yields back a natural number, so its input has type $\Tunit$, and its +output has type $\Tnat$. Similar reasoning is also applicable to +$\mathtt{output}$. $\mathtt{callcc}$ and $\mathtt{throw}$, on the +other hand, require higher-order arguments. The behavior of +$\callcc{\var}{\expr}$ is determined by its body that binds a +continuation and utilizes it, so a natural approach is to require +that its input is of type of its body, $(\latert X \rightarrow \latert +X) \rightarrow \latert X$. Moreover, the result of +$\callcc{\var}{\expr}$ is determined by its body, so its output is +$\latert X$. $\throw{\expr_1}{\expr_2}$ requires an expression and a +continuation, which are represented respectfully as $\latert X$ and +$\latert (X \rightarrow X)$. As for the output, +$\throw{\expr_1}{\expr_2}$ discard the current continuation, hence it +is safe to assume that its continuation is a unique function out of +the empty type. + +We write $\INPUT$, $\OUTPUT(n)$, $\callccGT(f)$, and $\throwGT(e)$ for +the \gitrees defined in~\cref{fig:io_constructors}. + +\begin{figure} + \begin{grammar} + \text{types} & \tau & \tnat \mid \tarr{\tau_1}{\tau_2} \mid \tcont{\tau} \\ + \text{expressions} & \expr & \val \mid \var \mid \eapp{\expr_1}{\expr_2} \mid \natop{\expr_1}{\expr_2} \mid \Input \mid \Output \expr \mid \If \expr_1 then \expr_2 \Else \expr_3 \\ + \GrmContinue & \mid \callcc{\var}{\expr} \mid \throw{\expr_1}{\expr_2} \\ + \text{values} & \val & n \mid \Rec f \var = \expr \mid \cont{K} \\ + \text{evaluation contexts} & K & \emptyK \mid \Output K \mid \If K then \expr_1 \Else \expr_2 \mid \eapp{K}{\val} \mid \eapp{\expr}{K} \mid \natop{\expr}{K} \mid \natop{K}{\val} \\ + \GrmContinue & \mid \throw{K}{\expr} \mid \throw{\val}{K} + \end{grammar} + \caption{Syntax of $\iocclang$.} + \label{fig:syn_lang} +\end{figure} + +\begin{figure} + \begin{mathpar} + \inferrule{\var \col \tau \in \Gamma}{\typeA{\Gamma}{\var}{\tau}} + \and + \inferrule{\typeA{\Gamma, f \col \tarr{\tau_1}{\tau_2}, \var \col \tau_1}{\expr}{\tau_2}}{\typeA{\Gamma}{\Rec f \var = \expr}{\tarr{\tau_1}{\tau_2}}} + \and + \inferrule{\typeA{\Gamma}{\expr_1}{\tarr{\tau_1}{\tau_2}} \\ \typeA{\Gamma}{\expr_2}{\tau_1}}{\typeA{\Gamma}{\eapp{\expr_1}{\expr_2}}{\tau_2}} + \and + \inferrule{}{\typeA{\Gamma}{\Input}{\tnat}} + \and + \inferrule{\typeA{\Gamma}{\expr_1}{\tnat} \\ \typeA{\Gamma}{\expr_2}{\tau} \\ \typeA{\Gamma}{\expr_3}{\tau}}{\typeA{\Gamma}{\If \expr_1 then \expr_2 \Else \expr_3}{\tau}} + \and + \inferrule{\typeA{\Gamma}{\expr}{\tnat}}{\typeA{\Gamma}{\Output \expr}{\tnat}} + \and + \inferrule{}{\typeA{\Gamma}{n}{\tnat}} + \and + \inferrule{\typeA{\Gamma}{\expr_1}{\tnat} \\ \typeA{\Gamma}{\expr_2}{\tnat}}{\typeA{\Gamma}{\natop{\expr_1}{\expr_2}}{\tnat}} + \and + \inferrule{\typeA{\Gamma, \var \col \cont{\tau}}{\expr}{\tau}}{\typeA{\Gamma}{\callcc{\var}{\expr}}{\tau}} + \and + \inferrule{\typeA{\Gamma}{\expr_1}{\tau} \\ \typeA{\Gamma}{\expr_2}{\cont{\tau}}}{\typeA{\Gamma}{\throw{\expr_1}{\expr_2}}{\tau'}} + \end{mathpar} + \caption{Static semantics $\iocclang$.} + \label{fig:stat_sem_lang} +\end{figure} + +\begin{figure} + \begin{mathpar} + \inferrule{}{\contrA{\eapp{\Rec f \var = \expr}{\val}, \sigma}{\subst{\subst{\expr}{f}{\Rec f \var = \expr}}{\var}{\val}, \sigma}{K}} + \and + \inferrule{}{\contrA{\If 0 then \expr_1 \Else \expr_2, \sigma}{\expr_2, \sigma}{K}} + \and + \inferrule{0 < n}{\contrA{\If n then \expr_1 \Else \expr_2, \sigma}{\expr_1, \sigma}{K}} + \and + \inferrule{\natop{n_1}{n_2} = n_3}{\contrA{\natop{n_1}{n_2}, \sigma}{n_3, \sigma}{K}} + \and + \inferrule{}{\contrA{\Input, (n\overline{n}, \overline{m})}{n, (\overline{n}, \overline{m})}{K}} + \and + \inferrule{}{\contrA{\Output m, (\overline{n}, \overline{m})}{0, (\overline{n}, m\overline{m})}{K}} + \and + \inferrule{}{\contrA{\callcc{\var}{\expr}, \sigma}{\subst{\expr}{\var}{\cont{K}}, \sigma}{K}} + \end{mathpar} + \caption{Dynamic semantics of $\iocclang$ (head-steps).} + \label{fig:dyn_sem_lang} +\end{figure} + +\begin{figure} + \begin{mathpar} + \inferrule{}{\contr{\plug{K}{\throw{\val}{\cont{K'}}}, \sigma}{\plug{K'}{\val}, \sigma}} + \and + \inferrule{\contrA{\expr_1, \sigma_1}{\expr_2, \sigma_2}{K}}{\contr{\plug{K}{\expr_1}, \sigma_1}{\plug{K}{\expr_2}, \sigma_2}} + \end{mathpar} + \caption{Dynamic semantics of $\iocclang$ (global-steps).} + \label{fig:dyn_global_sem_lang} +\end{figure} + +\begin{figure} + \begin{align*} + E_{io, callcc} &\eqdef \{\mathtt{input}, \mathtt{output}, \mathtt{callcc}, \mathtt{throw}\} &\\ + \Ins_{\mathtt{input}}(X) &\eqdef \Tunit & \Outs_{\mathtt{input}}(X) &\eqdef \Tnat\\ + \Ins_{\mathtt{output}}(X) &\eqdef \Tnat & \Outs_{\mathtt{ouput}}(X) &\eqdef \Tunit\\ + \Ins_{\mathtt{callcc}}(X) &\eqdef ((\latert X \rightarrow \latert X) \rightarrow \latert X) & \Outs_{\mathtt{callcc}}(X) &\eqdef \latert X \\ + \Ins_{\mathtt{throw}}(X) &\eqdef \latert X \times \latert (X \rightarrow X) & \Outs_{\mathtt{throw}}(X) &\eqdef O + \end{align*} + \caption{Effect signature for $\iocclang$.} + \label{fig:eff_sig_lang} +\end{figure} + +\begin{figure} + \begin{align*} + \INPUT \eqdef \Vis_{\mathtt{input}}((), \Lam n. \Next(\Rret(\inr(n)))) && \OUTPUT(n) \eqdef \Vis_{\mathtt{output}}(n, \Lam x. \Next (\Rret(\inl(())))) \\ + \callccGT(f) \eqdef \Vis_{\mathtt{callcc}}{(f, \imath)} && + \throwGT(e, f) \eqdef \Vis_{\mathtt{throw}}{(e, f, \mathrm{elim-0})} + \end{align*} + \caption{\gitrees for effects} + \label{fig:io_constructors} +\end{figure} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../main" +%%% End: diff --git a/docs/general/src/sections/lts.tex b/docs/general/src/sections/lts.tex new file mode 100644 index 0000000..dfce2b1 --- /dev/null +++ b/docs/general/src/sections/lts.tex @@ -0,0 +1,77 @@ +We aim to provide labeled transition systems corresponding +to visible effects happening in programs written in guarded interaction +trees. We pursue two aims. First, we want to study these LTSs as they are. +Second, we want to have an ability to hide some effects in case they are +invisible to external observers. Last, we want to be able to relate +two or more LTSs corresponding to different programs to argue +that they simulate each other up to possible hidden effects. +Thus, we can study security properties of programs, and, moreover, +obtain stronger reasoning principles for relating programs. + +\begin{figure} + \begin{align*} + E_{nondet} &\eqdef \{\mathtt{flip}\} \\ + \Ins_{\mathtt{flip}}(X) &\eqdef \Tunit \\ + \Outs_{\mathtt{flip}}(X) &\eqdef \Tbool \\ + \mathtt{br}~x~y & \eqdef \Vis_{\mathtt{flip}}((), \Lam b. \IF b \{ x \} \{ y \}) \\ + r_{\mathtt{flip}}((),b\vec{b},\kappa) &= \Some(\kappa~b, \vec{b}) + \end{align*} + \caption{state is a coinductive list of booleans} +\end{figure} + +\begin{align*} + \mathsf{spin} \cceq \MU a \col \latert \IT. \Tau(a) \equiv \Tick(\mathsf{spin}) +\end{align*} +\begin{align*} + \mathsf{p} \cceq \WHILE{\true}{\OUTPUT~0} \equiv \OUTPUT~0 \SEQ \WHILE{\true}{\OUTPUT~0} \equiv \dots +\end{align*} +\begin{align*} + \mathsf{q} \cceq \mathsf{br}~\mathsf{spin}~\mathsf{p} +\end{align*} + +\begin{align*} + (\alpha, \sigma) \prec^{\tau} (\beta, \sigma') & \cceq \alpha = \Tick(\beta) \wedge \sigma = \sigma' \\ + (\alpha, \sigma) \prec^{i_{x}} (\beta, \sigma') & \cceq \Exists i\,x\,k. \alpha = \Vis_i(x,k) + \wedge \reify(\alpha,\sigma) = (\Tick(\beta),\sigma') +\end{align*} + +\begin{figure} + \begin{tikzpicture} + \node[state] (1) {$\mathsf{q}$}; + \node[state, below left of=1] (2) {$\mathsf{p}$}; + \node[state, right of=2] (3) {$\mathsf{spin}$}; + \draw (2) edge[above] node{$\mathsf{flip}_{\mathsf{false}}$} (1) + (3) edge[loop right] node{$\tau$} (3) + (1) edge[loop right] node{$\OUTPUT~0$} (1) + (2) edge[below] node{$\mathsf{flip}_{\mathsf{true}}$} (3); + \end{tikzpicture} + \caption{reifiers are the same} +\end{figure} + +\begin{figure} + \begin{tikzpicture} + \node[state] (1) {$\mathsf{q}$}; + \node[state, below left of=1] (2) {$\mathsf{p}$}; + \node[state, right of=2] (3) {$\mathsf{spin}$}; + \draw (2) edge[above] node{$\tau$} (1) + (3) edge[loop right] node{$\tau$} (3) + (1) edge[loop right] node{$\OUTPUT~0$} (1) + (2) edge[below] node{$\tau$} (3); + \end{tikzpicture} + \caption{some effects can be marked as hidden} +\end{figure} + +\begin{figure} + \begin{tikzpicture} + \node[state] (1) {$\mathsf{q}$}; + \node[state, below left of=1] (2) {$\mathsf{p}$}; + \draw (2) edge[above] node{$\OUTPUT~0$} (1) + (1) edge[loop right] node{$\OUTPUT~0$} (1); + \end{tikzpicture} + \caption{wip} +\end{figure} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../main" +%%% End: diff --git a/docs/general/src/sections/reifier.tex b/docs/general/src/sections/reifier.tex new file mode 100644 index 0000000..aa89929 --- /dev/null +++ b/docs/general/src/sections/reifier.tex @@ -0,0 +1,106 @@ +Now, if we want to reason about a language with control operations, +such as $\iocclang$, we have to provide reifiers for its effects. +However, in the current setup, we cannot do that. Consider +$\callccGT(f)$. Before passing results of reification to the current +continuation, it is supposed to take the said continuation, and pass +it to $f$. Analogously, $\throwGT$ is not supposed to return results +of reification at all. With that being said, we cannot define reifiers +for $\callccGT$ and $\throwGT$. A solution to this problem is to make +reifiers accept continuation as an extra parameter, as shown +in~\cref{fig:different_reifiers}. + +There is, however, a tradeoff --- the lack of generic bind rule. + +\begin{mathpar} + \inferrule[wp-hom] + {f \in \Hom \and \wpre{\alpha}{\Ret \beta_v. \wpre{f(\beta_v)}{\Phi}}} + {\wpre{f(\alpha)}{\Phi}} +\end{mathpar} + +The reason for that is the following two lemmas, required to prove that steps can be performed under an arbitrary \gitrees context (i.e., under homomorphic functions). + +\begin{lemma} + \label{lem:hom_istep} + Let $f$ be a homomorphism. + Then $(\alpha,\sigma)\istep(\beta,\sigma')$ implies + $(f(\alpha),\sigma)\istep(f(\beta),\sigma')$. +\end{lemma} +\begin{lemma} + \label{lem:hom_istep_inv} + Let $f$ be a homomorphism. + If $(f(\alpha), \sigma)\istep(\beta',\sigma')$ then either + \begin{itemize} + \item $\alpha$ is a \gitree-value, or; + \item there exists $\beta$ such that + $(\alpha,\sigma)\istep(\beta,\sigma')$ and $\later(f(\beta) = \beta')$. + \end{itemize} +\end{lemma} + +Consider the second clauses of $\istep$ in both lemmas. By definition +of homomorphic functions, the preserve $\Vis$ constructors by +composition with their continuations. However, we cannot guarantee +that results of reification stay the same with different +continuations. + +However, we can recover the bind rule for effect signatures with only +context independent effects, as reifiers for context independent +effects do not depend upon continuations. + +Under the proposed modifications, it is possible to define reifiers +for $\callccGT(f)$ and $\throwGT(e)(f)$, as shown +in~\cref{fig:control_reifiers}. Reifiers for $\callccGT(f)$ and +$\throwGT(e)(f)$ are straitforward. $\callccGT(f)$ applies the current +continuation to $f$ `passing` it, and returns the result wrapped in +the current continuation. $\throwGT(e)(f)$ simply applies the second +argument to the first one, and ignores the current continuation +entirely. In addition, we can show the following rules for the +mentioned reifiers. + +\begin{lemma}{WP-throw.} + \label{lem:wp_throw} + $\sem{\sigma} \ast \later (\sem{\sigma} \wand \wpre{\eapp{f}{x}}{\Phi}) \vdash \wpre{\eapp{\kappa}{(\throwGT(\Next(x))(\Next(f)))}}{\Phi}$ +\end{lemma} + +\begin{lemma}{WP-callcc.} + \label{lem:wp_callcc} + $\sem{\sigma} \ast \later (\sem{\sigma} \wand \wpre{\eapp{\kappa}{(\eapp{f}{\kappa})}}{\Phi}) \vdash \wpre{\eapp{\kappa}{(\callccGT(\Next \circ f))}}{\Phi}$ +\end{lemma} + +\begin{figure} + \[ + r : \prod_{\idx \in E} \Ins_{\idx}(\latert \IT_E) \times \stateO \times (\Outs_{\idx}(\latert \IT_E \rightarrow \latert \IT_E)) \to \optionO(\latert \IT_E \times \stateO). + \] + \caption{New type for reifiers.} + \label{fig:different_reifiers} +\end{figure} + +\begin{figure} + \begin{mathpar} + \infer + {r_i(x,\sigma,\kappa) = \Some(\beta, \sigma')} + {\reify(\Vis_i(x, k), \sigma) = (\Tau(\beta), \sigma')} + \and + \infer + {r_i(x,\sigma,\kappa) = \None} + {\reify(\Vis_i(x, k), \sigma) = (\Err(\RunTime), \sigma)} + \end{mathpar} + \caption{New definition of reify function.} + \label{fig:different_reify} +\end{figure} + +\begin{figure} + \begin{align*} + r_{\mathtt{input}}((),(n\vec{n},\vec{m}),\kappa) &= \Some(\kappa~n, (\vec{n},\vec{m}))\\ + r_{\mathtt{input}}((),(\epsilon,\vec{m}),\kappa) &= \None\\ + r_{\mathtt{output}}(x,(\vec{n},\vec{m}),\kappa) &= \Some(\kappa~(), (\vec{n},x\vec{m}))\\ + r_{\mathtt{callcc}} (i, \sigma, \kappa) &= \Some(\kappa~(i~\kappa), \sigma)\\ + r_{\mathtt{throw}} (i, \sigma, \kappa) &= \Some((\pi_2~i)~(\pi_1~i), \sigma) + \end{align*} + \caption{Reifiers.} + \label{fig:control_reifiers} +\end{figure} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../main" +%%% End: diff --git a/docs/general/src/sections/sem.tex b/docs/general/src/sections/sem.tex new file mode 100644 index 0000000..2726ad7 --- /dev/null +++ b/docs/general/src/sections/sem.tex @@ -0,0 +1,158 @@ +Now we are ready to provide a full denotational model for $\iocclang$ +in \gitrees in~\cref{fig:lang_sem}. Note that the types of +continuations are slightly different in these signatures. However, we +can use the later whenever we need the former by applicative structure +of the later modality. + +To argue that the interpretation is reasonable, we show soundness and +adequacy of this interpretation. To clarify, we want to show that our +interpretation preserves operational steps, and, moreover, steps in +the interpretation reflect on the operational level. + +Let us start with soundness. + +\begin{lemma} + \label{lem:ectx_hom} + $\All K\;\gamma. \sem{K}_\gamma \in \Hom$. +\end{lemma} + +\begin{lemma}{Semantical substitution.} + \label{lem:semsubst} + $\sem{\plug{e}{\gamma}}_\rho = \sem{e}_{\sem{\_}_\rho \circ \gamma}$ +\end{lemma} + +\begin{lemma}{Soundness.} + \label{lem:soundness} + Let $\reds{\expr_1, \sigma_1}{\expr_2, \sigma_2}$ + then $\Exists n. \sem{\expr_1}_\gamma, \sigma_1 \istep \Tick^n \sem{\expr_2}_\gamma, \sigma_2$. +\end{lemma} +\begin{proof} + By case analysis on operational steps. + \begin{description} + \item[Case 1: $\contr{\plug{K}{\throw{\val}{\cont{K'}}}, \sigma}{\plug{K'}{\val}, \sigma}$.] + Let us choose $n = 2$. \\ + It suffices to show that $\sem{\plug{K}{\throw{\val}{\cont{K'}}}}_\gamma, \sigma \istep \Tick (\Tick (\sem{\plug{K'}{\val}}_\gamma))$. + By definition of interpretation,\\ + $\sem{\plug{K}{\throw{\val}{\cont{K'}}}}_\gamma, \sigma$ is equivalent to $\eapp{\sem{K}_\gamma}{\getval (\Lam x. \getfun (\Lam f. \throwGT(x, f) (\sem{\cont{K'}}_\gamma)) (\sem{\val}_\gamma))}, \sigma$, which, by definition of $\sem{\cont{K'}}_\gamma$ and $\getfun, \getval \in \Hom$, is equivalent to\\ + $\throwGT(\sem{\val}_\gamma, (\Next(\Lam x. \Tau(\APPsl{\sem{K'}_\gamma}{\Next(x)}))))$. + By definition of reify and reifier for $\throwGT$, + $\throwGT(\sem{\val}_\gamma, (\Next(\Lam x. \Tau(\APPsl{\sem{K'}_\gamma}{\Next(x)})))), \sigma \istep \Tau (\Next (\Tau (\Next (\eapp{\sem{K'}_\gamma}{\sem{v}_\gamma})))), \sigma$. + \item[Case 2: $\contr{\plug{K}{\callcc{\var}{\expr}}, \sigma}{\plug{K}{\subst{\expr}{\var}{\cont{K}}}, \sigma}$.] + Let us choose $n = 1$. \\ + It suffices to show that $\sem{\plug{K}{\callcc{\var}{\expr}}}_\gamma, \sigma \istep \Tick \sem{\plug{K}{\subst{\expr}{\var}{\cont{K}}}}_\gamma, \sigma$. + By definition of reify and reifier for $\callccGT$,\\ + $\sem{\plug{K}{\callcc{\var}{\expr}}}_\gamma, \sigma \istep \Tau(\eapp{\sem{K}_\gamma}{(\eapp{\Lam (f \col \latert \IT \rightarrow \latert \IT). \sem{\expr}_{\gamma[\var \mapsto \Fun (\Next (\Lam y. \Tau (f (\Next (y)))))]}}{\sem{K}_\gamma})}), \sigma$, + which is equivalent to $\Tick \sem{\plug{K}{\subst{\expr}{\var}{\cont{K}}}}_\gamma$ + by~\cref{lem:semsubst}. + \end{description} +\end{proof} + +To prove adequacy we define a context dependent logical relation +in~\cref{fig:logrel}. + +Note that the proof of adequacy relies on the fact that +interpretations of all evaluation contexts are homomorphisms, which +allows us to use a limited version of the bind rule, shown in~\cref{lem:obs_bind}. + +\begin{lemma}{Observational equivalence bind rule.} + \label{lem:obs_bind} + \newline + Let $\alpha \sim_{\sem{\tau_1}}^{\Expr} \expr$ and $\kappa \sim_{\sem{\tau_1}}^{\Ectx} K$ + then $\eapp{\kappa}{\alpha} \downarrow \plug{K}{\expr}$. +\end{lemma} + +\begin{lemma}{Semantically valid expression head-step.} + \label{lem:step} + \newline + Let $\contrA{\expr_1, \sigma_1}{\expr_2, \sigma_2}{K}$ and $\alpha \sim_{R}^{\Expr} \plug{K}{\expr_2}$ + then $\alpha \sim_{R}^{\Expr} \plug{K}{\expr_1}$. +\end{lemma} + +\begin{lemma}{Fundamental lemma.} + \label{lem:fundamental} + \newline + Let $\typeA{\Gamma}{\expr}{\tau}$ + then $\Gamma \vDash \expr \col \tau$. +\end{lemma} +\begin{proof} + By induction on typing derivation. + \begin{description} + \item[Case 1: $\typeA{\Gamma}{\throw{\expr_1}{\expr_2}}{\tau'}$.] + By induction hypothesis, $\Gamma \vDash \expr_1 \col \tau$ and $\Gamma \vDash \expr_2 \col \tcont{\tau}$.\\ + By~\cref{lem:obs_bind} and definition of logical relation, it suffices to show\\ + $\All (\rho, \gamma) \in \sem{\Gamma}\; \kappa \sim_{\sem{\tau'}}^\Ectx K. \eapp{\kappa}{\sem{\throw{\expr_1}{\expr_2}}_\rho} \downarrow \plug{K}{\throw{\plug{\expr_1}{\gamma}}{\plug{\expr_2}{\gamma}}}$.\\ + By~\cref{lem:obs_bind} and induction hypothesis, it suffices to show\\ + $\sem{\throw{\emptyK}{\expr_2}}_\rho \sim_{\sem{\tau}}^{\Ectx} \throw{\emptyK}{\plug{\expr_2}{\gamma}}$.\\ + By~\cref{lem:obs_bind} and induction hypothesis, it suffices to show\\ + $\throwGT(\beta\val_1)(\beta\val_2) \downarrow \throw{\val_1}{\val_2}$ for $(\val_1, \beta\val_1) \in \sem{\tau}$ and $(\val_2, \beta\val_2) \in \sem{\tcont{\tau}}$.\\ + The statement holds by~\cref{lem:wp_throw} and definition of $\downarrow$. + \item[Case 2: $\typeA{\Gamma}{\callcc{\var}{\expr}}{\tau}$.] + By induction hypothesis, $\Gamma, x \col \tcont{\tau} \vDash e \col \tau$.\\ + By definition of logical relation, it suffices to show\\ + $\eapp{\kappa}{\sem{\throw{}{}}_\rho} \downarrow \plug{K}{\callcc{\var}{\plug{\expr}{\gamma \uparrow}}}$ for $(\rho, \gamma) \in \sem{\Gamma}$ and $\kappa \sim_{\sem{\tau}}^{\Ectx} K$,\\ + which holds by~\cref{lem:wp_callcc}. + \end{description} +\end{proof} + +\begin{lemma}{Adequacy.} + \label{lem:adequacy} + \newline + Let $\sem{\expr}_{\sem{\cdot}}, \sigma_1 \istep \Rret~n, \sigma_2$ and $\typeA{\cdot}{\expr}{\tnat}$ + then $\expr, \sigma_1 \rightarrow^* n, \sigma_2$. +\end{lemma} +\begin{proof} + By fundamental lemma and adequacy of program logic. +\end{proof} + +\begin{figure} + \begin{align*} + &\sem{\expr} \col (\Var \rightarrow \IT) \rightarrow \IT \\ + &\sem{\var}_\gamma = \gamma(\var) \\ + &\sem{\eapp{\expr_1}{\expr_2}}_\gamma = \APPs{\sem{\expr_1}_\gamma}{\sem{\expr_2}_\gamma} \\ + &\sem{\natop{\expr_1}{\expr_2}}_\gamma = \NATOP_{\oplus}(\sem{\expr_1}_\gamma, \sem{\expr_2}_\gamma)\\ + &\sem{\Input}_\gamma = \INPUT \\ + &\sem{\Output e}_\gamma = \getnat(\sem{e}_\gamma, \OUTPUT) \\ + &\sem{\If \expr_1 then \expr_2 \Else \expr_3}_\gamma = \IF(\sem{\expr_1}_\gamma, \sem{\expr_2}_\gamma, \sem{\expr_3}_\gamma) \\ + &\sem{\callcc{\var}{\expr}}_{\gamma} = \callccGT(\Lam (f \col \latert \IT \rightarrow \latert \IT). \sem{\expr}_{\gamma[\var \mapsto \Fun (\Next (\Lam y. \Tau (f (\Next (y)))))]}) \\ + &\sem{\throw{\expr_1}{\expr_2}}_{\gamma} = \getval (\Lam x. \getfun (\Lam f. \throwGT(x, f) (\sem{\expr_2}_\gamma)) (\sem{\expr_1}_\gamma)\\ + \intertext{} + &\sem{\val} \col (\Var \rightarrow \IT) \rightarrow \IT \\ + &\sem{n}_\gamma = \Rret(n) \\ + &\sem{\Rec f \var = \expr}_\gamma = \fix_{\IT}(\Lam (t \col \latert \IT). + \Fun(\latert (\Lam \alpha\ v. \sem{\expr}_{\gamma[\var \mapsto v][f \mapsto \alpha]})(t)))\\ + &\sem{\cont K}_\gamma = \Fun(\Next(\Lam x. \Tau(\APPsl{\sem{K}_\gamma}{\Next(x)})))\\ + \intertext{} + &\sem{K} \col (\Var \rightarrow \IT) \rightarrow \IT \rightarrow \IT \\ + &\sem{\emptyK}_\gamma = \imath \\ + &\sem{\Output K}_\gamma = \Lam x. \getnat(\sem{K}_\gamma x, \OUTPUT) \\ + &\sem{\If K then \expr_1 \Else \expr_2}_\gamma = \Lam x. \IF(\sem{K}_\gamma x, \sem{\expr_1}_\gamma, \sem{\expr_2}_\gamma) \\ + &\sem{\eapp{K}{\val}}_\gamma = \Lam x. \APPs{\sem{K}_\gamma x}{\sem{\val}_\gamma} \\ + &\sem{\eapp{\expr}{K}}_\gamma = \Lam x. \APPs{\sem{\expr}_\gamma}{\sem{K}_\gamma x} \\ + &\sem{\natop{\expr}{K}}_\gamma = \Lam x. \NATOP_{\oplus}(\sem{\expr}_\gamma, \sem{K}_\gamma x) \\ + &\sem{\natop{K}{\val}}_\gamma = \Lam x. \NATOP_{\oplus}(\sem{K}_\gamma x, \sem{\val}_\gamma) \\ + &\sem{\throw{K}{\expr}}_\gamma = \Lam x. \getval (\Lam y. \getfun (\Lam f. \throwGT(y, f) (\sem{\expr}_\gamma)) (\sem{K}_\gamma x)\\ + &\sem{\throw{\val}{K}}_\gamma = \Lam x. \getval (\Lam y. \getfun (\Lam f. \throwGT(y, f) (\sem{K}_\gamma x)) (\sem{\val}_\gamma) + \end{align*} + \caption{Denotational semantics of $\iocclang$} + \label{fig:lang_sem} +\end{figure} + +\begin{figure} + \begin{align*} + \alpha \downarrow \expr &\eqdef \All \sigma. \sem{\sigma} \wand \wpre{\alpha}{\beta. \Exists \val\;\sigma'. \expr, \sigma \rightarrow^* \val, \sigma' \ast (\beta, \val) \in \sem{\tnat} \land \sem{\sigma'}}\\ + \sim_R^{\Ectx} &\eqdef \setComp{(\kappa, K)}{\All (\beta \sim_R \val). \eapp{\kappa}{\beta} \downarrow \plug{K}{\val}}\\ + \sim_R^{\Expr} &\eqdef \setComp{(\alpha, \expr)}{\All (\kappa \sim_R^{\Ectx} K). \eapp{\kappa}{\alpha} \downarrow \plug{K}{\expr}}\\ + \sem{\tnat} &\eqdef \setComp{(\beta, \val)}{\Exists n. \beta = \Rret(n) \land \val = n}\\ + \sem{\tarr{\tau_1}{\tau_2}} &\eqdef \setComp{(\Fun(f), \val)}{\All (\alpha, \val') \in \sem{\tau_1}. \APPs{f}{\alpha} \sim_{\sem{\tau_2}}^{\Expr} \eapp{\val}{\val'}}\\ + \sem{\tcont{\tau}} &\eqdef \setComp{(\Fun(\Next(\Lam x. \Tau (\APPsl{\kappa}{\Next(x)}))), \cont{K})}{\kappa \sim_{\sem{\tau}}^{\Ectx} K}\\ + \sem{\Gamma} &\eqdef \setComp{(\rho, \gamma)}{\All \var \col \tau \in \Gamma. \eapp{\rho}{\var} \sim_{\sem{\tau}}^{\Expr} \eapp{\gamma}{\var}}\\ + \Gamma \vDash \expr \col \tau &\eqdef \All (\rho, \gamma) \in \sem{\Gamma}. \sem{\expr}_\rho \sim_{\sem{\tau}}^{\Expr} \plug{\expr}{\gamma}) + \end{align*} +\caption{Logical relation.} +\label{fig:logrel} +\end{figure} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../main" +%%% End: diff --git a/docs/general/src/sections/tot.tex b/docs/general/src/sections/tot.tex new file mode 100644 index 0000000..b3d2d59 --- /dev/null +++ b/docs/general/src/sections/tot.tex @@ -0,0 +1,121 @@ +Our goal is to define a weak bisimularity relation of top of guarded +interaction trees. However, there is a subtlety that prevents us from +that. Consider a relation defined by guarded recursion. + +\begin{align*} +\end{align*} + +But now, if we unveil semantics of the classical topos of trees, +on top of which Iris is built, we can always find a number, for +which that fixpoint relates any guarded interaction tree to +the `bottom' tree defined as $\MU a \col \latert \IT. \Tau(a)$. +Indeed, for a given $n$ that forces the formula, consider instantiating +the existential with $n + 1$. Now, the relation trivially holds, as after +`stripping' $n$ laters, we end up with a proposition that trivially holds. + +If we instead consider Transfinite Iris that is meant by allowing us to +force formulas using elements from sets with bigger cardinalities, we +could resolve the problem. However, in this case we lose ability +to define guarded interaction trees as a solution to the recursive domain +equation. Hand-waving proof: the solution to a general recursive domain equation, +given by a locally contractive functor $F \col \ftrcat{\COFEs~\opCat \times \COFEs}{\COFEs}$ with a given element of $F(\One, \One)$ (given by $\One \toby{\mathsf{base}} F(\One, \One)$) is defined as co(limit) of +the following diagram (of type $\ftrcat{\omega}{\COFEs}$). +\begin{align*} + F_n & \col \COFEs \\ + F_0 & \cceq \One \\ + F_{n + 1} & \cceq F(F_n, F_n) \\ + e_n & \col F_n \toby{} F_{n + 1} \\ + p_n & \col F_{n + 1} \toby{} F_n \\ + e_0 & \cceq \mathsf{base} \\ + e_{n + 1} & \cceq F(p_n, e_n) \\ + p_0 & \cceq \; ! \\ + p_{n + 1} & \cceq F(e_n, p_n) +\end{align*} + +\[ + F_0 \stackrel[p_o]{e_0}{\rightleftarrows} + F_1 \stackrel[p_1]{e_1}{\rightleftarrows} + \ \cdots \ + \stackrel[p_{n - 1}]{e_{n - 1}}{\rightleftarrows} F_n +\] + +It is all nice and cool until we consider if we can take a limit of +$F_n$. Consider an arbitrary equalizing pair of arrows in $\COFEs$: +\parpair{X}{Y}{f}{g}. We want to find a unique ($E \col \COFEs$, $E +\toby{e} X$), s.t. $\forall x \col E. f(e(x)) \equiv g(e(x))$. In a +transfinite setting, it means that $e$ should be continuous (i.e., $e +(\mathsf{blim}_{\leftarrow \beta_i})$ should be preserved), however, +we have no guarantees that $E$, formed as a set-based equalizer, has all +bounded limits. + +We argue that working in $\psh{\lambda}$, where $\lambda$ --- an +arbitrary limit ordinal, is enough and sufficient for our goal. First, +sheaf condition (which we need for fixpoints) for $F \col +\psh{\lambda}$ is simple to handle: +\begin{align*} F(\lt{\beta_i}) \equiv \lt{F(\beta_i)} +\end{align*} + +Second, the notion of distance and local contractivity scales well +for $\lambda$-indexed (pre)sheaves. Let us debacle it. +Classically, $F$ is contractive, if $\Exists G. F \equiv G \circ \Next$. +\begin{align*} + \latert & \col \psh{\lambda} \rightarrow \psh{\lambda} \\ + \latert~X~0 & \cceq \One \\ + \latert~X~(n + 1) & \cceq X~n \\ + \latert~X~(\lt{\beta_i}) & \cceq X~(\lt{\beta_i}) +\end{align*} +\begin{align*} + \Next & \col X \rightarrow \latert X \\ + \Next_o & \cceq \; ! \\ + \Next_{n + 1} & \cceq \mathsf{restr}^{n + 1}_{n} \\ + \Next_{\lt{\beta_i}} & \cceq \imath +\end{align*} + +We define $x \stackrel{n}{\equiv} y \cceq \All (n \toby{\delta} n'). x(n') \equiv y(n')$. +$F$ is contractive iff $x \stackrel{n}{\equiv} y \implies F(x) \stackrel{n + 1}{\equiv} F(y)$. +Let us show that our notion of being contractive is sufficient: +$(\All (n' < n). x(n') \equiv y(n')) \implies (\All (n' < n + 1). G(\Next(x))(n') \equiv G(\Next(y))(n'))$. We show it by induction on $n'$. +% \begin{itemize} +% \item[$n' = 0$.] $G(\star) \equiv G(\star)$. +% \item[$n' = n'' + 1$.] Ists. +% \item[$\lt{\beta_i}$.] +% \end{itemize} + +What is done: +\begin{itemize} +\item Cartesian close structure of $\psh{\cat{C}}$. +\item Completeness and cocompleteness of $\psh{\cat{C}}$. +\item Wrappers around Kripke-Joyal semantics for $\psh{\cat{C}}$ that +we intend to use as internal language. +\item $\latert$, $\later$, $\Next$ for $\psh{\omega}$, including +fixpoints, L\"ob induction. +\item A machinery to piggy-back on Iris framework by using +$\psh{\omega}$ instead of $\COFEs$. (Includes bi-instance for internal logic.) +\item Half-finished solver for recursive domain equations for +$\psh{\omega}$. +\end{itemize} + +What remains to be done: +\begin{itemize} +\item Half-finish the solver for recursive domain equations for +$\psh{\omega}$. +\item Port $\psh{\omega}$-specific parts t $\psh{\lambda}$, where +$\lambda$ --- an arbitrary limit ordinal. +\item Port guarded interaction trees to $\psh{\lambda}$. +\end{itemize} + +What are some open problems: +\begin{itemize} +\item What flavor of ordinals we should use? Ideally, it should have +good induction scheme. +\end{itemize} + +% \begin{tikzcd} +% A \arrow[d, "g"] \arrow[r, "f"] & B \arrow[r, "\alpha"] \arrow[d, "\gamma"] & D \arrow[d, "\beta"] \\ +% C \arrow[rru, "h"] & B' \arrow[r, "\lambda"] & D' +% \end{tikzcd} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../main" +%%% End: diff --git a/docs/general/src/syn.sty b/docs/general/src/syn.sty new file mode 100644 index 0000000..f978726 --- /dev/null +++ b/docs/general/src/syn.sty @@ -0,0 +1,40 @@ +\newcommand{\col}{\mathrel{:}} +\newcommand{\cceq}{\col\col=} + +\newcolumntype{L}{>{$}l<{$}} +\newcommand\GrmContinue{\multicolumn{2}{l}{}} +\NewDocumentEnvironment{grammar}{}{ + \medskip + \begin{tabular}{lL@{\ \ $\cceq$\ \ }L} +}{ + \end{tabular} + \medskip +} + +\newcommand{\syn}[1]{{\mathsf{#1}}} +\newcommand{\synds}{\syn{.}~} + +\newcommand{\tarr}[2]{{#1}\mathop{\syn{\to}}{#2}} +\newcommand{\tnat}{\mathbb{N}} +\newcommand{\tcont}[1]{\mathit{cont}({#1})} + +\newcommand{\callcc}[2]{\langkw{call/cc}~(\syn{{#1}}\synds{#2})} +\newcommand{\cont}[1]{\langkw{cont}~{#1}} +\newcommand{\throw}[2]{\langkw{throw}~{#1}~\langkw{to}~{#2}} +\newcommand{\natop}[2]{{#1}\oplus{#2}} + +\newcommand{\emptyK}{\square} + +\newcommand{\vlam}[2]{\syn{\lambda}\,{#1}\synds{#2}} + +\newcommand{\elet}[3]{\langkw{let}\,{#1} = {#2}\,\langkw{in}\,{#3}} +\newcommand{\eapp}[2]{{#1}\;{#2}} + +\newcommand{\typeA}[3]{{#1}\vdash{#2}\col{#3}} + +\newcommand{\contr}[2]{{#1}\mapsto{#2}} +\newcommand{\contrA}[3]{{#1}\mapsto_{#3}{#2}} +\newcommand{\reds}[2]{{#1}\to{#2}} +\newcommand{\redsstar}[2]{{#1}\to^{*}{#2}} + +\newcommand{\plug}[2]{{#1}[{#2}]} \ No newline at end of file