From 0f303a57452f4dbcdecd07bf9b3a51a8f5b57300 Mon Sep 17 00:00:00 2001 From: Arvind Arasu Date: Mon, 13 Nov 2023 14:11:03 -0800 Subject: [PATCH] remove the unused old/ folder --- steel/crypto/old/Veritas.HashAccumulator.fst | 167 ------------------ steel/crypto/old/Veritas.HashAccumulator.fsti | 121 ------------- 2 files changed, 288 deletions(-) delete mode 100644 steel/crypto/old/Veritas.HashAccumulator.fst delete mode 100644 steel/crypto/old/Veritas.HashAccumulator.fsti diff --git a/steel/crypto/old/Veritas.HashAccumulator.fst b/steel/crypto/old/Veritas.HashAccumulator.fst deleted file mode 100644 index 606f8b78..00000000 --- a/steel/crypto/old/Veritas.HashAccumulator.fst +++ /dev/null @@ -1,167 +0,0 @@ -module Veritas.HashAccumulator - -#set-options "--fuel 0 --ifuel 0" - -module ST = FStar.HyperStack.ST -module HS = FStar.HyperStack -module B = LowStar.Buffer -module G = FStar.Ghost -module S = FStar.Seq -module U8 = FStar.UInt8 -module U32 = FStar.UInt32 -module U64 = FStar.UInt64 - -open FStar.HyperStack.ST -open LowStar.BufferOps - -let initial_hash - = Seq.create 32 0uy - -let hash_value (s:Seq.seq U8.t { Seq.length s <= blake2_max_input_length }) - : hash_value_t - = Hacl.Blake2b_32.spec s 0 Seq.empty 32 - - -noextract inline_for_extraction -let xor_bytes (s1: Seq.seq U8.t) - (s2: Seq.seq U8.t { S.length s1 == S.length s2 }) - : s3:Seq.seq U8.t { S.length s3 == S.length s1 } - = S.init (S.length s1) (fun i -> S.index s1 i `FStar.UInt8.logxor` S.index s2 i) - -let aggregate_hash_value (h0 h1: hash_value_t) - : hash_value_t - = xor_bytes h0 h1 - -let as_hash_value_pfx (b:hash_value_buf) (h:HS.mem) (n:nat { n <= 32 }) = - Seq.slice (as_hash_value b h) 0 n - -let state = hash_value_buf - -let invariant s h = B.live h s /\ B.freeable s - -let v_hash (s:state) (h:HS.mem) - : GTot hash_value_t - = as_hash_value s h - -let footprint s = B.loc_addr_of_buffer s - -let frame _ _ _ _ = () - -//////////////////////////////////////////////////////////////////////////////// - -(** Create an instance of a hash accumulator in the heap *) -let create_in () = B.malloc HS.root 0uy 32ul - -//////////////////////////////////////////////////////////////////////////////// -let aggregate_hash_value_buf b1 b2 = - let h0 = ST.get () in - let inv h (i:nat) = - let s1 = B.as_seq h0 b1 in - let s2 = B.as_seq h0 b2 in - i <= 32 /\ - B.live h b1 /\ - B.live h b2 /\ - Seq.slice (B.as_seq h b1) i 32 `Seq.equal` Seq.slice s1 i 32 /\ - B.modifies (B.loc_buffer b1) h0 h /\ - as_hash_value_pfx b1 h i `Seq.equal` - xor_bytes (Seq.slice s1 0 i) (Seq.slice s2 0 i) - in - let extend_inv (h:HS.mem) (i:nat) (h':HS.mem) - : Lemma - (requires - inv h i /\ - i < 32 /\ - B.as_seq h' b1 == - Seq.upd (B.as_seq h b1) - i - (U8.logxor - (B.get h b1 i) - (B.get h b2 i))) - (ensures ( - let s1 = B.as_seq h0 b1 in - let s2 = B.as_seq h0 b2 in - as_hash_value_pfx b1 h' (i + 1) `Seq.equal` - xor_bytes (Seq.slice s1 0 (i + 1)) - (Seq.slice s2 0 (i + 1)) /\ - Seq.slice (B.as_seq h' b1) (i + 1) 32 `Seq.equal` - Seq.slice s1 (i + 1) 32)) - = let s1 = B.as_seq h0 b1 in - let s2 = B.as_seq h0 b2 in - let s1_h = B.as_seq h b1 in - let s1_h' = B.as_seq h' b1 in - assert (as_hash_value_pfx b1 h' (i + 1) `Seq.equal` - Seq.snoc (as_hash_value_pfx b1 h i) - (Seq.index s1_h' i)); - assert (xor_bytes (Seq.slice s1 0 (i + 1)) - (Seq.slice s2 0 (i + 1)) `Seq.equal` - Seq.snoc - (xor_bytes (Seq.slice s1 0 i) - (Seq.slice s2 0 i)) - (U8.logxor (Seq.index s1 i) (Seq.index s2 i))); - assert (Seq.index (B.as_seq h b2) i == Seq.index s2 i); - assert (Seq.slice (B.as_seq h b1) i 32 == Seq.slice s1 i 32); - Seq.lemma_index_slice s1 i 32 0; - assert (Seq.index (B.as_seq h b1) i == Seq.index s1 i); - assert ((Seq.index s1_h' i) == - (U8.logxor (Seq.index s1 i) (Seq.index s2 i))); - assert (Seq.slice s1 (i + 1) 32 `Seq.equal` Seq.tail (Seq.slice s1 i 32)); - assert (Seq.slice (B.as_seq h' b1) (i + 1) 32 `Seq.equal` - Seq.tail (Seq.slice (B.as_seq h' b1) i 32)); - assert (Seq.slice (B.as_seq h' b1) (i + 1) 32 `Seq.equal` - Seq.slice s1 (i + 1) 32) - in - [@@inline_let] - let body (i:U32.t { U32.v i < 32 }) - : Stack unit - (fun h -> inv h (U32.v i)) - (fun h0 _ h1 -> inv h1 (U32.v i + 1)) - = let h = ST.get () in - let v1 = B.index b1 i in - let v2 = B.index b2 i in - B.upd b1 i (U8.logxor v1 v2); - let h' = ST.get () in - extend_inv h (U32.v i) h' - in - assert (inv h0 0); - let _ = - C.Loops.for 0ul 32ul inv body - in - let h = ST.get () in - assert (inv h 32); - assert (Seq.slice (B.as_seq h0 b1) 0 32 `Seq.equal` (B.as_seq h0 b1)); - assert (Seq.slice (B.as_seq h0 b2) 0 32 `Seq.equal` (B.as_seq h0 b2)); - B.gsub_zero_length b1; - assert (B.gsub b1 0ul 32ul == b1); - assert (as_hash_value b1 h == - aggregate_hash_value (as_hash_value b1 h0) (as_hash_value b2 h0)) - -//////////////////////////////////////////////////////////////////////////////// -let add s b l = - let h0 = ST.get () in - let b = B.sub b 0ul (Ghost.hide l) in - assert (invariant s h0); - push_frame (); - let acc = s in - let h1 = ST.get () in - assert (invariant s h1); - let tmp = B.alloca 0uy 32ul in - assert_norm (64 + Hacl.Blake2b_32.size_block < pow2 32); - assert_norm (64 < pow2 32); - assert_norm (64 <= Hacl.Blake2b_32.max_key); - let h1' = ST.get () in - Hacl.Blake2b_32.blake2b 32ul tmp l b 0ul B.null; - let h2 = ST.get () in - assert (B.as_seq h1' B.null `Seq.equal` Seq.empty #U8.t); - assert (B.as_seq h2 tmp == hash_value (B.as_seq h1 b)); - aggregate_hash_value_buf acc tmp; - let h = ST.get () in - assert (v_hash s h == - aggregate_hash_value (v_hash s h0) - (hash_value (B.as_seq h0 b))); - pop_frame () - -//////////////////////////////////////////////////////////////////////////////// -let get s out = B.blit s 0ul out 0ul 32ul - -//////////////////////////////////////////////////////////////////////////////// -let free s = B.free s diff --git a/steel/crypto/old/Veritas.HashAccumulator.fsti b/steel/crypto/old/Veritas.HashAccumulator.fsti deleted file mode 100644 index 172436b1..00000000 --- a/steel/crypto/old/Veritas.HashAccumulator.fsti +++ /dev/null @@ -1,121 +0,0 @@ -module Veritas.HashAccumulator - -#set-options "--fuel 0 --ifuel 0" - -module ST = FStar.HyperStack.ST -module HS = FStar.HyperStack -module B = LowStar.Buffer -module G = FStar.Ghost -module S = FStar.Seq -module U8 = FStar.UInt8 -module U32 = FStar.UInt32 -module U64 = FStar.UInt64 - -open FStar.HyperStack.ST - -// JP: not being agile over the hash algorithm for the moment, can be improved -// later; any keyed hash will do, HMAC would also work, AES-CMAC is the one -// currently used in Veritas - -// Note: this restriction does not come from the spec but rather from the -// implementation. Is this really necessary? See discussion on Slack, could -// easily be 2 ^ 64 - 128. -inline_for_extraction noextract -let blake2_max_input_length = pow2 32 - 1 - 128 - -// NOTE: we do not have an agile spec for the keyed hash functionality :(, so -// we're making Blake2-dependent assumptions without corresponding agile predicates -noextract inline_for_extraction -let hashable_bytes = s:Seq.seq U8.t { Seq.length s <= blake2_max_input_length } -let hashable_buffer = b:B.buffer U8.t { B.length b <= blake2_max_input_length } - -let hash_value_t = Seq.lseq U8.t 32 - -val initial_hash - : hash_value_t - -val hash_value (_:hashable_bytes) - : hash_value_t - -val aggregate_hash_value (_ _: hash_value_t) - : hash_value_t - -let hash_value_buf = B.lbuffer U8.t 32 - -let as_hash_value (b:hash_value_buf) (h:HS.mem) - : GTot hash_value_t - = B.as_seq h b - -val state: Type0 - -val invariant (s: state) (h:HS.mem) : Type0 - -val v_hash (s:state) (h:HS.mem) - : GTot hash_value_t - -(** A bunch of infrastructure related to framing **) -val footprint (s: state): GTot B.loc - -val frame: l:B.loc -> s:state -> h0:HS.mem -> h1:HS.mem -> Lemma - (requires ( - invariant s h0 /\ - B.loc_disjoint l (footprint s) /\ - B.modifies l h0 h1)) - (ensures ( - invariant s h1 /\ - v_hash s h0 == v_hash s h1)) - -(*** THE MAIN INTERFACE ***) - -(** Create an instance of a hash accumulator in the heap *) -val create_in: unit -> ST state - (requires fun h0 -> True) - (ensures fun h0 s h1 -> - invariant s h1 /\ - B.(modifies loc_none h0 h1) /\ - B.fresh_loc (footprint s) h0 h1 /\ - v_hash s h1 == initial_hash) - -(** Combine two hash values held in b1 and b2 into b1 *) -val aggregate_hash_value_buf (b1: hash_value_buf) (b2: hash_value_buf) - : Stack unit - (requires fun h0 -> - B.live h0 b1 /\ - B.live h0 b2 /\ - B.disjoint b1 b2) - (ensures fun h0 _ h1 -> - B.(modifies (loc_buffer b1) h0 h1) /\ - as_hash_value b1 h1 == aggregate_hash_value (as_hash_value b1 h0) - (as_hash_value b2 h0)) - -(** Hash the (input[0, l)) into the hash accumulate s *) -val add: s:state -> input:hashable_buffer -> l:U32.t -> Stack unit - (requires fun h0 -> - invariant s h0 /\ - B.live h0 input /\ - B.(loc_disjoint (loc_buffer input) (footprint s)) /\ - U32.v l <= U32.v (B.len input)) - (ensures fun h0 _ h1 -> - invariant s h1 /\ - B.modifies (footprint s) h0 h1 /\ - v_hash s h1 == - aggregate_hash_value (v_hash s h0) - (hash_value (Seq.slice (B.as_seq h0 input) 0 (U32.v l)))) - -(** Read the current value of the hash into out *) -val get: s:state -> out:hash_value_buf -> Stack unit - (requires fun h0 -> - invariant s h0 /\ - B.live h0 out /\ - B.loc_disjoint (B.loc_buffer out) (footprint s)) - (ensures fun h0 r h1 -> - invariant s h0 /\ - B.modifies (B.loc_buffer out) h0 h1 /\ - v_hash s h0 == as_hash_value out h1) - -(** Free the hash accumulator *) -val free: s:state -> ST unit - (requires fun h0 -> - invariant s h0) - (ensures (fun h0 _ h1 -> - B.modifies (footprint s) h0 h1))