Commit baeeaebd authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Update to modern coq directory structure; rename project to 'fri', set up opam.

parent b53c8c7b
# Makefile originally taken from coq-club
%: Makefile.coq
+make -f Makefile.coq $@
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
all: Makefile.coq
+make -f Makefile.coq all
+@make -f Makefile.coq all
.PHONY: all
clean: Makefile.coq
+make -f Makefile.coq clean
+@make -f Makefile.coq clean
find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
rm -f Makefile.coq
.PHONY: clean
Makefile.coq: _CoqProject Makefile
coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq
# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
# filename, so we do some file gymnastics.
Makefile.coq: _CoqProject Makefile awk.Makefile
coq_makefile -f _CoqProject -o Makefile.coq
mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
_CoqProject: ;
# Install build-dependencies
build-dep/opam: opam Makefile
# Creating the build-dep package.
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
build-dep: build-dep/opam phony
@# We want opam to not just instal the build-deps now, but to also keep satisfying these
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything.
@# Upgrading is needed in case the pin already exists, but the builddep package changed.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
echo "# Pinning build-dep package." && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
echo "# Updating build-dep package." && \
opam upgrade "$$BUILD_DEP_PACKAGE"
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
awk.Makefile: ;
opam: ;
.PHONY: all clean
# Phony wildcard targets
phony: ;
.PHONY: phony
......@@ -8,7 +8,22 @@ refinement.
This version is known to compile with:
- Coq 8.7.0
- ssreflect 1.6.4
- A development version of [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp)
The easiest way to install the correct versions of the dependencies is through
opam. You will need the Coq and Iris opam repositories:
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.
## Updating
After doing `git pull`, the development may fail to compile because of outdated
dependencies. To fix that, please run `opam update` followed by
`make build-dep`.
## Building Instructions
......
-Q . iris
-Q theories fri
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
prelude/list.v
prelude/compact.v
prelude/set_finite_setoid.v
algebra/irelations.v
algebra/relations.v
algebra/step.v
algebra/cmra.v
algebra/cmra_big_op.v
algebra/cmra_tactics.v
algebra/sts.v
algebra/auth.v
algebra/gmap.v
algebra/ofe.v
algebra/cofe_solver.v
algebra/base.v
algebra/dra.v
algebra/agree.v
algebra/dec_agree.v
algebra/excl.v
algebra/iprod.v
algebra/upred.v
algebra/upred_tactics.v
algebra/upred_big_op.v
algebra/upred_hlist.v
algebra/frac.v
algebra/csum.v
algebra/list.v
algebra/updates.v
algebra/local_updates.v
algebra/gset.v
algebra/coPset.v
program_logic/binders.v
program_logic/model.v
program_logic/adequacy.v
program_logic/adequacy_inf.v
program_logic/pstepshifts.v
program_logic/lifting.v
program_logic/invariants.v
program_logic/viewshifts.v
program_logic/stepshifts.v
program_logic/wsat.v
program_logic/ownership.v
program_logic/weakestpre.v
program_logic/weakestpre_fix.v
program_logic/pviewshifts.v
program_logic/resources.v
program_logic/hoare.v
program_logic/language.v
program_logic/delayed_language.v
program_logic/nat_delayed_language.v
program_logic/ectx_language.v
program_logic/ectxi_language.v
program_logic/ectx_lifting.v
program_logic/ghost_ownership.v
program_logic/global_functor.v
program_logic/saved_prop.v
program_logic/auth.v
program_logic/sts.v
program_logic/namespaces.v
program_logic/refine_raw.v
program_logic/refine_raw_adequacy.v
program_logic/refine.v
program_logic/refine_ectx.v
program_logic/refine_ectx_delay.v
program_logic/boxes.v
heap_lang/lang.v
heap_lang/tactics.v
heap_lang/wp_tactics.v
heap_lang/lifting.v
heap_lang/derived.v
heap_lang/notation.v
heap_lang/heap.v
heap_lang/refine.v
heap_lang/refine_heap.v
heap_lang/refine_proofmode.v
heap_lang/lib/assert.v
heap_lang/proofmode.v
heap_lang/substitution.v
chan_lang/lang.v
chan_lang/protocol.v
chan_lang/tactics.v
chan_lang/refine.v
chan_lang/derived.v
chan_lang/notation.v
chan_lang/refine_heap.v
chan_lang/refine_heap_proofmode.v
chan_lang/simple_types.v
chan_lang/substitution.v
chan2heap/chan2heap.v
chan2heap/simple_reln.v
chan2heap/compiler_correctness.v
chan2heap/refine_protocol.v
tests/heap_lang.v
tests/proofmode.v
locks/clh.v
locks/ticket.v
locks/lock_reln.v
locks/ticket_clh_triples.v
locks/ticket_clh_refinement.v
proofmode/coq_tactics.v
proofmode/pviewshifts.v
proofmode/pstepshifts.v
proofmode/environments.v
proofmode/intro_patterns.v
proofmode/spec_patterns.v
proofmode/tactics.v
proofmode/notation.v
proofmode/invariants.v
proofmode/weakestpre.v
proofmode/ghost_ownership.v
proofmode/sts.v
proofmode/classes.v
proofmode/class_instances.v
theories/prelude/list.v
theories/prelude/compact.v
theories/prelude/set_finite_setoid.v
theories/algebra/irelations.v
theories/algebra/relations.v
theories/algebra/step.v
theories/algebra/cmra.v
theories/algebra/cmra_big_op.v
theories/algebra/cmra_tactics.v
theories/algebra/sts.v
theories/algebra/auth.v
theories/algebra/gmap.v
theories/algebra/ofe.v
theories/algebra/cofe_solver.v
theories/algebra/base.v
theories/algebra/dra.v
theories/algebra/agree.v
theories/algebra/dec_agree.v
theories/algebra/excl.v
theories/algebra/iprod.v
theories/algebra/upred.v
theories/algebra/upred_tactics.v
theories/algebra/upred_big_op.v
theories/algebra/upred_hlist.v
theories/algebra/frac.v
theories/algebra/csum.v
theories/algebra/list.v
theories/algebra/updates.v
theories/algebra/local_updates.v
theories/algebra/gset.v
theories/algebra/coPset.v
theories/program_logic/binders.v
theories/program_logic/model.v
theories/program_logic/adequacy.v
theories/program_logic/adequacy_inf.v
theories/program_logic/pstepshifts.v
theories/program_logic/lifting.v
theories/program_logic/invariants.v
theories/program_logic/viewshifts.v
theories/program_logic/stepshifts.v
theories/program_logic/wsat.v
theories/program_logic/ownership.v
theories/program_logic/weakestpre.v
theories/program_logic/weakestpre_fix.v
theories/program_logic/pviewshifts.v
theories/program_logic/resources.v
theories/program_logic/hoare.v
theories/program_logic/language.v
theories/program_logic/delayed_language.v
theories/program_logic/nat_delayed_language.v
theories/program_logic/ectx_language.v
theories/program_logic/ectxi_language.v
theories/program_logic/ectx_lifting.v
theories/program_logic/ghost_ownership.v
theories/program_logic/global_functor.v
theories/program_logic/saved_prop.v
theories/program_logic/auth.v
theories/program_logic/sts.v
theories/program_logic/namespaces.v
theories/program_logic/refine_raw.v
theories/program_logic/refine_raw_adequacy.v
theories/program_logic/refine.v
theories/program_logic/refine_ectx.v
theories/program_logic/refine_ectx_delay.v
theories/program_logic/boxes.v
theories/heap_lang/lang.v
theories/heap_lang/tactics.v
theories/heap_lang/wp_tactics.v
theories/heap_lang/lifting.v
theories/heap_lang/derived.v
theories/heap_lang/notation.v
theories/heap_lang/heap.v
theories/heap_lang/refine.v
theories/heap_lang/refine_heap.v
theories/heap_lang/refine_proofmode.v
theories/heap_lang/lib/assert.v
theories/heap_lang/proofmode.v
theories/heap_lang/substitution.v
theories/chan_lang/lang.v
theories/chan_lang/protocol.v
theories/chan_lang/tactics.v
theories/chan_lang/refine.v
theories/chan_lang/derived.v
theories/chan_lang/notation.v
theories/chan_lang/refine_heap.v
theories/chan_lang/refine_heap_proofmode.v
theories/chan_lang/simple_types.v
theories/chan_lang/substitution.v
theories/chan2heap/chan2heap.v
theories/chan2heap/simple_reln.v
theories/chan2heap/compiler_correctness.v
theories/chan2heap/refine_protocol.v
theories/tests/heap_lang.v
theories/tests/proofmode.v
theories/locks/clh.v
theories/locks/ticket.v
theories/locks/lock_reln.v
theories/locks/ticket_clh_triples.v
theories/locks/ticket_clh_refinement.v
theories/proofmode/coq_tactics.v
theories/proofmode/pviewshifts.v
theories/proofmode/pstepshifts.v
theories/proofmode/environments.v
theories/proofmode/intro_patterns.v
theories/proofmode/spec_patterns.v
theories/proofmode/tactics.v
theories/proofmode/notation.v
theories/proofmode/invariants.v
theories/proofmode/weakestpre.v
theories/proofmode/ghost_ownership.v
theories/proofmode/sts.v
theories/proofmode/classes.v
theories/proofmode/class_instances.v
# awk program that patches the Makefile generated by Coq.
# Detect the name this project will be installed under.
/\$\(COQLIBINSTALL\)\/.*\/\$\$i/ {
# Wow, POSIX awk is really broken. I mean, isn't it supposed to be a text processing language?
# And there is not even a way to access the matched groups of a regexp...?!? Lucky enough,
# we can just split the string at '/' here.
split($0, PIECES, /\//);
PROJECT=PIECES[2];
}
# Patch the uninstall target to work properly, and to also uninstall stale files.
# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
# This (and the section above) can be removed once we no longer support Coq 8.6.
/^uninstall: / {
print "uninstall:";
print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
getline;
next
}
# Add new target quick2vo to (a) run "make quick" with the same number of jobs, ensuring
# that the .vio files are up-to-date, and (b) only schedule vio2vo for those
# files where the .vo is *older* than the .vio.
/^vio2vo:/ {
print "quick2vo:";
print "\t@make -j $(J) quick"
print "\t@VIOFILES=$$(for vofile in $(VOFILES); do viofile=\"$$(echo \"$$vofile\" | sed \"s/\\.vo/.vio/\")\"; if [ \"$$vofile\" -ot \"$$viofile\" -o ! -e \"$$vofile\" ]; then echo -n \"$$viofile \"; fi; done); \\"
print "\t echo \"VIO2VO: $$VIOFILES\"; \\"
print "\t if [ -n \"$$VIOFILES\" ]; then $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
print ".PHONY: quick2vo"
}
# This forwards all unchanged lines
1
__pycache__
build-times.log*
gitlab-extract
#!/usr/bin/env python3
import argparse, pprint, sys
import requests
import parse_log
def last(it):
r = None
for i in it:
r = i
return r
def first(it):
for i in it:
return i
return None
def req(path):
url = '%s/api/v3/%s' % (args.server, path)
return requests.get(url, headers={'PRIVATE-TOKEN': args.private_token})
# read command-line arguments
parser = argparse.ArgumentParser(description='Extract iris-coq build logs from GitLab')
parser.add_argument("-t", "--private-token",
dest="private_token", required=True,
help="The private token used to authenticate access.")
parser.add_argument("-s", "--server",
dest="server", default="https://gitlab.mpi-sws.org/",
help="The GitLab server to contact.")
parser.add_argument("-p", "--project",
dest="project", default="FP/iris-coq",
help="The name of the project on GitLab.")
parser.add_argument("-f", "--file",
dest="file", required=True,
help="Filename to store the load in.")
parser.add_argument("-c", "--commits",
dest="commits",
help="The commits to fetch. Default is everything since the most recent entry in the log file.")
args = parser.parse_args()
log_file = sys.stdout if args.file == "-" else open(args.file, "a")
# determine commit, if missing
if args.commits is None:
if args.file == "-":
raise Exception("If you do not give explicit commits, you have to give a logfile so that we can determine the missing commits.")
last_result = last(parse_log.parse(open(args.file, "r"), parse_times = False))
args.commits = "{}..origin/master".format(last_result.commit)
projects = req("projects")
project = first(filter(lambda p: p['path_with_namespace'] == args.project, projects.json()))
if project is None:
sys.stderr.write("Project not found.\n")
sys.exit(1)
for commit in parse_log.parse_git_commits(args.commits):
print("Fetching {}...".format(commit))
commit_data = req("/projects/{}/repository/commits/{}".format(project['id'], commit))
if commit_data.status_code != 200:
raise Exception("Commit not found?")
builds = req("/projects/{}/repository/commits/{}/builds".format(project['id'], commit))
if builds.status_code != 200:
# no build
continue
build = first(sorted(builds.json(), key = lambda b: -int(b['id'])))
if build is None or build['status'] == 'failed':
# build failed (or missing...??)
continue
if build['status'] == 'running':
# build still running, don't fetch this or any later commit
break
# now fetch the build times
build_times = requests.get("{}/builds/{}/artifacts/file/build-time.txt".format(project['web_url'], build['id']))
if build_times.status_code != 200:
raise Exception("No artifact at build?")
# Output in the log file format
log_file.write("# {}\n".format(commit))
log_file.write(build_times.text)
log_file.flush()
import re, subprocess
class Result:
def __init__(self, commit, times):
self.commit = commit
self.times = times
def parse(file, parse_times = True):
'''[file] should be a file-like object, an iterator over the lines.
yields a list of Result objects.'''
commit_re = re.compile("^# ([a-z0-9]+)$")
time_re = re.compile("^([a-zA-Z0-9_/-]+) \(user: ([0-9.]+) mem: ([0-9]+) ko\)$")
commit = None
times = None
for line in file:
# next commit?
m = commit_re.match(line)
if m is not None:
# previous commit, if any, is done now
if commit is not None:
yield Result(commit, times)
# start recording next commit
commit = m.group(1)
if parse_times:
times = {} # reset the recorded times
continue
# next file time?
m = time_re.match(line)
if m is not None:
if times is not None:
name = m.group(1)
time = float(m.group(2))
times[name] = time
continue
# nothing else we know about, ignore
# end of file. previous commit, if any, is done now.
if commit is not None:
yield Result(commit, times)
def parse_git_commits(commits):
'''Returns an iterable of SHA1s'''
if commits.find('..') >= 0:
# a range of commits
commits = subprocess.check_output(["git", "rev-list", commits])
else:
# a single commit
commits = subprocess.check_output(["git", "rev-parse", commits])
return reversed(commits.decode("utf-8").strip().split('\n'))
#!/usr/bin/env python3
import argparse, sys, pprint, itertools
import matplotlib.pyplot as plt
import parse_log
markers = itertools.cycle([(3, 0), (3, 0, 180), (4, 0), (4, 0, 45), (8, 0)])
# read command-line arguments
parser = argparse.ArgumentParser(description='Visualize iris-coq build times')
parser.add_argument("-f", "--file",
dest="file", required=True,
help="Filename to get the data from.")
parser.add_argument("-t", "--timings", nargs='+',
dest="timings",
help="The names of the Coq files (with or without the extension) whose timings should be extracted")
parser.add_argument("-c", "--commits",
dest="commits",
help="Restrict the graph to the given commits.")
args = parser.parse_args()
pp = pprint.PrettyPrinter()
log_file = sys.stdin if args.file == "-" else open(args.file, "r")
results = parse_log.parse(log_file, parse_times = True)
if args.commits:
commits = set(parse_log.parse_git_commits(args.commits))
results = filter(lambda r: r.commit in commits, results)
results = list(results)
timings = list(map(lambda t: t[:-2] if t.endswith(".v") else t, args.timings))
for timing in timings:
plt.plot(list(map(lambda r: r.times.get(timing), results)), marker=next(markers), markersize=8)
plt.legend(timings, loc = 'upper left', bbox_to_anchor=(1.05, 1.0))
plt.xticks(range(len(results)), list(map(lambda r: r.commit[:7], results)), rotation=70)
plt.subplots_adjust(bottom=0.2, right=0.7) # more space for the commit labels and legend
plt.xlabel('Commit')
plt.ylabel('Time (s)')
plt.title('Time to compile files')
plt.grid(True)
plt.show()
*.pdf
*.aux
*.log
*.out
*.synctex.gz
*.txss
*.thm
*.toc
*.bbl
*.blg
*.bcf
*.run.xml
_*_.tex
auto/*.el
\section{Algebraic Structures}
\subsection{COFE}
The model of Iris lives in the category of \emph{Complete Ordered Families of Equivalences} (COFEs).
This definition varies slightly from the original one in~\cite{catlogic}.
\begin{defn}[Chain]
Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \mathbb{N}}$ of equivalence relations, a \emph{chain} is a function $c : \mathbb{N} \to \cofe$ such that $\All n, m. n \leq m \Ra c (m) \nequiv{n} c (n)$.
\end{defn}
\begin{defn}
A \emph{complete ordered family of equivalences} (COFE) is a tuple $(\cofe, ({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \mathbb{N}}, \lim : \chain(\cofe) \to \cofe)$ satisfying
\begin{align*}
\All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{cofe-equiv} \\
\All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{cofe-mono} \\
\All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{cofe-limit} \\
\All n, c.& \lim(c) \nequiv{n} c(n+1) \tagH{cofe-compl}
\end{align*}
\end{defn}
The key intuition behind COFEs is that elements $x$ and $y$ are $n$-equivalent, notation $x \nequiv{n} y$, if they are \emph{equivalent for $n$ steps of computation}, \ie if they cannot be distinguished by a program running for no more than $n$ steps.
In other words, as $n$ increases, $\nequiv{n}$ becomes more and more refined (\ruleref{cofe-mono})---and in the limit, it agrees with plain equality (\ruleref{cofe-limit}).
In order to solve the recursive domain equation in \Sref{sec:model} it is also essential that COFEs are \emph{complete}, \ie that any chain has a limit (\ruleref{cofe-compl}).
\begin{defn}
An element $x \in \cofe$ of a COFE is called \emph{discrete} if
\[ \All y \in \cofe. x \nequiv{0} y \Ra x = y\]
A COFE $A$ is called \emph{discrete} if all its elements are discrete.
For a set $X$, we write $\Delta X$ for the discrete COFE with $x \nequiv{n} x' \eqdef x = x'$
\end{defn}
\begin{defn}
A function $f : \cofe \to \cofeB$ between two COFEs is \emph{non-expansive} (written $f : \cofe \nfn \cofeB$) if
\[\All n, x \in \cofe, y \in \cofe. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y) \]
It is \emph{contractive} if
\[ \All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(x) \]
\end{defn}
Intuitively, applying a non-expansive function to some data will not suddenly introduce differences between seemingly equal data.
Elements that cannot be distinguished by programs within $n$ steps remain indistinguishable after applying $f$.
The reason that contractive functions are interesting is that for every contractive $f : \cofe \to \cofe$ with $\cofe$ inhabited, there exists a fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$.
\begin{defn}
The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows.
\end{defn}
Note that $\COFEs$ is cartesian closed:
\begin{defn}
Given two COFEs $\cofe$ and $\cofeB$, the set of non-expansive functions $\set{f : \cofe \nfn \cofeB}$ is itself a COFE with
\begin{align*}
f \nequiv{n} g \eqdef{}& \All x \in \cofe. f(x) \nequiv{n} g(x)
\end{align*}
\end{defn}
\begin{defn}
A (bi)functor $F : \COFEs \to \COFEs$ is called \emph{locally non-expansive} if its action $F_1$ on arrows is itself a non-expansive map.
Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map.
\end{defn}
The function space $(-) \nfn (-)$ is a locally non-expansive bifunctor.
Note that the composition of non-expansive (bi)functors is non-expansive, and the composition of a non-expansive and a contractive (bi)functor is contractive.
\subsection{RA}
\begin{defn}
A \emph{resource algebra} (RA) is a tuple \\
$(\monoid, \mval \subseteq \monoid, \mcore{{-}}:
\monoid \to \maybe\monoid, (\mtimes) : \monoid \times \monoid \to \monoid)$ satisfying:
\begin{align*}
\All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{ra-assoc} \\
\All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{ra-comm} \\
\All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{ra-core-id} \\
\All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{ra-core-idem} \\
\All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{ra-core-mono} \\
\All \melt, \meltB.& (\melt \mtimes \meltB) \in \mval \Ra \melt \in \mval \tagH{ra-valid-op} \\
\text{where}\qquad %\qquad\\
\maybe\monoid \eqdef{}& \monoid \uplus \set{\mnocore} \qquad\qquad\qquad \melt^? \mtimes \mnocore \eqdef \mnocore \mtimes \melt^? \eqdef \melt^? \\
\melt \mincl \meltB \eqdef{}& \Exists \meltC \in \monoid. \meltB = \melt \mtimes \meltC \tagH{ra-incl}
\end{align*}
\end{defn}
\noindent
RAs are closely related to \emph{Partial Commutative Monoids} (PCMs), with two key differences:
\begin{enumerate}