From 9cd40a44cb6407477692cc50f2c84aed7531dac8 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Sat, 13 Jan 2024 15:28:40 +0100 Subject: [PATCH 1/2] new branch with alternative secret integer library --- .../fstar-secret-integers/Makefile.copy | 94 +++ proof-libs/fstar-secret-integers/README.md | 35 ++ .../core/Alloc.Alloc.fst | 3 + .../core/Alloc.Collections.Binary_heap.fsti | 28 + .../core/Alloc.Slice.fst | 5 + .../fstar-secret-integers/core/Alloc.Vec.fst | 36 ++ .../core/Core.Array.Iter.fsti | 5 + .../fstar-secret-integers/core/Core.Array.fst | 10 + .../fstar-secret-integers/core/Core.Clone.fst | 11 + .../fstar-secret-integers/core/Core.Cmp.fsti | 48 ++ .../core/Core.Convert.fst | 57 ++ .../core/Core.Iter.Adapters.Enumerate.fst | 5 + .../core/Core.Iter.Adapters.Step_by.fst | 9 + .../core/Core.Iter.Traits.Collect.fst | 14 + .../core/Core.Iter.Traits.Iterator.fst | 41 ++ .../fstar-secret-integers/core/Core.Iter.fsti | 116 ++++ .../core/Core.Marker.fst | 10 + .../core/Core.Num.Error.fsti | 4 + .../fstar-secret-integers/core/Core.Num.fsti | 45 ++ .../core/Core.Ops.Arith.Neg.fsti | 4 + .../core/Core.Ops.Arith.fsti | 16 + .../core/Core.Ops.Control_flow.fst | 6 + .../core/Core.Ops.Deref.fst | 3 + .../core/Core.Ops.Index.IndexMut.fst | 14 + .../core/Core.Ops.Index.fst | 8 + .../core/Core.Ops.Range.fsti | 131 ++++ .../core/Core.Ops.Try_trait.fst | 17 + .../fstar-secret-integers/core/Core.Ops.fst | 27 + .../core/Core.Option.fst | 13 + .../core/Core.Panicking.fst | 12 + .../core/Core.Result.fst | 7 + .../core/Core.Slice.Iter.fst | 8 + .../core/Core.Slice.fsti | 34 + .../core/Core.Str.Converts.fsti | 5 + .../core/Core.Str.Error.fsti | 3 + .../fstar-secret-integers/core/Core.Str.fsti | 6 + .../fstar-secret-integers/core/Core.fst | 8 + .../fstar-secret-integers/core/Makefile | 94 +++ .../fstar-secret-integers/core/README.md | 29 + .../fstar-secret-integers/hax_lib/Hax.Lib.fst | 27 + .../fstar-secret-integers/hax_lib/Makefile | 94 +++ .../rust_primitives/Makefile | 94 +++ .../Rust_primitives.Arrays.fst | 21 + .../Rust_primitives.Arrays.fsti | 91 +++ .../Rust_primitives.BitVectors.fst | 55 ++ .../Rust_primitives.BitVectors.fsti | 131 ++++ ...primitives.Hax.Monomorphized_update_at.fst | 30 + ...rimitives.Hax.Monomorphized_update_at.fsti | 58 ++ .../rust_primitives/Rust_primitives.Hax.fst | 48 ++ .../Rust_primitives.Integers.fst | 86 +++ .../Rust_primitives.Integers.fsti | 579 ++++++++++++++++++ .../Rust_primitives.Iterators.fsti | 63 ++ .../rust_primitives/Rust_primitives.fst | 27 + 53 files changed, 2425 insertions(+) create mode 100644 proof-libs/fstar-secret-integers/Makefile.copy create mode 100644 proof-libs/fstar-secret-integers/README.md create mode 100644 proof-libs/fstar-secret-integers/core/Alloc.Alloc.fst create mode 100644 proof-libs/fstar-secret-integers/core/Alloc.Collections.Binary_heap.fsti create mode 100644 proof-libs/fstar-secret-integers/core/Alloc.Slice.fst create mode 100644 proof-libs/fstar-secret-integers/core/Alloc.Vec.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Array.Iter.fsti create mode 100644 proof-libs/fstar-secret-integers/core/Core.Array.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Clone.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Cmp.fsti create mode 100644 proof-libs/fstar-secret-integers/core/Core.Convert.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Iter.Adapters.Enumerate.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Iter.Adapters.Step_by.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Iter.Traits.Collect.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Iter.Traits.Iterator.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Iter.fsti create mode 100644 proof-libs/fstar-secret-integers/core/Core.Marker.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Num.Error.fsti create mode 100644 proof-libs/fstar-secret-integers/core/Core.Num.fsti create mode 100644 proof-libs/fstar-secret-integers/core/Core.Ops.Arith.Neg.fsti create mode 100644 proof-libs/fstar-secret-integers/core/Core.Ops.Arith.fsti create mode 100644 proof-libs/fstar-secret-integers/core/Core.Ops.Control_flow.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Ops.Deref.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Ops.Index.IndexMut.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Ops.Index.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Ops.Range.fsti create mode 100644 proof-libs/fstar-secret-integers/core/Core.Ops.Try_trait.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Ops.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Option.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Panicking.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Result.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Slice.Iter.fst create mode 100644 proof-libs/fstar-secret-integers/core/Core.Slice.fsti create mode 100644 proof-libs/fstar-secret-integers/core/Core.Str.Converts.fsti create mode 100644 proof-libs/fstar-secret-integers/core/Core.Str.Error.fsti create mode 100644 proof-libs/fstar-secret-integers/core/Core.Str.fsti create mode 100644 proof-libs/fstar-secret-integers/core/Core.fst create mode 100644 proof-libs/fstar-secret-integers/core/Makefile create mode 100644 proof-libs/fstar-secret-integers/core/README.md create mode 100644 proof-libs/fstar-secret-integers/hax_lib/Hax.Lib.fst create mode 100644 proof-libs/fstar-secret-integers/hax_lib/Makefile create mode 100644 proof-libs/fstar-secret-integers/rust_primitives/Makefile create mode 100644 proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fst create mode 100644 proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fsti create mode 100644 proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.BitVectors.fst create mode 100644 proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.BitVectors.fsti create mode 100644 proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fst create mode 100644 proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fsti create mode 100644 proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Hax.fst create mode 100644 proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fst create mode 100644 proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fsti create mode 100644 proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Iterators.fsti create mode 100644 proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.fst diff --git a/proof-libs/fstar-secret-integers/Makefile.copy b/proof-libs/fstar-secret-integers/Makefile.copy new file mode 100644 index 000000000..bc9c0c8f4 --- /dev/null +++ b/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 "/bin/fstar.exe") +# (setq-default fstar-smt-executable "/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)/* diff --git a/proof-libs/fstar-secret-integers/README.md b/proof-libs/fstar-secret-integers/README.md new file mode 100644 index 000000000..bc9d4a9c4 --- /dev/null +++ b/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. + diff --git a/proof-libs/fstar-secret-integers/core/Alloc.Alloc.fst b/proof-libs/fstar-secret-integers/core/Alloc.Alloc.fst new file mode 100644 index 000000000..4c0870db2 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Alloc.Alloc.fst @@ -0,0 +1,3 @@ +module Alloc.Alloc + +let t_Global = () diff --git a/proof-libs/fstar-secret-integers/core/Alloc.Collections.Binary_heap.fsti b/proof-libs/fstar-secret-integers/core/Alloc.Collections.Binary_heap.fsti new file mode 100644 index 000000000..5c8875782 --- /dev/null +++ b/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)] + diff --git a/proof-libs/fstar-secret-integers/core/Alloc.Slice.fst b/proof-libs/fstar-secret-integers/core/Alloc.Slice.fst new file mode 100644 index 000000000..f9ea629b7 --- /dev/null +++ b/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 diff --git a/proof-libs/fstar-secret-integers/core/Alloc.Vec.fst b/proof-libs/fstar-secret-integers/core/Alloc.Vec.fst new file mode 100644 index 000000000..ef3dd3301 --- /dev/null +++ b/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); +} + diff --git a/proof-libs/fstar-secret-integers/core/Core.Array.Iter.fsti b/proof-libs/fstar-secret-integers/core/Core.Array.Iter.fsti new file mode 100644 index 000000000..b03e1e77c --- /dev/null +++ b/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 diff --git a/proof-libs/fstar-secret-integers/core/Core.Array.fst b/proof-libs/fstar-secret-integers/core/Core.Array.fst new file mode 100644 index 000000000..6e91fc6ca --- /dev/null +++ b/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 + diff --git a/proof-libs/fstar-secret-integers/core/Core.Clone.fst b/proof-libs/fstar-secret-integers/core/Core.Clone.fst new file mode 100644 index 000000000..a28310f3a --- /dev/null +++ b/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); +} + diff --git a/proof-libs/fstar-secret-integers/core/Core.Cmp.fsti b/proof-libs/fstar-secret-integers/core/Core.Cmp.fsti new file mode 100644 index 000000000..58fc8df97 --- /dev/null +++ b/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) diff --git a/proof-libs/fstar-secret-integers/core/Core.Convert.fst b/proof-libs/fstar-secret-integers/core/Core.Convert.fst new file mode 100644 index 000000000..785ee8add --- /dev/null +++ b/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; +} diff --git a/proof-libs/fstar-secret-integers/core/Core.Iter.Adapters.Enumerate.fst b/proof-libs/fstar-secret-integers/core/Core.Iter.Adapters.Enumerate.fst new file mode 100644 index 000000000..59a262a5b --- /dev/null +++ b/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 } + diff --git a/proof-libs/fstar-secret-integers/core/Core.Iter.Adapters.Step_by.fst b/proof-libs/fstar-secret-integers/core/Core.Iter.Adapters.Step_by.fst new file mode 100644 index 000000000..885d19d0e --- /dev/null +++ b/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; +} + diff --git a/proof-libs/fstar-secret-integers/core/Core.Iter.Traits.Collect.fst b/proof-libs/fstar-secret-integers/core/Core.Iter.Traits.Collect.fst new file mode 100644 index 000000000..9051db81f --- /dev/null +++ b/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; +} diff --git a/proof-libs/fstar-secret-integers/core/Core.Iter.Traits.Iterator.fst b/proof-libs/fstar-secret-integers/core/Core.Iter.Traits.Iterator.fst new file mode 100644 index 000000000..5a6c8b837 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Iter.Traits.Iterator.fst @@ -0,0 +1,41 @@ +module Core.Iter.Traits.Iterator +open Rust_primitives + +(*** Definition of the `iterator` trait *) +(** We define the types of the different method of the iterator trait +on their own. This is handy for revealing only certain fields of the +instances of the `iterator` trait. *) + +unfold type t_next self item + = self -> self * option item +unfold type t_contains self item + = self -> item -> Type0 +unfold type t_fold self (item: Type0) (contains: t_contains self item) + = #b:Type -> s:self -> b -> (b -> i:item{contains s i} -> b) -> b +unfold type t_enumerate self + = self -> Core.Iter.Adapters.Enumerate.t_Enumerate self +unfold type t_step_by self + = self -> usize -> Core.Iter.Adapters.Step_by.t_StepBy self +unfold type t_all self item + = self -> (item -> bool) -> self * bool + +(* Inference behaves strangly with type synonyms... :( *) +// class iterator (self: Type) = { +// f_Item: Type; +// f_next: t_next self f_Item; +// f_contains: t_contains self f_Item; (* hax-specific method *) +// f_fold: t_fold self f_Item f_contains; +// f_enumerate: t_enumerate self; +// } + +class iterator (self: Type u#0): Type u#1 = { + [@@@FStar.Tactics.Typeclasses.no_method] + f_Item: Type0; + f_next: self -> self * option f_Item; + f_contains: self -> f_Item -> Type0; + f_fold: #b:Type0 -> s:self -> b -> (b -> i:f_Item{f_contains s i} -> b) -> b; + f_enumerate: self -> Core.Iter.Adapters.Enumerate.t_Enumerate self; + f_step_by: self -> usize -> Core.Iter.Adapters.Step_by.t_StepBy self; + f_all: self -> (f_Item -> bool) -> self * bool; +} + diff --git a/proof-libs/fstar-secret-integers/core/Core.Iter.fsti b/proof-libs/fstar-secret-integers/core/Core.Iter.fsti new file mode 100644 index 000000000..ef2095e7f --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Iter.fsti @@ -0,0 +1,116 @@ +module Core.Iter + +open Rust_primitives + +open Core.Iter.Traits.Iterator + +(*** Instances for the `iterator` trait *) + +(**** Enumerate *) +(** This lives in this file for cyclic dependencies reasons. *) + +val iterator_enumerate_contains it (i: iterator it) + : t_contains (Core.Iter.Adapters.Enumerate.t_Enumerate it) (usize * i.f_Item) +val iterator_enumerate_fold it (i: iterator it) + : t_fold (Core.Iter.Adapters.Enumerate.t_Enumerate it) (usize * i.f_Item) (iterator_enumerate_contains it i) +val iterator_enumerate_enumerate it + : t_enumerate (Core.Iter.Adapters.Enumerate.t_Enumerate it) +val iterator_enumerate_all it (i: iterator it) + : t_all (Core.Iter.Adapters.Enumerate.t_Enumerate it) (usize * i.f_Item) +val iterator_enumerate_step_by it + : t_step_by (Core.Iter.Adapters.Enumerate.t_Enumerate it) + +instance iterator_enumerate it {| i: iterator it |}: iterator (Core.Iter.Adapters.Enumerate.t_Enumerate it) = + let open Core.Iter.Adapters.Enumerate in + { + f_Item = (usize * i.f_Item); + f_next = (fun {iter; count} -> + let open Core.Ops in + let iter, opt = f_next iter in + match opt with + | Some value -> if v count = max_usize + then {iter; count }, None + else {iter; count = count +. sz 1}, Some (count, value) + | None -> {iter; count}, None + ); + f_contains = iterator_enumerate_contains it i; + f_fold = iterator_enumerate_fold it i; + f_enumerate = iterator_enumerate_enumerate it; + f_step_by = iterator_enumerate_step_by it; + f_all = iterator_enumerate_all it i; + } + +(**** Step_by *) +(** This lives in this file for cyclic dependencies reasons. *) + +val iterator_step_by_contains it (i: iterator it) + : t_contains (Core.Iter.Adapters.Step_by.t_StepBy it) i.f_Item +val iterator_step_by_fold it (i: iterator it) + : t_fold (Core.Iter.Adapters.Step_by.t_StepBy it) i.f_Item (iterator_step_by_contains it i) +val iterator_step_by_next it (i: iterator it) + : t_next (Core.Iter.Adapters.Step_by.t_StepBy it) i.f_Item +val iterator_step_by_enumerate it + : t_enumerate (Core.Iter.Adapters.Step_by.t_StepBy it) +val iterator_step_by_all it (i: iterator it) + : t_all (Core.Iter.Adapters.Step_by.t_StepBy it) i.f_Item +val iterator_step_by_step_by it + : t_step_by (Core.Iter.Adapters.Step_by.t_StepBy it) + +unfold instance iterator_step_by it {| i: iterator it |}: iterator (Core.Iter.Adapters.Step_by.t_StepBy it) = + let open Core.Iter.Adapters.Enumerate in + { + f_Item = i.f_Item; + f_next = iterator_step_by_next it i; + f_contains = iterator_step_by_contains it i; + f_fold = iterator_step_by_fold it i; + f_enumerate = iterator_step_by_enumerate it ; + f_step_by = iterator_step_by_step_by it ; + f_all = iterator_step_by_all it i; + } + +(**** Slice *) +(** Slices are not iterable as such in Rust. We ignore this indirection here. *) +open Core.Ops.Range + +val iterator_slice_next t: t_next (t_Slice t) t +unfold +let iterator_slice_contains (t: eqtype): t_contains (t_Slice t) t + = fun s x -> Rust_primitives.Arrays.contains s x +val iterator_slice_fold (t: eqtype): t_fold (t_Slice t) t (iterator_slice_contains t) +val iterator_slice_enumerate (t: eqtype): t_enumerate (t_Slice t) +val iterator_slice_step_by (t: eqtype): t_step_by (t_Slice t) +val iterator_slice_all (t: eqtype): t_all (t_Slice t) t + +instance iterator_slice (t: eqtype): iterator (t_Slice t) = { + f_Item = t; + f_next = iterator_slice_next t; + // size_hint = (fun s -> Some (Rust_primitives.Arrays.length s)); + f_contains = iterator_slice_contains t; + f_fold = iterator_slice_fold t; + f_enumerate = iterator_slice_enumerate t; + f_step_by = iterator_slice_step_by t; + f_all = iterator_slice_all t; +} + +(**** Array *) +(** Arrays are not iterable as such in Rust. We ignore this indirection here. *) +val iterator_array_next t len: t_next (t_Array t len) t +unfold +let iterator_array_contains (t: eqtype) len: t_contains (t_Array t len) t + = fun s x -> Rust_primitives.Arrays.contains s x +val iterator_array_fold (t: eqtype) len: t_fold (t_Array t len) t (iterator_array_contains t len) +val iterator_array_enumerate (t: eqtype) len: t_enumerate (t_Array t len) +val iterator_array_step_by (t: eqtype) len: t_step_by (t_Array t len) +val iterator_array_all (t: eqtype) len: t_all (t_Array t len) t + +instance iterator_array (t: eqtype) len: iterator (t_Array t len) = { + f_Item = t; + f_next = iterator_array_next t len; + // size_hint = (fun (_s: t_Array t len) -> Some len); + f_contains = iterator_array_contains t len; + f_fold = iterator_array_fold t len; + f_enumerate = iterator_array_enumerate t len; + f_step_by = iterator_array_step_by t len; + f_all = iterator_array_all t len; +} + diff --git a/proof-libs/fstar-secret-integers/core/Core.Marker.fst b/proof-libs/fstar-secret-integers/core/Core.Marker.fst new file mode 100644 index 000000000..0ceacbe99 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Marker.fst @@ -0,0 +1,10 @@ +module Core.Marker + +class t_Sized (h: Type) = { + dummy_field: unit +} + +(** we consider everything to be sized *) +instance t_Sized_all t: t_Sized t = { + dummy_field = () +} diff --git a/proof-libs/fstar-secret-integers/core/Core.Num.Error.fsti b/proof-libs/fstar-secret-integers/core/Core.Num.Error.fsti new file mode 100644 index 000000000..31d75bbc1 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Num.Error.fsti @@ -0,0 +1,4 @@ +module Core.Num.Error +open Rust_primitives + +type t_ParseIntError = unit diff --git a/proof-libs/fstar-secret-integers/core/Core.Num.fsti b/proof-libs/fstar-secret-integers/core/Core.Num.fsti new file mode 100644 index 000000000..e5d1c9b22 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Num.fsti @@ -0,0 +1,45 @@ +module Core.Num +open Rust_primitives + +let impl__u8__wrapping_sub: u8 -> u8 -> u8 = sub_mod +let impl__u16__wrapping_add: u16 -> u16 -> u16 = add_mod +let impl__i32__wrapping_add: i32 -> i32 -> i32 = add_mod +let impl__i32__abs (a:i32{minint i32_inttype < v a}) : i32 = abs_int a + +let impl__u32__wrapping_add: u32 -> u32 -> u32 = add_mod +val impl__u32__rotate_left: u32 -> u32 -> u32 +val impl__u32__from_le_bytes: t_Array u8 (sz 4) -> u32 +val impl__u32__from_be_bytes: t_Array u8 (sz 4) -> u32 +val impl__u32__to_le_bytes: u32 -> t_Array u8 (sz 4) +val impl__u32__to_be_bytes: u32 -> t_Array u8 (sz 4) +val impl__u32__rotate_right: u32 -> u32 -> u32 +let impl__u32__BITS: u32 = classify (32ul <: pub_int_t u32_inttype) + +let impl__u64__wrapping_add: u64 -> u64 -> u64 = add_mod +val impl__u64__rotate_left: u32 -> u32 -> u32 +val impl__u64__from_le_bytes: t_Array u8 (sz 8) -> u64 +val impl__u64__from_be_bytes: t_Array u8 (sz 8) -> u64 +val impl__u64__to_le_bytes: u64 -> t_Array u8 (sz 8) +val impl__u64__to_be_bytes: u64 -> t_Array u8 (sz 8) +val impl__u64__rotate_right: u64 -> u64 -> u64 + +let impl__u128__wrapping_add (x: u128) (y: u128): u128 = add_mod x y //FStar.UInt128.add_underspec x y +val impl__u128__rotate_left: u128 -> u128 -> u128 +val impl__u128__from_le_bytes: t_Array u8 (sz 16) -> u128 +val impl__u128__from_be_bytes: t_Array u8 (sz 16) -> u128 +val impl__u128__to_le_bytes: u128 -> t_Array u8 (sz 16) +val impl__u128__to_be_bytes: u128 -> t_Array u8 (sz 16) +val impl__u128__rotate_right: u128 -> u128 -> u128 + +val impl__u8__pow: u8 -> u32 -> u8 +val impl__u16__pow (base: u16) (exponent: u32): result : u16 {v base == 2 /\ v exponent < 16 ==> result == mk_int #Lib.IntTypes.U16 (pow2 (v exponent))} +val impl__u32__pow (base: u32) (exponent: u32): result : u32 {v base == 2 /\ v exponent <= 16 ==> result == mk_int #Lib.IntTypes.U32 (pow2 (v exponent))} +val impl__u64__pow: u64 -> u32 -> u64 +val impl__u128__pow: u128 -> u32 -> u128 +val impl__i32__pow (base: i32) (exponent: u32): result: i32 {v base == 2 /\ v exponent <= 16 ==> result == mk_int #Lib.IntTypes.S32 (pow2 (v exponent))} + +val impl__u8__from_str_radix: string -> u32 -> Core.Result.t_Result u8 Core.Num.Error.t_ParseIntError + +val impl__usize__ilog2: i32 -> u32 + + diff --git a/proof-libs/fstar-secret-integers/core/Core.Ops.Arith.Neg.fsti b/proof-libs/fstar-secret-integers/core/Core.Ops.Arith.Neg.fsti new file mode 100644 index 000000000..c3eae7c30 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Ops.Arith.Neg.fsti @@ -0,0 +1,4 @@ +module Core.Ops.Arith.Neg +open Rust_primitives + +let neg #t #l (x:int_t_l t l) = zero #t #l -! x diff --git a/proof-libs/fstar-secret-integers/core/Core.Ops.Arith.fsti b/proof-libs/fstar-secret-integers/core/Core.Ops.Arith.fsti new file mode 100644 index 000000000..8ebc5c42a --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Ops.Arith.fsti @@ -0,0 +1,16 @@ +module Core.Ops.Arith +open Rust_primitives + + +class t_Add self rhs = { + add_output: Type; + add_in_bounds: self -> rhs -> Type0; + ( +! ): x:self -> y:rhs {add_in_bounds x y} -> add_output; +} + +class t_Sub self rhs = { + sub_output: Type; + sub_in_bounds: self -> rhs -> Type0; + ( -! ): x:self -> y:rhs {sub_in_bounds x y} -> sub_output; +} + diff --git a/proof-libs/fstar-secret-integers/core/Core.Ops.Control_flow.fst b/proof-libs/fstar-secret-integers/core/Core.Ops.Control_flow.fst new file mode 100644 index 000000000..5898e359e --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Ops.Control_flow.fst @@ -0,0 +1,6 @@ +module Core.Ops.Control_flow + +type t_ControlFlow (b c: Type) = + | ControlFlow_Continue of c + | ControlFlow_Break of b + diff --git a/proof-libs/fstar-secret-integers/core/Core.Ops.Deref.fst b/proof-libs/fstar-secret-integers/core/Core.Ops.Deref.fst new file mode 100644 index 000000000..c99ea9e6d --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Ops.Deref.fst @@ -0,0 +1,3 @@ +module Core.Ops.Deref + +let f_deref = id diff --git a/proof-libs/fstar-secret-integers/core/Core.Ops.Index.IndexMut.fst b/proof-libs/fstar-secret-integers/core/Core.Ops.Index.IndexMut.fst new file mode 100644 index 000000000..486a16af9 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Ops.Index.IndexMut.fst @@ -0,0 +1,14 @@ +module Core.Ops.Index.IndexMut + +class t_IndexMut t_Self t_Idx = { + f_Input: Type; + in_range: t_Self -> t_Idx -> Type0; + f_index_mut: s:t_Self -> i:t_Idx{in_range s i} -> v:f_Input -> t_Self; +} + +open Rust_primitives +instance impl__index_mut t l n: t_IndexMut (t_Array t l) (int_t n) + = { f_Input = t; + in_range = (fun (s: t_Array t l) (i: int_t n) -> v i >= 0 && v i < v l); + f_index_mut = (fun s i x -> Seq.upd s (v i) x); + } diff --git a/proof-libs/fstar-secret-integers/core/Core.Ops.Index.fst b/proof-libs/fstar-secret-integers/core/Core.Ops.Index.fst new file mode 100644 index 000000000..cfc366569 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Ops.Index.fst @@ -0,0 +1,8 @@ +module Core.Ops.Index + +class t_Index t_Self t_Idx = { + f_Output: Type; + in_range: t_Self -> t_Idx -> Type0; + f_index: s:t_Self -> i:t_Idx{in_range s i} -> f_Output; +} + diff --git a/proof-libs/fstar-secret-integers/core/Core.Ops.Range.fsti b/proof-libs/fstar-secret-integers/core/Core.Ops.Range.fsti new file mode 100644 index 000000000..5550fb88f --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Ops.Range.fsti @@ -0,0 +1,131 @@ +module Core.Ops.Range +open Rust_primitives + +type t_RangeTo (t: Type) = {f_end: t} +type t_RangeFrom (t: Type) = {f_start: t} +type t_Range (t: Type) = {f_start: t; f_end: t} +type t_RangeFull = | RangeFull + +open Core.Iter.Traits.Iterator +module LI = Lib.IntTypes + +let rec fold_range' #t + (min: Rust_primitives.pub_int_t t) (max: Rust_primitives.pub_int_t t{v min <= v max}) + (init: 'a) (f: ('a -> i:Rust_primitives.pub_int_t t{v i < v max /\ v i >= v min} -> 'a)) + : Tot 'a (decreases (v max - v min)) + = if min =. max + then init + else fold_range' (add min (Rust_primitives.mk_int_l #_ #LI.PUB 1)) max (f init min) f + +val iterator_range_enumerate t: t_enumerate (t_Range (Rust_primitives.pub_int_t t)) +val iterator_range_step_by t: t_step_by (t_Range (Rust_primitives.pub_int_t t)) +val iterator_range_all t: t_all (t_Range (Rust_primitives.pub_int_t t)) (Rust_primitives.pub_int_t t) + +instance iterator_range t: iterator (t_Range (Rust_primitives.pub_int_t t)) = + { f_Item = Rust_primitives.pub_int_t t; + f_next = (fun {f_start; f_end} -> + if f_start >=. f_end then ({f_start; f_end}, None) + else ({f_start = f_start +. Rust_primitives.mk_pub_int 0; f_end}, Some f_start) + ); + f_contains = (fun x i -> v i < v x.f_end /\ v i >= v x.f_start); + f_fold = (fun #b r init f -> if r.f_start >=. r.f_end then init + else fold_range' r.f_start r.f_end init (fun x i -> f x i)); + f_enumerate = iterator_range_enumerate t; + f_step_by = iterator_range_step_by t; + f_all = iterator_range_all t; + } + +open Core.Ops.Index + +instance impl_index_range_slice t n : t_Index (t_Slice t) (t_Range (pub_int_t n)) + = { f_Output = t_Slice t + ; in_range = (fun (s: t_Slice t) {f_start; f_end} -> + let len = Rust_primitives.length s in + v f_start >= 0 /\ v f_start <= v len /\ v f_end <= v len) + ; f_index = (fun s {f_start; f_end} -> + if f_start <. f_end then Seq.slice s (v f_start) (v f_end) + else Seq.empty)} + +instance impl_index_range_to_slice t n : t_Index (t_Slice t) (t_RangeTo (pub_int_t n)) + = { f_Output = t_Slice t + ; in_range = (fun (s: t_Slice t) ({f_end}: t_RangeTo (pub_int_t n)) -> + let len = Rust_primitives.length s in v f_end <= v len) + ; f_index = (fun s {f_end} -> if 0 < v f_end then Seq.slice s 0 (v f_end) else Seq.empty)} + +instance impl_index_range_from_slice t n : t_Index (t_Slice t) (t_RangeFrom (pub_int_t n)) + = { f_Output = t_Slice t + ; in_range = (fun (s: t_Slice t) ({f_start}: t_RangeFrom (pub_int_t n)) -> + let len = Rust_primitives.length s in v f_start >= 0 /\ v f_start <= v len) + ; f_index = (fun s {f_start} -> + let len = Rust_primitives.length s in + if v f_start = v len then Seq.empty else Seq.slice s (v f_start) (v len))} + +instance impl_index_range_full_slice t : t_Index (t_Slice t) t_RangeFull + = { f_Output = t_Slice t + ; in_range = (fun (s: t_Slice t) _ -> True) + ; f_index = (fun s _ -> s)} + +instance impl_range_index_array t len n : t_Index (t_Array t len) (t_Range (pub_int_t n)) = + let i = impl_index_range_slice t n in + { f_Output = i.f_Output + ; in_range = (fun (s: t_Array t len) r -> i.in_range s r) + ; f_index = (fun s r -> i.f_index s r) } + +instance impl_range_to_index_array t len n : t_Index (t_Array t len) (t_RangeTo (pub_int_t n)) = + let i = impl_index_range_to_slice t n in + { f_Output = i.f_Output + ; in_range = (fun (s: t_Array t len) r -> i.in_range s r) + ; f_index = (fun s r -> i.f_index s r) } + +instance impl_range_from_index_array t len n : t_Index (t_Array t len) (t_RangeFrom (pub_int_t n)) = + let i = impl_index_range_from_slice t n in + { f_Output = i.f_Output + ; in_range = (fun (s: t_Array t len) r -> i.in_range s r) + ; f_index = (fun s r -> i.f_index s r) } + +instance impl_range_full_index_array t len : t_Index (t_Array t len) t_RangeFull = + let i = impl_index_range_full_slice t in + { f_Output = i.f_Output + ; in_range = (fun (s: t_Array t len) r -> i.in_range s r) + ; f_index = (fun s r -> i.f_index s r) } + +open Rust_primitives.Hax + +let update_at_tc_array_range_super t l n: t_Index (t_Array t l) (t_Range (pub_int_t n)) + = FStar.Tactics.Typeclasses.solve +let update_at_tc_array_range_to_super t l n: t_Index (t_Array t l) (t_RangeTo (pub_int_t n)) + = FStar.Tactics.Typeclasses.solve +let update_at_tc_array_range_from_super t l n: t_Index (t_Array t l) (t_RangeFrom (pub_int_t n)) + = FStar.Tactics.Typeclasses.solve +let update_at_tc_array_range_full_super t l n: t_Index (t_Array t l) t_RangeFull + = FStar.Tactics.Typeclasses.solve + +val update_at_array_range t l n + (s: t_Array t l) (i: t_Range (pub_int_t n) {(update_at_tc_array_range_super t l n).in_range s i}) + : (update_at_tc_array_range_super t l n).f_Output -> t_Array t l +val update_at_array_range_to t l n + (s: t_Array t l) (i: t_RangeTo (pub_int_t n) {(update_at_tc_array_range_to_super t l n).in_range s i}) + : (update_at_tc_array_range_to_super t l n).f_Output -> t_Array t l +val update_at_array_range_from t l n + (s: t_Array t l) (i: t_RangeFrom (pub_int_t n) {(update_at_tc_array_range_from_super t l n).in_range s i}) + : (update_at_tc_array_range_from_super t l n).f_Output -> t_Array t l +val update_at_array_range_full t l n + (s: t_Array t l) (i: t_RangeFull) + : (update_at_tc_array_range_full_super t l n).f_Output -> t_Array t l + +instance update_at_tc_array_range t l n: update_at_tc (t_Array t l) (t_Range (pub_int_t n)) = { + super_index = update_at_tc_array_range_super t l n; + update_at = update_at_array_range t l n +} +instance update_at_tc_array_range_to t l n: update_at_tc (t_Array t l) (t_RangeTo (pub_int_t n)) = { + super_index = update_at_tc_array_range_to_super t l n; + update_at = update_at_array_range_to t l n +} +instance update_at_tc_array_range_from t l n: update_at_tc (t_Array t l) (t_RangeFrom (pub_int_t n)) = { + super_index = update_at_tc_array_range_from_super t l n; + update_at = update_at_array_range_from t l n +} +instance update_at_tc_array_range_full t l n: update_at_tc (t_Array t l) t_RangeFull = { + super_index = update_at_tc_array_range_full_super t l n; + update_at = update_at_array_range_full t l n +} diff --git a/proof-libs/fstar-secret-integers/core/Core.Ops.Try_trait.fst b/proof-libs/fstar-secret-integers/core/Core.Ops.Try_trait.fst new file mode 100644 index 000000000..871d2651a --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Ops.Try_trait.fst @@ -0,0 +1,17 @@ +module Core.Ops.Try_trait + +class t_FromResidual self r = { + f_from_residual: r -> self; +} + +class t_Try self = { + f_Output: Type; + f_Residual: Type; + [@@@FStar.Tactics.Typeclasses.tcresolve] + parent_FromResidual: t_FromResidual f_Residual f_Residual; + + f_from_output: f_Output -> self; + f_branch: self -> Core.Ops.Control_flow.t_ControlFlow f_Residual f_Output; +} + + diff --git a/proof-libs/fstar-secret-integers/core/Core.Ops.fst b/proof-libs/fstar-secret-integers/core/Core.Ops.fst new file mode 100644 index 000000000..a1110181f --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Ops.fst @@ -0,0 +1,27 @@ +module Core.Ops +open Rust_primitives + +// class add_tc self rhs = { +// output: Type; +// in_bounds: self -> rhs -> Type0; +// ( +! ): x:self -> y:rhs {in_bounds x y} -> output; +// } + +class negation_tc self = { + ( ~. ): self -> self; +} + +instance negation_for_integers #t: negation_tc (int_t t) = { + ( ~. ) = fun x -> lognot x +} + +instance negation_for_bool: negation_tc bool = { + ( ~. ) = not +} + +open Core.Ops.Index + +let ( .[] ) #self #idx {| inst: t_Index self idx |} + : s:self -> i:idx{in_range s i} -> inst.f_Output + = f_index + diff --git a/proof-libs/fstar-secret-integers/core/Core.Option.fst b/proof-libs/fstar-secret-integers/core/Core.Option.fst new file mode 100644 index 000000000..485742318 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Option.fst @@ -0,0 +1,13 @@ +module Core.Option + +type t_Option t = | Option_Some of t | Option_None + +let impl__and_then (self: t_Option 'self) (f: 'self -> t_Option 't): t_Option 't = + match self with + | Option_Some x -> f x + | Option_None -> Option_None + +let impl__unwrap #t (x: t_Option t {Option_Some? x}): t = Option_Some?._0 x + +let impl__is_some (self: t_Option 'self): bool = Option_Some? self + diff --git a/proof-libs/fstar-secret-integers/core/Core.Panicking.fst b/proof-libs/fstar-secret-integers/core/Core.Panicking.fst new file mode 100644 index 000000000..7b2c06d57 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Panicking.fst @@ -0,0 +1,12 @@ +module Core.Panicking + +open Rust_primitives +open Rust_primitives.Hax + +type t_AssertKind = | AssertKind_Eq + +let panic (message: string {False}): t_Never + = match () with + +let assert_failed (k: t_AssertKind) x y (z: Core.Option.t_Option unit {False}): t_Never + = match () with diff --git a/proof-libs/fstar-secret-integers/core/Core.Result.fst b/proof-libs/fstar-secret-integers/core/Core.Result.fst new file mode 100644 index 000000000..557bbeaa6 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Result.fst @@ -0,0 +1,7 @@ +module Core.Result + +type t_Result t e = | Result_Ok: v:t -> t_Result t e + | Result_Err of e + +let impl__unwrap (x: t_Result 't 'e {Result_Ok? x}): 't = Result_Ok?.v x + diff --git a/proof-libs/fstar-secret-integers/core/Core.Slice.Iter.fst b/proof-libs/fstar-secret-integers/core/Core.Slice.Iter.fst new file mode 100644 index 000000000..23eb3b734 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Slice.Iter.fst @@ -0,0 +1,8 @@ +module Core.Slice.Iter + +open Rust_primitives + +unfold let t_Chunks a = t_Slice (t_Slice a) +unfold let t_ChunksExact a = t_Slice (t_Slice a) +unfold let t_Iter a = t_Slice a + diff --git a/proof-libs/fstar-secret-integers/core/Core.Slice.fsti b/proof-libs/fstar-secret-integers/core/Core.Slice.fsti new file mode 100644 index 000000000..cff5480cf --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Slice.fsti @@ -0,0 +1,34 @@ +module Core.Slice +open Rust_primitives.Arrays +open Rust_primitives.Integers + +let impl__len (#t: Type) (s: t_Slice t) + : len: usize {len == sz (Seq.length s)} = + sz (Seq.length s) + +open Core.Slice.Iter + +val impl__chunks (x: t_Slice 'a) (cs: usize): t_Chunks 'a + +let impl__iter (s: t_Slice 't): t_Slice 't = s + +val impl__chunks_exact (x: t_Slice 'a) (cs: usize): + Pure (t_Slice (t_Slice 'a)) + (requires True) + (ensures (fun r -> forall i. i < v (length x) ==> length x == cs)) + +open Core.Ops.Index + +instance impl__index t n: t_Index (t_Slice t) (int_t n) + = { f_Output = t; + in_range = (fun (s: t_Slice t) (i: int_t n) -> v i >= 0 && v i < v (length s)); + f_index = (fun s i -> Seq.index s (v i)); + } + +let impl__copy_from_slice #t (x: t_Slice t) (y:t_Slice t) : t_Slice t = y + +val impl__split_at #t (s: t_Slice t) (mid: usize): Pure (t_Slice t * t_Slice t) + (requires (v mid <= Seq.length s)) + (ensures (fun (x,y) -> Seq.length x == v mid /\ Seq.length y == Seq.length s - v mid /\ + x == Seq.slice s 0 (v mid) /\ y == Seq.slice s (v mid) (Seq.length s) /\ + s == Seq.append x y)) diff --git a/proof-libs/fstar-secret-integers/core/Core.Str.Converts.fsti b/proof-libs/fstar-secret-integers/core/Core.Str.Converts.fsti new file mode 100644 index 000000000..fb097a1fd --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Str.Converts.fsti @@ -0,0 +1,5 @@ +module Core.Str.Converts +open Rust_primitives + +val from_utf8 (s: t_Slice u8): Core.Result.t_Result string Core.Str.Error.t_Utf8Error + diff --git a/proof-libs/fstar-secret-integers/core/Core.Str.Error.fsti b/proof-libs/fstar-secret-integers/core/Core.Str.Error.fsti new file mode 100644 index 000000000..3f0086063 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Str.Error.fsti @@ -0,0 +1,3 @@ +module Core.Str.Error + +type t_Utf8Error = unit diff --git a/proof-libs/fstar-secret-integers/core/Core.Str.fsti b/proof-libs/fstar-secret-integers/core/Core.Str.fsti new file mode 100644 index 000000000..2fb541709 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.Str.fsti @@ -0,0 +1,6 @@ +module Core.Str +open Rust_primitives + +val impl__str__len: string -> usize +val impl__str__as_bytes: string -> t_Slice u8 + diff --git a/proof-libs/fstar-secret-integers/core/Core.fst b/proof-libs/fstar-secret-integers/core/Core.fst new file mode 100644 index 000000000..6b279f8db --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Core.fst @@ -0,0 +1,8 @@ +module Core + +include Rust_primitives +include Core.Num +include Core.Iter +include Core.Ops + + diff --git a/proof-libs/fstar-secret-integers/core/Makefile b/proof-libs/fstar-secret-integers/core/Makefile new file mode 100644 index 000000000..bc9c0c8f4 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/Makefile @@ -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 "/bin/fstar.exe") +# (setq-default fstar-smt-executable "/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)/* diff --git a/proof-libs/fstar-secret-integers/core/README.md b/proof-libs/fstar-secret-integers/core/README.md new file mode 100644 index 000000000..5164f0279 --- /dev/null +++ b/proof-libs/fstar-secret-integers/core/README.md @@ -0,0 +1,29 @@ +# Core (and alloc) library + +This directory contains a model for the [Core Rust +library](https://doc.rust-lang.org/core/): the minimal Rust foundation +behind the [standard libarary of +Rust](https://doc.rust-lang.org/std/index.html). This also includes a +model for some part of the [`alloc` Rust +library](https://doc.rust-lang.org/stable/alloc/). + +Core is self-contained, and is dependency-free: it links to no +upstream or system libraries. Thus, even if it is minimal, it is not +small: it is around **75k LoC**, comments excluded. + +In this directory, you will find the first stage of our approach to +`core` in F\*: a hand-written model. Note that this model tries to +follow as much as possible the structure and naming found in the Rust +core library. + +The second stage of our approach to `core` is automatic generation +with specifications and models. +Our plan is to annotate the Rust `core` library with specifications +and models written directly as Rust annotations. +This will enable automatic generation of `core` models with consistent +semantics in all of hax backends (for now F\* and Coq). + +Note that we already started experimenting with this second approach: +hax is already able to digest and generate signature-only F\* for +more than 80% of core definitions. + diff --git a/proof-libs/fstar-secret-integers/hax_lib/Hax.Lib.fst b/proof-libs/fstar-secret-integers/hax_lib/Hax.Lib.fst new file mode 100644 index 000000000..dd7aa4d30 --- /dev/null +++ b/proof-libs/fstar-secret-integers/hax_lib/Hax.Lib.fst @@ -0,0 +1,27 @@ +module Hax.Lib +open Rust_primitives.Integers +open Rust_primitives.Arrays +open Core.Array + +type bounded_index (max: usize) = + | Bounded: n: usize {v n < v max} -> bounded_index max + +instance index_bounded_index_array + t (len: usize) + : index (array t len) (bounded_index len) + = let tc = index_array t len in + { + output = tc.output; + in_range = (fun (_: array t len) (_: bounded_index len) -> true); + (.[]) = (fun (s: array t len) (Bounded i) -> s.[i]) + } + +instance update_at_bounded_index_array + t (len: usize) + : update_at (array t len) (bounded_index len) + = let super_index = index_bounded_index_array t len in + { + super_index; + (.[]<-) = (fun (s: array t len) (Bounded i) x -> s.[i] <- x) + } + diff --git a/proof-libs/fstar-secret-integers/hax_lib/Makefile b/proof-libs/fstar-secret-integers/hax_lib/Makefile new file mode 100644 index 000000000..bc9c0c8f4 --- /dev/null +++ b/proof-libs/fstar-secret-integers/hax_lib/Makefile @@ -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 "/bin/fstar.exe") +# (setq-default fstar-smt-executable "/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)/* diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Makefile b/proof-libs/fstar-secret-integers/rust_primitives/Makefile new file mode 100644 index 000000000..bc9c0c8f4 --- /dev/null +++ b/proof-libs/fstar-secret-integers/rust_primitives/Makefile @@ -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 "/bin/fstar.exe") +# (setq-default fstar-smt-executable "/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)/* diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fst b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fst new file mode 100644 index 000000000..42b6255de --- /dev/null +++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fst @@ -0,0 +1,21 @@ +module Rust_primitives.Arrays + +open Rust_primitives.Integers + +let of_list (#t:Type) (l: list t {FStar.List.Tot.length l < maxint Lib.IntTypes.U16}): t_Slice t = Seq.seq_of_list l +let to_list (#t:Type) (s: t_Slice t): list t = Seq.seq_to_list s + +let to_of_list_lemma t l = Seq.lemma_list_seq_bij l +let of_to_list_lemma t l = Seq.lemma_seq_list_bij l + +let map_array #n (arr: t_Array 'a n) (f: 'a -> 'b): t_Array 'b n + = FStar.Seq.map_seq_len f arr; + FStar.Seq.map_seq f arr + +let createi #t l f = admit() + +let lemma_index_concat x y i = admit() + +let lemma_index_slice x y i = admit() + +let eq_intro a b = admit() diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fsti b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fsti new file mode 100644 index 000000000..68c03a4e1 --- /dev/null +++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fsti @@ -0,0 +1,91 @@ +module Rust_primitives.Arrays + +open Rust_primitives.Integers + +type t_Slice t = s:Seq.seq t{Seq.length s <= max_usize} +type t_Array t (l:usize) = s: Seq.seq t { Seq.length s == v l } +let length (s: t_Slice 'a): usize = sz (Seq.length s) +let contains (#t: eqtype) (s: t_Slice t) (x: t): bool = Seq.mem x s + + +val of_list (#t:Type) (l: list t {FStar.List.Tot.length l < maxint Lib.IntTypes.U16}): + t_Array t (sz (FStar.List.Tot.length l)) +val to_list (#t:Type) (s: t_Slice t): list t + +val map_array #n (arr: t_Array 'a n) (f: 'a -> 'b): t_Array 'b n + +val createi #t (l:usize) (f:(u:usize{u <. l} -> t)) + : Pure (t_Array t l) + (requires True) + (ensures (fun res -> (forall i. Seq.index res (v i) == f i))) + +unfold let map #p + (f:(x:'a{p x} -> 'b)) + (s: t_Slice 'a {forall (i:nat). i < Seq.length s ==> p (Seq.index s i)}): t_Slice 'b + = createi (length s) (fun i -> f (Seq.index s (v i))) + +let concat #t (x:t_Slice t) (y:t_Slice t{range (v (length x) + v (length y)) usize_inttype}) : + r:t_Array t (length x +! length y) = Seq.append x y + +val lemma_index_concat #t (x:t_Slice t) (y:t_Slice t{range (v (length x) + v (length y)) usize_inttype}) (i:usize{i <. length x +! length y}): + Lemma (if i <. length x then + Seq.index (concat x y) (v i) == Seq.index x (v i) + else + Seq.index (concat x y) (v i) == Seq.index y (v (i -! length x))) + [SMTPat (Seq.index (concat #t x y) i)] + +let slice #t (x:t_Slice t) (i:usize{i <=. length x}) (j:usize{i <=. j /\ j <=. length x}): + r:t_Array t (j -! i) = Seq.slice x (v i) (v j) + +val lemma_index_slice #t (x:t_Slice t) (i:usize{i <=. length x}) (j:usize{i <=. j /\ j <=. length x}) + (k:usize{k <. j -! i}): + Lemma (Seq.index (slice x i j) (v k) == Seq.index x (v (i +! k))) + [SMTPat (Seq.index (slice x i j) (v k))] + +val eq_intro #t (a : Seq.seq t) (b:Seq.seq t{Seq.length a == Seq.length b}): + Lemma + (requires forall i. {:pattern Seq.index a i; Seq.index b i} + i < Seq.length a ==> + Seq.index a i == Seq.index b i) + (ensures Seq.equal a b) + [SMTPat (Seq.equal a b)] + +let split #t (a:t_Slice t) (m:usize{m <=. length a}): + Pure (t_Array t m & t_Array t (length a -! m)) + True (ensures (fun (x,y) -> + x == slice a (sz 0) m /\ + y == slice a m (length a) /\ + concat #t x y == a)) = + let x = Seq.slice a 0 (v m) in + let y = Seq.slice a (v m) (Seq.length a) in + assert (Seq.equal a (concat x y)); + (x,y) + +let lemma_slice_append #t (x:t_Slice t) (y:t_Slice t) (z:t_Slice t): + Lemma (requires (range (v (length y) + v (length z)) usize_inttype /\ + length y +! length z == length x /\ + y == slice x (sz 0) (length y) /\ + z == slice x (length y) (length x))) + (ensures (x == concat y z)) = + assert (Seq.equal x (concat y z)) + +let lemma_slice_append_3 #t (x:t_Slice t) (y:t_Slice t) (z:t_Slice t) (w:t_Slice t): + Lemma (requires (range (v (length y) + v (length z) + v (length w)) usize_inttype /\ + length y +! length z +! length w == length x /\ + y == slice x (sz 0) (length y) /\ + z == slice x (length y) (length y +! length z) /\ + w == slice x (length y +! length z) (length x))) + (ensures (x == concat y (concat z w))) = + assert (Seq.equal x (Seq.append y (Seq.append z w))) + +let lemma_slice_append_4 #t (x y z w u:t_Slice t) : + Lemma (requires (range (v (length y) + v (length z) + v (length w) + v (length u)) usize_inttype /\ + length y +! length z +! length w +! length u == length x /\ + y == slice x (sz 0) (length y) /\ + z == slice x (length y) (length y +! length z) /\ + w == slice x (length y +! length z) (length y +! length z +! length w) /\ + u == slice x (length y +! length z +! length w) (length x))) + (ensures (x == concat y (concat z (concat w u)))) = + assert (Seq.equal x (Seq.append y (Seq.append z (Seq.append w u)))) + + diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.BitVectors.fst b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.BitVectors.fst new file mode 100644 index 000000000..f6d0b60f1 --- /dev/null +++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.BitVectors.fst @@ -0,0 +1,55 @@ +module Rust_primitives.BitVectors + +open FStar.Mul +open Rust_primitives.Arrays +open Rust_primitives.Integers + +#set-options "--fuel 0 --ifuel 1 --z3rlimit 40" + +let lemma_get_bit_bounded #t x d i = admit() + +let lemma_get_bit_bounded' #t x d = admit() + +let pow2_minus_one_mod_lemma1 (n: nat) (m: nat {m < n}) + : Lemma (((pow2 n - 1) / pow2 m) % 2 == 1) + = let d: pos = n - m in + Math.Lemmas.pow2_plus m d; + Math.Lemmas.lemma_div_plus (-1) (pow2 d) (pow2 m); + if d > 0 then Math.Lemmas.pow2_double_mult (d-1) + +let pow2_minus_one_mod_lemma2 (n: nat) (m: nat {n <= m}) + : Lemma (((pow2 n - 1) / pow2 m) % 2 == 0) + = Math.Lemmas.pow2_le_compat m n; + Math.Lemmas.small_div (pow2 n - 1) (pow2 m) + +let get_bit_pow2_minus_one #t #l n nth + = reveal_opaque (`%get_bit) (get_bit (mk_int_l #t #l (pow2 n - 1)) nth); + if v nth < n then pow2_minus_one_mod_lemma1 n (v nth) + else pow2_minus_one_mod_lemma2 n (v nth) + +let get_bit_pow2_minus_one_i32 x nth + = let n = Some?.v (mask_inv_opt x) in + assume (pow2 n - 1 == x); + mk_int_equiv_lemma #i32_inttype x; + get_bit_pow2_minus_one #i32_inttype #Lib.IntTypes.PUB n nth + +let get_bit_pow2_minus_one_u32 x nth + = let n = Some?.v (mask_inv_opt x) in + assume (pow2 n - 1 == x); + mk_int_equiv_lemma #u32_inttype x; + get_bit_pow2_minus_one #u32_inttype #Lib.IntTypes.PUB n nth + +let get_bit_pow2_minus_one_u16 x nth + = let n = Some?.v (mask_inv_opt x) in + assume (pow2 n - 1 == x); + mk_int_equiv_lemma #u16_inttype x; + get_bit_pow2_minus_one #u16_inttype #Lib.IntTypes.PUB n nth + +let get_bit_pow2_minus_one_u8 t x nth + = let n = Some?.v (mask_inv_opt x) in + assume (pow2 n - 1 == x); + mk_int_equiv_lemma #u8_inttype x; + get_bit_pow2_minus_one #u8_inttype #Lib.IntTypes.PUB n nth + +let get_last_bit_signed_lemma #t x + = admit () diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.BitVectors.fsti b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.BitVectors.fsti new file mode 100644 index 000000000..f0daa6aa8 --- /dev/null +++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.BitVectors.fsti @@ -0,0 +1,131 @@ +module Rust_primitives.BitVectors + +open FStar.Mul +open Rust_primitives.Arrays +open Rust_primitives.Integers + +/// Number of bits carried by an integer of type `t` +type bit_num t = d: nat {d > 0 /\ d <= bits t /\ (signed t ==> d <= bits t)} + +/// Number of bits carried by an integer of type `t` +type bounded #t (x:int_t t) (d:bit_num t) = + v x >= 0 /\ v x < pow2 d + +/// Integer of type `t` that carries `d` bits +type int_t_d t (d: bit_num t) = + n: int_t t {bounded n d} + +val lemma_get_bit_bounded #t (x:int_t t) (d:bit_num t) (i:usize): + Lemma ((bounded x d /\ v i >= d /\ v i < bits t) ==> + get_bit x i == 0) + [SMTPat (get_bit #t x i); SMTPat (bounded x d)] + +val lemma_get_bit_bounded' #t (x:int_t t) (d:bit_num t): + Lemma (requires forall i. v i > d ==> get_bit x i == 0) + (ensures bounded x d) + +type bit_vec (len: nat) = i:nat {i < len} -> bit + +/// Transform an array of integers to a bit vector +#push-options "--fuel 0 --ifuel 1 --z3rlimit 50" +let bit_vec_of_int_arr (#n: inttype) (#len: usize) + (arr: t_Array (int_t n) len) + (d: bit_num n): bit_vec (v len * d) + = fun i -> get_bit (Seq.index arr (i / d)) (sz (i % d)) +#pop-options + + +/// Transform an array of `nat`s to a bit vector +#push-options "--fuel 0 --ifuel 1 --z3rlimit 50" +let bit_vec_of_nat_arr (#len: usize) + (arr: t_Array nat len) + (d: nat) + : bit_vec (v len * d) + = fun i -> get_bit_nat (Seq.index arr (i / d)) (i % d) +#pop-options + +/// Bit-wise semantics of `2^n-1` +val get_bit_pow2_minus_one #t #l + (n: nat {pow2 n - 1 <= maxint t}) + (nth: usize {v nth < bits t}) + : Lemma ( get_bit (mk_int_l #t #l (pow2 n - 1)) nth + == (if v nth < n then 1 else 0)) + +/// Log2 table +unfold let mask_inv_opt = + function | 0 -> Some 0 + | 1 -> Some 1 + | 3 -> Some 2 + | 7 -> Some 3 + | 15 -> Some 4 + | 31 -> Some 5 + | 63 -> Some 6 + | 127 -> Some 7 + | 255 -> Some 8 + | 511 -> Some 9 + | 1023 -> Some 10 + | 2047 -> Some 11 + | 4095 -> Some 12 +(* | 8191 -> Some 13 + | 16383 -> Some 14 + | 32767 -> Some 15 + | 65535 -> Some 16 + | 131071 -> Some 17 + | 262143 -> Some 18 + | 524287 -> Some 19 + | 1048575 -> Some 20 + | 2097151 -> Some 21 + | 4194303 -> Some 22 + | 8388607 -> Some 23 + | 16777215 -> Some 24 + | 33554431 -> Some 25 + | 67108863 -> Some 26 + | 134217727 -> Some 27 + | 268435455 -> Some 28 + | 536870911 -> Some 29 + | 1073741823 -> Some 30 + | 2147483647 -> Some 31 + | 4294967295 -> Some 32 +*) | _ -> None + + +/// Specialized `get_bit_pow2_minus_one` lemmas with SMT patterns +/// targetting machine integer literals of type `i32` +val get_bit_pow2_minus_one_i32 + (x: int {x < pow2 31 /\ Some? (mask_inv_opt x)}) (nth: usize {v nth < 32}) + : Lemma ( get_bit (FStar.Int32.int_to_t x) nth + == (if v nth < Some?.v (mask_inv_opt x) then 1 else 0)) + [SMTPat (get_bit (FStar.Int32.int_to_t x) nth)] + +/// Specialized `get_bit_pow2_minus_one` lemmas with SMT patterns +/// targetting machine integer literals of type `u32` +val get_bit_pow2_minus_one_u32 + (x: int {x < pow2 32 /\ Some? (mask_inv_opt x)}) (nth: usize {v nth < 32}) + : Lemma ( get_bit (FStar.UInt32.uint_to_t x) nth + == (if v nth < Some?.v (mask_inv_opt x) then 1 else 0)) + [SMTPat (get_bit (FStar.UInt16.uint_to_t x) nth)] + +/// Specialized `get_bit_pow2_minus_one` lemmas with SMT patterns +/// targetting machine integer literals of type `u16` +val get_bit_pow2_minus_one_u16 + (x: int {x < pow2 16 /\ Some? (mask_inv_opt x)}) (nth: usize {v nth < 16}) + : Lemma ( get_bit (FStar.UInt16.uint_to_t x) nth + == (if v nth < Some?.v (mask_inv_opt x) then 1 else 0)) + [SMTPat (get_bit (FStar.UInt16.uint_to_t x) nth)] + +/// Specialized `get_bit_pow2_minus_one` lemmas with SMT patterns +/// targetting machine integer literals of type `u8` +val get_bit_pow2_minus_one_u8 + (t: _ {t == u8_inttype}) (x: int {x < pow2 8 /\ Some? (mask_inv_opt x)}) (nth: usize {v nth < 8}) + : Lemma ( get_bit #t #Lib.IntTypes.PUB (FStar.UInt8.uint_to_t x) nth + == (if v nth < Some?.v (mask_inv_opt x) then 1 else 0)) + [SMTPat (get_bit #t #Lib.IntTypes.PUB (FStar.UInt8.uint_to_t x) nth)] +// XXX: Why the #t here and not in the ones above? + +val get_last_bit_signed_lemma (#t: inttype{signed t}) (x: int_t t) + : Lemma ( get_bit x (mk_int_l (bits t - 1)) + == (if v x < 0 then 1 else 0)) + // [SMTPat (get_bit x (mk_int (bits t - 1)))] + + + diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fst b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fst new file mode 100644 index 000000000..278839338 --- /dev/null +++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fst @@ -0,0 +1,30 @@ +module Rust_primitives.Hax.Monomorphized_update_at + +open Rust_primitives +open Rust_primitives.Hax +open Core.Ops.Range + +let update_at_usize s i x = + update_at s i x + +let update_at_range #n s i x = + let res = update_at s i x in + admit(); // To be proved + res + +let update_at_range_to #n s i x = + let res = update_at s i x in + admit(); + res + +let update_at_range_from #n s i x = + let res = update_at s i x in + admit(); + res + +let update_at_range_full s i x = + let res = update_at s i x in + admit(); + res + + diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fsti b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fsti new file mode 100644 index 000000000..15aa4e12c --- /dev/null +++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fsti @@ -0,0 +1,58 @@ +module Rust_primitives.Hax.Monomorphized_update_at + +open Rust_primitives +open Rust_primitives.Hax +open Core.Ops.Range + +#set-options "--z3rlimit 30" + +val update_at_usize + (s: t_Slice 't) + (i: usize) + (x: 't) + : Pure (t_Array 't (length s)) + (requires (v i < Seq.length s)) + (ensures (fun res -> res == Seq.upd s (v i) x)) + +val update_at_range #n + (s: t_Slice 't) + (i: t_Range (pub_int_t n)) + (x: t_Slice 't) + : Pure (t_Array 't (length s)) + (requires (v i.f_start >= 0 /\ v i.f_start <= Seq.length s /\ + v i.f_end <= Seq.length s /\ + Seq.length x == v i.f_end - v i.f_start)) + (ensures (fun res -> + Seq.slice res 0 (v i.f_start) == Seq.slice s 0 (v i.f_start) /\ + Seq.slice res (v i.f_start) (v i.f_end) == x /\ + Seq.slice res (v i.f_end) (Seq.length res) == Seq.slice s (v i.f_end) (Seq.length s))) + +val update_at_range_to #n + (s: t_Slice 't) + (i: t_RangeTo (pub_int_t n)) + (x: t_Slice 't) + : Pure (t_Array 't (length s)) + (requires (v i.f_end >= 0 /\ v i.f_end <= Seq.length s /\ + Seq.length x == v i.f_end)) + (ensures (fun res -> + Seq.slice res 0 (v i.f_end) == x /\ + Seq.slice res (v i.f_end) (Seq.length res) == Seq.slice s (v i.f_end) (Seq.length s))) + +val update_at_range_from #n + (s: t_Slice 't) + (i: t_RangeFrom (pub_int_t n)) + (x: t_Slice 't) + : Pure (t_Array 't (length s)) + (requires ( v i.f_start >= 0 /\ v i.f_start <= Seq.length s /\ + Seq.length x == Seq.length s - v i.f_start)) + (ensures (fun res -> + Seq.slice res 0 (v i.f_start) == Seq.slice s 0 (v i.f_start) /\ + Seq.slice res (v i.f_start) (Seq.length res) == x)) + +val update_at_range_full + (s: t_Slice 't) + (i: t_RangeFull) + (x: t_Slice 't) + : Pure (t_Array 't (length s)) + (requires (Seq.length x == Seq.length s)) + (ensures (fun res -> res == x)) diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Hax.fst b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Hax.fst new file mode 100644 index 000000000..69b171eca --- /dev/null +++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Hax.fst @@ -0,0 +1,48 @@ +module Rust_primitives.Hax + +open Rust_primitives.Integers +open Rust_primitives.Arrays + +type t_Never = False +let never_to_any #t: t_Never -> t = (fun _ -> match () with) + +let repeat (x: 'a) (len: usize): t_Array 'a len = + FStar.Seq.create (v len) x + +open Core.Ops.Index +class update_at_tc self idx = { + [@@@FStar.Tactics.Typeclasses.tcinstance] + super_index: t_Index self idx; + update_at: s: self -> i: idx {in_range s i} -> super_index.f_Output -> self; +} + +open Core.Slice + +instance impl__index t n: t_Index (t_Slice t) (pub_int_t n) + = { f_Output = t; + in_range = (fun (s: t_Slice t) (i: pub_int_t n) -> v i >= 0 && v i < Seq.length s); + f_index = (fun s i -> Seq.index s (v i)); + } + +instance impl__index_array t l n: t_Index (t_Array t l) (pub_int_t n) + = { f_Output = t; + in_range = (fun (s: t_Array t l) (i: pub_int_t n) -> v i >= 0 && v i < v l); + f_index = (fun s i -> Seq.index s (v i)); + } + +instance update_at_tc_slice t n: update_at_tc (t_Slice t) (pub_int_t n) = { + super_index = FStar.Tactics.Typeclasses.solve <: t_Index (t_Slice t) (pub_int_t n); + update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x); +} + +instance update_at_tc_array t l n: update_at_tc (t_Array t l) (pub_int_t n) = { + super_index = FStar.Tactics.Typeclasses.solve <: t_Index (t_Array t l) (pub_int_t n); + update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x); +} + + +let (.[]<-) #self #idx {| update_at_tc self idx |} (s: self) (i: idx {in_range s i}) + = update_at s i + +let array_of_list #t = Rust_primitives.Arrays.of_list #t + diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fst b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fst new file mode 100644 index 000000000..055f2a655 --- /dev/null +++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fst @@ -0,0 +1,86 @@ +module Rust_primitives.Integers + +#set-options "--z3rlimit 100 --fuel 0 --ifuel 1" + + +let pow2_values x = + let p = pow2 x in + assert_norm (p == normalize_term (pow2 x)) + +let usize_inttype = LI.U32 +let isize_inttype = LI.S32 + +let v_injective #t a = LI.v_injective #t #LI.PUB a +let v_mk_int #t n = LI.v_mk_int #t #LI.PUB n + +let usize_to_uint32 x = x +let usize_to_uint64 x = Int.Cast.uint32_to_uint64 x +let size_to_uint64 x = Int.Cast.uint32_to_uint64 x + +let mk_int_l #t #l a = LI.mk_int #t #l a +let mk_int_equiv_lemma #_ = admit () +let mk_int_v_lemma #t a = () +let v_mk_int_lemma #t a = () + +let add_mod_equiv_lemma #t #l #l' a b = + LI.add_mod_lemma #_ #(meet l l') (classify a) (classify b) + +let add_equiv_lemma #t #l #l' a b = + LI.add_lemma #_ #(meet l l') (classify a) (classify b) + +let incr_equiv_lemma #t #l a = LI.incr_lemma #t #l a + +let mul_mod_equiv_lemma #t #l #l' a b = + LI.mul_mod_lemma #_ #(meet l l') (classify a) (classify b) + +let mul_equiv_lemma #t #l #l' a b = + LI.mul_lemma #_ #(meet l l') (classify a) (classify b) + +let sub_mod_equiv_lemma #t #l #l' a b = + LI.sub_mod_lemma #_ #(meet l l') (classify a) (classify b) + +let sub_equiv_lemma #t #l #l' a b = + LI.sub_lemma #_ #(meet l l') (classify a) (classify b) + +let decr_equiv_lemma #t a = LI.decr_lemma #t a + +let div_equiv_lemma #t a b = admit(); LI.div_lemma #t a b +let mod_equiv_lemma #t a b = admit(); LI.mod_lemma #t a b + +let lognot #t a = LI.lognot #t a +let lognot_lemma #t a = admit() + +let logxor #t #l1 #l2 a b = LI.logxor #t #(meet l1 l2) (classify a) (classify b) +let logxor_lemma #t a b = admit() + +let logand #t #l1 #l2 a b = LI.logand #t #(meet l1 l2) (classify a) (classify b) +let logand_lemma #t a b = admit() +let logand_mask_lemma #t a b = admit() + +let logor #t #l1 #l2 a b = LI.logor #t #(meet l1 l2) (classify a) (classify b) +let logor_lemma #t a b = admit() + +let shift_right_equiv_lemma #t a b = admit() +let shift_left_equiv_lemma #t a b = admit() + +let rotate_right #t a b = LI.rotate_right #t a (cast b) +let rotate_right_equiv_lemma #t a b = () +let rotate_left #t a b = LI.rotate_left #t a (cast b) +let rotate_left_equiv_lemma #t a b = () + +let abs_int_equiv_lemma #t a = admit() + +let neg_equiv_lemma #_ _ = admit() + +let get_bit_and _x _y _i = admit () +let get_bit_or _x _y _i = admit () +let get_bit_shl _x _y _i = admit () +let get_bit_shr _x _y _i = admit () + +let get_bit_cast #t #u #l x nth + = reveal_opaque (`%get_bit) (get_bit x nth); + reveal_opaque (`%get_bit) (get_bit (cast_mod #t #u x <: int_t_l u l) nth); + admit () + +let get_bit_cast_extend #t #u x nth + = admit () diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fsti b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fsti new file mode 100644 index 000000000..fb59c6885 --- /dev/null +++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fsti @@ -0,0 +1,579 @@ +module Rust_primitives.Integers + +open FStar.Mul + +module LI = Lib.IntTypes + +#set-options "--max_fuel 0 --max_ifuel 1 --z3rlimit 20" + +val pow2_values: x:nat -> Lemma + (let p = pow2 x in + match x with + | 0 -> p=1 + | 1 -> p=2 + | 8 -> p=256 + | 16 -> p=65536 + | 31 -> p=2147483648 + | 32 -> p=4294967296 + | 63 -> p=9223372036854775808 + | 64 -> p=18446744073709551616 + | 2 | 3 | 4 | 5 | 6 | 7 + | 9 | 10 | 11 | 12 | 13 | 14 | 15 + | 17 | 18 | 19 | 20 | 21 | 22 | 23 + | 24 | 25 | 26 | 27 | 28 | 29 | 30 + | 33 | 34 | 35 | 36 | 37 | 38 | 39 + | 40 | 41 | 42 | 43 | 44 | 45 | 46 + | 47 | 48 | 49 | 50 | 51 | 52 | 53 + | 54 | 55 | 56 | 57 | 58 | 59 | 60 + | 61 | 62 | 63 | 65 | 127 | 128 -> p = normalize_term (pow2 x) + | _ -> True) + [SMTPat (pow2 x)] + +type inttype = LI.inttype +let unsigned = LI.unsigned +let signed = LI.signed +type uinttype = t:inttype{unsigned t} +let int_t_l t l = LI.int_t t l +let int_t t = int_t_l t LI.SEC +let pub_int_t t = int_t_l t LI.PUB + +let meet (l1 l2:LI.secrecy_level) : LI.secrecy_level = + match l1, l2 with + | LI.SEC, LI.PUB -> LI.SEC + | LI.SEC, LI.SEC -> LI.SEC + | LI.PUB, LI.SEC -> LI.SEC + | LI.PUB, LI.PUB -> LI.PUB + +let can_flow (l1 l2:LI.secrecy_level) : bool = + match l1, l2 with + | LI.PUB, LI.PUB -> true + | LI.SEC, LI.SEC -> true + | LI.PUB, LI.SEC -> true + | LI.SEC, LI.PUB -> false + +let bits t = LI.bits t +let u8_inttype = LI.U8 +let i8_inttype = LI.S8 +let u16_inttype = LI.U16 +let i16_inttype = LI.S16 +let u32_inttype = LI.U32 +let i32_inttype = LI.S32 +let u64_inttype = LI.U64 +let i64_inttype = LI.S64 +let u128_inttype = LI.U128 +let i128_inttype = LI.S128 +val usize_inttype: t:inttype{unsigned t /\ (t = LI.U32 \/ t = LI.U64)} +val isize_inttype: t:inttype{signed t /\ (t = LI.S32 \/ t = LI.S64)} + +type u8 = int_t LI.U8 +type i8 = int_t LI.S8 +type u16 = int_t LI.U16 +type i16 = int_t LI.S16 +type u32 = int_t LI.U32 +type i32 = int_t LI.S32 +type u64 = int_t LI.U64 +type i64= int_t LI.S64 +type u128 = int_t LI.U128 +type i128 = int_t LI.S128 + +type pub_u8 = pub_int_t LI.U8 +type pub_i8 = pub_int_t LI.S8 +type pub_u16 = pub_int_t LI.U16 +type pub_i16 = pub_int_t LI.S16 +type pub_u32 = pub_int_t LI.U32 +type pub_i32 = pub_int_t LI.S32 +type pub_u64 = pub_int_t LI.U64 +type pub_i64= pub_int_t LI.S64 +type pub_u128 = pub_int_t LI.U128 +type pub_i128 = pub_int_t LI.S128 + +type usize = int_t_l usize_inttype LI.PUB +type isize = int_t_l isize_inttype LI.PUB + +let minint (t:LI.inttype) = + if unsigned t then 0 else -(pow2 (bits t - 1)) +let maxint (t:LI.inttype) = + if unsigned t then pow2 (bits t) - 1 + else pow2 (bits t - 1) - 1 +let modulus (t:LI.inttype) = pow2 (bits t) + +let max_usize = maxint usize_inttype +let max_isize = maxint isize_inttype + +//let range_bits (n:int) (n:bits) : bool = +// minint t <= n && n <= maxint t + +let range (n:int) (t:inttype) : bool = + minint t <= n && n <= maxint t +type range_t (t:inttype) = x:int{range x t} + +[@(strict_on_arguments [0])] +let v (#t:inttype) (#l) (x:int_t_l t l) : range_t t = LI.v #t #l x + +[@(strict_on_arguments [0])] +val mk_int_l (#t:inttype) (#l:LI.secrecy_level) (n:range_t t) : int_t_l t l + +[@(strict_on_arguments [0])] +let mk_int (#t:inttype) (n:range_t t) : int_t t = mk_int_l n + +[@(strict_on_arguments [0])] +let mk_pub_int (#t:inttype) (n:range_t t) : int_t_l t LI.PUB = mk_int_l n + +[@(strict_on_arguments [0])] +val mk_int_equiv_lemma #t (n:range_t t) : + Lemma ( + match t with + | LI.U8 -> mk_int_l #u8_inttype n == UInt8.uint_to_t n + | LI.S8 -> mk_int_l #i8_inttype n == Int8.int_to_t n + | LI.U16 -> mk_int_l #u16_inttype n == UInt16.uint_to_t n + | LI.S16 -> mk_int_l #i16_inttype n == Int16.int_to_t n + | LI.U32 -> mk_int_l #u32_inttype n == UInt32.uint_to_t n + | LI.S32 -> mk_int_l #i32_inttype n == Int32.int_to_t n + | LI.U64 -> mk_int_l #u64_inttype n == UInt64.uint_to_t n + | LI.S64 -> mk_int_l #i64_inttype n == Int64.int_to_t n + | LI.U128 -> mk_int_l #u128_inttype n == UInt128.uint_to_t n + | LI.S128 -> mk_int_l #i128_inttype n == Int128.int_to_t n + | _ -> True) + +let sz (n:range_t usize_inttype) : usize = mk_int_l n +let isz (n:range_t isize_inttype) : isize = mk_int_l n + +val mk_int_v_lemma: #t:inttype -> #l:LI.secrecy_level -> a:int_t_l t l -> Lemma + (mk_int_l #t (v #t #l a) == a) + [SMTPat (mk_int_l #t #l (v #t #l a))] + +val v_mk_int_lemma: #t:inttype -> #l:LI.secrecy_level -> n:range_t t -> Lemma + (v #t #l (mk_int_l #t #l n) == n) + [SMTPat (v #t #l (mk_int_l #t #l n))] + +(* Wrap-around modulo: wraps into [-p/2; p/2[ *) +let op_At_Percent (v:int) (p:int{p>0/\ p%2=0}) : Tot int = + let m = v % p in if m >= p/2 then m - p else m + +[@(strict_on_arguments [0])] +let op_At_Percent_Dot x t : range_t t = + if unsigned t then x % modulus t + else x @% modulus t + +let cast (#t:inttype) (#t':inttype) (#l:LI.secrecy_level) + (u1:int_t_l t l{range (v u1) t'}) = + mk_int_l #t' #l (v u1) +let cast_mod (#t:inttype) (#t':inttype) (#l:LI.secrecy_level) + (u1:int_t_l t l) = + mk_int_l #t' #l (v u1 @%. t') + +/// Arithmetic operations +/// +let add_mod (#t:inttype) + (#l #l':LI.secrecy_level) + (a:int_t_l t l) (b:int_t_l t l') = + mk_int_l #t #(meet l l') ((v a + v b) @%. t) + +let classify #t #l (#l':LI.secrecy_level{can_flow l l'}) + (a:int_t_l t l) + : int_t_l t l' = + match l,l' with + | LI.PUB, LI.SEC -> LI.secret #t a + | LI.PUB, LI.PUB -> a + | LI.SEC, LI.SEC -> a + +val add_mod_equiv_lemma: #t:uinttype + -> #l:LI.secrecy_level + -> #l':LI.secrecy_level + -> a:int_t_l t l + -> b:int_t_l t l' + -> Lemma + (add_mod a b == LI.add_mod #_ #(meet l l') (classify a) (classify b)) + +let add (#t:inttype) (#l #l':LI.secrecy_level) (a:int_t_l t l) + (b:int_t_l t l'{range (v a + v b) t}) = + mk_int_l #t #(meet l l') (v a + v b) + +val add_equiv_lemma: #t:uinttype -> #l:LI.secrecy_level -> #l':LI.secrecy_level + -> a:int_t_l t l + -> b:int_t_l t l'{range (v a + v b) t} + -> Lemma + (add a b == LI.add #t #(meet l l') (classify a) (classify b)) + +let incr (#t:inttype) (#l:LI.secrecy_level) (a:int_t_l t l{v a < maxint t}) = + mk_int_l #t #l (v a + 1) + +val incr_equiv_lemma: #t:inttype -> #l:LI.secrecy_level + -> a:int_t_l t l{v a < maxint t} + -> Lemma (incr a == LI.incr a) + +let mul_mod (#t:inttype) (#l #l':LI.secrecy_level) + (a:int_t_l t l) + (b:int_t_l t l') = + mk_int_l #t #(meet l l') (v a * v b @%. t) + +val mul_mod_equiv_lemma: #t:uinttype{not (LI.U128? t)} + -> #l:LI.secrecy_level + -> #l':LI.secrecy_level + -> a:int_t_l t l + -> b:int_t_l t l' + -> Lemma (mul_mod a b == LI.mul_mod #t #(meet l l') (classify a) (classify b)) + +let mul (#t:inttype) (#l #l':LI.secrecy_level) + (a:int_t_l t l) + (b:int_t_l t l'{range (v a * v b) t}) = + mk_int_l #t #(meet l l') (v a * v b) + +val mul_equiv_lemma: #t:uinttype{not (LI.U128? t)} + -> #l:LI.secrecy_level + -> #l':LI.secrecy_level + -> a:int_t_l t l + -> b:int_t_l t l'{range (v a * v b) t} + -> Lemma (mul a b == LI.mul #t #(meet l l') (classify a) (classify b)) + +let sub_mod (#t:inttype) (#l #l':LI.secrecy_level) + (a:int_t_l t l) (b:int_t_l t l') = + mk_int_l #t #(meet l l') ((v a - v b) @%. t) + +val sub_mod_equiv_lemma: #t:uinttype + -> #l:LI.secrecy_level + -> #l':LI.secrecy_level + -> a:int_t_l t l + -> b:int_t_l t l' + -> Lemma + (sub_mod a b == LI.sub_mod #_ #(meet l l') (classify a) (classify b)) + +let sub (#t:inttype) (#l #l':LI.secrecy_level) + (a:int_t_l t l) + (b:int_t_l t l'{range (v a - v b) t}) = + mk_int_l #t #(meet l l') (v a - v b) + +val sub_equiv_lemma: #t:uinttype + -> #l:LI.secrecy_level + -> #l':LI.secrecy_level + -> a:int_t_l t l + -> b:int_t_l t l'{range (v a - v b) t} + -> Lemma + (sub a b == LI.sub #t #(meet l l') (classify a) (classify b)) + +let decr (#t:inttype) (#l:LI.secrecy_level) (a:int_t_l t l{minint t < v a}) = + mk_int_l #t #l (v a - 1) + +val decr_equiv_lemma: #t:inttype -> #l:LI.secrecy_level + -> a:int_t_l t l{minint t < v a} + -> Lemma (decr a == LI.decr a) + +let div (#t:inttype) (a:int_t_l t LI.PUB) (b:int_t_l t LI.PUB{v b <> 0}) = + assume(unsigned t \/ range (v a / v b) t); + mk_int_l #t #LI.PUB (v a / v b) + +val div_equiv_lemma: #t:inttype{~(LI.U128? t) /\ ~(LI.S128? t)} + -> a:int_t_l t LI.PUB + -> b:int_t_l t LI.PUB{v b <> 0 /\ (unsigned t \/ range FStar.Int.(v a / v b) t)} + -> Lemma (div a b == LI.div a b) + +let mod (#t:inttype) (a:int_t_l t LI.PUB) (b:int_t_l t LI.PUB{v b <> 0}) = + mk_int_l #t #LI.PUB (v a % v b) + + +val mod_equiv_lemma: #t:inttype{~(LI.U128? t) /\ ~(LI.S128? t)} + -> a:int_t_l t LI.PUB + -> b:int_t_l t LI.PUB{v b <> 0 /\ (unsigned t \/ range FStar.Int.(v a / v b) t)} + -> Lemma (mod a b == LI.mod a b) + + +/// Comparison Operators +/// +let eq (#t:inttype) (a:int_t_l t LI.PUB) (b:int_t_l t LI.PUB) = v a = v b +let ne (#t:inttype) (a:int_t_l t LI.PUB) (b:int_t_l t LI.PUB) = v b <> v b +let lt (#t:inttype) (a:int_t_l t LI.PUB) (b:int_t_l t LI.PUB) = v a < v b +let lte (#t:inttype) (a:int_t_l t LI.PUB) (b:int_t_l t LI.PUB) = v a <= v b +let gt (#t:inttype) (a:int_t_l t LI.PUB) (b:int_t_l t LI.PUB) = v a > v b +let gte (#t:inttype) (a:int_t_l t LI.PUB) (b:int_t_l t LI.PUB) = v a >= v b + + +/// Bitwise Operations + + +let ones (#t:inttype) (#l:LI.secrecy_level) : n:int_t_l t l = + if unsigned t then mk_int_l #t #l (pow2 (bits t) - 1) + else mk_int_l #t #l (-1) + +let zero (#t:inttype) (#l:LI.secrecy_level) : n:int_t_l t l = + mk_int_l #t #l 0 + +val lognot: #t:inttype -> #l:LI.secrecy_level -> int_t_l t l -> int_t_l t l +val lognot_lemma: #t:inttype -> #l:LI.secrecy_level -> a:int_t_l t l -> Lemma + (lognot a == LI.lognot a /\ + lognot #t #l zero == ones /\ + lognot #t #l ones == zero /\ + lognot (lognot a) == a /\ + (signed t ==> v (lognot a) = -1 - v a) /\ + (unsigned t ==> v (lognot a) = pow2 (bits t) - 1 - v a) + ) + +val logxor: #t:inttype + -> #l:LI.secrecy_level + -> #l':LI.secrecy_level + -> int_t_l t l + -> int_t_l t l' + -> int_t_l t (meet l l') + +val logxor_lemma: #t:inttype + -> #l:LI.secrecy_level + -> #l':LI.secrecy_level + -> a:int_t_l t l + -> b:int_t_l t l' -> Lemma + (logxor a b == LI.logxor #t #(meet l l') (classify a) (classify b) /\ + a `logxor` a == zero #t #l /\ + (a `logxor` b == zero #t #(meet l l') ==> v b == v a) /\ + v (a `logxor` (a `logxor` b)) == v b /\ + v (a `logxor` (b `logxor` a)) == v b /\ + zero #t #l' `logxor` a == classify a /\ + a `logxor` zero #t #l' == classify a /\ + v (ones #t #l' `logxor` a) == v (lognot a) /\ + v (a `logxor` ones #t #l') == v (lognot a)) + +val logand: #t:inttype -> #l:LI.secrecy_level -> #l':LI.secrecy_level + -> int_t_l t l + -> int_t_l t l' + -> int_t_l t (meet l l') + +val logand_lemma: #t:inttype -> #l:LI.secrecy_level -> #l':LI.secrecy_level -> a:int_t_l t l -> b:int_t_l t l' -> + Lemma (logand a b == LI.logand #t #(meet l l') (classify a) (classify b) /\ + v (logand a (zero #t #l')) == v (zero #t #l') /\ + v (logand (zero #t #l') a) == v (zero #t #l') /\ + v (logand a (ones #t #l')) == v a /\ + v (logand (ones #t #l') a) == v a /\ + (v a >= 0 ==> (v (logand a b) >= 0) /\ (v (logand a b) <= v a)) /\ + (v b >= 0 ==> (v (logand a b) >= 0) /\ (v (logand a b) <= v b))) + +val logand_mask_lemma: #t:inttype -> #l:LI.secrecy_level + -> a:int_t_l t l + -> m:nat{m < bits t} -> + Lemma (pow2 m < maxint t /\ + logand a (sub #t (mk_int_l #t #l (pow2 m)) (mk_int_l #t #l 1)) == + mk_int_l #t #l (v a % pow2 m)) + [SMTPat (logand #t a (sub #t (mk_int_l #t #l (pow2 m)) (mk_int_l #t #l 1)))] + +val logor: #t:inttype -> #l:LI.secrecy_level -> #l':LI.secrecy_level + -> int_t_l t l + -> int_t_l t l' + -> int_t_l t (meet l l') + +val logor_lemma: #t:inttype + -> #l:LI.secrecy_level + -> #l':LI.secrecy_level + -> a:int_t_l t l + -> b:int_t_l t l' -> + Lemma (logor a b == LI.logor #t #(meet l l') (classify a) (classify b) /\ + v (logor a (zero #t #l')) == v a /\ + v (logor a (ones #t #l')) == v (ones #t #l') /\ + v (logor (zero #t #l') a) == v a /\ + v (logor (ones #t #l') a) == v (ones #t #l') /\ + ((v a >= 0 /\ v b >= 0) ==> (v (logor a b) >= v a /\ v (logor a b) >= v b))) + +unfold type shiftval (t:inttype) (t':inttype) = + b:int_t_l t' LI.PUB{v b >= 0 /\ v b < bits t} +unfold type rotval (t:inttype) (t':inttype) = + b:int_t_l t' LI.PUB{v b > 0 /\ v b < bits t} + +let shift_right (#t:inttype) (#t':inttype) (#l:LI.secrecy_level) + (a:int_t_l t l) (b:shiftval t t') = + LI.shift_right_lemma a (LI.size (v b)); + mk_int_l #t #l (v a / pow2 (v b)) + +val shift_right_equiv_lemma: #t:inttype -> #t':inttype -> #l:LI.secrecy_level + -> a:int_t_l t l -> b:shiftval t t' + -> Lemma + (v ((cast #t' #u32_inttype b <: LI.size_t)) < bits t /\ + shift_right #t #t' a b == + LI.shift_right a (cast #t' #u32_inttype b <: LI.size_t)) + +let shift_left (#t:inttype) (#t':inttype) (#l:LI.secrecy_level) + (a:int_t_l t l) (b:shiftval t t') = + let x:range_t t = (v a * pow2 (v b)) @%. t in + mk_int_l #t #l x + +val shift_left_equiv_lemma: #t:inttype -> #t':inttype -> #l:LI.secrecy_level + -> a:int_t_l t l -> b:shiftval t t' + -> Lemma + ((v a >= 0 /\ range (v a * pow2 (v b)) t) ==> + (v (cast #_ #u32_inttype b) < bits t /\ + shift_left #t #t' a b == + LI.shift_left a (cast b))) + +val rotate_right: #t:uinttype -> #t':inttype -> #l:LI.secrecy_level + -> a:int_t_l t l + -> rotval t t' + -> int_t_l t l + +val rotate_right_equiv_lemma: #t:uinttype -> #t':inttype -> #l:LI.secrecy_level + -> a:int_t_l t l -> b:rotval t t' + -> Lemma (v (cast #_ #u32_inttype b) > 0 /\ + rotate_right a b == + LI.rotate_right a (cast b)) + +val rotate_left: #t:uinttype -> #t':inttype -> #l:LI.secrecy_level + -> a:int_t_l t l + -> rotval t t' + -> int_t_l t l + +val rotate_left_equiv_lemma: #t:uinttype -> #t':inttype -> #l:LI.secrecy_level + -> a:int_t_l t l -> b:rotval t t' + -> Lemma (v (cast #_ #u32_inttype b) > 0 /\ + rotate_left a b == + LI.rotate_left a (cast b)) + +let shift_right_i (#t:inttype) (#t':inttype) (#l:LI.secrecy_level) (s:shiftval t t') (u:int_t_l t l) : int_t_l t l = shift_right u s + +let shift_left_i (#t:inttype) (#t':inttype) (#l:LI.secrecy_level) (s:shiftval t t') (u:int_t_l t l{v u >= 0}) : int_t_l t l = shift_left u s + +let rotate_right_i (#t:uinttype) (#t':inttype) (#l:LI.secrecy_level) (s:rotval t t') (u:int_t_l t l) : int_t_l t l = rotate_right u s + +let rotate_left_i (#t:uinttype) (#t':inttype) (#l:LI.secrecy_level) (s:rotval t t') (u:int_t_l t l) : int_t_l t l = rotate_left u s + +let abs_int (#t:inttype) (#l:LI.secrecy_level) (a:int_t_l t l{minint t < v a}) = + mk_int_l #t #l (abs (v a)) + +val abs_int_equiv_lemma: #t:inttype{signed t /\ not (LI.S128? t)} + -> #l:LI.secrecy_level + -> a:int_t_l t l{minint t < v a} + -> Lemma (abs_int a == LI.ct_abs a) + +let neg (#t:inttype{signed t}) (#l:LI.secrecy_level) (a:int_t_l t l{range (0 - v a) t}) = + mk_int_l #t #l (0 - (v a)) + +val neg_equiv_lemma: #t:inttype{signed t /\ not (LI.S128? t)} -> #l:LI.secrecy_level + -> a:int_t_l t l{range (0 - v a) t} + -> Lemma (neg a == sub (mk_int_l #t #l 0) a /\ + (lognot a == sub (neg a) (mk_int_l #t #l 1))) + + +/// +/// Operators available for all machine integers +/// + +// Strict: with precondition +unfold +let (+!) #t #l #l' = add #t #l #l' + +// Wrapping: no precondition +unfold +let (+.) #t #l #l' = add_mod #t #l #l' + +unfold +let ( *! ) #t #l #l' = mul #t #l #l' + +unfold +let ( *. ) #t #l #l' = mul_mod #t #l #l' + +unfold +let ( -! ) #t #l #l' = sub #t #l #l' + +unfold +let ( -. ) #t #l #l' = sub_mod #t #l #l' + +unfold +let ( >>! ) #t #t' #l = shift_right #t #t' #l + +unfold +let ( <>>. ) #t #t' #l = rotate_right #t #t' #l + +unfold +let ( <<<. ) #t #t' #l = rotate_left #t #t' #l + +unfold +let ( ^. ) #t #l #l' = logxor #t #l #l' + +unfold +let ( |. ) #t #l #l' = logor #t #l #l' + +unfold +let ( &. ) #t #l #l' = logand #t #l #l' + +unfold +let ( ~. ) #t #l = lognot #t #l + +unfold +let (/!) #t = div #t + +unfold +let (%!) #t = mod #t + +unfold +let (=.) #t = eq #t + +unfold +let (<>.) #t = ne #t + +unfold +let (<.) #t = lt #t + +unfold +let (<=.) #t = lte #t + +unfold +let (>.) #t = gt #t + +unfold +let (>=.) #t = gte #t + + +type bit = n: nat {n < 2} + +/// Mathematical `get_bit` definition on `nat`s +let get_bit_nat (x: nat) (nth: nat): bit + = (x / pow2 nth) % 2 + +/// `get_bit` definition for machine integer of any size and signedness +[@"opaque_to_smt"] +let get_bit (#t: inttype) (#l:LI.secrecy_level) + (x: int_t_l t l) (nth: usize {v nth < bits t}): bit + = if v x >= 0 then get_bit_nat (v x) (v nth) + else // two's complement + get_bit_nat (pow2 (bits t) + v x) (v nth) + +unfold let bit_and (x y: bit): bit = match x, y with | (1, 1) -> 1 | _ -> 0 +unfold let bit_or (x y: bit): bit = (x + y) % 2 + +/// Bit-wise semantics for `&.` +val get_bit_and #t #l (x y: int_t_l t l) (i: usize {v i < bits t}) + : Lemma (get_bit (x &. y) i == get_bit x i `bit_and` get_bit y i) + [SMTPat (get_bit (x &. y) i)] + +/// Bit-wise semantics for `|.` +val get_bit_or #t #l (x y: int_t_l t l) (i: usize {v i < bits t}) + : Lemma (get_bit (x |. y) i == get_bit x i `bit_or` get_bit y i) + [SMTPat (get_bit (x |. y) i)] + +/// Bit-wise semantics for `<= 0 /\ v y < bits t) + (ensures get_bit (x <>!` +val get_bit_shr #t #u #l (x: int_t_l t l) (y: int_t_l u LI.PUB) (i: usize {v i < bits t}) + : Lemma (requires v y >= 0 /\ v y < bits t) + (ensures get_bit (x >>! y) i + == (if v i < bits t - v y + then get_bit x (mk_int_l (v i + v y)) + else if signed t + then get_bit x (mk_int_l (bits t - 1)) + else 0)) + [SMTPat (get_bit (x >>! y) i)] + +// TODO: check for neg numbers +/// Bit-wise semantics of integer casts +val get_bit_cast #t #u #l + (x: int_t_l t l) (nth: usize) + : Lemma (requires v nth < bits u /\ v nth < bits t) + (ensures get_bit (cast_mod #t #u x) nth == get_bit x nth) + [SMTPat (get_bit (cast_mod #t #u x) nth)] + +val get_bit_cast_extend #t #u #l + (x: int_t_l t l) (nth: usize) + : Lemma (requires bits t < bits u /\ v nth >= bits t /\ v nth < bits u) + (ensures get_bit (cast_mod #t #u x) nth == 0) + [SMTPat (get_bit (cast_mod #t #u x) nth)] + diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Iterators.fsti b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Iterators.fsti new file mode 100644 index 000000000..48cb8564a --- /dev/null +++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Iterators.fsti @@ -0,0 +1,63 @@ +module Rust_primitives.Iterators + +open Rust_primitives +open Core.Ops.Range +open FStar.Mul + +val foldi_range (#n:inttype) (#acc_t:Type) + (#inv:(acc_t -> i:pub_int_t n -> Type)) + (r: t_Range (pub_int_t n){r.f_start <=. r.f_end}) + (acc:acc_t{inv acc r.f_start}) + (f: (acc:acc_t -> i:pub_int_t n{i >=. r.f_start /\ i <. r.f_end /\ inv acc i} + -> acc':acc_t{inv acc' (i +! mk_pub_int 1)})) + : res:acc_t{inv res r.f_end} + +val foldi_range_step_by (#n:inttype) (#acc_t:Type) + (#inv:(acc_t -> i:pub_int_t n -> Type)) + (r: t_Range (pub_int_t n){r.f_start <=. r.f_end}) + (step: usize{v step > 0 /\ range (v step) n /\ range (v r.f_end + v step) n}) + (acc:acc_t{inv acc r.f_start}) + (f: (acc:acc_t -> i:pub_int_t n{i >=. r.f_start /\ i <. r.f_end /\ + (v i - v r.f_start) % (v step) == 0 /\ inv acc i} + -> acc':acc_t{inv acc' (i +! mk_int #n (v step))})) + : res:acc_t{inv res r.f_end} + + +val foldi_chunks_exact + (#t:Type) (#acc_t:Type) + (#inv:(acc_t -> usize -> Type)) + (s:t_Slice t) + (chunk_len:usize{v chunk_len > 0}) + (acc:acc_t{inv acc (sz 0)}) + (f: (acc:acc_t -> it:(usize & t_Array t chunk_len){ + let (i,item) = it in + v i >= 0 /\ + v i < Seq.length s / v chunk_len /\ + inv acc i} + -> acc':acc_t{inv acc' (fst it +! sz 1)})) + : res:acc_t{inv res (length s /! chunk_len)} + +val fold_chunks_exact + (#t:Type) (#acc_t:Type) + (#inv:(acc_t -> Type)) + (s:t_Slice t) + (chunk_len:usize{v chunk_len > 0}) // /\ Seq.length s % v chunk_len == 0}) + (acc:acc_t{inv acc}) + (f: (acc:acc_t -> it:t_Array t chunk_len{inv acc} + -> acc':acc_t{inv acc'})) + : res:acc_t{inv res} + + +val foldi_slice (#t:Type) (#acc_t:Type) + (#inv:(acc_t -> usize -> Type)) + (sl: t_Slice t) + (acc:acc_t{inv acc (sz 0)}) + (f: (acc:acc_t -> it:(usize & t){ + let (i,item) = it in + v i >= 0 /\ + v i < Seq.length sl /\ + Seq.index sl (v i) == item /\ + inv acc i} + -> acc':acc_t{inv acc' (fst it +! sz 1)})) + : res:acc_t{inv res (length sl)} + diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.fst b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.fst new file mode 100644 index 000000000..096498965 --- /dev/null +++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.fst @@ -0,0 +1,27 @@ +module Rust_primitives + +include Rust_primitives.Integers +include Rust_primitives.Arrays +include Rust_primitives.BitVectors + +class cast_tc a b = { + cast: a -> b; +} + +/// Rust's casts operations on integers are non-panicking +instance cast_tc_integers (t:inttype) (t':inttype) (l:Lib.IntTypes.secrecy_level) + : cast_tc (int_t_l t l) (int_t_l t' l) + = { cast = (fun x -> Rust_primitives.Integers.cast_mod #t #t' x) } + +class unsize_tc source = { + output: Type; + unsize: source -> output; +} + +instance array_to_slice_unsize t n: unsize_tc (t_Array t n) = { + output = t_Slice t; + unsize = (fun (arr: t_Array t n) -> + arr <: t_Slice t); +} + + From 2236a93c62ee010e28f87a5e82984cd3b4ced801 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Sun, 14 Jan 2024 00:05:54 +0100 Subject: [PATCH 2/2] fixup for secret integers --- .../fstar-secret-integers/core/Makefile | 2 +- .../rust_primitives/Makefile | 2 +- .../Rust_primitives.Arrays.fsti | 3 ++- .../Rust_primitives.Integers.fst | 2 ++ .../Rust_primitives.Integers.fsti | 22 ++++++++++++------- 5 files changed, 20 insertions(+), 11 deletions(-) diff --git a/proof-libs/fstar-secret-integers/core/Makefile b/proof-libs/fstar-secret-integers/core/Makefile index bc9c0c8f4..5f9dc43d0 100644 --- a/proof-libs/fstar-secret-integers/core/Makefile +++ b/proof-libs/fstar-secret-integers/core/Makefile @@ -29,7 +29,7 @@ # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) # -HAX_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar +HAX_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar-secret-integers 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") diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Makefile b/proof-libs/fstar-secret-integers/rust_primitives/Makefile index bc9c0c8f4..5f9dc43d0 100644 --- a/proof-libs/fstar-secret-integers/rust_primitives/Makefile +++ b/proof-libs/fstar-secret-integers/rust_primitives/Makefile @@ -29,7 +29,7 @@ # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) # -HAX_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar +HAX_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar-secret-integers 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") diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fsti b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fsti index 68c03a4e1..d8c45a55e 100644 --- a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fsti +++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fsti @@ -78,6 +78,7 @@ let lemma_slice_append_3 #t (x:t_Slice t) (y:t_Slice t) (z:t_Slice t) (w:t_Slice (ensures (x == concat y (concat z w))) = assert (Seq.equal x (Seq.append y (Seq.append z w))) +#push-options "--z3rlimit 100" let lemma_slice_append_4 #t (x y z w u:t_Slice t) : Lemma (requires (range (v (length y) + v (length z) + v (length w) + v (length u)) usize_inttype /\ length y +! length z +! length w +! length u == length x /\ @@ -87,5 +88,5 @@ let lemma_slice_append_4 #t (x y z w u:t_Slice t) : u == slice x (length y +! length z +! length w) (length x))) (ensures (x == concat y (concat z (concat w u)))) = assert (Seq.equal x (Seq.append y (Seq.append z (Seq.append w u)))) - +#pop-options diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fst b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fst index 055f2a655..1961ab0de 100644 --- a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fst +++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fst @@ -22,6 +22,8 @@ let mk_int_equiv_lemma #_ = admit () let mk_int_v_lemma #t a = () let v_mk_int_lemma #t a = () +let declassify #t #l #l' a = admit() + let add_mod_equiv_lemma #t #l #l' a b = LI.add_mod_lemma #_ #(meet l l') (classify a) (classify b) diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fsti b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fsti index fb59c6885..851f7be57 100644 --- a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fsti +++ b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fsti @@ -162,13 +162,6 @@ let cast_mod (#t:inttype) (#t':inttype) (#l:LI.secrecy_level) (u1:int_t_l t l) = mk_int_l #t' #l (v u1 @%. t') -/// Arithmetic operations -/// -let add_mod (#t:inttype) - (#l #l':LI.secrecy_level) - (a:int_t_l t l) (b:int_t_l t l') = - mk_int_l #t #(meet l l') ((v a + v b) @%. t) - let classify #t #l (#l':LI.secrecy_level{can_flow l l'}) (a:int_t_l t l) : int_t_l t l' = @@ -176,7 +169,20 @@ let classify #t #l (#l':LI.secrecy_level{can_flow l l'}) | LI.PUB, LI.SEC -> LI.secret #t a | LI.PUB, LI.PUB -> a | LI.SEC, LI.SEC -> a - + +(* NOTE: Use with extreme care, and clearly document each use case *) +val declassify #t #l #l' + (a:int_t_l t l) + : int_t_l t l' + + +/// Arithmetic operations +/// +let add_mod (#t:inttype) + (#l #l':LI.secrecy_level) + (a:int_t_l t l) (b:int_t_l t l') = + mk_int_l #t #(meet l l') ((v a + v b) @%. t) + val add_mod_equiv_lemma: #t:uinttype -> #l:LI.secrecy_level -> #l':LI.secrecy_level