-
Notifications
You must be signed in to change notification settings - Fork 38
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'main' into igor/bug1133
- Loading branch information
Showing
31 changed files
with
12,593 additions
and
12,187 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,18 @@ | ||
| # Emacs support | ||
|
|
||
| We have 2 packages for enabling support for Quint in Emacs. | ||
|
|
||
| 1. `quint-mode` is a major mode that enables simple syntax highlighting | ||
| 2. `lsp-quint` is a client for `lsp-mode`, enabling IDE features provided by `quint-language-server` | ||
|
|
||
| These packages are not published anywhere for the moment. You can clone this git repo and add a configuration like the following (which uses `use-package`): | ||
|
|
||
| ```elisp | ||
| (load-file "<path-to-quint-repo>/editor-plugins/emacs/quint-mode.el") | ||
| (load-file "<path-to-quint-repo>/editor-plugins/emacs/lsp-quint.el") | ||
| (require 'quint-mode) | ||
| (add-to-list 'auto-mode-alist '("\\.qnt" . quint-mode)) | ||
| (use-package lsp-quint | ||
| :ensure t | ||
| :hook (quint-mode . lsp)) | ||
| ``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,56 @@ | ||
| ;;; lsp-quint.el --- Quint LSP Client settings | ||
| ;;; | ||
| ;; Copyright (C) 2023 Gabriela Moreira | ||
|
|
||
| ;; Author: Gabriela Moreira ([email protected]) | ||
| ;; URL: https://github.com/informalsystems/quint | ||
| ;; Version: 1.0.0 | ||
| ;; Created: 28 Aug 2023 | ||
| ;; Updated 21 Aug 2023 | ||
| ;; Keywords: languages | ||
|
|
||
| ;; This file is not part of GNU Emacs. | ||
|
|
||
| ;;; Commentary: | ||
|
|
||
| ;; A client for lsp-mode for the Quint Specification Language, using the quint language server. | ||
|
|
||
| ;;; Code: | ||
|
|
||
| (require 'lsp-mode) | ||
| (require 'lsp-completion) | ||
|
|
||
| (defgroup lsp-quint nil | ||
| "LSP support for the Quint Specification Language, using the quint language server." | ||
| :link '(url-link "https://github.com/informalsystems/quint") | ||
| :group 'lsp-mode | ||
| :package-version '(lsp-mode . "6.3.2")) | ||
|
|
||
| (lsp-dependency 'quint-language-server | ||
| '(:system "quint-language-server") | ||
| '(:npm :package "@informalsystems/quint-language-server" | ||
| :path "quint-language-server")) | ||
|
|
||
| (add-to-list 'lsp-language-id-configuration '(quint-mode . "quint")) | ||
| (lsp-register-client | ||
| (make-lsp-client :new-connection (lsp-stdio-connection | ||
| (lambda () (list (lsp-package-path 'quint-language-server) "--stdio"))) | ||
| :major-modes '(quint-mode) | ||
| :activation-fn (lsp-activate-on "quint") | ||
| :language-id "quint" | ||
| :priority 0 | ||
| :server-id 'quint-language-server | ||
| :completion-in-comments? t | ||
| :download-server-fn (lambda (_client callback error-callback _update?) | ||
| (lsp-package-ensure | ||
| 'quint-language-server | ||
| (-partial #'lsp-package-ensure | ||
| 'quint-language-server | ||
| callback | ||
| error-callback) | ||
| error-callback)))) | ||
|
|
||
| (lsp-consistency-check lsp-quint) | ||
|
|
||
| (provide 'lsp-quint) | ||
| ;;; lsp-quint.el ends here |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,90 @@ | ||
| /** | ||
| * The module `hashes` provides the standard means of hashing byte sequences in | ||
| * Quint. A direct implementation of a hash (e.g., of SHA256) in Quint would | ||
| * produce plenty of hard-to-solve arithmetic constraints in a Quint | ||
| * specification. To this end, we introduce a different specification of a hash | ||
| * that has the following important properties: | ||
| * | ||
| * 1. For two sequences of bytes `bs1` and `bs2`, it holds that `bs1 == bs2` if | ||
| * and only if `hash(bs1) == hash(bs2)`. That is, our hash is perfect, it does | ||
| * not produce any collisions. | ||
| * | ||
| * 2. Hashes can be nested, e.g., `hash(hash(bs1).hconcat(bs2))`. Nested hashes | ||
| * preserve the property (1). | ||
| * | ||
| * 3. The operator `hlen` computes the length of byte sequences, some of | ||
| * which may have been computed via `hash`. | ||
| * | ||
| * 4. Plain text byte sequences and hashes may be concatenated via `hconcat`. | ||
| * | ||
| * Importantly, this modeling does not guarantee that a byte sequence would look | ||
| * exactly the same, as if it was computed via a real hash implementation. | ||
| * We will introduce integration with actual hash implementations later. | ||
| * | ||
| * Igor Konnov, Informal Systems, 2023. | ||
| */ | ||
| module hashes { | ||
| /// the length of a hashed sequence in bytes, e.g., 32 for SHA-256. | ||
| const HASH_LEN: int | ||
|
|
||
| /// A data structure that carries plain texts and hashed texts. | ||
| /// We could simply use `List[int]`, but a designated type indicates that | ||
| /// the user should not look inside. | ||
| type HMessage = { | ||
| _bytes: List[int] | ||
| } | ||
|
|
||
| /// Construct HText from plain text, that is, a list of bytes. | ||
| /// | ||
| /// @param bytes the input to wrap, all list elements shall be in the range | ||
| /// of [0, 255]. | ||
| /// @returns the HMessage representation of bytes | ||
| pure def hplain(bytes: List[int]): HMessage = { | ||
| { _bytes: bytes } | ||
| } | ||
|
|
||
| /// Concatenate two messages, possibly hashed. | ||
| /// | ||
| /// @param first the first message | ||
| /// @param second the second message | ||
| /// @returns new message, in which `second` follows `first`. | ||
| pure def hconcat(first: HMessage, second: HMessage): HMessage = { | ||
| { _bytes: first._bytes.concat(second._bytes) } | ||
| } | ||
|
|
||
| /// Hash a sequence of bytes, some of which may have been hashed already. | ||
| /// | ||
| /// @param input the input to hash | ||
| /// @returns the hashed sequence of bytes | ||
| pure def hash(input: HMessage): HMessage = { | ||
| // We simply wrap the whole sequence of bytes with two markers -1. | ||
| // Since some parts of the input may have been hashed already, we decrease | ||
| // the hash markers in `input._bytes` first. | ||
| pure val decreased: List[int] = input._bytes.foldl([], | ||
| (l, b) => l.append(if (b >= 0) b else (b - 1)) | ||
| ) | ||
| // wrap with the markers -1 | ||
| { _bytes: [-1].concat(decreased).append(-1) } | ||
| } | ||
|
|
||
| /// Compute the length of a message that may contain hashes or just plain text | ||
| /// | ||
| /// @param input the input to calculate the length of | ||
| /// @returns the length of the sequence | ||
| pure def hlen(input: HMessage): int = { | ||
| input._bytes.foldl((0, false), | ||
| (p, b) => | ||
| if (b == -1) { | ||
| val newLen = p._1 + if (p._2) HASH_LEN else 0 // We add the total hash length at the terminator | ||
| (newLen, not(p._2)) // toggle the "in hash" flag | ||
| } else { | ||
| val newLen = p._1 + if (p._2) 0 else 1 // if in hash, the total hash length gets added in the terminator | ||
| (newLen, p._2) | ||
| } | ||
| )._1 | ||
| } | ||
| } | ||
|
|
||
| module sha256 { | ||
| import hashes(HASH_LEN = 32).* | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,37 @@ | ||
| module hashesTest { | ||
| import hashes(HASH_LEN = 32).* from "./hashes" | ||
|
|
||
| pure def hplainTest = and { | ||
| assert(hplain([ 2, 3, 4 ]) == hplain([ 2, 3, 4 ])), | ||
| assert(hplain([ 2, 3, 4 ]) != hplain([ 3, 4, 5 ])), | ||
| } | ||
|
|
||
| pure def hashTest = and { | ||
| assert(hash(hplain([ 2, 3, 4 ])) == hash(hplain([ 2, 3, 4 ]))), | ||
| assert(hash(hplain([ 2, 3, 4 ])) != hash(hplain([ 3, 4, 5 ]))), | ||
| assert(hash(hplain([ 2, 3, 4 ])) != hplain([ 2, 3, 4 ])), | ||
| assert(hash(hash(hplain([ 2, 3, 4 ]))) != hash(hplain([ 2, 3, 4 ]))), | ||
| } | ||
|
|
||
| pure def hconcatTest = and { | ||
| pure val t234then567 = hplain([ 2, 3, 4 ]).hconcat(hplain([ 5, 6, 7 ])) | ||
| pure val t234567 = hplain([ 2, 3, 4, 5, 6, 7 ]) | ||
| assert(t234then567 == t234567), | ||
| pure val h234then567 = hash(hplain([ 2, 3, 4 ])).hconcat(hplain([ 5, 6, 7 ])) | ||
| assert(h234then567 != hplain([ 2, 3, 4, 5, 6, 7 ])), | ||
| pure def l = | ||
| (hash(hplain([ 2, 3, 4 ])).hconcat(hplain([ 5, 6, 7 ]))).hconcat(hplain([ 8, 9 ])) | ||
| pure def r = | ||
| hash(hplain([ 2, 3, 4 ])).hconcat((hplain([ 5, 6, 7 ])).hconcat(hplain([ 8, 9 ]))) | ||
| assert(l == r), | ||
| } | ||
|
|
||
| pure def hlenTest = and { | ||
| assert(hlen(hash(hplain([ 2, 3, 4 ]))) == 32), | ||
| assert(hlen(hash(hash(hplain([ 2, 3, 4 ])))) == 32), | ||
| assert(hlen(hplain([ 2, 3, 4, 5, 6, 7 ])) == 6), | ||
| pure def l = | ||
| (hash(hplain([ 2, 3, 4 ])).hconcat(hplain([ 5, 6, 7 ]))).hconcat(hplain([ 8, 9 ])) | ||
| assert(hlen(l) == 37) | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.