diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 69f169c..de03ce0 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -13,8 +13,8 @@
 ## Contributing code
 
 Please read the [contribution
-guidelines](https://github.com/vanadium/docs/blob/master/contributing/README.md)
-before sending patches.
+guidelines](https://vanadium.github.io/community/contributing.html) before
+sending patches.
 
 **We do not accept GitHub pull requests.** (We use
 [Gerrit](https://www.gerritcodereview.com/) instead for code reviews.)
diff --git a/content/proofs/authentication/index.md b/content/proofs/authentication/index.md
new file mode 100644
index 0000000..7ea718a
--- /dev/null
+++ b/content/proofs/authentication/index.md
@@ -0,0 +1,173 @@
+= yaml =
+title: Verifying the Vanadium Authentication Protocol
+layout: default
+toc: true
+= yaml =
+
+This project defines a formalization of the [Vanadium authentication protocol][auth]
+and verifies the desired security properties for it using the automatic cryptographic protocol verifier [ProVerif][proverif].
+
+The authentication protocol is used during a [Vanadium RPC][rpc] for mutual
+authentication and setting up an encrypted channel for sending RPC data.
+More specifically, the protocol allows each end of an RPC to exchange [blessings]
+with the other end and verify that the other end possesses the private key corresponding
+to the public key to which its blessings are bound. At the end of the protocol,
+an encrypted channel is established between the two ends for performing the
+RPC. The blessings learned as part of the authentication may be used to
+authorize the RPC (e.g., by checking that the blessing name is present on
+a particular [access list][acl]).
+
+The design of the protocol is very similar to the [SIGMA-I][sigma] protocol from
+the literature. It involves a [Diffie-Hellman key exchange][ecdhe], followed by an
+exchange of blessings and private key possession proofs. However, the protocol
+differs from SIGMA-I in how this private key possession proof is represented. We
+refer the reader to the [design doc][auth] for a detailed specification of the
+protocol.
+
+Decades of research in protocol design has shown that manually assessing the
+security of a protocol is challenging as it is difficult to enumerate and
+examine all possible attack scenarios. There have been a number of instances
+of published protocols that intuitively seemed secure but had serious
+vulnerabilities, e.g., the [Needham-Schroeder protocol][needham]. The only way to
+guarantee security of a protocol is to formally specify it and mathematically
+prove its security properties.
+
+# ProVerif
+
+[ProVerif][proverif] is a tool for automatically analyzing properties of security
+protocols. It is capable of proving reachability properties, correspondence assertions,
+and observational equivalence properties of protocols. The ProVerif specification language
+is a variant of the [applied pi-calculus][applied-pi-calculus]. We refer the reader to the
+[ProVerif manual][proverif-manual] for the authoritative definition of the language.
+
+ProVerif analyzes protocols in the symbolic, [Dolev-Yao][dolev-yao] attacker model.
+In this model, the attacker controls the communication channel between the protocol
+participants and can read, modify, delete and inject messages. But the attacker
+cannot "break" cryptographic primitives and can only use them via their legitimate
+interfaces. For instance, the attacker can only decrypt those encrypted messages for
+which it knows the encryption key.
+
+ProVerif is sound but not complete. This means that if ProVerif confirms
+that a security property is true then the property is indeed true in the Dolev-Yao attacker
+model. However, not all true properties may be provable by ProVerif.
+
+# Protocol Formalization
+
+The complete formalization of the authentication protocol along with all cryptographic
+primitives, and Vanadium primitives (such as: certificates and blessings) is specified
+in [`protocol.pv`](/proofs/authentication/protocol.pv). The steps of the protocol are captured in the process
+`handshake` that is parametric on the blessing and private key of the dialer and
+the acceptor. Dialer (aka client) is the initiator of the first handshake message
+and Acceptor (aka server) is the responder of the first handshake message.
+
+# Security Properties
+
+We verify three key properties of the authentication protocol.
+
+(1) _Mutual Authentication_: The dialer and acceptor must agree on the
+	established encryption key and each others blessings. This property
+	is formalized as a pair of correspondence properties in ProVerif stating that a
+	acceptor accepts a session if and only if the dialer accepts the same
+	session, where a session is defined by the session encryption key and
+	the public keys of the dialer's and acceptor's blessings.
+
+(2) _Channel Confidentiality_: The session encryption key established
+	is protected from attackers. This property is verified by checking
+	that a message encrypted under the session key and sent from the
+	acceptor to the dialer is not revealed to the attacker. This is specified
+	as a reachability property in ProVerif.
+
+(3) _Dialer Privacy_: The dialer's public key is never revealed to the attacker. This
+	is specified as a reachability property in ProVerif. The acceptor's public key does get
+	revealed to the attacker, and we verify this using another reachability
+	property in ProVerif.
+
+We verify security properties for an instantiation of the protocol process
+(`authProtocol`) with randomly chosen private keys for the dialer and acceptor,
+and randomly chosen blessings of depth two for the dialer and acceptor. We note
+that the depth of the blessings in the instantiation should not affect the
+security properties, i.e., the verification should go through for arbitrary
+depth blessings if it goes through for depth two blessings. However, a formal
+proof of this statement remains to be shown.
+
+# Running the Verification
+
+## Installing ProVerif
+Running the verification requires installing the [ProVerif][proverif] tool.
+Instructions for installing the tool can be found [here][proverif-install]
+
+## Running ProVerif
+Once ProVerif is installed, please set the environment variable
+`PROVERIF` to point at the ProVerif binary.
+
+```
+export PROVERIF=<path to ProVerif binary>
+```
+
+The verification can be run using the following command.
+
+```
+$PROVERIF protocol.pv
+```
+
+## Intrepting the results
+The aforesaid command prints out a bunch of ProVerif messages (we recommend
+reading Section 3 of the [ProVerif manual][proverif-manual] to understand
+these messages) with the verification results for the various properties
+printed towards the end.
+
+A simple way of printing just the verification results is to run the following
+command:
+
+```
+$PROVERIF protocol.pv | grep RESULT
+```
+
+This command should print the following:
+
+(We add line numbers for ease of reading.)
+
+```
+1. RESULT not attacker(publicKey(privKeyAcceptor[])) is false.
+
+2. RESULT not attacker(publicKey(privKeyDialer[])) is true.
+
+3. RESULT not attacker(privKeyAcceptor[]) is true.
+
+4. RESULT not attacker(privKeyDialer[]) is true.
+
+5. RESULT not attacker(secretMessage[]) is true.
+
+6. RESULT event(termDialer(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) ==> event(acceptsAcceptor(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) is true.
+
+7. RESULT event(acceptsAcceptor(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) ==> event(acceptsDialer(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) is true.
+```
+
+The first two messages respectively state that the attacker learns the
+public key of the acceptor but not the dialer. This verifies the _dialer privacy_
+property.
+
+The next three messages respectively state that the attacker _does not_
+learn the private key of the acceptor, the private key of the dialer, and
+the secret message sent by the acceptor to the dialer over the established
+encrypted channel. This verifies the _channel secrecy_ property.
+
+The last two messages state two correspondence properties that
+together imply that a dialer accepts a certain session if and
+only if the acceptor also accepts the same session, where a session
+is defined by the session encryption key and the public keys of
+the dialer's and acceptor's blessings. This verifies the _mutual authentication_
+property.
+
+[auth]:/designdocs/authentication.html
+[rpc]:/concepts/rpc.html
+[acl]:/glossary.html#access-list
+[blessings]:/glossary.html#blessings
+[sigma]:http://webee.technion.ac.il/~hugo/sigma.html
+[ecdhe]:https://en.wikipedia.org/wiki/Elliptic_curve_Diffie%E2%80%93Hellman
+[proverif]:http://prosecco.gforge.inria.fr/personal/bblanche/proverif/
+[proverif-manual]:http://prosecco.gforge.inria.fr/personal/bblanche/proverif/manual.pdf
+[proverif-install]:http://prosecco.gforge.inria.fr/personal/bblanche/proverif/README
+[applied-pi-calculus]:http://crysys.hu/members/tvthong/pispi/applied.pdf
+[dolev-yao]:https://en.wikipedia.org/wiki/Dolev%E2%80%93Yao_model
+[needham]:https://en.wikipedia.org/wiki/Needham%E2%80%93Schroeder_protocol
diff --git a/content/proofs/authentication/protocol.pv b/content/proofs/authentication/protocol.pv
new file mode 100644
index 0000000..d7ed92b
--- /dev/null
+++ b/content/proofs/authentication/protocol.pv
@@ -0,0 +1,343 @@
+(* Vanadium Authentication Protocol --------------------------------------------
+
+Informal Protocol Specification:
+D is Dialer, A is Acceptor
+D         : Dialer
+A         : Acceptor
+
+g         : Diffie-Hellman Group generator
+x,y       : exponents
+P_X       : Public Key of X
+B_X       : Blessing of X
+sign_X(M) : Private Key Signature of M by Principal X
+key(n)    : A symmetric key generated with Diffie-Hellman secret n
+{M}_k     : Message M encrypted with symmetric key k
+
+Protocol:
+
+D generates x, and A generates y
+
+D ---> A: g^x
+A ---> D: g^y
+A ---> D: {B_A, sign_A(hash("A", g^x, g^y))}_key(g^xy)
+D ---> A: {B_D, sign_D(hash("D", g^x, g^y))}_key(g^xy)
+D ---> A: {M}_key(g^xy)
+
+We are interested in verifying the following correctness properties:
+
+(1) Mutual Authentication
+    Acceptor only authenticates a session once the dialer has authenticated
+    the same session, where a session is defined by the session encryption
+    key and the public key of the dialer's and acceptor's blessings.
+
+(2) Channel Secrecy
+    Any message sent from dialer to acceptor on the established
+    encrypted channel is not revealed to the attacker.
+
+(3) Dialer Privacy
+    The dialer's public key is never revealed to the attacker.
+
+The acceptor reveals its blessing to any dialer that wants to talk to it,
+therefore the acceptor's public key is not a secret. We verify that the
+acceptor's public key can be obtained by the attacker.
+------------------------------------------------------------------------------*)
+
+set predicatesImplementable = nocheck.
+set maxDepth                = 20.
+set maxHyp                  = none.
+set ignoreTypes = true.
+set attacker    = active.
+set keyCompromise = none.
+set simplifyDerivation = true.
+set abbreviateDerivation = true.
+set explainDerivation = true.
+set reconstructTrace = true.
+set unifyDerivation = true.
+set reconstructDerivation = true.
+set displayDerivation = true.
+set traceBacktracking = true.
+set traceDisplay = short.
+set verboseClauses = none.
+set abbreviateClauses = true.
+set removeUselessClausesBeforeDisplay = true.
+set verboseEq = true.
+set verboseRules = false.
+set verboseRedundant = false.
+
+(* DiffieHellmanGroup ----------------------------------------------------------
+   Defines a group type G that facilitates the running of the Diffie-Hellman
+   protocol.
+------------------------------------------------------------------------------*)
+
+type G.         (*Diffie-Hellman Group*)
+type Exponent.  (*Diffie-Hellman Group Exponents*)
+
+const g:G [data].  (*The generator of G, publicly known*)
+
+(* Type Conversion -----------------------------------------------------------*)
+fun gToBitstring(G):bitstring [data].
+
+(* Group Definition ---------------------------------------------------------*)
+fun exp(G, Exponent):G.
+
+(* Associativity of group multiplication abstracted *)
+equation
+   forall x:Exponent, y:Exponent;
+      exp(exp(g, x), y) = exp(exp(g, y), x).
+
+(* Symmetric key crypto primitives ---------------------------------------------
+   Symmetric key encryption and decryption primitives.
+------------------------------------------------------------------------------*)
+
+type SymmetricKey.
+
+fun generateKey(bitstring):SymmetricKey.
+
+(* Type Conversion -----------------------------------------------------------*)
+fun keyToBitstring(SymmetricKey):bitstring [data].
+
+(* symmetricEncrypt(msg, key): Authenticated encryption of 'msg' using symmetric key 'key' *)
+fun symmetricEncrypt(bitstring, SymmetricKey):bitstring.
+
+(* symmetricDecrypt(ciphertext, key): Decrypt 'ciphertext' using symmetric key 'key' *)
+fun symmetricDecrypt(bitstring, SymmetricKey):bitstring
+reduc
+   forall key:SymmetricKey, message:bitstring;
+      symmetricDecrypt(symmetricEncrypt(message, key), key) = message.
+
+(* Public key crypto primitives ------------------------------------------------
+   Signing and verification primitives.
+------------------------------------------------------------------------------*)
+
+(* publicKey(PrivateKey):Corresponding PublicKey *)
+fun publicKey(bitstring):bitstring.
+
+(* sign(message, PrivateKey):signed message bitstring
+   Signed message cannot be decrypted. *)
+fun sign(bitstring, bitstring):bitstring.
+
+(* verifySignature(PublicKey, plaintext, signed) *)
+pred verifySignature(bitstring, bitstring, bitstring).
+clauses
+   forall privateKey:bitstring, msg:bitstring;
+      verifySignature(publicKey(privateKey), msg, sign(msg, privateKey)).
+
+(* Tuples and Hashing  ---------------------------------------------------------
+   Defines the arbitrary length bitstring tuple and associated functions.
+------------------------------------------------------------------------------*)
+
+const null:bitstring [data]. (*Empty Tuple*)
+
+(* t(Tuple, bitstring): bitstring representation of tuple concatenation *)
+fun t(bitstring, bitstring):bitstring [data].
+
+(* hash(item): a truly one-way hash function on item *)
+fun hash(bitstring):bitstring.
+
+(* Certificate -----------------------------------------------------------------
+   A Vanadium Certificate:
+      A tuple (Name, PublicKey, Caveats, Signature)
+------------------------------------------------------------------------------*)
+
+(* certificate(Name, PublicKey, Caveats, Signature) *)
+fun certificate(bitstring, bitstring, bitstring, bitstring):bitstring [data].
+
+(* Blessing --------------------------------------------------------------------
+   A Vanadium Blessing:
+      An arbitrary length tuple/list of Certificates
+------------------------------------------------------------------------------*)
+
+(* publicKeyBlessing(blessing): Returns the public key of last certificate of the
+   certificate chain represented by 'blessing'. *)
+fun publicKeyBlessing(bitstring):bitstring
+reduc forall blessing:bitstring, nm:bitstring, pk:bitstring,
+             cavs:bitstring, sgn:bitstring;
+         publicKeyBlessing(t(blessing, certificate(nm, pk, cavs, sgn))) = pk.
+
+(* verifyBlessing(blessing): Returns whether the certificate chain represented by
+   'blessing' is cryptographically valid. *)
+pred verifyBlessing(bitstring).
+clauses
+   forall nm:bitstring, pk:bitstring, cavs:bitstring, sgn:bitstring;
+      verifySignature(pk, hash(t(t(t(null, nm), pk), cavs)), sgn)
+         -> verifyBlessing(t(null, certificate(nm, pk, cavs, sgn)));
+   forall b:bitstring,
+          nm:bitstring, pk:bitstring, cavs:bitstring, sgn:bitstring;
+      verifySignature(
+         publicKeyBlessing(b),
+         hash(t(hash(b), hash(t(t(t(null, nm), pk), cavs)))),
+         sgn
+      ) &&
+      verifyBlessing(b)
+         -> verifyBlessing(t(b, certificate(nm, pk, cavs, sgn))).
+
+(* newSelfBlessing(privateKey): Returns a new blessing with a single certificate
+   self-signed by the provided 'privateKey'. *)
+letfun newSelfBlessing(privKey:bitstring) =
+   new nm:bitstring;
+   new cavs:bitstring;
+   let pubKey = publicKey(privKey) in
+   let contentHash = hash(t(t(t(null, nm), pubKey), cavs)) in
+   let signature = sign(contentHash, privKey) in
+   let cert = certificate(nm, pubKey, cavs, sign(contentHash, privKey)) in
+   t(null, cert).
+
+(* bless(pubKey, withBlessing, withPrivKey): Returns a new blessing with a
+   certificate for 'pubKey' chained on to certificate chain represented by
+   'withBlessing'. *)
+letfun bless(pubKey:bitstring, withBlessing:bitstring, withPrivKey:bitstring) =
+   new nm:bitstring;
+   new cavs:bitstring;
+   let contentHash = hash(t(t(t(null, nm), pubKey), cavs)) in
+   let signature = sign(hash(t(hash(withBlessing), contentHash)), withPrivKey) in
+   let cert = certificate(nm, pubKey, cavs, signature) in
+   t(withBlessing, cert).
+
+(* Authentication Protocol ----------------------------------------------------
+   Formalizes the Vanadium authentication protocol.
+------------------------------------------------------------------------------*)
+letfun signedChannelBinding(privKey:bitstring, tag:bitstring, binding:bitstring) =
+   sign(hash(t(tag, binding)), privKey).
+
+letfun verifyChannelBinding(pubKey:bitstring, tag:bitstring, binding:bitstring, signature:bitstring) =
+   verifySignature(pubKey, hash(t(tag, binding)), signature).
+
+(* Public communication network. *)
+free dToACh:channel.  (* channel simulating a network pipe from dialer to acceptor *)
+free aToDCh:channel.  (* channel simulating a network pipe from acceptor to dialer *)
+
+free acceptorTag:bitstring.
+free dialerTag:bitstring.
+free messageTag:bitstring.
+
+event acceptsAcceptor(SymmetricKey, bitstring, bitstring).
+event acceptsDialer(SymmetricKey, bitstring, bitstring).
+event termDialer(SymmetricKey, bitstring, bitstring).
+
+let encrypter(key:SymmetricKey, inCh:channel, outCh:channel) =
+  in(inCh, msg:bitstring);
+  out(outCh, symmetricEncrypt(msg, key)).
+
+let decrypter(key:SymmetricKey, inCh:channel, outCh:channel) =
+  in(inCh, ctxt:bitstring);
+  let ptxt = symmetricDecrypt(ctxt, key) in
+  out(outCh, ptxt).
+
+(* Setup performs a Diffie-Hellman key exchange and returns the generated
+   symmetric key, the local and remote channel bindings on retCh. *)
+let setup(outCh:channel, inCh:channel, retCh:channel) =
+   new x:Exponent;
+   let g_x = exp(g, x) in
+   out(outCh, g_x) | 
+   in(inCh, g_y:G);
+   let key = generateKey(gToBitstring(exp(g_y, x))) in
+   let localBnd = t(gToBitstring(g_x), gToBitstring(g_y)) in
+   let remoteBnd = t(gToBitstring(g_y), gToBitstring(g_x)) in
+   out(retCh, t(t(keyToBitstring(key), localBnd), remoteBnd)).
+
+(* readRemoteAuth receives the auth message (blessings + signed channel binding) sent
+   by the remote end and verifies it. If verification succeeds, it returns the public
+   key of the remote end on retCh. *)
+let readRemoteAuth(inCh:channel, key: SymmetricKey, binding: bitstring, tag: bitstring, retCh:channel) =
+   in(inCh, auth:bitstring);
+   let t(blessing:bitstring, chBinding:bitstring) = symmetricDecrypt(auth, key) in
+   let pubKey = publicKeyBlessing(blessing) in
+   (* Verify authentication message and return pubKey only if verification succeeeds. *)
+   if (
+      verifyBlessing(blessing) &&
+      verifyChannelBinding(pubKey, tag, binding, chBinding)
+   ) then
+   out(retCh, pubKey).
+
+(* Dialer process which takes as input the blessings and private key to
+   be used during authentication, the expected public key of the acceptor
+   (used for authorizing the acceptor's blessings). *)
+let dialHandshake(blessing:bitstring, privKey:bitstring, pubKeyExpected:bitstring) =
+   (* Setup *)
+   new retCh1:channel;
+   setup(dToACh, aToDCh, retCh1) |
+   in(retCh1, t(t(keyToBitstring(key:SymmetricKey), localBnd:bitstring), remoteBnd:bitstring));
+
+   (* Receive auth mesage *)
+   new retCh2:channel;
+   readRemoteAuth(aToDCh, key, remoteBnd, acceptorTag, retCh2) |
+   in(retCh2, pubKeyAcceptor:bitstring);
+   event acceptsDialer(key, publicKeyBlessing(blessing), pubKeyAcceptor);
+
+   (* Send auth message *)
+   if (pubKeyAcceptor = pubKeyExpected) then
+   let signedBinding = signedChannelBinding(privKey, dialerTag, localBnd) in
+   out(dToACh, symmetricEncrypt(t(blessing, signedBinding), key));
+
+   (* Receive auth success confirmation. *)
+   in(aToDCh, msg:bitstring);
+   let t(tag:bitstring, pubKey:bitstring) = symmetricDecrypt(msg, key) in
+   if tag = messageTag then
+   if pubKey = publicKeyBlessing(blessing) then
+   event termDialer(key, publicKeyBlessing(blessing), pubKeyAcceptor).
+
+(* Acceptor process which takes as input the blessings and private key to
+   be used during authentication. *)
+let acceptHandshake(blessing:bitstring, privKey:bitstring) =
+   (* Setup *)
+   new retCh:channel;
+   setup(aToDCh, dToACh, retCh) |
+
+   (* Send auth message *)
+   in(retCh, t(t(keyToBitstring(key:SymmetricKey), localBnd:bitstring), remoteBnd:bitstring));
+   let signedBinding = signedChannelBinding(privKey, acceptorTag, localBnd) in
+   let acceptorAuth = t(blessing, signedBinding) in
+   out(aToDCh, symmetricEncrypt(acceptorAuth, key));
+
+   (* Receive auth message *)
+   new retCh2:channel;
+   readRemoteAuth(dToACh, key, remoteBnd, dialerTag, retCh2) |
+   in(retCh2, pubKeyDialer:bitstring);
+   event acceptsAcceptor(key, pubKeyDialer, publicKeyBlessing(blessing));
+
+   (* Send auth success confirmation. *)
+   out(aToDCh, symmetricEncrypt(t(messageTag, pubKeyDialer), key)).
+
+(* Protocol Process *)
+let handshake(
+    blessingDialer:bitstring,
+    privKeyDialer:bitstring,
+    blessingAcceptor:bitstring,
+    privKeyAcceptor:bitstring) =
+   let pubKeyAcceptor = publicKeyBlessing(blessingAcceptor) in
+   dialHandshake(blessingDialer, privKeyDialer, pubKeyAcceptor) |
+   acceptHandshake(blessingAcceptor, privKeyAcceptor) .
+
+(* Authentication Protocol Instance --------------------------------------------
+   Instantiates the Vanadium authentication protocol for specific dialer and
+   acceptor blessings and formalizes the desired correctness properties -- mutual
+   authentication, channel secrecy and dialer privacy.
+------------------------------------------------------------------------------*)
+
+free privKeyDialer:bitstring [private].
+free privKeyAcceptor:bitstring [private].
+
+let handshakeInstance() =
+    new rootPrivKey:bitstring;
+    let rootBlessing = newSelfBlessing(rootPrivKey) in
+    let blessingDialer = bless(publicKey(privKeyDialer), rootBlessing, rootPrivKey) in
+    let blessingAcceptor = bless(publicKey(privKeyAcceptor), rootBlessing, rootPrivKey) in
+    handshake(blessingDialer, privKeyDialer, blessingAcceptor, privKeyAcceptor) .
+
+(* Authenticity *)
+query k:SymmetricKey;
+   event(acceptsAcceptor(k, publicKey(privKeyDialer), publicKey(privKeyAcceptor))) ==> event(acceptsDialer(k, publicKey(privKeyDialer), publicKey(privKeyAcceptor))).
+   (* Desired ProVerif output: event(acceptsAcceptor(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) ==> event(acceptsDialer(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) is true *)
+query k:SymmetricKey;
+   event(termDialer(k, publicKey(privKeyDialer), publicKey(privKeyAcceptor))) ==> event(acceptsAcceptor(k, publicKey(privKeyDialer), publicKey(privKeyAcceptor))).
+   (* Desired ProVerif output: event(termDialer(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) ==> event(acceptsAcceptor(k,publicKey(privKeyDialer[]),publicKey(privKeyAcceptor[]))) is true *)
+
+(* Channel Secrecy and Dialer Privacy*)
+query attacker(privKeyDialer).  (* Desired ProVerif output: not attacker(privKeyDialer) is true *)
+query attacker(privKeyAcceptor).  (* Desired ProVerif output: not attacker(privKeyAcceptor) is true *)
+query attacker(publicKey(privKeyDialer)).  (* Desired ProVerif output: not attacker(publicKey(privKeyDialer)) is true *)
+
+(* Lack of Acceptor Privacy *)
+query attacker(publicKey(privKeyAcceptor)).  (* Desired ProVerif output: not attacker(publicKey(privKeyAcceptor)) is false *)
+
+process handshakeInstance()
\ No newline at end of file
diff --git a/content/tutorials/syncbase/syncql-tutorial.md b/content/tutorials/syncbase/syncql-tutorial.md
new file mode 100644
index 0000000..8abed1e
--- /dev/null
+++ b/content/tutorials/syncbase/syncql-tutorial.md
@@ -0,0 +1,1107 @@
+= yaml =
+title: SyncQL Tutorial
+layout: tutorial
+wherein: you learn about the Syncbase query language.
+toc: true
+= yaml =
+
+# Overview
+
+Syncbase is Vanadium's key/value store and provides persistent data with fine grained access and synchronization across Syncbase instances.
+
+SyncQL is a SQL-like query language for Syncbase.
+
+This tutorial walks one through the setup of a sample database and then dives into teaching syncQL by running command-line queries.
+
+# How to Take this Tutorial
+
+This tutorial assumes one has a working Vanadium development environment.
+
+All of the steps are independent, so one can pick up anywhere he wishes.  Just perform the [setup](#setup) steps to start/restart and the [teardown](#teardown) steps to finish/take a break.
+
+It's OK to cut and paste the [setup](#setup) and [teardown](#teardown) steps, but please consider typing the queries rather than cutting and pasting them.  Actually typing the queries (and making mistakes and correcting them) is a great way to learn.
+
+# Setup
+
+This set of step-by-step instructions assumes one has a working Vanadium development environment, which includes having the `JIRI_ROOT` environment variable set.
+
+**[NOTE]** For the Vanadium and/or Syncbase literate, it's OK to skip and/or modify some of these steps.
+
+1. Build and install the necessary executables (principal program, mount table daemon, Syncbase daemon, Syncbase command-line program):
+
+        jiri go install v.io/x/ref/cmd/principal v.io/x/ref/services/mounttable/mounttabled v.io/x/ref/services/syncbase/syncbased v.io/x/ref/cmd/sb
+
+2. Create a principal using a self-signed blessing:
+
+        $JIRI_ROOT/release/go/bin/principal create /tmp/me $($JIRI_ROOT/release/go/bin/principal blessself)
+
+3. Start the mounttable and Syncbase daemons (start in foreground to enter root password, then send to background):
+
+        $JIRI_ROOT/release/go/bin/mounttabled -v23.tcp.address=:8101
+        <ctrl-z>
+        bg
+        $JIRI_ROOT/release/go/bin/syncbased -name '/:8101/syncbase' -v23.credentials=/tmp/me -root-dir=/tmp/sbroot
+        <ctrl-z>
+        bg
+
+4. Start `sb` (Syncbase command-line program):
+
+        $JIRI_ROOT/release/go/bin/sb sh -create-missing -v23.credentials=/tmp/me demoapp demodb
+
+5. Create a demo database:
+
+        ? make-demo;
+
+**[NOTE]** When you finish the tutorial (or want to take a break), execute the [teardown](#teardown) steps below to clean up!
+
+# Executing Queries in "sb"
+
+If one has performed the setup steps above, he will be sitting in `sb` at the '?' prompt.
+
+To make sure everything is running properly, dump the database with the following command (be sure to include the semicolon):
+
+    dump;
+
+If a bunch of data prints to the screen, everything is properly setup.  If not, execute the [teardown](#teardown) steps below and then re-execute the steps above.
+
+Don't try to understand all of the data that was printed with the dump command.  The tables in the demo database are overly complicated in order to demonstrate all of the features of syncQL.  We'll take things a step at a time and only explain the data as needed.
+
+Note: The vdl objects stored in the demo database are described in the following file:
+
+    $JIRI_ROOT/release/go/src/v.io/x/ref/cmd/sb/internal/demodb/db_objects.vdl
+
+# SyncQL 101
+
+## The Basics
+
+SyncQL looks a lot like SQL.  Each table in a Syncbase database looks like a table with exactly two columns, k and v:
+
+* `k`
+    * the key portion of key/value pairs in the table
+    * always of type string
+* `v`
+    * the value portion of key/value pairs in the table
+    * always of type vdl.Value
+
+### vdl
+
+A vdl.Value can represent the following types:
+
+<!-- TODO: Maybe use GFM tables here. -->
+<table>
+  <tr>
+    <td>Any</td>
+    <td>Array</td>
+    <td>Bool</td>
+    <td>Byte</td>
+    <td>Complex64</td>
+    <td>Complex128</td>
+    <td>Enum</td>
+  </tr>
+  <tr>
+    <td>Float32</td>
+    <td>Float64</td>
+    <td>Int16</td>
+    <td>Int32</td>
+    <td>Int64</td>
+    <td>List</td>
+    <td>Map</td>
+  </tr>
+  <tr>
+    <td>Set</td>
+    <td>String</td>
+    <td>Struct</td>
+    <td>Time</td>
+    <td>TypeObject</td>
+    <td>Union</td>
+    <td>Uint16</td>
+  </tr>
+  <tr>
+    <td>Uint32</td>
+    <td>Uint64</td>
+    <td>?&lt;type&gt;</td>
+    <td></td>
+    <td></td>
+    <td></td>
+    <td></td>
+  </tr>
+</table>
+
+## A Simple Query
+
+The Customers table stores values of type Customer and of type Invoice.
+
+Let's select all of the keys in the Customer table.  Again, note the semicolon.  The semicolon is **not** part of the query, but `sb` uses it as a marker for end of statement.
+
+    ? select k from Customers;
+    +--------+
+    |      k |
+    +--------+
+    | 001    |
+    | 001001 |
+    | 001002 |
+    | 001003 |
+    | 002    |
+    | 002001 |
+    | 002002 |
+    | 002003 |
+    | 002004 |
+    +--------+
+
+### Checker-time Errors
+
+Let's do the above query, but use Customer as the table name (i.e., forget to type the 's' at the end):
+
+    ? select k from Customer;
+    Error:
+    select k from Customer
+                  ^
+    15: Table Customer does not exist (or cannot be accessed): syncbased:"demoapp/demodb".Exec: Does not exist: $table:Customer.
+
+The query can be fixed by up-arrowing and fixing it or by simply retyping it.
+
+    ? select k from Customers;
+    +--------+
+    |      k |
+    +--------+
+    | 001    |
+    | 001001 |
+    | 001002 |
+    | 001003 |
+    | 002    |
+    | 002001 |
+    | 002002 |
+    | 002003 |
+    | 002004 |
+    +--------+
+
+SyncQL will catch and report the following types of errors before attempting to execute:
+
+* malformed queries (e.g., forgetting the required from clause)
+* mistyped table names
+* wrong number of arguments to a function
+* wrong type of literal (as an argument to a function or to a like expression)
+
+Unfortunately, mistyping field names will **not** be caught.  This is because syncQL doesn't know the fields of the values in the database.  That's because Syncbase allows anything to be stored in values.
+
+### Drilling Into the 'v' Column
+
+The Customer type has a Name field.  Let's ask for it by using dot notation:
+
+    ? select k, v.Name from Customers;
+    +--------+---------------+
+    |      k |        v.Name |
+    +--------+---------------+
+    | 001    | John Smith    |
+    | 001001 |               |
+    | 001002 |               |
+    | 001003 |               |
+    | 002    | Bat Masterson |
+    | 002001 |               |
+    | 002002 |               |
+    | 002003 |               |
+    | 002004 |               |
+    +--------+---------------+
+
+You will notice that only keys "001" and "002" have values for Name.  Let's see why that is.
+
+### Discovering Type of Values
+
+Let's find out the types of the values in the Customers table:
+
+    ? select k, Type(v) from Customers;
+    +--------+--------------------------------------------+
+    |      k |                                       Type |
+    +--------+--------------------------------------------+
+    | 001    | v.io/x/ref/cmd/sb/internal/demodb.Customer |
+    | 001001 | v.io/x/ref/cmd/sb/internal/demodb.Invoice  |
+    | 001002 | v.io/x/ref/cmd/sb/internal/demodb.Invoice  |
+    | 001003 | v.io/x/ref/cmd/sb/internal/demodb.Invoice  |
+    | 002    | v.io/x/ref/cmd/sb/internal/demodb.Customer |
+    | 002001 | v.io/x/ref/cmd/sb/internal/demodb.Invoice  |
+    | 002002 | v.io/x/ref/cmd/sb/internal/demodb.Invoice  |
+    | 002003 | v.io/x/ref/cmd/sb/internal/demodb.Invoice  |
+    | 002004 | v.io/x/ref/cmd/sb/internal/demodb.Invoice  |
+    +--------+--------------------------------------------+
+
+We now have an explanation for why the Name column is missing on some rows.  The type is not Customer on these rows.  It is Invoice and-it just so happens-Invoice has no field with the name of "Name".  Unresolved fields in the select clause return nil.  `sb` represents nil as empty in output.
+
+### Limiting Rows by Type
+
+Let's print the name of only rows where the value type is Customer.
+
+    ? select v.Name from Customers where Type(v) = "v.io/x/ref/cmd/sb/internal/demodb.Customer";
+    +---------------+
+    |        v.Name |
+    +---------------+
+    | John Smith    |
+    | Bat Masterson |
+    +---------------+
+
+`Type()` is a function available in syncQL.  It returns a string representing a fully qualified type.  It can be used in a where clause to limit the rows (i.e., the k/v pairs) matching a query.
+
+Having to specify a fully qualified type is rarely necessary.  Let's use the like operator to write a simpler query:
+
+    ? select v.Name from Customers where Type(v) like "%Customer";
+    +---------------+
+    |        v.Name |
+    +---------------+
+    | John Smith    |
+    | Bat Masterson |
+    +---------------+
+
+The like operator takes a string value on the right-hand-side.  In this value, `%` matches 0 or more of any character.  (Also, `_` matches any single character.)
+
+### The Invoice Type
+
+The Invoice type is defined as:
+
+    type Invoice struct {
+            CustId     int64
+            InvoiceNum int64
+            Amount     int64
+            ShipTo     AddressInfo
+    }
+
+Let's print CustId, InvoiceNum and Amount for values of type Invoice:
+
+    ? select v.CustId, v.InvoiceNum, v.Amount from Customers where Type(v) like "%Invoice";
+    +----------+--------------+----------+
+    | v.CustId | v.InvoiceNum | v.Amount |
+    +----------+--------------+----------+
+    |        1 |         1000 |       42 |
+    |        1 |         1003 |        7 |
+    |        1 |         1005 |       88 |
+    |        2 |         1001 |      166 |
+    |        2 |         1002 |      243 |
+    |        2 |         1004 |      787 |
+    |        2 |         1006 |       88 |
+    +----------+--------------+----------+
+
+The where clause can contain any number of comparison expressions joined with "and" or "or".  Parentheses are used to specify precedence.  For example, let's make a [nonsensical] query for all customer #1 invoices for an amount < 50 and all customer #2 invoices for an amount > 200:
+
+    ? select v.CustId, v.InvoiceNum, v.Amount from Customers where Type(v) like "%Invoice" and ((v.CustId = 1 and v.Amount < 50) or (v.CustId = 2 and v.Amount > 200));
+    +----------+--------------+----------+
+    | v.CustId | v.InvoiceNum | v.Amount |
+    +----------+--------------+----------+
+    |        1 |         1000 |       42 |
+    |        1 |         1003 |        7 |
+    |        2 |         1002 |      243 |
+    |        2 |         1004 |      787 |
+    +----------+--------------+----------+
+
+### Unresolved Fields in the Where Clause
+
+We've already seen that unresolved fields in the select clause return nil.  Unresolved fields in expressions in the where clause result in the expression evaluating to false.
+
+Let's see this in action:
+
+The Customer type is defined as:
+
+    type Customer struct {
+            Name    string
+            Id      int64
+            Active  bool
+            Address AddressInfo
+            Credit  CreditReport
+    }
+
+Let's select Customers with `Id > 0`:
+
+    ? select v.Name from Customers where v.Id > 0;
+    +---------------+
+    |        v.Name |
+    +---------------+
+    | John Smith    |
+    | Bat Masterson |
+    +---------------+
+
+Since `v.Id` is not resolvable for Invoice records (which do not contain an Id field), the expression `v.Id > 0` returns false for Invoice rows.  As such, the query excludes invoices and returns only the Customer rows.
+
+# SyncQL 201: A Closer Look
+
+## Select Clause
+
+Let's take a close look at what columns can be specified in the select clause.
+
+A column may be of one of the following categories:
+
+* k - the key column
+* v - the value column
+* field - a specific field in the value
+* function - a function which takes zero or more arguments (k, v, field or function)
+
+Let's select a column from each category above:
+
+    ? select k, v, v.ShipTo.City, Lowercase(v.ShipTo.City) from Customers where Type(v) like "%Invoice";
+    +--------+---------------------------------------------------------------------------------------------------------------------------+---------------+-----------+
+    |      k |                                                                                                                         v | v.ShipTo.City | Lowercase |
+    +--------+---------------------------------------------------------------------------------------------------------------------------+---------------+-----------+
+    | 001001 | {CustId: 1, InvoiceNum: 1000, Amount: 42, ShipTo: {Street: "1 Main St.", City: "Palo Alto", State: "CA", Zip: "94303"}}   | Palo Alto     | palo alto |
+    | 001002 | {CustId: 1, InvoiceNum: 1003, Amount: 7, ShipTo: {Street: "2 Main St.", City: "Palo Alto", State: "CA", Zip: "94303"}}    | Palo Alto     | palo alto |
+    | 001003 | {CustId: 1, InvoiceNum: 1005, Amount: 88, ShipTo: {Street: "3 Main St.", City: "Palo Alto", State: "CA", Zip: "94303"}}   | Palo Alto     | palo alto |
+    | 002001 | {CustId: 2, InvoiceNum: 1001, Amount: 166, ShipTo: {Street: "777 Any St.", City: "Collins", State: "IA", Zip: "50055"}}   | Collins       | collins   |
+    | 002002 | {CustId: 2, InvoiceNum: 1002, Amount: 243, ShipTo: {Street: "888 Any St.", City: "Collins", State: "IA", Zip: "50055"}}   | Collins       | collins   |
+    | 002003 | {CustId: 2, InvoiceNum: 1004, Amount: 787, ShipTo: {Street: "999 Any St.", City: "Collins", State: "IA", Zip: "50055"}}   | Collins       | collins   |
+    | 002004 | {CustId: 2, InvoiceNum: 1006, Amount: 88, ShipTo: {Street: "101010 Any St.", City: "Collins", State: "IA", Zip: "50055"}} | Collins       | collins   |
+    +--------+---------------------------------------------------------------------------------------------------------------------------+---------------+-----------+
+
+Depending on how wide your window is, the above mayh be a mess to look at.  Selecting v in a program is often useful, but selecting such an aggregate from `sb` is less so.  Let's do that query again without selecting v as a whole:
+
+    ? select k, v.ShipTo.City, Lowercase(v.ShipTo.City) from Customers where Type(v) like "%Invoice";
+    +--------+---------------+-----------+
+    |      k | v.ShipTo.City | Lowercase |
+    +--------+---------------+-----------+
+    | 001001 | Palo Alto     | palo alto |
+    | 001002 | Palo Alto     | palo alto |
+    | 001003 | Palo Alto     | palo alto |
+    | 002001 | Collins       | collins   |
+    | 002002 | Collins       | collins   |
+    | 002003 | Collins       | collins   |
+    | 002004 | Collins       | collins   |
+    +--------+---------------+-----------+
+
+v.ShipTo.City is interesting because it reaches into a nested struct.  In this case, ShipTo is a field in type Invoice.  ShipTo is of type AddressInfo, which is defined as:
+
+    type AddressInfo struct {
+            Street string
+            City   string
+            State  string
+            Zip    string
+    }
+
+v.ShipTo resolves to an instance of AddressInfo.  v.ShipTo.City resolves to an instance of string since City is a string field in AddressInfo.
+
+The Lowercase function takes a single string argument and simply returns a lowercase version of the argument.
+
+### Details on Value Field Specifications
+
+Up until now, we've used dot notation to specify fields within a struct (e.g., v.Name).  Let's look at the full picture.
+
+As mentioned before, values in Syncbase are vdl.Values.  A vdl.Value can represent any of the following types:
+
+<!-- TODO: Maybe use GFM tables here. -->
+<table>
+  <tr>
+    <td>Any</td>
+    <td>Array</td>
+    <td>Bool</td>
+    <td>Byte</td>
+    <td>Complex64</td>
+    <td>Complex128</td>
+    <td>Enum</td>
+  </tr>
+  <tr>
+    <td>Float32</td>
+    <td>Float64</td>
+    <td>Int16</td>
+    <td>Int32</td>
+    <td>Int64</td>
+    <td>List</td>
+    <td>Map</td>
+  </tr>
+  <tr>
+    <td>Set</td>
+    <td>String</td>
+    <td>Struct</td>
+    <td>Time</td>
+    <td>TypeObject</td>
+    <td>Union</td>
+    <td>Uint16</td>
+  </tr>
+  <tr>
+    <td>Uint32</td>
+    <td>Uint64</td>
+    <td>?&lt;type&gt;</td>
+    <td></td>
+    <td></td>
+    <td></td>
+    <td></td>
+  </tr>
+</table>
+
+#### Primitives
+
+The following vdl types are primitives and cannot be drilled into further:
+
+* Bool
+* Byte
+* Complex64
+* Complex128
+* Enum
+* Float32
+* Float64
+* Int16
+* Int32
+* Int64
+* String
+* Time (not a vdl primitive, but treated like primitives in syncQL)
+* TypeObject
+* Uint16
+* Uint32
+* Uint64
+
+#### ?&lt;type&gt;
+
+If missing, optional fields resolve to nil.
+
+#### Composites
+
+Any vdl composite type can be drilled into, and the result drilled into, until the result is a primitive data type.  Following are the rules for how to drill into composite types, presented as examples:
+
+For the next few vdl.Value types, we'll be using the Composites table.  The values in the table are of type Composite, which is defined as:
+
+    type Composite struct {
+            Arr     Array2String
+            ListInt []int32
+            MySet   set[int32]
+            Map     map[string]int32
+    }
+
+In this type:
+
+* Arr is an array of length two and contains string elements.
+* ListInt is a list of int32s.
+* MySet is a set of int32s.
+* Map contains string keys with int32 values.
+
+Let's have a look at the single row in the Composites table:
+
+    ? select k, v from Composites;
+    +-----+----------------------------------------------------------------------------------+
+    |   k |                                                                                v |
+    +-----+----------------------------------------------------------------------------------+
+    | uno | {Arr: ["foo", "bar"], ListInt: [1, 2], MySet: {1, 2}, Map: {"bar": 2, "foo": 1}} |
+    +-----+----------------------------------------------------------------------------------+
+
+#### Array and List
+
+Array elements are specified with bracket syntax:
+
+    ? select v.Arr[0], v.Arr[1], v.Arr[2] from Composites;
+    +----------+----------+----------+
+    | v.Arr[0] | v.Arr[1] | v.Arr[2] |
+    +----------+----------+----------+
+    | foo      | bar      |          |
+    +----------+----------+----------+
+
+The first two columns above return the elements in the array.  The third column can't be resolved as the array is of size 2.  As such, syncQL returns nil.
+
+The index need not be a literal:
+
+    ? select v.Arr[v.ListInt[0]] from Composites;
+    +---------------------+
+    | v.Arr[v.ListInt[0]] |
+    +---------------------+
+    | bar                 |
+    +---------------------+
+
+In the query above, the index is another field, the ListInt field.  The first element of the list contains the value 1 and v.Arr[1] contains "bar".  The index could be a function also.
+
+As you can see, from v.ListInt[0] in the query above, lists are treated the same as arrays in syncQL - to address a single element, put the index in brackets.
+
+By the way, syncQL will try to convert the value specified as the index into an int.  Such as in this case where a float is converted to an int.
+
+    ? select v.ListInt[1.0] from Composites;
+    +--------------+
+    | v.ListInt[1] |
+    +--------------+
+    |            2 |
+    +--------------+
+
+If syncQL cannot convert the value to an int, nil is returned as the field cannot be resolved.  This is a hard and fast rule for fields in the select clause: if they can't be resolved, they are nil.
+
+#### Map
+
+Values in maps are specified by supplying a key with bracket syntax.  Note: The key need not be a literal; functions and fields work also.
+
+    ? select v.Map["foo"] from Composites;
+    +------------+
+    | v.Map[foo] |
+    +------------+
+    |          1 |
+    +------------+
+
+#### Set
+
+Brackets are also used for sets in syncQL.  For sets, if the value specified inside the brackets is present in the set, the field evaluates to true.  Otherwise, it evaluates to false.
+
+Let's execute a query on MySet - an int32 set which contains the values 1 and 2:
+
+    ? select v.MySet[-23], v.MySet[2], v.MySet[55], v.MySet["xyzzy"] from Composites;
+    +--------------+------------+-------------+----------------+
+    | v.MySet[-23] | v.MySet[2] | v.MySet[55] | v.MySet[xyzzy] |
+    +--------------+------------+-------------+----------------+
+    |        false |       true |       false |                |
+    +--------------+------------+-------------+----------------+
+
+The values -23 and 55 are not in the set; hence, the columns are false.  The value 2 is in the set; hence, true.  The value "xyzzy" cannot be converted to an int32; hence, nil is returned.
+
+#### Struct
+
+As we have seen earlier, structs are drilled into my specifying the name of the field in dot notation.
+
+Let's revisit the Customer type:
+
+    type Customer struct {
+            Name    string
+            Id      int64
+            Active  bool
+            Address AddressInfo
+            Credit  CreditReport
+    }
+
+Now, let's print the `Id`, `Name` and `Active` status for Customer 1.
+
+    ? select v.Id, v.Name, v.Active from Customers where v.Id = 1;
+    +------+------------+----------+
+    | v.Id |     v.Name | v.Active |
+    +------+------------+----------+
+    |    1 | John Smith |     true |
+    +------+------------+----------+
+
+#### Union
+
+Dot notation is also used to drill into unions.  If a specific field in the union is specified, but is not present in the instance, nil is returned.
+
+An example will help to explain this.  The Students table contains the Student type which contains a union:
+
+    type ActOrSatScore union {
+            ActScore uint16
+            SatScore uint16
+    }
+
+    type Student struct {
+            Name     string
+            TestTime time.Time
+            Score    ActOrSatScore
+    }
+
+Let's print the k, Name and Score columns in the Students table:
+
+    ? select k, v.Name, v.Score from Students;
+    +---+------------+----------------+
+    | k |     v.Name |        v.Score |
+    +---+------------+----------------+
+    | 1 | John Smith | ActScore: 36   |
+    | 2 | Mary Jones | SatScore: 1200 |
+    +---+------------+----------------+
+
+Student #1, John Smith has an ACT score.  Student #2, Mary Jones has an SAT score.  `sb` has pretty printed the ActOrSatScore union.
+
+Let's print ActScore and SatScore:
+
+    ? select k, v.Name, v.Score.ActScore, v.Score.SatScore from Students;
+    +---+------------+------------------+------------------+
+    | k |     v.Name | v.Score.ActScore | v.Score.SatScore |
+    +---+------------+------------------+------------------+
+    | 1 | John Smith |               36 |                  |
+    | 2 | Mary Jones |                  | 1200             |
+    +---+------------+------------------+------------------+
+
+SatScore for John is nil.  ActScore for Mary is nil.
+
+#### Any
+
+Lastly, let's look at how type any is handled.  The AnythingGoes table contains the following type:
+
+    type AnythingGoes struct {
+            NameOfType string
+            Anything   any
+    }
+
+The demo database contains two k/v pairs in this table.  A Customer instance and a Student instance.  Let's query for the key, the NameOfType field, the Name field (which is contained in both types), the Active field (contained in Customer) and the Score.ActScore (contained in Student's union field).
+
+    ? select v.NameOfType, v.Anything.Name, v.Anything.Active, v.Anything.Score.ActScore from AnythingGoes;
+    +--------------+-----------------+-------------------+---------------------------+
+    | v.NameOfType | v.Anything.Name | v.Anything.Active | v.Anything.Score.ActScore |
+    +--------------+-----------------+-------------------+---------------------------+
+    | Student      | John Smith      |                   |                        36 |
+    | Customer     | Bat Masterson   | true              |                           |
+    +--------------+-----------------+-------------------+---------------------------+
+
+Any fields resolve to the actual type and value for the particular instance (which could be nil).
+
+### Functions in the Select Clause
+
+Functions can be freely used in the select clause, including as arguments to other functions and between brackets to drill into maps, sets, arrays and lists.
+
+#### List of Functions
+
+##### Time Functions
+
+* **Time(layout, value string) Time** - go's `time.Parse`, [doc](https://golang.org/pkg/time/#Parse)
+* **Now() Time** - returns the current time
+* **Year(time Time, Loc string) int** - Year of the time argument in location `Loc`.
+* **Month(time Time, Loc string) int** - Month of the time argument in location `Loc`.
+* **Day(time Time, Loc string) int** - Day of the time argument in location `Loc`.
+* **Hour(time Time, Loc string) int** - Hour of the time argument in location `Loc`.
+* **Minute(time Time, Loc string) int** - Minute of the time argument in location `Loc`.
+* **Second(time Time, Loc string) int** - Second of the time argument in location `Loc`.
+* **Nanosecond(time Time, Loc string) int** - Nanosecond of the time argument in location `Loc`.
+* **Weekday(time Time, Loc string) int** - Day of the week of the time argument in location `Loc`.
+* **YearDay(time Time, Loc string) int** - Day of the year of the time argument in location `Loc`.
+
+##### String Functions
+
+* **Atoi(s string) int** - converts `s` to an int
+* **Atof(s string) int** - converts `s` to a float
+* **HtmlEscape(s string) string** - go's `html.EscapeString`, [doc](https://golang.org/pkg/html/#EscapeString)
+* **HtmlUnescape(s string) string** - go's `html.UnescapeString`, [doc](https://golang.org/pkg/html/#UnescapeString)
+* **Lowercase(s string) string** - lowercase of `s`
+* **Split(s, sep string) []string** - substrings between separator `sep`
+* **Type(v vdl.Value) string** - the type of `v`
+* **Uppercase(s string) string** - uppercase of `s`
+* **RuneCount(s string) int** - the number of runes in `s`
+* **Sprintf(fmt string, a ...vdl.Value) string** - go's `fmt.Sprintf`, [doc](https://golang.org/pkg/fmt/#Sprintf)
+* **Str(v vdl.Value) string** - converts `v` to a string
+* **StrCat(s ...string) string** - concatenation of `s` args
+* **StrIndex(s, sep string) int** - index of `sep` in `s`, or -1 if `sep` is not present
+* **StrRepeat(s string, count int) string** - `s` repeated count times
+* **StrReplace(s, old, new string) string** - `s` with first instance of `old` replaced by `new`
+* **StrLastIndex(s, sep string) int** - index of the last instance of `sep` in `s`, or -1
+* **Trim(s string) string** - `s` with all leading and trailing whitespace removed (as defined by Unicode)
+* **TrimLeft(s string) string** - `s` with all leading whitespace removed (as defined by Unicode)
+* **TrimRight(s string) string** - `s` with trailing whitespace removed (as defined by Unicode)
+
+##### Math Functions
+
+* **Ceiling(x float) int** - least integer value greater than or equal to `x`
+* **Complex(r, i float) complex** - complex value from `r` and `i`
+* **Floor(x float) int** - greatest integer value less than or equal to `x`
+* **IsInf(f float, sign int) bool** - true if `f` is an infinity, according to `sign`
+* **IsNaN(f float) bool** - true if `f` is an IEEE 754 "not-a-number" value
+* **Log(x float) float** - natural logarithm of `x`
+* **Log10(x float) float** - decimal logarithm of `x`
+* **Pow(x, y float) float** - `x**y`
+* **Pow10(e int) float** - `10**e`
+* **Mod(x, y float) float** - remainder of `x/y`
+* **Real(c complex) float** - the real part of `c`
+* **Truncate(x float) float** - integer value of `x`
+* **Remainder(x, y float) float** - IEEE 754 floating-point remainder of `x/y`
+
+##### Len Function
+
+* **Len(v vdl.Value) int** - # entries in array/list/map/set, # bytes in string, 0 for nil, otherwise error
+
+#### Function Examples
+
+Let's use the Student table again.  Recall that it contains Student types defined as:
+
+    type Student struct {
+            Name     string
+            TestTime time.Time
+            Score    ActOrSatScore
+    }
+
+To print the day of the week (in PDT) that a student's tests were taken:
+
+    ? select v.Name, Weekday(v.TestTime, "America/Los_Angeles") from Students;
+    +------------+---------+
+    |     v.Name | Weekday |
+    +------------+---------+
+    | John Smith |       3 |
+    | Mary Jones |       5 |
+    +------------+---------+
+
+Three things to remember about using functions are:
+
+1. If the function contains only literals (or other functions that can be evaluated before query execution), the function will be executed beforehand and, if an error is encountered, it will be returned to the user.
+2. If any arguments are literals and the literal arguments can be checked before query execution, they are checked and an error returned to the user.
+3. If the error can't be found before query execution-that is, if the error occurs when evaluating a specific k/v pair, the column evaluates to nil (the same as always for the select clause).
+
+An example of case #1 above is the Now() function.
+
+Examples of case #2 are the many functions that contain a location argument.  This argument is often a literal.  Here's an example of getting the location wrong and getting an error before query execution:
+
+? select v.Name, Weekday(v.TestTime, "MyPlace") from Students;
+    Error:
+    select v.Name, Weekday(v.TestTime, "MyPlace") from Students
+                                       ^
+    36: Can't convert to location: cannot find MyPlace in zip file /usr/local/go/lib/time/zoneinfo.zip.
+
+### As
+
+There just one more thing to say about the select clause.  Sometimes you might want the column heading to be prettier than what is returned by default.  This can be accomplished by using As.  Let's try using it.
+
+    ? select v.Name as Name from Customers where Type(v) like "%Customer";
+    +---------------+
+    |          Name |
+    +---------------+
+    | John Smith    |
+    | Bat Masterson |
+    +---------------+
+
+Instead of a column header of v.Name, the column is labeled Name.
+
+## From Clause
+
+The from clause must follow the where clause.  There's not much to this clause.  Just pick the table.  If you get it wrong (or if you don't have access to the table), you will get an error before query execution.
+
+    ? select k from Cust;
+    Error:
+    select k from Cust
+                  ^
+    15: Table Cust does not exist (or cannot be accessed): syncbased:"demoapp/demodb".Exec: Does not exist: $table:Cust.
+    ? select k from Customers;
+    +--------+
+    |      k |
+    +--------+
+    | 001    |
+    | 001001 |
+    | 001002 |
+    | 001003 |
+    | 002    |
+    | 002001 |
+    | 002002 |
+    | 002003 |
+    | 002004 |
+    +--------+
+
+## Where Clause
+
+The where clause is optional and is used to filter the k/v pairs in a table.  If the where clause evaluates to true for any given k/v pair, the pair is included in the results.
+
+We've already seen the where clause in action to limit the pairs returned in the Customers table to just those of type Customer:
+
+    ? select k, v.Name from Customers where Type(v) like "%Customer";
+    +-----+---------------+
+    |   k |        v.Name |
+    +-----+---------------+
+    | 001 | John Smith    |
+    | 002 | Bat Masterson |
+    +-----+---------------+
+
+For the two k/v pairs in the Customers table that contain a value of type Customer, the where clause returns true.
+
+In the query above, `Type(v) like "%Customer"` is a *comparison expression*.  The where clause may contain multiple comparison expressions separated by 'and' or 'or' to form logical expressions.  Furthermore, logical expressions may be grouped for precedence with parenthesis.
+
+Let' try another query with a logical expression grouped with parenthesis:
+
+    ? select v.InvoiceNum, v.Amount from Customers where Type(v) like "%Invoice" and (v.Amount = 7 or v.Amount = 787);
+    +--------------+----------+
+    | v.InvoiceNum | v.Amount |
+    +--------------+----------+
+    |         1003 |        7 |
+    |         1004 |      787 |
+    +--------------+----------+
+
+### Comparison Expressions
+
+Comparison expressions are of the form:
+
+<*left-operand*> <*operator*> <*right-operand*>
+
+There's good news!  Everything (Note: OK, not everything.  Using 'As' doesn't make sense and can't be used in the where clause.) you've learned about what can be specified in the select clause can be specified as an operand in the where clause.
+
+Having said that, there is one important difference regarding fields that cannot be resolved.  In the select clause, unresolved fields return nil.  **_In the where clause, unresolved fields cause the comparison expression to be false._**
+
+To illustrate this point, let's do the following query:
+
+    ? select v.InvoiceNum, v.Amount from Customers where v.Amount <> 787;
+    +--------------+----------+
+    | v.InvoiceNum | v.Amount |
+    +--------------+----------+
+    |         1000 |       42 |
+    |         1003 |        7 |
+    |         1005 |       88 |
+    |         1001 |      166 |
+    |         1002 |      243 |
+    |         1006 |       88 |
+    +--------------+----------+
+
+The above query doesn't print invoice number 1004, which is for the amount 787; but it also doesn't print the Customer records (which would have nil for InvoiceNum and Amount) because the comparison expression evaluates to false.  It evaluates to false because v.Amount cannot be resolved for Customer types.
+
+Let's try another query to bring home the point.  Let's match customer name with a wildcard expression that will match anything:
+
+    ? select v.Name from Customers where v.Name like "%";
+    +---------------+
+    |        v.Name |
+    +---------------+
+    | John Smith    |
+    | Bat Masterson |
+    +---------------+
+
+The above is a backhanded way limit the query to just Customer types.  Any name will do with the like "%" expression, but v.Name can't be resolved for values of type Invoice; thus, the comparision expression evaluates to false.
+
+#### Operators
+
+The following operators are available in syncQL:
+
+<table>
+  <tr>
+    <td>=</td>
+    <td>!=</td>
+    <td>&lt;</td>
+    <td>&lt;=</td>
+    <td>&gt;</td>
+  </tr>
+  <tr>
+    <td>&gt;=</td>
+    <td>is</td>
+    <td>is not</td>
+    <td>like</td>
+    <td>not like</td>
+  </tr>
+</table>
+
+The `is` and `like` operators deserve explanations.
+
+##### Is/Is Not
+
+The `is` and `is not` operators are used to test against nil. They can be used to test for nil and are the exception to the otherwise hard and fast rule that operands that can't be resolved result in the comparison expression returning false.
+
+A backhanded way to select only invoice values is to select values where v.Name is nil.  Invoice doesn't have a Name field, so Invoice values will be returned.
+
+? select v.InvoiceNum from Customers where v.Name is nil;
+
+    +--------------+
+    | v.InvoiceNum |
+    +--------------+
+    |         1000 |
+    |         1003 |
+    |         1005 |
+    |         1001 |
+    |         1002 |
+    |         1004 |
+    |         1006 |
+    +--------------+
+
+One could also use the query:
+
+    ? select v.InvoiceNum from Customers where v.InvoiceNum is not nil;
+    +--------------+
+    | v.InvoiceNum |
+    +--------------+
+    |         1000 |
+    |         1003 |
+    |         1005 |
+    |         1001 |
+    |         1002 |
+    |         1004 |
+    |         1006 |
+    +--------------+
+
+Important: Field Contains Nil vs. Field Cannot be Resolved
+
+SyncQL makes no distinction between a field with a nil value vs. a field that cannot be resolved.  As such, the first "backhanded" query above wouldn't work if the Name field could be nil in values of type Customer.  Ditto for the second query-it wouldn't work if InvoiceNum could be nil in an Invoice.
+
+##### Like/Not Like
+
+Like and not like require the right-hand-side operand to evaluate to a string.  The rhs operand may contain zero or more of the following wildcard characters:
+
+* % - A substitute for zero or more characters
+* _ - A substitute for a single character
+
+Let's find invoices where the ship to address is any house on Main St.
+
+    ? select v.InvoiceNum, v.ShipTo.Street from Customers where Type(v) like "%Invoice" and v.ShipTo.Street like "%Main St.";
+    +--------------+-----------------+
+    | v.InvoiceNum | v.ShipTo.Street |
+    +--------------+-----------------+
+    |         1000 | 1 Main St.      |
+    |         1003 | 2 Main St.      |
+    |         1005 | 3 Main St.      |
+    +--------------+-----------------+
+
+Just one more thing. To escape a '%' or '_' wildcard character, the escape clause must be included in the query to specify an escape character to use.  For example, to find all customers whose name includes an underscore character, one can write the following (using the '^' character to escape the underscore).  Note: The backslash and space characters cannot be used as the escape character.
+
+    ? select v.Id, v.Name from Customers where Type(v) like "%Customer" and v.Name like "%^_%" escape '^';
+    +------+------------+
+    | v.Id |     v.Name |
+    +------+------------+
+    +------+------------+
+
+Alas, there are no customers with an underscore in their name.  We can cheat by using a literal on the left hand side of the like.
+    ? select v.Id, v.Name from Customers where Type(v) like "%Customer" and "John_Doe" like "%^_%" escape '^';
+    +------+---------------+
+    | v.Id |        v.Name |
+    +------+---------------+
+    |    1 | John Smith    |
+    |    2 | Bat Masterson |
+    +------+---------------+
+Since the like expression is now true for all customer rows, we see both of them.
+
+Let's do the same thing to look for a percent.
+    ? select v.Id, v.Name from Customers where Type(v) like "%Customer" and "John%Doe" like "%^%%" escape '^';
+    +------+---------------+
+    | v.Id |        v.Name |
+    +------+---------------+
+    |    1 | John Smith    |
+    |    2 | Bat Masterson |
+    +------+---------------+
+
+#### Operand Value Coercion
+
+SyncQL will try to convert operands on either side of comparison expression to like types in order to perform a comparison.
+
+For example, let's find the customer with an `Id` of 1 (an int64 value); but use a float in the comparison.  SyncQL converts `v.Id` to a float and then compares it against the 1.0 float literal.
+
+    ? select v.Id, v.Name from Customers where Type(v) like "%Customer" and v.Id = 1.0;
+    +------+------------+
+    | v.Id |     v.Name |
+    +------+------------+
+    |    1 | John Smith |
+    +------+------------+
+
+Congratulations, you are finished with the where clause (and nearing the end of the tutorial)!
+
+## Offset and Limit Clauses
+
+The limit clause can be used to fetch the first n results.  The limit clause together with the offset clause can be used to fetch query results in batches.
+
+Let's print the first two keys in the Customers table:
+
+    ? select k from Customers limit 2;
+    +--------+
+    |      k |
+    +--------+
+    | 001    |
+    | 001001 |
+    +--------+
+
+Now, let's fetch the next two keys:
+
+    ? select k from Customers limit 2 offset 2;
+    +--------+
+    |      k |
+    +--------+
+    | 001002 |
+    | 001003 |
+    +--------+
+
+## Executing Delete Statements
+
+In addition to select statements, syncql supports delete statements.  (Insert and Update statements are planned.)
+
+The delete statement takes the form:
+    delete from <table> [<where-clause>] [<limit-clause>]
+
+The where and limit clauses for delete are identical to the where and limit caluses for select.
+
+To delete all k/v pairs in a table, leave off the where and limit clauses:
+
+    ? delete from Customers;
+    +-------+
+    | Count |
+    +-------+
+    |     9 |
+    +-------+
+
+Exactly one row with exactly one "Count" column is always returned from an execution of the delete statement.  The value of the column is the number of k/v paris deleted.  In this case, all nine k/v pairs in the Customers table have been deleted.  To verify this, select all entries in the Customers table:
+
+    ? select k from Customers;
+    +---+
+    | k |
+    +---+
+    +---+
+
+Let's restore the entries by executing make-demo again.
+    ? make-demo;
+    Demo tables created and populated.
+
+Now, let's use the where clause to delete only invoice entries:
+? delete from Customers where Type(v) like "%.Invoice";
+
+    +-------+
+    | Count |
+    +-------+
+    |     7 |
+    +-------+
+
+The seven invoice entries have been deleted.  A select reveals the delete indeed deleted what we expected.
+
+    ? select k, Type(v) from Customers;
+    +-----+--------------------------------------------+
+    |   k |                                       Type |
+    +-----+--------------------------------------------+
+    | 001 | v.io/x/ref/cmd/sb/internal/demodb.Customer |
+    | 002 | v.io/x/ref/cmd/sb/internal/demodb.Customer |
+    +-----+--------------------------------------------+
+
+Lastly, let's delete all Customers where the address is not Palo Alto:
+
+    ? delete from Customers where v.Address.City <> "Palo Alto";
+    +-------+
+    | Count |
+    +-------+
+    |     1 |
+    +-------+
+
+Since customer 001, John Smith, is in Palo Alto, the delete statement did not delete him. A select reveals Bat Masteson, who resides in Collins, IA, was indeed deleted.
+
+    ? select k from Customers;
+    +-----+
+    |   k |
+    +-----+
+    | 001 |
+    +-----+
+
+Let's restore the tables before we try the limit clause on a delete:
+
+    ? make-demo;
+    Demo tables created and populated.
+
+Now, let's delete Invoice entries again, but put a limit of two on the statement:
+
+    ? delete from Customers where Type(v) like "%.Invoice" limit 2;
+    +-------+
+    | Count |
+    +-------+
+    |     2 |
+    +-------+
+
+A select reveals only the first two invoices (in ascending key order) have been deleted ("001001" and "001002"):
+
+    ? select k from Customers;
+    +--------+
+    |      k |
+    +--------+
+    | 001    |
+    | 001003 |
+    | 002    |
+    | 002001 |
+    | 002002 |
+    | 002003 |
+    | 002004 |
+    +--------+
+
+Congratulations!  You've finished the syncQL tutorial.  Don't forget to proceed to the [teardown](#teardown) steps to clean up!  Also, check out the brief introduction to executing syncQL queries from a Go program.
+
+# Teardown
+
+Exit `sb` with <ctrl-d>, kill the syncbased and mounttabled background jobs and delete the principal directory:
+
+    <ctrl-d>
+    sudo kill $(jobs -p)
+    rm -rf /tmp/me
+
+# Executing SyncQL from a Go Program
+
+When using Syncbase's Get() and Put() functions, the programmer can often ignore the fact that keys and values are stored as type vdl.Value; but this is not true when making syncQL queries as returned columns are always of type vdl.Value.  For example, given the following query:
+
+    select k, v.Id, v.Address.Zip from Customers where Type(v) like \"%Customer\"
+
+a triple of vdl.Values will be returned for each k/v pair in the Customer table.  The caller could interrogate the vdl.Value as to the actual types stored inside, but usually the caller will know the types.  As such, the calling code will just need to call the String() functions for the first and third columns and the Int() function for the second column.
+
+The following code snippet might help to clarify the above:
+
+    q := "select k, v.Id, v.Address.Zip from Customers where Type(v) like \"%Customer\""
+    h, rs, err := db.Exec(ctx, q)
+    if err != nil {
+      fmt.Printf("Error: %v\n", err)
+    } else {
+      // Print Headers
+      fmt.Printf("%30.30s,%8.8s, %5.5s\n", h[0], h[1], h[2])
+      for rs.Advance() {
+        c := rs.Result()
+        fmt.Printf("%s30.30 %8.8d %5.5s\n", c[0], c[1], c[2])
+      }
+      if rs.Error() {
+        fmt.Printf("Error: %v\n", err)
+      }
+    }
+
+One will need to take the Syncbase tutorial before attempting to execute syncQL queries in a Go program; but once you are comfortable with Syncbase, the Exec function is straightforward.  Exec can be performed on the database object or from a readonly or writable batch object.
+
+Exec simply takes a context and the syncQL query (don't end it with a semicolon).  If successful, an array of column headers will be returned along with a stream of vdl.Value tuples.  Iteration over the stream will be familiar to Vanadium developers.
diff --git a/content/tutorials/syncbase/user-guide.md b/content/tutorials/syncbase/user-guide.md
new file mode 100644
index 0000000..741ee10
--- /dev/null
+++ b/content/tutorials/syncbase/user-guide.md
@@ -0,0 +1,405 @@
+= yaml =
+title: Syncbase User Guide
+layout: tutorial
+wherein: you learn about Syncbase
+toc: true
+= yaml =
+
+# Overview
+
+Syncbase is a storage system for developers that makes it easy to synchronize
+app data between devices. It works even when devices are not connected to the
+Internet.
+
+- Synchronization between one user's devices is trivial to configure; multiple
+  users can synchronize specific data too
+  - Low latency synchronization enables many apps to use storage for
+    asynchronous communication
+- Internet connection not required
+  - Local storage still works when not connected to the internet
+  - Synchronization protocol is peer-to-peer and works just as well over local
+    WiFi or Bluetooth as the internet
+- Conflict resolution system merges data when devices have been working offline
+- Unified storage model handles both structured data and blobs
+  - Structured databases are easy to use and queryable
+  - Blob caching policies work well on resource-limited devices
+- Powerful management tools
+  - Leverages the Vanadium namespace and security system
+  - Open source reference implementation of Syncbase for developers who want
+    tight control over the data
+
+The initial version of Syncbase is ready for testing and evaluation by early
+adopters - it is suitable for prototyping, but not for production applications.
+
+This document covers installation and basic usage. It should be enough for
+developers to get started using Syncbase. For more details on the design, see
+the [Syncbase Overview] document.
+
+# Installation
+
+Syncbase is a Go program that depends on Vanadium and several other libraries.
+The following steps cover all of the prerequisites, and should work on both
+Linux and OS X.
+
+1. Follow the [installation instructions] to install prerequisites and fetch the
+   Vanadium repositories, which include Syncbase as well as the Todos demo app.
+
+   The instructions below assume you've set the `JIRI_ROOT` environment variable
+   and have added `$JIRI_ROOT/devtools/bin` to your `PATH`:
+
+        # Edit to taste.
+        export JIRI_ROOT=${HOME}/vanadium
+        export PATH=$PATH:$JIRI_ROOT/devtools/bin
+
+   Recommended: Add the lines above to your `~/.bashrc` or similar.
+
+2. Run the Syncbase tests.
+
+        jiri go test v.io/v23/syncbase/...
+
+3. Build the Syncbase server binary and other Vanadium tools.
+
+        jiri go install v.io/...
+
+<!-- TODO: On OS X, step (2) opens a bunch of warning popups about accepting
+incoming connections. We should make all test servers listen on the loopback
+address. -->
+
+Note, the `jiri go` command simply augments the `GOPATH` environment variable
+with the various paths to Vanadium Go code under the `JIRI_ROOT` directory, and
+then runs the standard `go` tool.
+
+You should now have the following binaries available, among others:
+
+- `$JIRI_ROOT/release/go/bin/mounttabled`
+- `$JIRI_ROOT/release/go/bin/syncbased`
+- `$JIRI_ROOT/release/go/bin/vrpc`
+
+<!-- TODO: Add instructions about how to run a cloud instance of Syncbase. -->
+
+## Running the Todos Demo App
+
+The [Todos demo app] is a web application that runs in Chrome. Before you can
+run it, you must install the [Vanadium Chrome extension].
+
+To run the app, follow the demo setup instructions here:
+https://github.com/vanadium/todos/blob/master/demo.md
+
+To get a fresh copy of the Vanadium source code and rebuild everything for the
+demo, run these commands from the todos root dir:
+
+    jiri update
+    make clean
+
+If you get certificate signature verification errors when running the webapp,
+try uninstalling and reinstalling your [Vanadium Chrome extension].
+
+# Basic Usage
+
+In this section we demonstrate the basics of working with a local instance of
+Syncbase: setting up an initial `<app>/<database>/<table>` hierarchy, reading
+and writing data, and using batches.
+
+Application developers are expected to use Syncbase through a client library.
+Currently we provide client libraries for
+[Go](https://vanadium.googlesource.com/roadmap.go.syncbase/+/master/v23/syncbase/model.go),
+[JavaScript](https://vanadium.googlesource.com/roadmap.js.syncbase/+/master/src/syncbase.js),
+[Java](#todo) (Android), and [Dart](#todo) (Mojo/Sky). In this guide, to keep
+things simple and concise, we use the Go client library and ignore all errors
+returned from Syncbase.
+
+Let's create an app with a single NoSQL database, containing a single table. The
+following code snippets assume we have a Syncbase instance serving at
+`localhost:4002`.
+
+    import "v.io/syncbase/v23/syncbase"
+    ctx, shutdown := v23.Init() // initialize the Vanadium runtime
+    defer shutdown()
+    s := syncbase.NewService("/localhost:4002")
+    a := s.App("myapp")
+    a.Create(ctx, perms) // assumes "perms" is defined
+    d := a.NoSQLDatabase("mydb", nil) // nil means no schema
+    d.Create(ctx, perms)
+    t := d.Table("mytable")
+    t.Create(ctx, nil) // nil means copy perms from db
+
+We've created the hierarchy `myapp/mydb/mytable`. Now, let's read and write some
+key-value data to our table.
+
+    t.Put(ctx, "foo", "mystr")
+    t.Put(ctx, "bar", 600673)
+    t.Put(ctx, "baz", mystruct) // assumes "mystruct" is defined
+    var s1, s2 string
+    var i1 int
+    t.Get(ctx, "foo", &s1) // s1 will be "mystr"
+    t.Get(ctx, "bar", &i1) // i1 will be 600673
+    expectError(t.Get(ctx, "baz", &s2))  // s2 is the wrong type
+
+Next, let's scan over a range of key-value records. Scan returns a stream object
+that reads from a consistent snapshot taken at the time of the RPC.
+
+    it := t.Scan(ctx, nosql.Range("a", "z")) // covers ["a", "z")
+    it := t.Scan(ctx, nosql.Prefix("ba")) // covers keys with prefix "ba"
+    for it.Advance() {
+      var v *vdl.Value // can represent any type
+      it.Value(&v)
+      fmt.Println(it.Key(), v)
+    }
+    handleError(it.Err())
+
+Syncbase also supports SQL-like queries to scan over rows that match some
+predicate. For more information, see the [Queries](#queries) section of this
+guide.
+
+Finally, let's perform a set of operations in a batch. Batches follow ACID
+semantics on the local Syncbase instance, and relaxed ACID semantics when used
+with synchronization, as described in the [Syncbase Overview] document.
+
+    // For a read-only batch (i.e. to read from a snapshot), we'd set
+    // BatchOptions.ReadOnly to true.
+    nosql.RunInBatch(ctx, d, wire.BatchOptions{},
+                     func(bd nosql.BatchDatabase) error {
+      bt = bd.Table("mytable")
+      bt.Get(ctx, "bar", &i1) // i1 will be 600673
+      bt.Put(ctx, "foo", fmt.Sprintf(i1))
+      bt.Put(ctx, "bar", 2*i1)
+    })
+
+This batch writes the old value of "bar" to "foo" (as a string), then replaces
+"bar" with twice its original value. `nosql.RunInBatch` is a helper function
+that handles creating and committing the batch, as well as retrying the batch if
+a concurrent batch preempted ours.
+
+This concludes the "basic usage" section. For the complete Syncbase API, consult
+the client library in your language of choice. For "real-world usage", see the
+todos example app code.
+
+# Data Modeling
+
+Syncbase organizes data hierarchically: App > Database > Table > Row
+
+The "App" layer of hierarchy allows for multiple apps to share the same Syncbase
+instance, so that (for example) we can run a single Syncbase instance on a
+mobile device to service all apps running on that device.
+
+The Database is a set of NoSQL tables. It provides the scope for queries and
+batches similar to many relational databases. We expect that most apps will have
+a single database. It exists primarily because we expect to provide other types
+of databases in the future (e.g. SQL, timeseries).
+
+A Table is a lexicographically ordered set of rows with each row key mapping to
+a single value. Values can be anything representable by [VOM] such as simple
+types like string and int32 or complex, application-defined structs. We expect
+that many developers will choose to use [VDL] to model their data, though they
+are free to define structs in their native programming language. The values in a
+single table can be heterogeneous, allowing for better spatial locality than
+splitting the values into homogeneous tables.
+
+We expect developers to give a common key prefix to related data. For example, a
+TODO list might have a table like:
+
+    <list uuid>                -> List
+    <list uuid>/entries/<uuid> -> Entry
+    <list uuid>/entries/<uuid> -> Entry
+
+All entries in the list have a common prefix, making it easy to find all of the
+entries in the list. Note the use of Universally Unique Identifiers (UUIDs). The
+act of sharing and synchronizing this list with another user will cause this
+list to be spliced into that user's database. By using UUIDs, we ensure that
+this list will not collide with a list already in that database.
+
+##  Access Control
+
+Syncbase provides fine grained access control, using the [Vanadium security
+model] for identification and authentication. Developers provide a key prefix to
+control which rows are covered by a given access control list (ACL). If there
+are multiple ACL prefixes for a row, the one with the longest prefix wins. This
+behavior makes it easy to set an ACL on related data and have new data
+automatically inherit the right ACL if possible.
+
+In our example above, the list is fully collaborative, so the developer would
+set a simple ACL like:
+
+    <list uuid> -> {<owner>: Read, Write, Admin; <friends>: Read, Write}
+
+All entries in the list would inherit this ACL. We expect that most apps will
+use a single ACL for a group of related data, so we optimized for this case. To
+hide an entry from the friends, the owner would create another ACL:
+
+    <list uuid>/entries/<uuid> -> {<owner>: Read, Write, Admin}
+
+The existence of this ACL is revealed to the lowest levels of Syncbase on the
+friends' devices, but the content of the entry is not.
+
+## Syncgroups
+
+As you think about how to model the data for your application, it is important
+to understand how to specify which data to sync between devices. A syncgroup
+represents both what data should be synced and who to sync it with. The what is
+specified with a set of key prefixes similar to access control. Therefore, it is
+essential that related data have a common key prefix. See the section on
+[Sync](#sync) below for more details. The who is specified by a syncgroup ACL
+that determines the devices that are allowed to join the syncgroup. Typically
+this is done by specifying the identities of the device owners (and not their
+specific devices) to give each user the flexibility in selecting from which of
+their device(s) to join the syncgroup and participate in the data
+synchronization.
+
+# Queries
+
+The Syncbase query language, [syncQL], is very similar to SQL. SyncQL uses the
+general structure of SQL's SELECT statement. It efficiently evaluates predicates
+(the WHERE clause) inside the Syncbase process. It does not currently support
+JOINs or indexes.
+
+SyncQL uses the keywords k and v to represent the key and value for the row.
+SyncQL can unpack structs to evaluate the fields within. In this example, the
+structs in the Customer table have a field called "State". The query returns the
+row key and complete value struct for each row where State is 'CA'.
+
+    SELECT k, v FROM Customer WHERE v.State = 'CA'
+
+Because the key has significant structure, it is useful to restrict the query to
+a subset of the data. For example, to fetch all of the data for a customer with
+UUID 12345 (i.e. all rows with the prefix 12345):
+
+    SELECT v FROM Customer WHERE k LIKE "12345%"
+
+See the syncQL specification for the complete language and more examples.
+
+<!-- TODO: Add an example here that shows what Go code the developer would
+write. -->
+
+# Blobs
+
+A blob is created within a database and identified by a unique BlobRef. The app
+stores the BlobRef in a row in a NoSQL table (i.e. in the value structure of a
+NoSQL entry). When the table is synchronized to another device, the BlobRef can
+be used to fetch the blob and cache it in that device's local store. Blobs give
+the app a mechanism for lazy-fetching of data compared to the eager syncing of
+the NoSQL tables.
+
+Because blobs are typically large, the APIs to put and get blobs use a streaming
+interface.
+
+    // Create a blob. Assumes an existing hierarchy myapp/mydb/mytable.
+    s := syncbase.NewService("/localhost:4002")
+    d := s.App("myapp").NoSQLDatabase("mydb", nil)
+    b, err := d.CreateBlob(ctx)
+    bw, err := b.Put(ctx)
+    for moreData {
+      err = bw.Send(dataByteArray)
+    }
+    err = bw.Close()
+    err = b.Commit()
+    blobRef := b.Ref()
+    fmt.Printf("Blob written: BlobRef %s\n", blobRef)
+
+The BlobRef is used to get the blob data. If the blob is not available locally,
+Syncbase locates a device that has a copy of the blob, fetches it, caches it
+locally, and streams it to the client.
+
+    // Retrieve a blob. Assumes the same initialization above.
+    b := d.Blob(blobRef)
+    br, err := b.Get(ctx, 0) // Get the full blob, i.e. from offset 0.
+    var data []byte
+    for br.Advance() {
+      data = append(data, br.Value()...)
+    }
+    err = br.Err()
+    fmt.Printf("Blob read: BlobRef %s, len %d\n", blobRef, len(data))
+
+# Sync
+
+Syncbase provides peer-to-peer synchronization of data between a set of devices.
+The cloud is just another peer, and is not required. Devices attempt to discover
+one another by all means available, including the local network (over mDNS, aka
+Bonjour) and a configurable set of name servers.
+
+The fundamental unit of synchronization is a syncgroup. Syncgroups are tied to a
+database and can span tables. A syncgroup specifies what data to sync (as a set
+of table names and key prefixes) and who to sync it with (as an ACL specifying
+who can join the syncgroup). Syncgroup data may overlap or be nested within the
+data of other syncgroups. For example SG1 may specify prefixes "foo" and "bar"
+with SG2 specifying prefixes "f" and/or "bar123".
+
+To guarantee consistent access behavior across all devices within a syncgroup,
+the app must create a prefix-ACL (aka data-ACL) for each syncgroup prefix before
+it creates the syncgroup. Syncbase enforces this setup and synchronizes the
+prefix-ACLs along with the data. This way on every device the same prefix-ACLs
+are available and enforced for the synchronized data.
+
+A syncgroup is identified by a globally unique name selected by the creator.
+This name is given out-of-band to the other devices so they can join the
+syncgroup. The syncgroup name is a Vanadium name that is used to make the RPC
+calls to create or join the syngroup. Thus the syncgroup name must start with a
+Vanadium-resolvable server name.
+
+In many apps, you'll have one device create a syncgroup (e.g. a new todo list),
+and other devices join that syncgroup. The following code creates a syncgroup
+with table "mytable" and key prefix "foo".
+
+<!-- TODO: This syncgroup setup code is somewhat obtuse. Hopefully we can
+simplify the setup and improve the documentation. Various issues have been filed
+to track this. -->
+
+    // Assumes we've already created the hierarchy myapp/mydb/mytable.
+    s := syncbase.NewService("/localhost:4002")
+    d := s.App("myapp").NoSQLDatabase("mydb", nil)
+    sg := d.Syncgroup("/localhost:4002/%%sync/myapp/mydb/mysg")
+    sg.Create(ctx, wire.SyncgroupSpec{
+      Description: "my syncgroup",
+      Perms:       perms,
+      Prefixes:    []wire.TableRow{{TableName: "mytable", Row: "foo"}},
+      MountTables: []string{"/ns.dev.v.io:8101"},
+    }, wire.SyncgroupMemberInfo{
+      SyncPriority: 8
+    })
+
+The code below joins the syncgroup.
+
+    sg.Join(ctx, wire.SyncgroupMemberInfo{
+      SyncPriority: 8
+    })
+
+In some cases, an app won't know in advance whether it should create a syncgroup
+or join an existing syncgroup. For example, this can happen when an app uses a
+syncgroup to sync a user's data across their devices; in this case, the app
+won't know in advance whether it has already been installed on some other device
+belonging to the user. This implies that the syncgroup name must be known in
+advance by all instances of the app. In this case, the recommended approach is
+to try to join that syncgroup. If the join fails with an error indicating that
+the syncgroup does not exist (ErrNoExist), as opposed to a permission denial or
+a network communication error, then create the syncgroup. This could still lead
+to multiple concurrent creations of the syncgroup. In the future we plan to
+provide a mechanism for apps to merge such disconnected syncgroups when there is
+no ambiguity as to whether they really ought to be the same syncgroup.
+
+## Conflict Resolution
+
+Syncbase was designed to allow for predefined conflict resolution policies such
+as last-write-wins as well as custom, app-driven conflict resolution. The
+Syncbase implementation does not yet expose hooks for custom resolvers;
+last-write-wins is the only resolver currently available.
+
+*TODO: Expand this section once we finish adding support for custom conflict
+resolvers, additional types of predefined resolvers, CRDTs, etc.*
+
+*TODO: Maybe add some info about schemas here.*
+
+## Interaction with ACLs
+
+*TODO: Fill this out.*
+
+# Frequently Asked Questions
+
+*TODO: Grow this section as questions arise.*
+
+[Syncbase Overview]: ../concepts/syncbase-overview.md
+[installation instructions]: ../installation.md
+[syncQL]: syncql-tutorial.md
+[VOM]: ../concepts/rpc.md#vom
+[VDL]: ../concepts/rpc.md#vdl
+[Vanadium security model]: ../concepts/security.md
+[todos demo app]: https://github.com/vanadium/todos
+[Vanadium Chrome extension]: ../tools/vanadium-chrome-extension.md