Skip to content

Commit 9c4cbfc

Browse files
cfmcfm
committed
refactor: hax Core_models.Convert supports TryFrom<&[T]> but not TryFrom<Vec<T>>
1 parent 9e282ae commit 9c4cbfc

10 files changed

Lines changed: 55 additions & 44 deletions

‎securedrop-protocol/protocol-minimal/proofs/fstar/extraction/Securedrop_protocol_minimal.Message.fst‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -481,14 +481,14 @@ let auth_enc
481481
| Core_models.Result.Result_Ok (c1_vec, cp) ->
482482
let (c1: t_Array u8 (mk_usize 32)):t_Array u8 (mk_usize 32) =
483483
Core_models.Result.impl__expect #(t_Array u8 (mk_usize 32))
484-
#(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
485-
(Core_models.Convert.f_try_into #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
484+
#Core_models.Array.t_TryFromSliceError
485+
(Core_models.Convert.f_try_into #(t_Slice u8)
486486
#(t_Array u8 (mk_usize 32))
487487
#FStar.Tactics.Typeclasses.solve
488-
c1_vec
488+
(Alloc.Vec.impl_1__as_slice #u8 #Alloc.Alloc.t_Global c1_vec <: t_Slice u8)
489489
<:
490490
Core_models.Result.t_Result (t_Array u8 (mk_usize 32))
491-
(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
491+
Core_models.Array.t_TryFromSliceError)
492492
"DHKEM(X25519) encapsulation output has unexpected length"
493493
in
494494
let hax_temp_output:Core_models.Result.t_Result t_MessageCiphertext Anyhow.t_Error =

‎securedrop-protocol/protocol-minimal/proofs/fstar/extraction/Securedrop_protocol_minimal.Metadata.fst‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -201,14 +201,14 @@ let encrypt (pk_r: t_MetadataPublicKey) (m: t_Slice u8) : t_MetadataCiphertext =
201201
in
202202
let (c: t_Array u8 (mk_usize 1120)):t_Array u8 (mk_usize 1120) =
203203
Core_models.Result.impl__expect #(t_Array u8 (mk_usize 1120))
204-
#(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
205-
(Core_models.Convert.f_try_into #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
204+
#Core_models.Array.t_TryFromSliceError
205+
(Core_models.Convert.f_try_into #(t_Slice u8)
206206
#(t_Array u8 (mk_usize 1120))
207207
#FStar.Tactics.Typeclasses.solve
208-
c_vec
208+
(Alloc.Vec.impl_1__as_slice #u8 #Alloc.Alloc.t_Global c_vec <: t_Slice u8)
209209
<:
210210
Core_models.Result.t_Result (t_Array u8 (mk_usize 1120))
211-
(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
211+
Core_models.Array.t_TryFromSliceError)
212212
"X-Wing encapsulation output has unexpected length"
213213
in
214214
{ f_c = c; f_cp = cp } <: t_MetadataCiphertext

‎securedrop-protocol/protocol-minimal/proofs/fstar/extraction/Securedrop_protocol_minimal.Primitives.Dh_akem.fst‎

Lines changed: 13 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -141,18 +141,18 @@ let typed (sk: Libcrux_kem.t_PrivateKey) (pk: Libcrux_kem.t_PublicKey)
141141
else
142142
match
143143
Core_models.Result.impl__map_err #(t_Array u8 (mk_usize 32))
144-
#(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
144+
#Core_models.Array.t_TryFromSliceError
145145
#Anyhow.t_Error
146-
#(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global -> Anyhow.t_Error)
147-
(Core_models.Convert.f_try_into #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
146+
#(Core_models.Array.t_TryFromSliceError -> Anyhow.t_Error)
147+
(Core_models.Convert.f_try_into #(t_Slice u8)
148148
#(t_Array u8 (mk_usize 32))
149149
#FStar.Tactics.Typeclasses.solve
150-
private_key_bytes
150+
(Alloc.Vec.impl_1__as_slice #u8 #Alloc.Alloc.t_Global private_key_bytes <: t_Slice u8)
151151
<:
152152
Core_models.Result.t_Result (t_Array u8 (mk_usize 32))
153-
(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
153+
Core_models.Array.t_TryFromSliceError)
154154
(fun temp_0_ ->
155-
let _:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = temp_0_ in
155+
let _:Core_models.Array.t_TryFromSliceError = temp_0_ in
156156
let error:Anyhow.t_Error =
157157
Anyhow.__private.format_err (Core_models.Fmt.Rt.impl_1__new_const (mk_usize 1)
158158
(let list = ["Failed to convert private key bytes"] in
@@ -169,18 +169,19 @@ let typed (sk: Libcrux_kem.t_PrivateKey) (pk: Libcrux_kem.t_PublicKey)
169169
let private_key:t_DhAkemPrivateKey = impl_DhAkemPrivateKey__from_bytes hoist2 in
170170
(match
171171
Core_models.Result.impl__map_err #(t_Array u8 (mk_usize 32))
172-
#(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
172+
#Core_models.Array.t_TryFromSliceError
173173
#Anyhow.t_Error
174-
#(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global -> Anyhow.t_Error)
175-
(Core_models.Convert.f_try_into #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
174+
#(Core_models.Array.t_TryFromSliceError -> Anyhow.t_Error)
175+
(Core_models.Convert.f_try_into #(t_Slice u8)
176176
#(t_Array u8 (mk_usize 32))
177177
#FStar.Tactics.Typeclasses.solve
178-
public_key_bytes
178+
(Alloc.Vec.impl_1__as_slice #u8 #Alloc.Alloc.t_Global public_key_bytes <: t_Slice u8
179+
)
179180
<:
180181
Core_models.Result.t_Result (t_Array u8 (mk_usize 32))
181-
(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
182+
Core_models.Array.t_TryFromSliceError)
182183
(fun temp_0_ ->
183-
let _:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = temp_0_ in
184+
let _:Core_models.Array.t_TryFromSliceError = temp_0_ in
184185
let error:Anyhow.t_Error =
185186
Anyhow.__private.format_err (Core_models.Fmt.Rt.impl_1__new_const (mk_usize 1)
186187
(let list = ["Failed to convert public key bytes"] in

‎securedrop-protocol/protocol-minimal/proofs/fstar/extraction/Securedrop_protocol_minimal.Primitives.Mlkem.fst‎

Lines changed: 13 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -86,18 +86,18 @@ let typed (sk: Libcrux_kem.t_PrivateKey) (pk: Libcrux_kem.t_PublicKey)
8686
else
8787
match
8888
Core_models.Result.impl__map_err #(t_Array u8 (mk_usize 2400))
89-
#(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
89+
#Core_models.Array.t_TryFromSliceError
9090
#Anyhow.t_Error
91-
#(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global -> Anyhow.t_Error)
92-
(Core_models.Convert.f_try_into #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
91+
#(Core_models.Array.t_TryFromSliceError -> Anyhow.t_Error)
92+
(Core_models.Convert.f_try_into #(t_Slice u8)
9393
#(t_Array u8 (mk_usize 2400))
9494
#FStar.Tactics.Typeclasses.solve
95-
private_key_bytes
95+
(Alloc.Vec.impl_1__as_slice #u8 #Alloc.Alloc.t_Global private_key_bytes <: t_Slice u8)
9696
<:
9797
Core_models.Result.t_Result (t_Array u8 (mk_usize 2400))
98-
(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
98+
Core_models.Array.t_TryFromSliceError)
9999
(fun temp_0_ ->
100-
let _:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = temp_0_ in
100+
let _:Core_models.Array.t_TryFromSliceError = temp_0_ in
101101
let error:Anyhow.t_Error =
102102
Anyhow.__private.format_err (Core_models.Fmt.Rt.impl_1__new_const (mk_usize 1)
103103
(let list = ["Failed to convert private key bytes"] in
@@ -114,18 +114,19 @@ let typed (sk: Libcrux_kem.t_PrivateKey) (pk: Libcrux_kem.t_PublicKey)
114114
let private_key:t_MLKEM768PrivateKey = impl_MLKEM768PrivateKey__from_bytes hoist7 in
115115
(match
116116
Core_models.Result.impl__map_err #(t_Array u8 (mk_usize 1184))
117-
#(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
117+
#Core_models.Array.t_TryFromSliceError
118118
#Anyhow.t_Error
119-
#(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global -> Anyhow.t_Error)
120-
(Core_models.Convert.f_try_into #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
119+
#(Core_models.Array.t_TryFromSliceError -> Anyhow.t_Error)
120+
(Core_models.Convert.f_try_into #(t_Slice u8)
121121
#(t_Array u8 (mk_usize 1184))
122122
#FStar.Tactics.Typeclasses.solve
123-
public_key_bytes
123+
(Alloc.Vec.impl_1__as_slice #u8 #Alloc.Alloc.t_Global public_key_bytes <: t_Slice u8
124+
)
124125
<:
125126
Core_models.Result.t_Result (t_Array u8 (mk_usize 1184))
126-
(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
127+
Core_models.Array.t_TryFromSliceError)
127128
(fun temp_0_ ->
128-
let _:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = temp_0_ in
129+
let _:Core_models.Array.t_TryFromSliceError = temp_0_ in
129130
let error:Anyhow.t_Error =
130131
Anyhow.__private.format_err (Core_models.Fmt.Rt.impl_1__new_const (mk_usize 1)
131132
(let list = ["Failed to convert public key bytes"] in

‎securedrop-protocol/protocol-minimal/proofs/fstar/extraction/Securedrop_protocol_minimal.Primitives.Xwing.fst‎

Lines changed: 13 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -123,18 +123,18 @@ let typed (sk: Libcrux_kem.t_PrivateKey) (pk: Libcrux_kem.t_PublicKey)
123123
else
124124
match
125125
Core_models.Result.impl__map_err #(t_Array u8 (mk_usize 32))
126-
#(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
126+
#Core_models.Array.t_TryFromSliceError
127127
#Anyhow.t_Error
128-
#(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global -> Anyhow.t_Error)
129-
(Core_models.Convert.f_try_into #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
128+
#(Core_models.Array.t_TryFromSliceError -> Anyhow.t_Error)
129+
(Core_models.Convert.f_try_into #(t_Slice u8)
130130
#(t_Array u8 (mk_usize 32))
131131
#FStar.Tactics.Typeclasses.solve
132-
private_key_bytes
132+
(Alloc.Vec.impl_1__as_slice #u8 #Alloc.Alloc.t_Global private_key_bytes <: t_Slice u8)
133133
<:
134134
Core_models.Result.t_Result (t_Array u8 (mk_usize 32))
135-
(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
135+
Core_models.Array.t_TryFromSliceError)
136136
(fun temp_0_ ->
137-
let _:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = temp_0_ in
137+
let _:Core_models.Array.t_TryFromSliceError = temp_0_ in
138138
let error:Anyhow.t_Error =
139139
Anyhow.__private.format_err (Core_models.Fmt.Rt.impl_1__new_const (mk_usize 1)
140140
(let list = ["Failed to convert private key bytes"] in
@@ -151,18 +151,19 @@ let typed (sk: Libcrux_kem.t_PrivateKey) (pk: Libcrux_kem.t_PublicKey)
151151
let private_key:t_XWingPrivateKey = impl_XWingPrivateKey__from_bytes hoist12 in
152152
(match
153153
Core_models.Result.impl__map_err #(t_Array u8 (mk_usize 1216))
154-
#(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
154+
#Core_models.Array.t_TryFromSliceError
155155
#Anyhow.t_Error
156-
#(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global -> Anyhow.t_Error)
157-
(Core_models.Convert.f_try_into #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
156+
#(Core_models.Array.t_TryFromSliceError -> Anyhow.t_Error)
157+
(Core_models.Convert.f_try_into #(t_Slice u8)
158158
#(t_Array u8 (mk_usize 1216))
159159
#FStar.Tactics.Typeclasses.solve
160-
public_key_bytes
160+
(Alloc.Vec.impl_1__as_slice #u8 #Alloc.Alloc.t_Global public_key_bytes <: t_Slice u8
161+
)
161162
<:
162163
Core_models.Result.t_Result (t_Array u8 (mk_usize 1216))
163-
(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
164+
Core_models.Array.t_TryFromSliceError)
164165
(fun temp_0_ ->
165-
let _:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = temp_0_ in
166+
let _:Core_models.Array.t_TryFromSliceError = temp_0_ in
166167
let error:Anyhow.t_Error =
167168
Anyhow.__private.format_err (Core_models.Fmt.Rt.impl_1__new_const (mk_usize 1)
168169
(let list = ["Failed to convert public key bytes"] in

‎securedrop-protocol/protocol-minimal/src/message.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -232,6 +232,7 @@ pub fn auth_enc<R: RngCore + CryptoRng>(
232232

233233
// c1 is always LEN_DHKEM_SHAREDSECRET_ENCAPS bytes for DHKEM(X25519)
234234
let c1: [u8; DH_AKEM_ENCAPS_SECRET_LEN] = c1_vec
235+
.as_slice()
235236
.try_into()
236237
.expect("DHKEM(X25519) encapsulation output has unexpected length");
237238

‎securedrop-protocol/protocol-minimal/src/metadata.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -127,6 +127,7 @@ pub fn encrypt(pk_r: &MetadataPublicKey, m: &[u8]) -> MetadataCiphertext {
127127

128128
// XWing will always produce this length ciphertext, so this .expect is fine.
129129
let c: [u8; LEN_XWING_SHAREDSECRET_ENCAPS] = c_vec
130+
.as_slice()
130131
.try_into()
131132
.expect("X-Wing encapsulation output has unexpected length");
132133

‎securedrop-protocol/protocol-minimal/src/primitives/dh_akem.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -122,11 +122,13 @@ fn typed(
122122

123123
let private_key = DhAkemPrivateKey::from_bytes(
124124
private_key_bytes
125+
.as_slice()
125126
.try_into()
126127
.map_err(|_| anyhow::anyhow!("Failed to convert private key bytes"))?,
127128
);
128129
let public_key = DhAkemPublicKey::from_bytes(
129130
public_key_bytes
131+
.as_slice()
130132
.try_into()
131133
.map_err(|_| anyhow::anyhow!("Failed to convert public key bytes"))?,
132134
);

‎securedrop-protocol/protocol-minimal/src/primitives/mlkem.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -97,11 +97,13 @@ fn typed(
9797

9898
let private_key = MLKEM768PrivateKey::from_bytes(
9999
private_key_bytes
100+
.as_slice()
100101
.try_into()
101102
.map_err(|_| anyhow::anyhow!("Failed to convert private key bytes"))?,
102103
);
103104
let public_key = MLKEM768PublicKey::from_bytes(
104105
public_key_bytes
106+
.as_slice()
105107
.try_into()
106108
.map_err(|_| anyhow::anyhow!("Failed to convert public key bytes"))?,
107109
);

‎securedrop-protocol/protocol-minimal/src/primitives/xwing.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,11 +98,13 @@ fn typed(
9898

9999
let private_key = XWingPrivateKey::from_bytes(
100100
private_key_bytes
101+
.as_slice()
101102
.try_into()
102103
.map_err(|_| anyhow::anyhow!("Failed to convert private key bytes"))?,
103104
);
104105
let public_key = XWingPublicKey::from_bytes(
105106
public_key_bytes
107+
.as_slice()
106108
.try_into()
107109
.map_err(|_| anyhow::anyhow!("Failed to convert public key bytes"))?,
108110
);

0 commit comments

Comments
 (0)