Skip to content

Commit a6a0949

Browse files
msprotzmsprotz
committed
Remove more trailing whitespace
1 parent 4dddeb8 commit a6a0949

22 files changed

Lines changed: 111 additions & 111 deletions

‎code/sha3/Hacl.Hash.SHA3.Scalar.fst‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -171,7 +171,7 @@ let state_free s =
171171
[@@ Comment "Absorb number of input blocks and write the output state
172172
173173
This function is intended to receive a hash state and input buffer.
174-
It prcoesses an input of multiple of 168-bytes (SHAKE128 block size),
174+
It processes an input of multiple of 168-bytes (SHAKE128 block size),
175175
any additional bytes of final partial block are ignored.
176176
177177
The argument `state` (IN/OUT) points to hash state, i.e., uint64_t[25]
@@ -194,14 +194,14 @@ let shake128_absorb_nblocks state input inputByteLen =
194194
[@@ Comment "Absorb a final partial block of input and write the output state
195195
196196
This function is intended to receive a hash state and input buffer.
197-
It prcoesses a sequence of bytes at end of input buffer that is less
197+
It processes a sequence of bytes at end of input buffer that is less
198198
than 168-bytes (SHAKE128 block size),
199199
any bytes of full blocks at start of input buffer are ignored.
200200
201201
The argument `state` (IN/OUT) points to hash state, i.e., uint64_t[25]
202202
The argument `input` (IN) points to `inputByteLen` bytes of valid memory,
203203
i.e., uint8_t[inputByteLen]
204-
204+
205205
Note: Full size of input buffer must be passed to `inputByteLen` including
206206
the number of full-block bytes at start of input buffer that are ignored"]
207207
val shake128_absorb_final:
@@ -236,7 +236,7 @@ val shake128_squeeze_nblocks:
236236
live h output /\ live h state /\ disjoint output state)
237237
(ensures fun h0 _ h1 ->
238238
modifies (loc state |+| loc output) h0 h1 /\
239-
(let s', b' =
239+
(let s', b' =
240240
V.squeeze_nblocks #M32 168 (v outputByteLen) (as_seq h0 state, as_seq_multi h0 (ntup1 output)) in
241241
as_seq h1 state == s' /\
242242
as_seq_multi h1 (ntup1 output) == b'))

‎code/sha3/Hacl.Hash.SHA3.Simd256.fst‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -359,12 +359,12 @@ let state_free s =
359359
[@@ Comment "Absorb number of blocks of 4 input buffers and write the output states
360360
361361
This function is intended to receive a quadruple hash state and 4 input buffers.
362-
It prcoesses an inputs of multiple of 168-bytes (SHAKE128 block size),
362+
It processes an inputs of multiple of 168-bytes (SHAKE128 block size),
363363
any additional bytes of final partial block for each buffer are ignored.
364364
365365
The argument `state` (IN/OUT) points to quadruple hash state,
366366
i.e., Lib_IntVector_Intrinsics_vec256[25]
367-
The arguments `input0/input1/input2/input3` (IN) point to `inputByteLen` bytes
367+
The arguments `input0/input1/input2/input3` (IN) point to `inputByteLen` bytes
368368
of valid memory for each buffer, i.e., uint8_t[inputByteLen]"]
369369
val shake128_absorb_nblocks:
370370
state:lbuffer_t MUT (vec_t U64 4) 25ul
@@ -392,15 +392,15 @@ let shake128_absorb_nblocks state _ input0 input1 input2 input3 inputByteLen =
392392
[@@ Comment "Absorb a final partial blocks of 4 input buffers and write the output states
393393
394394
This function is intended to receive a quadruple hash state and 4 input buffers.
395-
It prcoesses a sequence of bytes at end of each input buffer that is less
395+
It processes a sequence of bytes at end of each input buffer that is less
396396
than 168-bytes (SHAKE128 block size),
397397
any bytes of full blocks at start of input buffers are ignored.
398398
399399
The argument `state` (IN/OUT) points to quadruple hash state,
400400
i.e., Lib_IntVector_Intrinsics_vec256[25]
401-
The arguments `input0/input1/input2/input3` (IN) point to `inputByteLen` bytes
401+
The arguments `input0/input1/input2/input3` (IN) point to `inputByteLen` bytes
402402
of valid memory for each buffer, i.e., uint8_t[inputByteLen]
403-
403+
404404
Note: Full size of input buffers must be passed to `inputByteLen` including
405405
the number of full-block bytes at start of each input buffer that are ignored"]
406406
val shake128_absorb_final:
@@ -434,7 +434,7 @@ let shake128_absorb_final state _ input0 input1 input2 input3 inputByteLen =
434434
435435
The argument `state` (IN) points to quadruple hash state,
436436
i.e., Lib_IntVector_Intrinsics_vec256[25]
437-
The arguments `output0/output1/output2/output3` (OUT) point to `outputByteLen` bytes
437+
The arguments `output0/output1/output2/output3` (OUT) point to `outputByteLen` bytes
438438
of valid memory for each buffer, i.e., uint8_t[inputByteLen]"]
439439
val shake128_squeeze_nblocks:
440440
state:lbuffer_t MUT (vec_t U64 4) 25ul
@@ -460,7 +460,7 @@ val shake128_squeeze_nblocks:
460460
disjoint output3 state)
461461
(ensures fun h0 _ h1 ->
462462
modifies (loc state |+| loc output0 |+| loc output1 |+| loc output2 |+| loc output3) h0 h1 /\
463-
(let s', b' =
463+
(let s', b' =
464464
V.squeeze_nblocks #M256 168 (v outputByteLen) (as_seq h0 state, as_seq_multi h0 (ntup4 #(lbuffer uint8 outputByteLen) #4 (output0, (output1, (output2, output3))))) in
465465
as_seq h1 state == s' /\
466466
as_seq_multi h1 (ntup4 #(lbuffer uint8 outputByteLen) #4 (output0, (output1, (output2, output3)))) == b'))

‎code/sha3/Hacl.Impl.SHA3.Vec.fsti‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ val squeeze_nblocks: #m:m_spec
104104
disjoint_multi b s)
105105
(ensures fun h0 _ h1 ->
106106
modifies (loc s |+| loc_multi b) h0 h1 /\
107-
(let s', b' =
107+
(let s', b' =
108108
V.squeeze_nblocks #m (v rateInBytes) (v outputByteLen) (as_seq h0 s, as_seq_multi h0 b) in
109109
as_seq h1 s == s' /\
110110
as_seq_multi h1 b == b'))

‎code/sha3/Hacl.Spec.SHA3.Equiv.fst‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -556,7 +556,7 @@ val loadState_lemma_l:
556556
Lemma
557557
(requires
558558
forall l. l < lanes m ==> (forall j. (j >= r /\ j < 256) ==> Seq.index b.(|l|) j == u8 0))
559-
(ensures
559+
(ensures
560560
(state_spec_v (loadState #m r b s)).[l] ==
561561
Spec.loadState r (Seq.slice b.(|l|) 0 r) (state_spec_v s).[l])
562562

@@ -1043,7 +1043,7 @@ let storeState_update_b_last_lemma_l #m r outputByteLen outRem b s l =
10431043
val absorb_inner_lemma_l:
10441044
#m:m_spec
10451045
-> r:size_nat{r > 0 /\ r <= 200}
1046-
-> input:multiseq (lanes m) 256{forall l. l < lanes m ==>
1046+
-> input:multiseq (lanes m) 256{forall l. l < lanes m ==>
10471047
(forall i. (i >= r /\ i < 256) ==> Seq.index input.(|l|) i == u8 0)}
10481048
-> s:state_spec m
10491049
-> l:nat{l < lanes m} ->
@@ -1163,12 +1163,12 @@ val load_last_block_lemma_helper:
11631163
Seq.index b rem == byte_to_uint8 delimitedSuffix /\
11641164
(forall i. (i >= (rem + 1) /\ i < r) ==> Seq.index b i == u8 0))
11651165

1166-
let load_last_block_lemma_helper #m delimitedSuffix r rem input =
1166+
let load_last_block_lemma_helper #m delimitedSuffix r rem input =
11671167
let b_0 = update_sub (create r (u8 0)) 0 rem input in
11681168
let b = b_0.[rem] <- byte_to_uint8 delimitedSuffix in
11691169
eq_intro (slice #uint8 #r b_0 (rem + 1) r)
11701170
(create (r - (rem + 1)) (u8 0));
1171-
assert (forall j. (j >= 0 /\ j < (r - (rem + 1))) ==>
1171+
assert (forall j. (j >= 0 /\ j < (r - (rem + 1))) ==>
11721172
Seq.index (slice #uint8 #r b (rem + 1) r) j ==
11731173
Seq.index b ((rem + 1) + j));
11741174
assert (forall j. (j >= (rem + 1) /\ j < r) ==> (j - (rem + 1) >= 0))
@@ -1178,7 +1178,7 @@ let load_last_block_lemma_helper #m delimitedSuffix r rem input =
11781178
-> delimitedSuffix:byte_t
11791179
-> r:size_nat{r > 0 /\ r <= 200}
11801180
-> rem:size_nat{rem < r}
1181-
-> input:multiseq (lanes m) 256{forall l. l < lanes m ==>
1181+
-> input:multiseq (lanes m) 256{forall l. l < lanes m ==>
11821182
(forall i. (i >= rem /\ i < 256) ==> Seq.index input.(|l|) i == u8 0)}
11831183
-> l:nat{l < lanes m} ->
11841184
Lemma
@@ -1197,7 +1197,7 @@ val absorb_last_lemma_l:
11971197
-> delimitedSuffix:byte_t
11981198
-> r:size_nat{r > 0 /\ r <= 200}
11991199
-> rem:size_nat{rem < r}
1200-
-> input:multiseq (lanes m) 256{forall l. l < lanes m ==>
1200+
-> input:multiseq (lanes m) 256{forall l. l < lanes m ==>
12011201
(forall i. (i >= rem /\ i < 256) ==> Seq.index input.(|l|) i == u8 0)}
12021202
-> s:state_spec m
12031203
-> l:nat{l < lanes m} ->
@@ -1457,7 +1457,7 @@ let absorb_inner_repeat_blocks_multi_lemma r inputByteLen input s =
14571457
reveal_vec_1 U64;
14581458
let aux_s (i:nat{i < 25}) : Lemma (s.[i] == (vec_v #U64 #1 s.[i]).[0]) =
14591459
reveal_vec_v_1 #U64 s.[i] in
1460-
let aux_n (i:nat{i < 25}) : Lemma ((absorb_inner_nblocks #M32 r inputByteLen input s).[i] ==
1460+
let aux_n (i:nat{i < 25}) : Lemma ((absorb_inner_nblocks #M32 r inputByteLen input s).[i] ==
14611461
((vec_v (absorb_inner_nblocks #M32 r inputByteLen input s).[i]).[0] <: vec_t U64 1)) =
14621462
reveal_vec_v_1 (absorb_inner_nblocks #M32 r inputByteLen input s).[i] in
14631463

@@ -1473,7 +1473,7 @@ let absorb_inner_block_r_lemma r input s =
14731473
reveal_vec_1 U64;
14741474
let aux_s (i:nat{i < 25}) : Lemma (s.[i] == (vec_v #U64 #1 s.[i]).[0]) =
14751475
reveal_vec_v_1 #U64 s.[i] in
1476-
let aux_n (i:nat{i < 25}) : Lemma ((absorb_inner_block #M32 r r input 0 s).[i] ==
1476+
let aux_n (i:nat{i < 25}) : Lemma ((absorb_inner_block #M32 r r input 0 s).[i] ==
14771477
((vec_v (absorb_inner_block #M32 r r input 0 s).[i]).[0] <: vec_t U64 1)) =
14781478
reveal_vec_v_1 (absorb_inner_block #M32 r r input 0 s).[i] in
14791479

@@ -1491,7 +1491,7 @@ let absorb_last_r_lemma delimitedSuffix r inputByteLen input s =
14911491
let aux_s (i:nat{i < 25}) : Lemma (s.[i] == (vec_v #U64 #1 s.[i]).[0]) =
14921492
reveal_vec_v_1 #U64 s.[i] in
14931493
let aux_n (i:nat{i < 25}) : Lemma
1494-
((absorb_final #M32 s r inputByteLen input delimitedSuffix).[i] ==
1494+
((absorb_final #M32 s r inputByteLen input delimitedSuffix).[i] ==
14951495
((vec_v (absorb_final #M32 s r inputByteLen input
14961496
delimitedSuffix).[i]).[0] <: vec_t U64 1)) =
14971497
reveal_vec_v_1 (absorb_final #M32 s r inputByteLen input delimitedSuffix).[i] in

0 commit comments

Comments
 (0)