Don't tag encoded expressions with their hash (#362)

Fixes #335

The binary representation of Dhall expressions no longer includes the
version string, which enables hash stability across standard version
changes.

This implies that changes to the language standard should take care to avoid
reusing the same encoding to mean different things over time.  This also
implies that interpreters will need to make a greater effort to anticipate
likely decoding failures for older expressions and provide helpful
error messages.

standard/binary.md

@@ -44,8 +44,6 @@ expressions to and from a binary representation
     * [Imports](#imports-1)
     * [`let`-expressions](#let-expressions-1)
     * [Type annotations](#type-annotations-1)
-* [Versioning](#versioning)
-* [Protocol evolution](#protocol-evolution)
 
 ## Motivation
 
@@ -1388,54 +1386,3 @@ Decode a CBOR array beginning with a `25` as a `let` expression:
     decode(t₁) = t₀   decode(T₁) = T₀
     ─────────────────────────────────────────
     decode([ 26, t₁, T₁ ]) = t₀ : T₀
-
-
-## Versioning
-
-You can find versioning information in the following separate document:
-
-* [Versioning](./versioning.md)
-
-In particular, that document contains the `currentVersion` judgment referenced
-in this section.
-
-You can encode a Dhall expression tagged with a version string using the
-following judgment:
-
-    encodeWithVersion(dhall) = cbor
-
-... where:
-
-* `dhall` (the input) is a Dhall expression
-* `cbor` (the output) is a CBOR expression
-
-You can decode a Dhall expression tagged with a version string using
-the following judgment:
-
-    decodeWithVersion(cbor) = dhall
-
-... where:
-
-* `dhall` (the input) is a Dhall expression
-* `cbor` (the output) is a CBOR expression
-
-`encodeWithVersion` and `decodeWithVersion` are both a wrappers around `encode`
-and `decode` that include/expect the current version tag, respectively:
-
-    currentVersion = v   encode(e₀) = e₁
-    ────────────────────────────────────
-    encodeWithVersion(e₀) = [ v, e₁ ]
-
-
-    currentVersion = v   decode(e₀) = e₁
-    ────────────────────────────────────
-    decodeWithVersion([ v, e₁ ]) = e₀
-
-The version string format might change in the future.  For example, at some
-point the version string might become a URI or a SHA256 hash.  Therefore,
-implementations MUST only match on the exact version string when
-implementing `decodeWithVersion`.  In particular, implementations MUST NOT match
-a prefix of the version string, MUST NOT attempt to parse the version string as
-a more structured version number, and MUST NOT attempt to interpret the version
-string in any way other than to test the string for exactly equality with the
-expected version string for the currently enabled version.

standard/semantics.md

@@ -4991,8 +4991,8 @@ expression protected by a semantic integrity check:
   `"${XDG_CACHE_HOME}/dhall/${base16Hash}"` or
   `"${HOME}/.cache/dhall/${base16Hash}"`
 * If the file exists and is readable, verify the file's byte contents match the
-  hash and then decode the expression from the bytes using the
-  `decodeWithVersion` judgment instead of importing the expression
+  hash and then decode the expression from the bytes using the `decode` judgment
+  instead of importing the expression
 * Otherwise, import the expression as normal
 
 An implementation MUST fail and alert the user if hash verification fails,
@@ -5005,15 +5005,15 @@ Or in judgment form:
     Γ("${XDG_CACHE_HOME}/dhall/${base16Hash}") = binary
     sha256(binary) = byteHash
     base16Encode(byteHash) = base16Hash                  ; Verify the hash
-    decodeWithVersion(binary) = e
+    decode(binary) = e
     ───────────────────────────────────────────────────  ; Import is already cached under `$XDG_CACHE_HOME`
     Δ × Γ ⊢ import₀ sha256:base16Hash @ here ⇒ e ⊢ Γ
 
 
     Γ("${HOME}/.cache/dhall/${base16Hash}") = binary
     sha256(binary) = byteHash
     base16Encode(byteHash) = base16Hash                  ; Verify the hash
-    decodeWithVersion(binary) = e
+    decode(binary) = e
     ───────────────────────────────────────────────────  ; Otherwise, import is cached under `$HOME`
     Δ × Γ ⊢ import₀ sha256:base16Hash @ here ⇒ e ⊢ Γ
 
@@ -5022,7 +5022,7 @@ Or in judgment form:
     ε ⊢ e₁ : T
     e₁ ⇥ e₂
     e₂ ↦ e₃
-    encode-1.0(e₃) = binary
+    encode(e₃) = binary
     sha256(binary) = byteHash
     base16Encode(byteHash) = base16Hash  ; Verify the hash
     ─────────────────────────────────────────────────────────────────────────────────────────────────────  ; Import is not cached, try to save under `$XDG_CACHE_HOME`
@@ -5033,7 +5033,7 @@ Or in judgment form:
     ε ⊢ e₁ : T
     e₁ ⇥ e₂
     e₂ ↦ e₃
-    encode-1.0(e₃) = binary
+    encode(e₃) = binary
     sha256(binary) = byteHash
     base16Encode(byteHash) = base16Hash  ; Verify the hash
     ──────────────────────────────────────────────────────────────────────────────────────────────────  ; Otherwise, try `HOME`
@@ -5044,7 +5044,7 @@ Or in judgment form:
     ε ⊢ e₁ : T
     e₁ ⇥ e₂
     e₂ ↦ e₃
-    encode-1.0(e₃) = binary
+    encode(e₃) = binary
     sha256(binary) = byteHash
     base16Encode(byteHash) = base16Hash                 ; Verify the hash
     ─────────────────────────────────────────────────── ; Otherwise, don't cache

standard/versioning.md

@@ -15,7 +15,6 @@ The current version string is:
 This version string is used by implementations to:
 
 * identify which release(s) of the standard they comply with
-* tag encoded Dhall expressions in their binary representation
 
 ## What is a "version"
 
@@ -71,13 +70,6 @@ are `Natural` numbers:
 
     Example: a change in the documentation or renaming terminals in the grammar
 
-All three changes require users to update their semantic integrity checks if
-they upgrade since the entire version string is an input to the hash in a
-semantic integrity check.  Implementations SHOULD support older versions of the
-standard that match in the first version component so that users can defer
-upgrading their code until they are ready to regenerate their semantic
-integrity checks.
-
 This versioning scheme is only a convention that provides humans a convenient
 mnemonic for tracking releases.  The version number selected for a release could
 be incorrect and the release process only guarantees a best effort attempt to
@@ -111,21 +103,8 @@ specified in that release of the standard.  An implementation MUST NOT mix and
 match functionality from different releases of the standard within any given
 run.
 
-For example, suppose that version "2.0.0" of the implementation imported an
-expression protected by a semantic integrity check:
-
-    ./example.dhall sha256:bb1e096305428d2e155282d156ddec47cca75cd61bc0ef1aa6ce4cf5eae91e38
-
-... and that expression was cached underneath
-`~/.cache/dhall/bb1e096305428d2e155282d156ddec47cca75cd61bc0ef1aa6ce4cf5eae91e38`
-tagged with version "2.0.0".  Now suppose that an interpreter upgraded and
-supported both versions "2.0.0" and "2.1.0" of the standard.  If the
-interpreter enabled version "2.1.0" of the standard then the interpreter would
-not be allowed to import the above expression (even though version "2.1.0" might
-be otherwise backwards compatible with "2.0.0").  If the interpreter enabled
-version "2.0.0" of the standard then the import would succeed, but that
-expression (and the rest of the program) would be type-checked and normalized as
-using only version "2.0.0" of the standard.
+For example, if the file `./foo.dhall` imports `./bar.dhall`, then both files
+must be interpreted using the same version of the standard.
 
 ## Standard evolution
 

tests/import/success/fieldOrderA.dhall

@@ -1,5 +1,5 @@
 { example0 =
-    ../data/fieldOrder/1.dhall sha256:261b3aca810973f81175d19b16226aaa5e76df7ea51c5d45e890dd6cdc49abbd
+    ../data/fieldOrder/1.dhall sha256:d8ae15ff5a40ee7973a23ba75cd98f8e39d14aeb6e1e3f18aadb092fcb825194
 , example1 =
-    ../data/fieldOrder/2.dhall sha256:261b3aca810973f81175d19b16226aaa5e76df7ea51c5d45e890dd6cdc49abbd
+    ../data/fieldOrder/2.dhall sha256:d8ae15ff5a40ee7973a23ba75cd98f8e39d14aeb6e1e3f18aadb092fcb825194
 }

tests/import/success/issue553B.dhall

@@ -1 +1 @@
-./issue553A.dhall sha256:250873549ddd262f27f3b197b2a2631fb569e7bdfe12446fc0912b4a2359a83e
+./issue553A.dhall sha256:010fac8c3ce6a9a428ee41e206d956d7607b1a0d7a042172464b1f447f76bf0d