Document not found (404)
+This URL is invalid, sorry. Please use the navigation bar or search to continue.
+ +
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/src/developers/hacspec_architecture.png b/archive/developers/hacspec_architecture.png
similarity index 100%
rename from archive/src/developers/hacspec_architecture.png
rename to archive/developers/hacspec_architecture.png
diff --git a/archive/developers/index.html b/archive/developers/index.html
new file mode 100644
index 0000000..5f1ae13
--- /dev/null
+++ b/archive/developers/index.html
@@ -0,0 +1,232 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Working on the compiler
+High-level architecture
+
The Rustspec compiler intervenes after the regular Rust typechecking, +by translating the Rust AST into a stricter hacspec AST, +yielding error messages if you're not in the subset.
+The hacspec AST then undergoes a typechecking phase that replicates the +formal typechecking judgment of hacspec, before being compiled +to the proof backends like F* or Coq.
+Code organization
+The source code for the compiler is located in the language/ folder.
+main.rs is the file containing the driver for the different compiler
+passes.
Hacspec AST
+The main file of the compiler is rustspec.rs and it contains the AST
+structure.
Types are usually enclosed into Spanned<...> blocks that attach a location
+information to an AST node, thereby providing a way to display beautiful error
+message.
Several nodes also contain a Fillable<...> node standing for information
+that is filled by the typechecking phase but that can be left to None when
+building the AST.
Translation from Rust AST
+This phase is contained in ast_to_rustspec.rs. The trickyness of this
+translation is that it needs to be aware of certain special names contained
+in the structure SpecialNames. Indeed, while the Rust AST treats the application
+enum constructors like function applications, the hacspec AST considers them as
+proper injection so we need to distinguish them in the Rust AST. For that, we
+need to know all declared enums at this point of the program.
Enums and other SpecialNames are also defined in the ExternalData that
+contains the signatures and types imported in crates used by the hacspec
+program being compiled.
Name resolution
+When the translation from Rust AST is finished, the identifiers for all +variables inside function bodies are of the following type:
+pub enum Ident {
+ Unresolved(String),
+ Local(LocalIdent),
+ TopLevel(TopLevelIdent),
+}More precisely, they are still in the Ident::Unresolved case. The compiler
+pass in name_resolution.rs resolves the identifiers by linking them to local or global identifiers,
+each one having a unique ID. hacspec does not feature De Bruijn variable
+handling, instead relying on unique fresh IDs for differentiating local
+and global variables from each other.
External data
+A hacspec file can never (in principal) be considered alone, as it usually imports +at least several other crates like the hacspec standard library. These external +crates must pre-populate the typechecking context with the types and function +signatures that they define.
+It's the job of hir_to_rustspec.rs to retrieve this data. The critical
+piece of code in this file is the following:
let num_def_ids = crate_store.num_def_ids_untracked(*krate_num);
+let def_ids = (0..num_def_ids).into_iter().map(|id| DefId {
+ krate: *krate_num,
+ index: DefIndex::from_usize(id),
+});First, we retrieve the number of exported symbols by an external crate using
+num_def_ids_untracked, a function that is specifically labeled
+as critical to the hacspec compiler in the Rust compiler codebase. Then,
+we manufacture definition IDs for all these exported symbols, relying on the
+invariant that they are numbered from 0 to the number of exported symbols
+in Rust's compiled crate metadata format.
Then, we use those definition IDs (DefId) to query the Rust compiler
+via the central TyCtxt
+data structure. If the DefId corresponds to a type definition, we examine the
+type definition structurally and check whether it corresponds to a hacspec-compatible
+type definition. Notably, the type definitions generated by macros like array!
+or nat_mod! are only seen here in their expanded version, so we have to retro-engineer
+which expanded version corresponds to which macro expansion. This is a vulnerability
+of the compiler since it's possible to break the abstraction of the language
+by smuggling in a type not defined via a hacspec macro this way. That's why hacspec
+developers should be very careful about which dependencies they import in order
+to have a 100% safety guarantee.
For DefIds corresponding to functions, the signature of the function is analysed
+and if it fits the subset of types expected by hacspec, the function is imported
+along with its type in a pre-populated typechecking context.
Note that it is not possible any more at this point to retrieve the #[in_hacspec],
+#[unsafe_hacspec], etc. attributes that would tag the external definitions,
+since these attributes get erased by the Rust compiler before reaching the
+compiled crates metadata.
Typechecking
+The typechecking is done in typechecker.rs and follows a very regular structure,
+making heavy use of immutable data structures to not mess up the various
+context manipulations.
Note that we need to perform a full typechecking complete with method resolution +because the proof backends need very fine-grained typechecking information +to generate correct code.
+Be careful: types often need to be de-aliased with dealias_type before
+being matched on structurally. Forgetting to dealias will lead to bugs with
+type aliases.
Proof backends
+The different proof backends (rustspec_to_fstar.rs, etc) all enjoy a similar
+structure that ought to be refactored to showcase their commonality. The backends
+don't use an intermediate AST to generate the code in the proof assistant but
+rather directly print code as string using the pretty
+pretty-printing library. If you want to start a new proof backend, the easiest
+solution is probably to copy an existing proof backend and tweak it until
+you get the right result.
The code generation has to be fine-tuned to interface with a replica of the +hacspec standard library in the host proof assistant, whose correspondence with +the original hacspec library in Rust is part of the trusted code base. More specially, +clever solutions to encode sequences and array, as well as all the different types +of public and secret machine integers, and the interaction between the two +(seeing a double as a string of bytes) have to be implemented through proof +assistant libraries.
+Unit tests
+The compiler has various unit tests that are controlled trough the language/tests
+files. Please enrich the unit tests bases in language-tests,
+negative-language-tests and test-crate as you implement new features for
+the compiler. The compiler can also be tested against all the hacspec cryptographic
+specifications by running examples/typecheck_examples.sh from the root of
+the repository.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/elasticlunr.min.js b/archive/elasticlunr.min.js
new file mode 100644
index 0000000..94b20dd
--- /dev/null
+++ b/archive/elasticlunr.min.js
@@ -0,0 +1,10 @@
+/**
+ * elasticlunr - http://weixsong.github.io
+ * Lightweight full-text search engine in Javascript for browser search and offline search. - 0.9.5
+ *
+ * Copyright (C) 2017 Oliver Nightingale
+ * Copyright (C) 2017 Wei Song
+ * MIT Licensed
+ * @license
+ */
+!function(){function e(e){if(null===e||"object"!=typeof e)return e;var t=e.constructor();for(var n in e)e.hasOwnProperty(n)&&(t[n]=e[n]);return t}var t=function(e){var n=new t.Index;return n.pipeline.add(t.trimmer,t.stopWordFilter,t.stemmer),e&&e.call(n,n),n};t.version="0.9.5",lunr=t,t.utils={},t.utils.warn=function(e){return function(t){e.console&&console.warn&&console.warn(t)}}(this),t.utils.toString=function(e){return void 0===e||null===e?"":e.toString()},t.EventEmitter=function(){this.events={}},t.EventEmitter.prototype.addListener=function(){var e=Array.prototype.slice.call(arguments),t=e.pop(),n=e;if("function"!=typeof t)throw new TypeError("last argument must be a function");n.forEach(function(e){this.hasHandler(e)||(this.events[e]=[]),this.events[e].push(t)},this)},t.EventEmitter.prototype.removeListener=function(e,t){if(this.hasHandler(e)){var n=this.events[e].indexOf(t);-1!==n&&(this.events[e].splice(n,1),0==this.events[e].length&&delete this.events[e])}},t.EventEmitter.prototype.emit=function(e){if(this.hasHandler(e)){var t=Array.prototype.slice.call(arguments,1);this.events[e].forEach(function(e){e.apply(void 0,t)},this)}},t.EventEmitter.prototype.hasHandler=function(e){return e in this.events},t.tokenizer=function(e){if(!arguments.length||null===e||void 0===e)return[];if(Array.isArray(e)){var n=e.filter(function(e){return null===e||void 0===e?!1:!0});n=n.map(function(e){return t.utils.toString(e).toLowerCase()});var i=[];return n.forEach(function(e){var n=e.split(t.tokenizer.seperator);i=i.concat(n)},this),i}return e.toString().trim().toLowerCase().split(t.tokenizer.seperator)},t.tokenizer.defaultSeperator=/[\s\-]+/,t.tokenizer.seperator=t.tokenizer.defaultSeperator,t.tokenizer.setSeperator=function(e){null!==e&&void 0!==e&&"object"==typeof e&&(t.tokenizer.seperator=e)},t.tokenizer.resetSeperator=function(){t.tokenizer.seperator=t.tokenizer.defaultSeperator},t.tokenizer.getSeperator=function(){return t.tokenizer.seperator},t.Pipeline=function(){this._queue=[]},t.Pipeline.registeredFunctions={},t.Pipeline.registerFunction=function(e,n){n in t.Pipeline.registeredFunctions&&t.utils.warn("Overwriting existing registered function: "+n),e.label=n,t.Pipeline.registeredFunctions[n]=e},t.Pipeline.getRegisteredFunction=function(e){return e in t.Pipeline.registeredFunctions!=!0?null:t.Pipeline.registeredFunctions[e]},t.Pipeline.warnIfFunctionNotRegistered=function(e){var n=e.label&&e.label in this.registeredFunctions;n||t.utils.warn("Function is not registered with pipeline. This may cause problems when serialising the index.\n",e)},t.Pipeline.load=function(e){var n=new t.Pipeline;return e.forEach(function(e){var i=t.Pipeline.getRegisteredFunction(e);if(!i)throw new Error("Cannot load un-registered function: "+e);n.add(i)}),n},t.Pipeline.prototype.add=function(){var e=Array.prototype.slice.call(arguments);e.forEach(function(e){t.Pipeline.warnIfFunctionNotRegistered(e),this._queue.push(e)},this)},t.Pipeline.prototype.after=function(e,n){t.Pipeline.warnIfFunctionNotRegistered(n);var i=this._queue.indexOf(e);if(-1===i)throw new Error("Cannot find existingFn");this._queue.splice(i+1,0,n)},t.Pipeline.prototype.before=function(e,n){t.Pipeline.warnIfFunctionNotRegistered(n);var i=this._queue.indexOf(e);if(-1===i)throw new Error("Cannot find existingFn");this._queue.splice(i,0,n)},t.Pipeline.prototype.remove=function(e){var t=this._queue.indexOf(e);-1!==t&&this._queue.splice(t,1)},t.Pipeline.prototype.run=function(e){for(var t=[],n=e.length,i=this._queue.length,o=0;n>o;o++){for(var r=e[o],s=0;i>s&&(r=this._queue[s](r,o,e),void 0!==r&&null!==r);s++);void 0!==r&&null!==r&&t.push(r)}return t},t.Pipeline.prototype.reset=function(){this._queue=[]},t.Pipeline.prototype.get=function(){return this._queue},t.Pipeline.prototype.toJSON=function(){return this._queue.map(function(e){return t.Pipeline.warnIfFunctionNotRegistered(e),e.label})},t.Index=function(){this._fields=[],this._ref="id",this.pipeline=new t.Pipeline,this.documentStore=new t.DocumentStore,this.index={},this.eventEmitter=new t.EventEmitter,this._idfCache={},this.on("add","remove","update",function(){this._idfCache={}}.bind(this))},t.Index.prototype.on=function(){var e=Array.prototype.slice.call(arguments);return this.eventEmitter.addListener.apply(this.eventEmitter,e)},t.Index.prototype.off=function(e,t){return this.eventEmitter.removeListener(e,t)},t.Index.load=function(e){e.version!==t.version&&t.utils.warn("version mismatch: current "+t.version+" importing "+e.version);var n=new this;n._fields=e.fields,n._ref=e.ref,n.documentStore=t.DocumentStore.load(e.documentStore),n.pipeline=t.Pipeline.load(e.pipeline),n.index={};for(var i in e.index)n.index[i]=t.InvertedIndex.load(e.index[i]);return n},t.Index.prototype.addField=function(e){return this._fields.push(e),this.index[e]=new t.InvertedIndex,this},t.Index.prototype.setRef=function(e){return this._ref=e,this},t.Index.prototype.saveDocument=function(e){return this.documentStore=new t.DocumentStore(e),this},t.Index.prototype.addDoc=function(e,n){if(e){var n=void 0===n?!0:n,i=e[this._ref];this.documentStore.addDoc(i,e),this._fields.forEach(function(n){var o=this.pipeline.run(t.tokenizer(e[n]));this.documentStore.addFieldLength(i,n,o.length);var r={};o.forEach(function(e){e in r?r[e]+=1:r[e]=1},this);for(var s in r){var u=r[s];u=Math.sqrt(u),this.index[n].addToken(s,{ref:i,tf:u})}},this),n&&this.eventEmitter.emit("add",e,this)}},t.Index.prototype.removeDocByRef=function(e){if(e&&this.documentStore.isDocStored()!==!1&&this.documentStore.hasDoc(e)){var t=this.documentStore.getDoc(e);this.removeDoc(t,!1)}},t.Index.prototype.removeDoc=function(e,n){if(e){var n=void 0===n?!0:n,i=e[this._ref];this.documentStore.hasDoc(i)&&(this.documentStore.removeDoc(i),this._fields.forEach(function(n){var o=this.pipeline.run(t.tokenizer(e[n]));o.forEach(function(e){this.index[n].removeToken(e,i)},this)},this),n&&this.eventEmitter.emit("remove",e,this))}},t.Index.prototype.updateDoc=function(e,t){var t=void 0===t?!0:t;this.removeDocByRef(e[this._ref],!1),this.addDoc(e,!1),t&&this.eventEmitter.emit("update",e,this)},t.Index.prototype.idf=function(e,t){var n="@"+t+"/"+e;if(Object.prototype.hasOwnProperty.call(this._idfCache,n))return this._idfCache[n];var i=this.index[t].getDocFreq(e),o=1+Math.log(this.documentStore.length/(i+1));return this._idfCache[n]=o,o},t.Index.prototype.getFields=function(){return this._fields.slice()},t.Index.prototype.search=function(e,n){if(!e)return[];e="string"==typeof e?{any:e}:JSON.parse(JSON.stringify(e));var i=null;null!=n&&(i=JSON.stringify(n));for(var o=new t.Configuration(i,this.getFields()).get(),r={},s=Object.keys(e),u=0;u
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ For Developers
+This section contains a handy guide for hacspec developers working on the +standard library or the compiler.
+ +
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/theme/favicon.png b/archive/favicon.png
similarity index 100%
rename from theme/favicon.png
rename to archive/favicon.png
diff --git a/theme/favicon.svg b/archive/favicon.svg
similarity index 100%
rename from theme/favicon.svg
rename to archive/favicon.svg
diff --git a/theme/fonts/OPEN-SANS-LICENSE.txt b/archive/fonts/OPEN-SANS-LICENSE.txt
similarity index 100%
rename from theme/fonts/OPEN-SANS-LICENSE.txt
rename to archive/fonts/OPEN-SANS-LICENSE.txt
diff --git a/theme/fonts/SOURCE-CODE-PRO-LICENSE.txt b/archive/fonts/SOURCE-CODE-PRO-LICENSE.txt
similarity index 100%
rename from theme/fonts/SOURCE-CODE-PRO-LICENSE.txt
rename to archive/fonts/SOURCE-CODE-PRO-LICENSE.txt
diff --git a/theme/fonts/fonts.css b/archive/fonts/fonts.css
similarity index 100%
rename from theme/fonts/fonts.css
rename to archive/fonts/fonts.css
diff --git a/theme/fonts/open-sans-v17-all-charsets-300.woff2 b/archive/fonts/open-sans-v17-all-charsets-300.woff2
similarity index 100%
rename from theme/fonts/open-sans-v17-all-charsets-300.woff2
rename to archive/fonts/open-sans-v17-all-charsets-300.woff2
diff --git a/theme/fonts/open-sans-v17-all-charsets-300italic.woff2 b/archive/fonts/open-sans-v17-all-charsets-300italic.woff2
similarity index 100%
rename from theme/fonts/open-sans-v17-all-charsets-300italic.woff2
rename to archive/fonts/open-sans-v17-all-charsets-300italic.woff2
diff --git a/theme/fonts/open-sans-v17-all-charsets-600.woff2 b/archive/fonts/open-sans-v17-all-charsets-600.woff2
similarity index 100%
rename from theme/fonts/open-sans-v17-all-charsets-600.woff2
rename to archive/fonts/open-sans-v17-all-charsets-600.woff2
diff --git a/theme/fonts/open-sans-v17-all-charsets-600italic.woff2 b/archive/fonts/open-sans-v17-all-charsets-600italic.woff2
similarity index 100%
rename from theme/fonts/open-sans-v17-all-charsets-600italic.woff2
rename to archive/fonts/open-sans-v17-all-charsets-600italic.woff2
diff --git a/theme/fonts/open-sans-v17-all-charsets-700.woff2 b/archive/fonts/open-sans-v17-all-charsets-700.woff2
similarity index 100%
rename from theme/fonts/open-sans-v17-all-charsets-700.woff2
rename to archive/fonts/open-sans-v17-all-charsets-700.woff2
diff --git a/theme/fonts/open-sans-v17-all-charsets-700italic.woff2 b/archive/fonts/open-sans-v17-all-charsets-700italic.woff2
similarity index 100%
rename from theme/fonts/open-sans-v17-all-charsets-700italic.woff2
rename to archive/fonts/open-sans-v17-all-charsets-700italic.woff2
diff --git a/theme/fonts/open-sans-v17-all-charsets-800.woff2 b/archive/fonts/open-sans-v17-all-charsets-800.woff2
similarity index 100%
rename from theme/fonts/open-sans-v17-all-charsets-800.woff2
rename to archive/fonts/open-sans-v17-all-charsets-800.woff2
diff --git a/theme/fonts/open-sans-v17-all-charsets-800italic.woff2 b/archive/fonts/open-sans-v17-all-charsets-800italic.woff2
similarity index 100%
rename from theme/fonts/open-sans-v17-all-charsets-800italic.woff2
rename to archive/fonts/open-sans-v17-all-charsets-800italic.woff2
diff --git a/theme/fonts/open-sans-v17-all-charsets-italic.woff2 b/archive/fonts/open-sans-v17-all-charsets-italic.woff2
similarity index 100%
rename from theme/fonts/open-sans-v17-all-charsets-italic.woff2
rename to archive/fonts/open-sans-v17-all-charsets-italic.woff2
diff --git a/theme/fonts/open-sans-v17-all-charsets-regular.woff2 b/archive/fonts/open-sans-v17-all-charsets-regular.woff2
similarity index 100%
rename from theme/fonts/open-sans-v17-all-charsets-regular.woff2
rename to archive/fonts/open-sans-v17-all-charsets-regular.woff2
diff --git a/theme/fonts/source-code-pro-v11-all-charsets-500.woff2 b/archive/fonts/source-code-pro-v11-all-charsets-500.woff2
similarity index 100%
rename from theme/fonts/source-code-pro-v11-all-charsets-500.woff2
rename to archive/fonts/source-code-pro-v11-all-charsets-500.woff2
diff --git a/theme/highlight.css b/archive/highlight.css
similarity index 100%
rename from theme/highlight.css
rename to archive/highlight.css
diff --git a/theme/highlight.jsold b/archive/highlight.js
similarity index 100%
rename from theme/highlight.jsold
rename to archive/highlight.js
diff --git a/archive/index.html b/archive/index.html
new file mode 100644
index 0000000..8ac450e
--- /dev/null
+++ b/archive/index.html
@@ -0,0 +1,243 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Examples
+The main hacspec repository contains a set of example specifications. +In this section we pull out some interesting bits to demonstrate the hacspec +language.
+There's also a provider that bundles the different cryptographic primitives +into a single library. +The provider implements the RustCrypto traits in order to facilitate interoperability.
+ +
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/language/core.html b/archive/language/core.html
new file mode 100644
index 0000000..1d9e2f5
--- /dev/null
+++ b/archive/language/core.html
@@ -0,0 +1,320 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Introduction
+hacspec is a specification language for crypto primitives, protocols, and more. +It is a subset of the Rust programming language, focused on functional +programming and it avoids the use of mutable state as much as possible.
+This book gives an overview of:
+-
+
- The hacspec language; +
- The different parts of the project: + + +
- How to use hacspec to write specifications for standards and verification; +
- How to use hacspec to generate test vectors; +
- Work on the hacspec compiler and tooling itself. +
For a quick introduction you can also check out these slides from April 2021. +An in-depth technical report is also available, and serves as a reference +for the language formalization.
+ +
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/language/enums.html b/archive/language/enums.html
new file mode 100644
index 0000000..93be503
--- /dev/null
+++ b/archive/language/enums.html
@@ -0,0 +1,269 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ The core of hacspec
+Crates and modules
+hacspec only supports single-module crates, due to a technical limitation +of the Rust compiler. Inside this single file, a hacspec program shall always +start with:
+use hacspec_lib::*;
+
+// Optional: dependencies on other crates containing hacspec programs
+use other_hacpsec_crate::*;No other form of use is allowed in hacspec, because allowing Rust's
+complex import patterns would increase the complexity of the hacspec compiler
+and conflict with the module systems of most proof assistants.
Functions
+hacspec is a functional language, and only supports the declaration of +top-level functions:
+fn hacspec_function(x: bool) -> () {
+ ...
+}The functions can take any number of arguments, and may return a value (or not). +Note that recursive functions are forbidden in hacspec.
+The control flow inside hacspec functions is limited, as return statements
+are forbidden.
Basic Types
+hacspec supports all the Rust primitive types: integers (signed and unsigned), +booleans, unit, tuples. hacspec possesses some support for generic +types, but only for primitive types defined by the language creators, and +not for user-defined types.
+Type aliases are allowed in hacspec:
+type OneTypeAlias = u32;Borrows
+hacspec forbids mutable borrows in all places. Immutable borrows are allowed +in hacspec, but only for function arguments. Indeed, you can declare a function +argument as immutably borrowed:
+fn hacspec_function(arg: &Seq<u8>) {
+ ...
+}You can also immutably borrow a value at the call site of a function:
+hacspec_function(&Seq::<u8>::new(64))In particular, return types cannot contain references, and the same is true +for types inside tuples or any data structure.
+Constants
+hacspec allows the declaration of constants:
+const ONE_CONST : bool = false;Assignments
+Inside a function body, hacspec allows regular Rust let-bindings:
+let x = ...;hacspec also allows mutable let bindings, and subsequent reassignments:
+let mut x = ...;
+...
+x = ...;This allowing of mutable variable might come as a contradiction to hacspec's +philosophy of forbidding mutable state. But in fact, mutable local variables in +hacspec can be translated to a completely side-effect free form with a state-passing +like monadic structure.
+Left-hand sides of assignments support destructuring, which is currently the +only way to access the members of a tuple:
+let (x, y) = z;Loops
+Looping is severely restricted in hacspec compared to Rust, as the only accepted form is
+for looping with a counter over an integer range:
for i in low..hi {
+ ... // The block can use i and reassign mutable variables
+}The motivation for this restriction is to ease the proof of termination of
+loops. break or continue statements are forbidden.
Conditionals
+hacspec allows statement-like conditionals as well as expression-like +conditionals:
+if cond1 {
+ ... // the block can modify mutable variables
+} else { // else block is optional here
+ ...
+}
+let x = if cond2 { ... } else { ... };Statements and expressions
+In regular Rust, statements and expressions can be mixed together freely. +This not the case in hacspec that imposes a strict precedence of statements +over expressions. For instance, the following code is not allowed in +hacspec:
+let x = if cond {
+ y = true; // ERROR: the reassignment is a statement, which cannot
+ // be contained in the expression to which x is assigned.
+ 3
+} else {
+ 4
+};Visibility
+hacspec allows for both pub and non-pub versions of item declarations
+(pub, non-pub, etc). You simply have to respect the Rust visibility rules. Note
+that these visibility distinctions might not be translated in the proof
+backends.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/language/errors.html b/archive/language/errors.html
new file mode 100644
index 0000000..861bcf8
--- /dev/null
+++ b/archive/language/errors.html
@@ -0,0 +1,239 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Structs and enums
+hacspec also supports user-defined structs and enums with some restrictions.
+Structs
+The only form of struct declaration currently allowed in hacspec is:
+struct Foo(u32, Seq<u32>);The struct thus declared can have one or more components. This form of struct +declaration effectively corresponds to a single-case enum, and is implemented +as such. Struct components can be accessed through let-binding destructuring:
+let Foo(x, y) = z;Note that you can't store borrowed types inside hacspec structs, hence there is no +need for lifetime variables.
+Enums
+hacspec supports very restricted enum declarations:
enum Foo {
+ CaseA,
+ CaseB(u16),
+ CaseC(Seq<bool>, u64)
+}These declaration don't support the basic Rust features such as C-style +union declarations with assignments for each case.
+Enumeration values can be pattern-matched in an expression:
+match x {
+ Foo::CaseA => ...,
+ Foo::CaseB(y) => ...,
+ Foo::CaseC(y,z) => ...
+}Note that you can't store borrowed types inside hacspec enums, hence there is no +need for lifetime variables.
+Option and Result
+User-defined structs and enums presented above don't support generic type
+parameters yet. However, the built-in enums Option<T> and Result<T,U>
+support type parameters. Those type parameters have to be explicitly declared
+each time, as hacspec does not currently support type inference:
match x {
+ Result::<Seq<u8>, bool>::Ok(y) => ...,
+ Result::<Seq<u8>, bool>::Err(err) => ...
+}Such type parameter declaration is cumbersome; as a workaround we advise +to declare a type alias as such:
+type MyResult = Result::<Seq<u8>, bool>;
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/language/index.html b/archive/language/index.html
new file mode 100644
index 0000000..a56335a
--- /dev/null
+++ b/archive/language/index.html
@@ -0,0 +1,243 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Error handling
+Error handling in Rust is done via the Result type (see the structs and
+enums section). But on top of explicit pattern-matching, hacspec also
+supports the popular ? operator to quickly perform an early return and
+propagate the error case upwards.
? is only allowed at the very end of an expression in a let-binding or
+reassignment statement:
let x = foo(true)?; // GOOD
+let y = foo(bar(0)?); // ERROR: the ? is not at the end of the statementCurrently, ? is the only way to return early in a hacspec function.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/language/seq.html b/archive/language/seq.html
new file mode 100644
index 0000000..637660f
--- /dev/null
+++ b/archive/language/seq.html
@@ -0,0 +1,251 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ The hacspec language
+This section gives an informal description of the hacspec language, whose +goal is to provide hands-on documentation for users of the language. For +a formal specification of the semantics of the language, please refer +to the technical report.
+hacspec is a domain-specific language embedded inside Rust. This means that +all correct hacspec programs are correct Rust programs: you can use +the usual Rust tooling for working on your hacspec developments. However, +hacspec is a strict subset of Rust: this means that some features of Rust +are forbidden inside hacspec. The goal of restricting the expressiveness of +the language is twofold: first, help domain experts such as cryptographers +convey their specifications in a fashion that should help them avoid +mistakes; second, provide a way for Rust programmers to interact with theorem +provers such as F* or Coq.
+ +
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/language/syntax.html b/archive/language/syntax.html
new file mode 100644
index 0000000..1a84bdb
--- /dev/null
+++ b/archive/language/syntax.html
@@ -0,0 +1,285 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Sequences and arrays
+Sequences
+The staple Vec type is forbidden in hacspec. Instead, you have to use the
+type Seq, which is implemented as a wrapper around Vec.
The most notable differences between Seq and Vec is that Seq is not
+resizable, and does not support push and pop operations. Instead, the
+final length of the seq has to be provided at creation time. See the
+hacspec standard library documentation for more details.
Seq is a built-in generic type that always has to be indexed by the content of the
+cells: Seq<u8>, etc.
Arrays
+The native Rust array types [<type of contents>, <size>] is forbidden in
+hacspec. Instead, you have to declare nominally at the top-level new array types
+for a specific cell content and size with:
array!(FooArray, u8, 64);
+// This declares type FooArray as an array of u8 of size 64
+bytes!(BarArray, 64);
+// bytes! is a specialized version of array! with secret bytes
+array!(BazArray, u8, 64, type_for_indexes:BazIndex);
+// The additional argument type_for_indexes defines an alias of usize
+// intended to spot which usizes are used to index BazArray (useful for
+// verification)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/mark.min.js b/archive/mark.min.js
new file mode 100644
index 0000000..1636231
--- /dev/null
+++ b/archive/mark.min.js
@@ -0,0 +1,7 @@
+/*!***************************************************
+* mark.js v8.11.1
+* https://markjs.io/
+* Copyright (c) 2014–2018, Julian Kühnel
+* Released under the MIT license https://git.io/vwTVl
+*****************************************************/
+!function(e,t){"object"==typeof exports&&"undefined"!=typeof module?module.exports=t():"function"==typeof define&&define.amd?define(t):e.Mark=t()}(this,function(){"use strict";var e="function"==typeof Symbol&&"symbol"==typeof Symbol.iterator?function(e){return typeof e}:function(e){return e&&"function"==typeof Symbol&&e.constructor===Symbol&&e!==Symbol.prototype?"symbol":typeof e},t=function(e,t){if(!(e instanceof t))throw new TypeError("Cannot call a class as a function")},n=function(){function e(e,t){for(var n=0;n
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Syntax
+P ::= [i]\* Program items
+i ::= array!(t, μ, n) Array type declaration where n is a natural number
+ | nat_mod!(t, n) Modular integer
+ | fn f([d]+) -> μ b Function declaration
+ | type t = enum { [c(μ)]+ } Enum declaration (with constructors)
+ | type t = struct([μ]+) Struct declaration (without named fields)
+ | const x: μ = e Constant declaration
+ | use crate::* External crate import
+ | use mod::* Internal module import
+d ::= x: τ Function argument
+ | mut x: τ Mutable function argument
+μ ::= unit|bool|u8|U8|i8|I8... Base types
+ | Seq<μ> Sequence
+ | String Strings
+ | ([μ]+) Tuple
+ | unit Unit type
+ | t Named type
+τ ::= μ Plain type
+ | &μ Immutable reference
+b ::= {[s;]+} Block
+p ::= x Variable pattern
+ | ([p]+) Tuple pattern
+ | t (p) Struct constructor pattern
+ | _ Wildcard pattern
+s ::= let p: τ = e Let binding
+ | let mut p: τ = e Mutable let binding
+ | x = e Variable reassignment
+ | x = e? Variable reassignment with result/option catching
+ | let p: τ = e? Let binding with result/option catching
+ | if e then b (else b) Conditional statements
+ | c(e) Enum injection
+ | match e { [c(p) => e]+ } Pattern matching
+ | for x in e..e b For loop (integers only)
+ | e Return expression
+ | b Statement block
+e ::= ()|true|false Unit and boolean literals
+ | n Integer literal
+ | U8(e)|I8(e)|... Secret integer classification
+ | "..." String literal
+ | t([e]+) Array literal
+ | e as μ Integer casting
+ | x Variable
+ | () Unit
+ | f([a]+) Function call
+ | if e then e else e Conditional expression
+ | e ⊙ e Binary operations
+ | ⊘ e Unary operations
+ | ([e]+) Tuple constructor
+ | x[e] Array or sequence index
+a ::= e Linear argument
+ | &e Call-site borrowing
+⊙ ::= + | - | * | / | &&
+ | || | == | != | > | <
+⊘ ::= - | ~
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/print.html b/archive/print.html
new file mode 100644
index 0000000..084422a
--- /dev/null
+++ b/archive/print.html
@@ -0,0 +1,789 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Contributors
+A list of contributors to the hacspec project.
+-
+
- Franziskus Kiefer (franziskuskiefer) +
- Denis Merigoux (denismerigoux) +
- Karthik Bhargavan +
- Tomer Yavor (TomerHawk) +
- Tanmay Garg (tanmay2004) +
- Peter Schwabe (cryptojedi) +
- Kaspar Schleiser (kaspar030) +
- Kasserne +
- Tony Arcieri (tarcieri) +
If you feel you're missing from this list, feel free to add yourself in a PR.
+ +
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/searcher.js b/archive/searcher.js
new file mode 100644
index 0000000..dc03e0a
--- /dev/null
+++ b/archive/searcher.js
@@ -0,0 +1,483 @@
+"use strict";
+window.search = window.search || {};
+(function search(search) {
+ // Search functionality
+ //
+ // You can use !hasFocus() to prevent keyhandling in your key
+ // event handlers while the user is typing their search.
+
+ if (!Mark || !elasticlunr) {
+ return;
+ }
+
+ //IE 11 Compatibility from https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/String/startsWith
+ if (!String.prototype.startsWith) {
+ String.prototype.startsWith = function(search, pos) {
+ return this.substr(!pos || pos < 0 ? 0 : +pos, search.length) === search;
+ };
+ }
+
+ var search_wrap = document.getElementById('search-wrapper'),
+ searchbar = document.getElementById('searchbar'),
+ searchbar_outer = document.getElementById('searchbar-outer'),
+ searchresults = document.getElementById('searchresults'),
+ searchresults_outer = document.getElementById('searchresults-outer'),
+ searchresults_header = document.getElementById('searchresults-header'),
+ searchicon = document.getElementById('search-toggle'),
+ content = document.getElementById('content'),
+
+ searchindex = null,
+ doc_urls = [],
+ results_options = {
+ teaser_word_count: 30,
+ limit_results: 30,
+ },
+ search_options = {
+ bool: "AND",
+ expand: true,
+ fields: {
+ title: {boost: 1},
+ body: {boost: 1},
+ breadcrumbs: {boost: 0}
+ }
+ },
+ mark_exclude = [],
+ marker = new Mark(content),
+ current_searchterm = "",
+ URL_SEARCH_PARAM = 'search',
+ URL_MARK_PARAM = 'highlight',
+ teaser_count = 0,
+
+ SEARCH_HOTKEY_KEYCODE = 83,
+ ESCAPE_KEYCODE = 27,
+ DOWN_KEYCODE = 40,
+ UP_KEYCODE = 38,
+ SELECT_KEYCODE = 13;
+
+ function hasFocus() {
+ return searchbar === document.activeElement;
+ }
+
+ function removeChildren(elem) {
+ while (elem.firstChild) {
+ elem.removeChild(elem.firstChild);
+ }
+ }
+
+ // Helper to parse a url into its building blocks.
+ function parseURL(url) {
+ var a = document.createElement('a');
+ a.href = url;
+ return {
+ source: url,
+ protocol: a.protocol.replace(':',''),
+ host: a.hostname,
+ port: a.port,
+ params: (function(){
+ var ret = {};
+ var seg = a.search.replace(/^\?/,'').split('&');
+ var len = seg.length, i = 0, s;
+ for (;i
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ The
+
+
+
+
+ Introduction
+hacspec is a specification language for crypto primitives, protocols, and more. +It is a subset of the Rust programming language, focused on functional +programming and it avoids the use of mutable state as much as possible.
+This book gives an overview of:
+-
+
- The hacspec language; +
- The different parts of the project: + + +
- How to use hacspec to write specifications for standards and verification; +
- How to use hacspec to generate test vectors; +
- Work on the hacspec compiler and tooling itself. +
For a quick introduction you can also check out these slides from April 2021. +An in-depth technical report is also available, and serves as a reference +for the language formalization.
+The hacspec language
+This section gives an informal description of the hacspec language, whose +goal is to provide hands-on documentation for users of the language. For +a formal specification of the semantics of the language, please refer +to the technical report.
+hacspec is a domain-specific language embedded inside Rust. This means that +all correct hacspec programs are correct Rust programs: you can use +the usual Rust tooling for working on your hacspec developments. However, +hacspec is a strict subset of Rust: this means that some features of Rust +are forbidden inside hacspec. The goal of restricting the expressiveness of +the language is twofold: first, help domain experts such as cryptographers +convey their specifications in a fashion that should help them avoid +mistakes; second, provide a way for Rust programmers to interact with theorem +provers such as F* or Coq.
+Syntax
+P ::= [i]\* Program items
+i ::= array!(t, μ, n) Array type declaration where n is a natural number
+ | nat_mod!(t, n) Modular integer
+ | fn f([d]+) -> μ b Function declaration
+ | type t = enum { [c(μ)]+ } Enum declaration (with constructors)
+ | type t = struct([μ]+) Struct declaration (without named fields)
+ | const x: μ = e Constant declaration
+ | use crate::* External crate import
+ | use mod::* Internal module import
+d ::= x: τ Function argument
+ | mut x: τ Mutable function argument
+μ ::= unit|bool|u8|U8|i8|I8... Base types
+ | Seq<μ> Sequence
+ | String Strings
+ | ([μ]+) Tuple
+ | unit Unit type
+ | t Named type
+τ ::= μ Plain type
+ | &μ Immutable reference
+b ::= {[s;]+} Block
+p ::= x Variable pattern
+ | ([p]+) Tuple pattern
+ | t (p) Struct constructor pattern
+ | _ Wildcard pattern
+s ::= let p: τ = e Let binding
+ | let mut p: τ = e Mutable let binding
+ | x = e Variable reassignment
+ | x = e? Variable reassignment with result/option catching
+ | let p: τ = e? Let binding with result/option catching
+ | if e then b (else b) Conditional statements
+ | c(e) Enum injection
+ | match e { [c(p) => e]+ } Pattern matching
+ | for x in e..e b For loop (integers only)
+ | e Return expression
+ | b Statement block
+e ::= ()|true|false Unit and boolean literals
+ | n Integer literal
+ | U8(e)|I8(e)|... Secret integer classification
+ | "..." String literal
+ | t([e]+) Array literal
+ | e as μ Integer casting
+ | x Variable
+ | () Unit
+ | f([a]+) Function call
+ | if e then e else e Conditional expression
+ | e ⊙ e Binary operations
+ | ⊘ e Unary operations
+ | ([e]+) Tuple constructor
+ | x[e] Array or sequence index
+a ::= e Linear argument
+ | &e Call-site borrowing
+⊙ ::= + | - | * | / | &&
+ | || | == | != | > | <
+⊘ ::= - | ~
+The core of hacspec
+Crates and modules
+hacspec only supports single-module crates, due to a technical limitation +of the Rust compiler. Inside this single file, a hacspec program shall always +start with:
+use hacspec_lib::*;
+
+// Optional: dependencies on other crates containing hacspec programs
+use other_hacpsec_crate::*;No other form of use is allowed in hacspec, because allowing Rust's
+complex import patterns would increase the complexity of the hacspec compiler
+and conflict with the module systems of most proof assistants.
Functions
+hacspec is a functional language, and only supports the declaration of +top-level functions:
+fn hacspec_function(x: bool) -> () {
+ ...
+}The functions can take any number of arguments, and may return a value (or not). +Note that recursive functions are forbidden in hacspec.
+The control flow inside hacspec functions is limited, as return statements
+are forbidden.
Basic Types
+hacspec supports all the Rust primitive types: integers (signed and unsigned), +booleans, unit, tuples. hacspec possesses some support for generic +types, but only for primitive types defined by the language creators, and +not for user-defined types.
+Type aliases are allowed in hacspec:
+type OneTypeAlias = u32;Borrows
+hacspec forbids mutable borrows in all places. Immutable borrows are allowed +in hacspec, but only for function arguments. Indeed, you can declare a function +argument as immutably borrowed:
+fn hacspec_function(arg: &Seq<u8>) {
+ ...
+}You can also immutably borrow a value at the call site of a function:
+hacspec_function(&Seq::<u8>::new(64))In particular, return types cannot contain references, and the same is true +for types inside tuples or any data structure.
+Constants
+hacspec allows the declaration of constants:
+const ONE_CONST : bool = false;Assignments
+Inside a function body, hacspec allows regular Rust let-bindings:
+let x = ...;hacspec also allows mutable let bindings, and subsequent reassignments:
+let mut x = ...;
+...
+x = ...;This allowing of mutable variable might come as a contradiction to hacspec's +philosophy of forbidding mutable state. But in fact, mutable local variables in +hacspec can be translated to a completely side-effect free form with a state-passing +like monadic structure.
+Left-hand sides of assignments support destructuring, which is currently the +only way to access the members of a tuple:
+let (x, y) = z;Loops
+Looping is severely restricted in hacspec compared to Rust, as the only accepted form is
+for looping with a counter over an integer range:
for i in low..hi {
+ ... // The block can use i and reassign mutable variables
+}The motivation for this restriction is to ease the proof of termination of
+loops. break or continue statements are forbidden.
Conditionals
+hacspec allows statement-like conditionals as well as expression-like +conditionals:
+if cond1 {
+ ... // the block can modify mutable variables
+} else { // else block is optional here
+ ...
+}
+let x = if cond2 { ... } else { ... };Statements and expressions
+In regular Rust, statements and expressions can be mixed together freely. +This not the case in hacspec that imposes a strict precedence of statements +over expressions. For instance, the following code is not allowed in +hacspec:
+let x = if cond {
+ y = true; // ERROR: the reassignment is a statement, which cannot
+ // be contained in the expression to which x is assigned.
+ 3
+} else {
+ 4
+};Visibility
+hacspec allows for both pub and non-pub versions of item declarations
+(pub, non-pub, etc). You simply have to respect the Rust visibility rules. Note
+that these visibility distinctions might not be translated in the proof
+backends.
Sequences and arrays
+Sequences
+The staple Vec type is forbidden in hacspec. Instead, you have to use the
+type Seq, which is implemented as a wrapper around Vec.
The most notable differences between Seq and Vec is that Seq is not
+resizable, and does not support push and pop operations. Instead, the
+final length of the seq has to be provided at creation time. See the
+hacspec standard library documentation for more details.
Seq is a built-in generic type that always has to be indexed by the content of the
+cells: Seq<u8>, etc.
Arrays
+The native Rust array types [<type of contents>, <size>] is forbidden in
+hacspec. Instead, you have to declare nominally at the top-level new array types
+for a specific cell content and size with:
array!(FooArray, u8, 64);
+// This declares type FooArray as an array of u8 of size 64
+bytes!(BarArray, 64);
+// bytes! is a specialized version of array! with secret bytes
+array!(BazArray, u8, 64, type_for_indexes:BazIndex);
+// The additional argument type_for_indexes defines an alias of usize
+// intended to spot which usizes are used to index BazArray (useful for
+// verification)Structs and enums
+hacspec also supports user-defined structs and enums with some restrictions.
+Structs
+The only form of struct declaration currently allowed in hacspec is:
+struct Foo(u32, Seq<u32>);The struct thus declared can have one or more components. This form of struct +declaration effectively corresponds to a single-case enum, and is implemented +as such. Struct components can be accessed through let-binding destructuring:
+let Foo(x, y) = z;Note that you can't store borrowed types inside hacspec structs, hence there is no +need for lifetime variables.
+Enums
+hacspec supports very restricted enum declarations:
enum Foo {
+ CaseA,
+ CaseB(u16),
+ CaseC(Seq<bool>, u64)
+}These declaration don't support the basic Rust features such as C-style +union declarations with assignments for each case.
+Enumeration values can be pattern-matched in an expression:
+match x {
+ Foo::CaseA => ...,
+ Foo::CaseB(y) => ...,
+ Foo::CaseC(y,z) => ...
+}Note that you can't store borrowed types inside hacspec enums, hence there is no +need for lifetime variables.
+Option and Result
+User-defined structs and enums presented above don't support generic type
+parameters yet. However, the built-in enums Option<T> and Result<T,U>
+support type parameters. Those type parameters have to be explicitly declared
+each time, as hacspec does not currently support type inference:
match x {
+ Result::<Seq<u8>, bool>::Ok(y) => ...,
+ Result::<Seq<u8>, bool>::Err(err) => ...
+}Such type parameter declaration is cumbersome; as a workaround we advise +to declare a type alias as such:
+type MyResult = Result::<Seq<u8>, bool>;Error handling
+Error handling in Rust is done via the Result type (see the structs and
+enums section). But on top of explicit pattern-matching, hacspec also
+supports the popular ? operator to quickly perform an early return and
+propagate the error case upwards.
? is only allowed at the very end of an expression in a let-binding or
+reassignment statement:
let x = foo(true)?; // GOOD
+let y = foo(bar(0)?); // ERROR: the ? is not at the end of the statementCurrently, ? is the only way to return early in a hacspec function.
The hacspec std library
+The hacspec standard library contains a host of functions, type generators +and methods that define the base objects manipulated in classic cryptographic +primitives.
+Methods in the standard library can be divided into three categories:
+-
+
- The
not_hacspecmethods whose signature and body does not belong to the +hacspec fragment of Rust. They should not be used in hacspec code, but can +be used as helpers for e.g. testing.
+ - The
unsafe_hacspecmethods whose signature belongs to hacspec but not +the body. These methods can be used in hacspec programs but their body +is part of the trusted codebase.
+ - The
in_hacspecmethods whose signatures and bodies belong to the +hacspec fragment of Rust. These can be used safely in hacspec programs.
+
Arithmetic
+hacspec overloads the arithmetic operators for a wide variety of types +corresponding to mathematical values mentioned in cryptographic specifications.
+The Numeric trait
+All of these types implement the Numeric trait defined by the hacspec standard
+library. The arithmetic operators work for all kinds of integers, but also
+arrays and sequences (point-wise operations).
Note that the list of types implementing Numeric is hardcoded in the
+hacspec compiler, and as of this day cannot be extended by the user.
While the Rust compiler can infer the type of integer literals automatically, +this feature is not implemented by the hacspec compiler:
+let w: u32 = 0; // ERROR: an integer without a suffix will have type usize
+let x: u64 = 0x64265u64; // GOOD
+let y: u64 = 4u64; // GOOD
+Public and secret integers
+One of hacspec's goal is to enable users to quickly check whether their
+application does not obviously break the constant-time guarantee.
+Certain processor instructions take more or less time to complete depending
+on their inputs, which can cause secret leakage and break the security of
+an application. Hence, hacspec offers for each type of integer (u8, u32, etc.)
+a mirror secret integer type (U8, U32, etc.) for which operations
+that break constant-timedness are forbidden.
This public/private distinction can be found at a lot of places in the standard +library, and is made to forbid functions and data structures from leaking secrets.
+Conversions between public and secret integers are restricted to two functions:
+classify and declassify.
Abstract integers
+Some cryptographic specifications talk about modular arithmetic in large
+fields, whose size overflows even u128. To ease the expression of such
+specifications, hacspec offers wrapper types around BigInt that can be
+declared using the following API:
abstract_nat_mod!(
+ NameOfModularInts,
+ NameOfUnderlyingByteRepresentation,
+ 256, // Number of bits for the representation of the big integer,
+ "ffffffffffffffff00000000000065442", // Hex representation of the modulo value as hex
+)
+
+abstract_public_nat_mod!(
+ ... // Public version of above
+)Integers as bytes
+It is often useful to view an integer as a sequence of bytes that can be +manipulated individually. The hacspec standard library provides a number +of function to translate back and forth from integer to sequence of bytes:
+pub fn u16_to_le_bytes(x: u16) -> u16Word;
+
+pub fn u16_from_le_bytes(s: u16Word) -> u16;
+
+pub fn U64_to_be_bytes(x: U64) -> U64Word;
+
+pub fn U64_from_be_bytes(s: U64Word) -> U64;
+
+...Sequence and array operations
+Operations common to sequences and arrays
+Base traits
+Some operations are common to both sequences and arrays +by design, and can be used as the interoperability base between the two types +of collections. These operations are the following:
+-
+
len: gives the length of an array or sequence;
+iter: iterates over the content of the array or sequence +(unsafe in hacspec but can be used for implementing primitives)
+create: creates a sequence or array and initializes the elements to the +default value (0 for arithmetic types);
+update_slice,updateandupdate_start: produce a new sequence or array +with modified contents.
+
Both sequences and arrays implement indexing with any type of unsigned public +integer.
+Chunking
+Both arrays and sequences support chunking with methods like:
+-
+
num_chunksandnum_exact_chunks(whole or partial blocks);
+get_chunk,get_exact_chunkandget_remainder_chunk;
+set_chunkandset_exact_chunk.
+
The read operations borrow the sequence or array, but the write operations +create a new sequence or array.
+Conversions
+Sequences and arrays can be created from other types via methods like:
+-
+
from_public_sliceandfrom_slice;
+from_vecandfrom_native_slice;
+from_public_seqandfrom_seq(to convert a seq into an array of the correct size);
+from_stringandfrom_hexfor byte or hex strings (hex only foru8sequences and arrays).
+
Secrecy
+The methods prefixed by public performs an element-wise classification of the
+data under the hood.
Ownage
+Some methods have two versions: an owned and a non-owned version, depending
+on whether the self argument is consumed or not by the method. This distinction
+is useful to avoid unnecessary copies and thus be more performant.
Array-specific operations
+Since array length is known statically, new does not take any argument,
+same as length. slices of arrays become Seq.
Sequence-specific operations
+Sequences can be extended (by creating a new sequence under the hood) with
+push or concat. Sequences can also be sliced with slice.
Examples
+The main hacspec repository contains a set of example specifications. +In this section we pull out some interesting bits to demonstrate the hacspec +language.
+There's also a provider that bundles the different cryptographic primitives +into a single library. +The provider implements the RustCrypto traits in order to facilitate interoperability.
+Usage
+Specifications
+Verification
+Coq
+QuickCheck / QuickChick
+You can test your hacspec code using QuickCheck (a Rust library for randomized property-based testing), by simply implementing quickcheck::Arbitrary for the type you want to generate tests for. For example:
impl Arbitrary for Fp {
+ fn arbitrary(g: &mut Gen) -> Fp {
+ let mut a: [u64; 6] = [0; 6];
+ for i in 0..6 {
+ a[i] = u64::arbitrary(g);
+ }
+ let mut b: [u8; 48] = [0; 48];
+ for i in 0..6 {
+ let val: u64 = a[i];
+ b[(i*8)..((i+1)*8)].copy_from_slice(&(val.to_le_bytes()));
+ }
+ Fp::from_byte_seq_le(Seq::<U8>::from_public_slice(&b))
+ }
+}then you can use the quickcheck attribute, to make QuickCheck do property based testing for this function:
#[cfg(test)]
+#[quickcheck] //Using the fp arbitraty implementation from above to generate fp2 elements.
+fn test_fp2_prop_add_neg(a: Fp2) -> bool {
+ let b = fp2neg(a);
+ fp2fromfp(Fp::ZERO()) == fp2add(a, b)
+}which will run when you do cargo test. If you then add the tag #[cfg(proof)] and export to Coq,
cargo hacspec -o coq/src/<output_file_name>.v <input_crate_name>
+then you get corresponding QuickChick test,
+Definition test_fp2_prop_add_neg (a_320 : fp2) : bool :=
+ let b_321 :=
+ fp2neg (a_320) in
+ (fp2fromfp (nat_mod_zero )) =.? (fp2add (a_320) (b_321)).
+
+QuickChick (forAll g_fp2 (fun a_320 : fp2 =>test_fp2_prop_add_neg a_320)).
+and generators will be constructed for the types automatically as,
+Instance show_fp : Show (fp) := Build_Show (fp) (fun x => show (GZnZ.val _ x)).
+Definition g_fp : G (fp) := @bindGen Z (fp) (arbitrary) (fun x => returnGen (@Z_in_nat_mod _ x)).
+Instance gen_fp : Gen (fp) := Build_Gen fp g_fp.
+which you can then run through coq in the folder coq/
coqc -R src/ Hacspec src/<output_file_name>.v
+Make sure you run:
+coqc -R src/ Hacspec src/MachineIntegers.v
+coqc -R src/ Hacspec src/Lib.v
+or make to generate the .vo files used by <output_file_name>.v.
For more information:
+-
+
- on QuickCheck (in rust): BurntSushi/quickcheck +
- on QuickChick: Software foundations book on QuickChick +
Test Vectors
+For Developers
+This section contains a handy guide for hacspec developers working on the +standard library or the compiler.
+Working on the compiler
+High-level architecture
+
The Rustspec compiler intervenes after the regular Rust typechecking, +by translating the Rust AST into a stricter hacspec AST, +yielding error messages if you're not in the subset.
+The hacspec AST then undergoes a typechecking phase that replicates the +formal typechecking judgment of hacspec, before being compiled +to the proof backends like F* or Coq.
+Code organization
+The source code for the compiler is located in the language/ folder.
+main.rs is the file containing the driver for the different compiler
+passes.
Hacspec AST
+The main file of the compiler is rustspec.rs and it contains the AST
+structure.
Types are usually enclosed into Spanned<...> blocks that attach a location
+information to an AST node, thereby providing a way to display beautiful error
+message.
Several nodes also contain a Fillable<...> node standing for information
+that is filled by the typechecking phase but that can be left to None when
+building the AST.
Translation from Rust AST
+This phase is contained in ast_to_rustspec.rs. The trickyness of this
+translation is that it needs to be aware of certain special names contained
+in the structure SpecialNames. Indeed, while the Rust AST treats the application
+enum constructors like function applications, the hacspec AST considers them as
+proper injection so we need to distinguish them in the Rust AST. For that, we
+need to know all declared enums at this point of the program.
Enums and other SpecialNames are also defined in the ExternalData that
+contains the signatures and types imported in crates used by the hacspec
+program being compiled.
Name resolution
+When the translation from Rust AST is finished, the identifiers for all +variables inside function bodies are of the following type:
+pub enum Ident {
+ Unresolved(String),
+ Local(LocalIdent),
+ TopLevel(TopLevelIdent),
+}More precisely, they are still in the Ident::Unresolved case. The compiler
+pass in name_resolution.rs resolves the identifiers by linking them to local or global identifiers,
+each one having a unique ID. hacspec does not feature De Bruijn variable
+handling, instead relying on unique fresh IDs for differentiating local
+and global variables from each other.
External data
+A hacspec file can never (in principal) be considered alone, as it usually imports +at least several other crates like the hacspec standard library. These external +crates must pre-populate the typechecking context with the types and function +signatures that they define.
+It's the job of hir_to_rustspec.rs to retrieve this data. The critical
+piece of code in this file is the following:
let num_def_ids = crate_store.num_def_ids_untracked(*krate_num);
+let def_ids = (0..num_def_ids).into_iter().map(|id| DefId {
+ krate: *krate_num,
+ index: DefIndex::from_usize(id),
+});First, we retrieve the number of exported symbols by an external crate using
+num_def_ids_untracked, a function that is specifically labeled
+as critical to the hacspec compiler in the Rust compiler codebase. Then,
+we manufacture definition IDs for all these exported symbols, relying on the
+invariant that they are numbered from 0 to the number of exported symbols
+in Rust's compiled crate metadata format.
Then, we use those definition IDs (DefId) to query the Rust compiler
+via the central TyCtxt
+data structure. If the DefId corresponds to a type definition, we examine the
+type definition structurally and check whether it corresponds to a hacspec-compatible
+type definition. Notably, the type definitions generated by macros like array!
+or nat_mod! are only seen here in their expanded version, so we have to retro-engineer
+which expanded version corresponds to which macro expansion. This is a vulnerability
+of the compiler since it's possible to break the abstraction of the language
+by smuggling in a type not defined via a hacspec macro this way. That's why hacspec
+developers should be very careful about which dependencies they import in order
+to have a 100% safety guarantee.
For DefIds corresponding to functions, the signature of the function is analysed
+and if it fits the subset of types expected by hacspec, the function is imported
+along with its type in a pre-populated typechecking context.
Note that it is not possible any more at this point to retrieve the #[in_hacspec],
+#[unsafe_hacspec], etc. attributes that would tag the external definitions,
+since these attributes get erased by the Rust compiler before reaching the
+compiled crates metadata.
Typechecking
+The typechecking is done in typechecker.rs and follows a very regular structure,
+making heavy use of immutable data structures to not mess up the various
+context manipulations.
Note that we need to perform a full typechecking complete with method resolution +because the proof backends need very fine-grained typechecking information +to generate correct code.
+Be careful: types often need to be de-aliased with dealias_type before
+being matched on structurally. Forgetting to dealias will lead to bugs with
+type aliases.
Proof backends
+The different proof backends (rustspec_to_fstar.rs, etc) all enjoy a similar
+structure that ought to be refactored to showcase their commonality. The backends
+don't use an intermediate AST to generate the code in the proof assistant but
+rather directly print code as string using the pretty
+pretty-printing library. If you want to start a new proof backend, the easiest
+solution is probably to copy an existing proof backend and tweak it until
+you get the right result.
The code generation has to be fine-tuned to interface with a replica of the +hacspec standard library in the host proof assistant, whose correspondence with +the original hacspec library in Rust is part of the trusted code base. More specially, +clever solutions to encode sequences and array, as well as all the different types +of public and secret machine integers, and the interaction between the two +(seeing a double as a string of bytes) have to be implemented through proof +assistant libraries.
+Unit tests
+The compiler has various unit tests that are controlled trough the language/tests
+files. Please enrich the unit tests bases in language-tests,
+negative-language-tests and test-crate as you implement new features for
+the compiler. The compiler can also be tested against all the hacspec cryptographic
+specifications by running examples/typecheck_examples.sh from the root of
+the repository.
Contributors
+A list of contributors to the hacspec project.
+-
+
- Franziskus Kiefer (franziskuskiefer) +
- Denis Merigoux (denismerigoux) +
- Karthik Bhargavan +
- Tomer Yavor (TomerHawk) +
- Tanmay Garg (tanmay2004) +
- Peter Schwabe (cryptojedi) +
- Kaspar Schleiser (kaspar030) +
- Kasserne +
- Tony Arcieri (tarcieri) +
If you feel you're missing from this list, feel free to add yourself in a PR.
+ +
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/std/index.html b/archive/std/index.html
new file mode 100644
index 0000000..26bf61d
--- /dev/null
+++ b/archive/std/index.html
@@ -0,0 +1,244 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ The
+
+
+
+
+ Arithmetic
+hacspec overloads the arithmetic operators for a wide variety of types +corresponding to mathematical values mentioned in cryptographic specifications.
+The Numeric trait
+All of these types implement the Numeric trait defined by the hacspec standard
+library. The arithmetic operators work for all kinds of integers, but also
+arrays and sequences (point-wise operations).
Note that the list of types implementing Numeric is hardcoded in the
+hacspec compiler, and as of this day cannot be extended by the user.
While the Rust compiler can infer the type of integer literals automatically, +this feature is not implemented by the hacspec compiler:
+let w: u32 = 0; // ERROR: an integer without a suffix will have type usize
+let x: u64 = 0x64265u64; // GOOD
+let y: u64 = 4u64; // GOOD
+Public and secret integers
+One of hacspec's goal is to enable users to quickly check whether their
+application does not obviously break the constant-time guarantee.
+Certain processor instructions take more or less time to complete depending
+on their inputs, which can cause secret leakage and break the security of
+an application. Hence, hacspec offers for each type of integer (u8, u32, etc.)
+a mirror secret integer type (U8, U32, etc.) for which operations
+that break constant-timedness are forbidden.
This public/private distinction can be found at a lot of places in the standard +library, and is made to forbid functions and data structures from leaking secrets.
+Conversions between public and secret integers are restricted to two functions:
+classify and declassify.
Abstract integers
+Some cryptographic specifications talk about modular arithmetic in large
+fields, whose size overflows even u128. To ease the expression of such
+specifications, hacspec offers wrapper types around BigInt that can be
+declared using the following API:
abstract_nat_mod!(
+ NameOfModularInts,
+ NameOfUnderlyingByteRepresentation,
+ 256, // Number of bits for the representation of the big integer,
+ "ffffffffffffffff00000000000065442", // Hex representation of the modulo value as hex
+)
+
+abstract_public_nat_mod!(
+ ... // Public version of above
+)Integers as bytes
+It is often useful to view an integer as a sequence of bytes that can be +manipulated individually. The hacspec standard library provides a number +of function to translate back and forth from integer to sequence of bytes:
+pub fn u16_to_le_bytes(x: u16) -> u16Word;
+
+pub fn u16_from_le_bytes(s: u16Word) -> u16;
+
+pub fn U64_to_be_bytes(x: U64) -> U64Word;
+
+pub fn U64_from_be_bytes(s: U64Word) -> U64;
+
+...
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/std/seq.html b/archive/std/seq.html
new file mode 100644
index 0000000..ab578fb
--- /dev/null
+++ b/archive/std/seq.html
@@ -0,0 +1,276 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ The hacspec std library
+The hacspec standard library contains a host of functions, type generators +and methods that define the base objects manipulated in classic cryptographic +primitives.
+Methods in the standard library can be divided into three categories:
+-
+
- The
not_hacspecmethods whose signature and body does not belong to the +hacspec fragment of Rust. They should not be used in hacspec code, but can +be used as helpers for e.g. testing.
+ - The
unsafe_hacspecmethods whose signature belongs to hacspec but not +the body. These methods can be used in hacspec programs but their body +is part of the trusted codebase.
+ - The
in_hacspecmethods whose signatures and bodies belong to the +hacspec fragment of Rust. These can be used safely in hacspec programs.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/tomorrow-night.css b/archive/tomorrow-night.css
new file mode 100644
index 0000000..81fe276
--- /dev/null
+++ b/archive/tomorrow-night.css
@@ -0,0 +1,102 @@
+/* Tomorrow Night Theme */
+/* https://github.com/jmblog/color-themes-for-highlightjs */
+/* Original theme - https://github.com/chriskempson/tomorrow-theme */
+/* https://github.com/jmblog/color-themes-for-highlightjs */
+
+/* Tomorrow Comment */
+.hljs-comment {
+ color: #969896;
+}
+
+/* Tomorrow Red */
+.hljs-variable,
+.hljs-attribute,
+.hljs-tag,
+.hljs-regexp,
+.ruby .hljs-constant,
+.xml .hljs-tag .hljs-title,
+.xml .hljs-pi,
+.xml .hljs-doctype,
+.html .hljs-doctype,
+.css .hljs-id,
+.css .hljs-class,
+.css .hljs-pseudo {
+ color: #cc6666;
+}
+
+/* Tomorrow Orange */
+.hljs-number,
+.hljs-preprocessor,
+.hljs-pragma,
+.hljs-built_in,
+.hljs-literal,
+.hljs-params,
+.hljs-constant {
+ color: #de935f;
+}
+
+/* Tomorrow Yellow */
+.ruby .hljs-class .hljs-title,
+.css .hljs-rule .hljs-attribute {
+ color: #f0c674;
+}
+
+/* Tomorrow Green */
+.hljs-string,
+.hljs-value,
+.hljs-inheritance,
+.hljs-header,
+.hljs-name,
+.ruby .hljs-symbol,
+.xml .hljs-cdata {
+ color: #b5bd68;
+}
+
+/* Tomorrow Aqua */
+.hljs-title,
+.css .hljs-hexcolor {
+ color: #8abeb7;
+}
+
+/* Tomorrow Blue */
+.hljs-function,
+.python .hljs-decorator,
+.python .hljs-title,
+.ruby .hljs-function .hljs-title,
+.ruby .hljs-title .hljs-keyword,
+.perl .hljs-sub,
+.javascript .hljs-title,
+.coffeescript .hljs-title {
+ color: #81a2be;
+}
+
+/* Tomorrow Purple */
+.hljs-keyword,
+.javascript .hljs-function {
+ color: #b294bb;
+}
+
+.hljs {
+ display: block;
+ overflow-x: auto;
+ background: #1d1f21;
+ color: #c5c8c6;
+}
+
+.coffeescript .javascript,
+.javascript .xml,
+.tex .hljs-formula,
+.xml .javascript,
+.xml .vbscript,
+.xml .css,
+.xml .hljs-cdata {
+ opacity: 0.5;
+}
+
+.hljs-addition {
+ color: #718c00;
+}
+
+.hljs-deletion {
+ color: #c82829;
+}
diff --git a/archive/usage/index.html b/archive/usage/index.html
new file mode 100644
index 0000000..9a6d8af
--- /dev/null
+++ b/archive/usage/index.html
@@ -0,0 +1,230 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Sequence and array operations
+Operations common to sequences and arrays
+Base traits
+Some operations are common to both sequences and arrays +by design, and can be used as the interoperability base between the two types +of collections. These operations are the following:
+-
+
len: gives the length of an array or sequence;
+iter: iterates over the content of the array or sequence +(unsafe in hacspec but can be used for implementing primitives)
+create: creates a sequence or array and initializes the elements to the +default value (0 for arithmetic types);
+update_slice,updateandupdate_start: produce a new sequence or array +with modified contents.
+
Both sequences and arrays implement indexing with any type of unsigned public +integer.
+Chunking
+Both arrays and sequences support chunking with methods like:
+-
+
num_chunksandnum_exact_chunks(whole or partial blocks);
+get_chunk,get_exact_chunkandget_remainder_chunk;
+set_chunkandset_exact_chunk.
+
The read operations borrow the sequence or array, but the write operations +create a new sequence or array.
+Conversions
+Sequences and arrays can be created from other types via methods like:
+-
+
from_public_sliceandfrom_slice;
+from_vecandfrom_native_slice;
+from_public_seqandfrom_seq(to convert a seq into an array of the correct size);
+from_stringandfrom_hexfor byte or hex strings (hex only foru8sequences and arrays).
+
Secrecy
+The methods prefixed by public performs an element-wise classification of the
+data under the hood.
Ownage
+Some methods have two versions: an owned and a non-owned version, depending
+on whether the self argument is consumed or not by the method. This distinction
+is useful to avoid unnecessary copies and thus be more performant.
Array-specific operations
+Since array length is known statically, new does not take any argument,
+same as length. slices of arrays become Seq.
Sequence-specific operations
+Sequences can be extended (by creating a new sequence under the hood) with
+push or concat. Sequences can also be sliced with slice.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/archive/usage/specifications.html b/archive/usage/specifications.html
new file mode 100644
index 0000000..41924fe
--- /dev/null
+++ b/archive/usage/specifications.html
@@ -0,0 +1,230 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Usage
+ +
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/theme/index.hbs b/archive/usage/test_vectors.html
similarity index 55%
rename from theme/index.hbs
rename to archive/usage/test_vectors.html
index 080b785..cb9595b 100644
--- a/theme/index.hbs
+++ b/archive/usage/test_vectors.html
@@ -1,64 +1,44 @@
-
+
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Specifications
+ +
@@ -83,7 +63,7 @@
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
if (theme === null || theme === undefined) { theme = default_theme; }
var html = document.querySelector('html');
- html.classList.remove('{{ default_theme }}')
+ html.classList.remove('light')
html.classList.add(theme);
var body = document.querySelector('body');
body.classList.remove('no-js')
@@ -110,7 +90,7 @@