Merge pull request #430 from hacspec/alternative_libs_secret_integers

Secret independence support for F*

proof-libs/fstar-secret-integers/Makefile.copy

@@ -0,0 +1,94 @@
+# This is a generically useful Makefile for F* that is self-contained
+#
+# It is tempting to factor this out into multiple Makefiles but that
+# makes it less portable, so resist temptation, or move to a more
+# sophisticated build system.
+#
+# We expect FSTAR_HOME to be set to your FSTAR repo/install directory
+# We expect HACL_HOME to be set to your HACL* repo location
+# We expect HAX_LIBS_HOME to be set to the folder containing core, rust_primitives etc.
+#
+# ROOTS contains all the top-level F* files you wish to verify
+# The default target `verify` verified ROOTS and its dependencies
+# To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line
+#
+#
+# To make F* emacs mode use the settings in this file, you need to
+# add the following lines to your .emacs
+#
+# (setq-default fstar-executable "<YOUR_FSTAR_HOME>/bin/fstar.exe")
+# (setq-default fstar-smt-executable "<YOUR_Z3_HOME>/bin/z3")
+#
+# (defun my-fstar-compute-prover-args-using-make ()
+#   "Construct arguments to pass to F* by calling make."
+#   (with-demoted-errors "Error when constructing arg string: %S"
+#     (let* ((fname (file-name-nondirectory buffer-file-name))
+# 	   (target (concat fname "-in"))
+# 	   (argstr (car (process-lines "make" "--quiet" target))))
+#       (split-string argstr))))
+# (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
+#
+
+HAX_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar
+FSTAR_HOME    ?= $(HAX_LIBS_HOME)/../../../FStar
+HACL_HOME     ?= $(HAX_LIBS_HOME)/../../../hacl-star
+FSTAR_BIN     ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
+
+CACHE_DIR     ?= $(HAX_LIBS_HOME)/.cache
+HINT_DIR      ?= $(HAX_LIBS_HOME)/.hints
+
+.PHONY: all verify clean
+
+all:
+	rm -f .depend && $(MAKE) .depend
+	$(MAKE) verify
+
+# By default, we process all the files in the current directory. Here, we
+# *extend* the set of relevant files with the tests.
+ROOTS = $(wildcard *.fst)
+
+FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_LIBS_HOME)/rust_primitives $(HAX_LIBS_HOME)/core $(HAX_LIBS_HOME)/hax_lib
+
+FSTAR_FLAGS = --cmi \
+  --warn_error -331 \
+  --cache_checked_modules --cache_dir $(CACHE_DIR) \
+  --already_cached "+Prims+FStar+LowStar+C+Spec.Loops+TestLib" \
+  $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
+
+FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) $(OTHERFLAGS)
+
+
+.depend: $(HINT_DIR) $(CACHE_DIR)
+	$(info $(ROOTS))
+	$(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@
+
+include .depend
+
+$(HINT_DIR):
+	mkdir -p $@
+
+$(CACHE_DIR):
+	mkdir -p $@
+
+$(CACHE_DIR)/%.checked: | .depend $(HINT_DIR) $(CACHE_DIR)
+	$(FSTAR) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints
+
+verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS)))
+
+# Targets for interactive mode
+
+%.fst-in:
+	$(info $(FSTAR_FLAGS) \
+	  $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fst.hints)
+
+%.fsti-in:
+	$(info $(FSTAR_FLAGS) \
+	  $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fsti.hints)
+
+
+# Clean targets
+
+SHELL=/usr/bin/env bash
+
+clean:
+	rm -rf $(CACHE_DIR)/*

proof-libs/fstar-secret-integers/README.md

@@ -0,0 +1,35 @@
+## Libraries for Hax
+
+The goal of this directory is to serve as a snapshot of the current F*
+supporting libraries for Hax.
+
+The dependency chain is:
+
+`rust_primitives` <- `core` <- `hax_lib`
+
+# Rust Primitives
+
+The `/rust_primitives` directory contains hand-written models for Rust
+built-in features like machine integers and arrays. In particular, the
+code in this directory reconciles any type or semantic differences
+between Rust and F*. A number of files in this directory use the 
+[HACL Library](https://github.com/hacl-star/hacl-star/tree/main/lib).
+
+# Core & Alloc
+
+The `/core` directory contains hand-written models for some parts of
+the Core and Alloc libraries of Rust.
+
+As a first goal, we would like to typecheck the code in this directory
+against interfaces generated from Rust Core and Alloc.
+
+As a second goal, we would like to generate the code in this directory
+from an annotated version of Rust Core and Alloc.
+
+# Hax Library
+
+The `/hax_lib` directory contains hand-written and generated code
+for the Hax library which adds new features and functionality to Rust
+to help programmers. For example, this library includes bounded indexes
+for arrays, unbounded integers etc.
+

proof-libs/fstar-secret-integers/core/Alloc.Alloc.fst

@@ -0,0 +1,3 @@
+module Alloc.Alloc
+
+let t_Global = ()

proof-libs/fstar-secret-integers/core/Alloc.Collections.Binary_heap.fsti

@@ -0,0 +1,28 @@
+module Alloc.Collections.Binary_heap
+open Rust_primitives
+
+val t_BinaryHeap: Type -> eqtype
+
+val impl_9__new: #t:Type -> t_BinaryHeap t
+val impl_9__push: #t:Type -> t_BinaryHeap t -> t -> t_BinaryHeap t
+val impl_10__len: #t:Type -> t_BinaryHeap t -> usize
+val impl_10__iter: #t:Type -> t_BinaryHeap t -> t_Slice t
+
+open Core.Option
+
+val impl_10__peek: #t:Type -> t_BinaryHeap t -> t_Option t
+val impl_9__pop: #t:Type -> t_BinaryHeap t -> t_BinaryHeap t & t_Option t
+
+unfold
+let nonempty h = v (impl_10__len h) > 0
+
+val lemma_peek_len: #t:Type -> h: t_BinaryHeap t 
+  -> Lemma (Option_Some? (impl_10__peek h) <==> nonempty h)
+
+val lemma_pop_len: #t:Type -> h: t_BinaryHeap t 
+  -> Lemma (Option_Some? (snd (impl_9__pop h)) <==> nonempty h)
+
+val lemma_peek_pop: #t:Type -> h: t_BinaryHeap t 
+  -> Lemma (impl_10__peek h == snd (impl_9__pop h))
+          [SMTPat (impl_10__peek h)]
+

proof-libs/fstar-secret-integers/core/Alloc.Slice.fst

@@ -0,0 +1,5 @@
+module Alloc.Slice
+open Rust_primitives.Arrays
+open Alloc.Vec
+
+let impl__to_vec (s: t_Slice 'a): t_Vec 'a Alloc.Alloc.t_Global = s

proof-libs/fstar-secret-integers/core/Alloc.Vec.fst

@@ -0,0 +1,36 @@
+module Alloc.Vec
+open Rust_primitives
+
+unfold type t_Vec t (_: unit) = s:t_Slice t
+
+let impl__new #t: t_Vec t () = FStar.Seq.empty
+
+let impl_2__extend_from_slice #t (self: t_Vec t ()) (other: t_Slice t{Seq.length self + Seq.length other <= max_usize}): t_Vec t ()
+  = FStar.Seq.append self other
+
+let impl__with_capacity (_capacity: usize) = impl__new
+
+// TODO: missing precondition For now, `impl_1__push` has a wrong
+// semantics: pushing on a "full" vector does nothing. It should panic
+// instead.
+let impl_1__push
+  (v: t_Vec 't ())// Removed: {Seq.length v + 1 <= max_usize})
+  (x: 't)
+   : t_Vec 't () = 
+     if Seq.length v <= max_usize then v else
+     FStar.Seq.append v (FStar.Seq.create 1 x)
+
+let impl_1__len (v: t_Vec 't ()) =
+  let n = Seq.length v in
+  assert (n <= maxint usize_inttype);
+  mk_int #usize_inttype (Seq.length v)
+
+let from_elem (item: 'a) (len: usize) = Seq.create (v len) item
+
+open Rust_primitives.Hax
+open Core.Ops.Index
+instance update_at_tc_array t n: update_at_tc (t_Vec t ()) (int_t n) = {
+  super_index = FStar.Tactics.Typeclasses.solve <: t_Index (t_Vec t ()) (int_t n);
+  update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x);
+}
+

proof-libs/fstar-secret-integers/core/Core.Array.Iter.fsti

@@ -0,0 +1,5 @@
+module Core.Array.Iter
+open Rust_primitives
+
+let into_iter = Core.Iter.iterator_array
+let t_IntoIter t l = t_Array t l

proof-libs/fstar-secret-integers/core/Core.Array.fst

@@ -0,0 +1,10 @@
+module Core.Array
+open Rust_primitives
+
+type t_TryFromSliceError = | TryFromSliceError
+
+let impl_23__map n (arr: t_Array 'a n) (f: 'a -> 'b): t_Array 'b n 
+  = map_array arr f
+
+let impl_23__as_slice len (arr: t_Array 'a len): t_Slice 'a = arr
+

proof-libs/fstar-secret-integers/core/Core.Clone.fst

@@ -0,0 +1,11 @@
+module Core.Clone
+
+class t_Clone self = {
+  f_clone: x:self -> r:self {x == r}
+}
+
+(** Everything is clonable *)
+instance clone_all (t: Type): t_Clone t = {
+  f_clone = (fun x -> x);
+}
+

proof-libs/fstar-secret-integers/core/Core.Cmp.fsti

@@ -0,0 +1,48 @@
+module Core.Cmp
+open Rust_primitives
+
+let min (#t:inttype) (a:int_t t) (b:int_t t) =
+  if a <. b then a else b
+
+type t_Ordering =
+  | Ordering_Less : t_Ordering
+  | Ordering_Equal : t_Ordering
+  | Ordering_Greater : t_Ordering
+
+class t_Ord (v_Self: Type) = {
+  f_cmp:v_Self -> v_Self -> t_Ordering;
+  // f_max:v_Self -> v_Self -> v_Self;
+  // f_min:v_Self -> v_Self -> v_Self;
+  // f_clamp:v_Self -> v_Self -> v_Self -> v_Self
+}
+
+class t_PartialEq (v_Self: Type) (v_Rhs: Type) = {
+  // __constraint_1069563329_t_PartialEq:t_PartialEq v_Self v_Rhs;
+  f_eq:v_Self -> v_Rhs -> bool;
+  f_ne:v_Self -> v_Rhs -> bool
+}
+
+instance all_eq (a: eqtype): t_PartialEq a a = {
+  f_eq = (fun x y -> x = y);
+  f_ne = (fun x y -> x <> y);
+}
+
+class t_PartialOrd (v_Self: Type) (v_Rhs: Type) = {
+  __constraint_Rhs_t_PartialEq:t_PartialEq v_Self v_Rhs;
+  // __constraint_Rhs_t_PartialOrd:t_PartialOrd v_Self v_Rhs;
+  f_partial_cmp:v_Self -> v_Rhs -> Core.Option.t_Option t_Ordering;
+  // f_lt:v_Self -> v_Rhs -> bool;
+  // f_le:v_Self -> v_Rhs -> bool;
+  // f_gt:v_Self -> v_Rhs -> bool;
+  // f_ge:v_Self -> v_Rhs -> bool
+}
+
+type t_Reverse t = | Reverse of t
+
+let impl__then x y = x
+
+[@FStar.Tactics.Typeclasses.tcinstance]
+val ord_u64: t_Ord u64
+
+[@FStar.Tactics.Typeclasses.tcinstance]
+val ord_reverse t {| t_Ord t |}: t_Ord (t_Reverse t)

proof-libs/fstar-secret-integers/core/Core.Convert.fst

@@ -0,0 +1,57 @@
+
+module Core.Convert
+open Rust_primitives
+
+class try_into_tc self t = {
+  [@@@FStar.Tactics.Typeclasses.no_method]
+  f_Error: Type;
+  f_try_into: self -> Core.Result.t_Result t f_Error
+}
+
+instance impl_6 (t: Type0) (len: usize): try_into_tc (t_Slice t) (t_Array t len) = {
+  f_Error = Core.Array.t_TryFromSliceError;
+  f_try_into = (fun (s: t_Slice t) -> 
+    if Core.Slice.impl__len s = len
+    then Core.Result.Result_Ok (s <: t_Array t len)
+    else Core.Result.Result_Err Core.Array.TryFromSliceError
+  )
+}
+
+
+instance impl_6_refined (t: Type0) (len: usize): try_into_tc (s: t_Slice t {Core.Slice.impl__len s == len}) (t_Array t len) = {
+  f_Error = Core.Array.t_TryFromSliceError;
+  f_try_into = (fun (s: t_Slice t {Core.Slice.impl__len s == len}) -> 
+    Core.Result.Result_Ok (s <: t_Array t len)
+  )
+}
+
+class t_Into self t = {
+  f_into: self -> t;
+}
+
+class t_From self t = {
+  f_from: t -> self;
+}
+
+class t_TryFrom self t = {
+  [@@@FStar.Tactics.Typeclasses.no_method]
+  f_Error: Type;
+  f_try_from: t -> Core.Result.t_Result self f_Error;
+}
+
+instance integer_into
+  (t:inttype) (t':inttype { minint t >= minint t' /\ maxint t <= maxint t' })
+  : t_From (int_t t') (int_t t)
+  = { f_from = (fun (x: int_t t) -> Rust_primitives.Integers.cast #t #t' x) }
+
+instance into_from_from a b {| t_From a b |}: t_Into b a = {
+  f_into = (fun x -> f_from x)
+}
+
+instance from_id a: t_From a a = {
+  f_from = (fun x -> x)
+}
+
+class t_AsRef self t = {
+  f_as_ref:  self -> t;
+}

proof-libs/fstar-secret-integers/core/Core.Iter.Adapters.Enumerate.fst

@@ -0,0 +1,5 @@
+module Core.Iter.Adapters.Enumerate
+open Rust_primitives
+
+type t_Enumerate t = { iter: t; count: usize }
+

proof-libs/fstar-secret-integers/core/Core.Iter.Adapters.Step_by.fst

@@ -0,0 +1,9 @@
+module Core.Iter.Adapters.Step_by
+open Rust_primitives
+
+type t_StepBy t = { 
+  f_iter: t;
+  f_step: n: usize {v n > 0};
+  f_first_take: bool;
+}
+

proof-libs/fstar-secret-integers/core/Core.Iter.Traits.Collect.fst

@@ -0,0 +1,14 @@
+module Core.Iter.Traits.Collect
+
+class into_iterator self = {
+  f_IntoIter: Type;
+  // f_Item: Type;
+  f_into_iter: self -> f_IntoIter;
+}
+
+let t_IntoIterator = into_iterator
+
+unfold instance impl t {| Core.Iter.Traits.Iterator.iterator t |}: into_iterator t = {
+  f_IntoIter = t;
+  f_into_iter = id;
+}