Skip to content

Commit ec48146

Browse files
coord-ecoord-e
committed
Replace some std annotations with thrust_macros
1 parent 1385b70 commit ec48146

1 file changed

Lines changed: 107 additions & 83 deletions

File tree

‎std.rs‎

Lines changed: 107 additions & 83 deletions
Original file line numberDiff line numberDiff line change
@@ -244,98 +244,107 @@ mod thrust_models {
244244
}
245245

246246
#[thrust::extern_spec_fn]
247-
#[thrust::requires(true)]
248-
#[thrust::ensures(result == <x>)]
249-
fn _extern_spec_box_new<T>(x: T) -> Box<T> where T: thrust_models::Model {
247+
#[thrust_macros::requires(true)]
248+
#[thrust_macros::ensures(result == thrust_models::model::Box::new(x))]
249+
fn _extern_spec_box_new<T>(x: T) -> Box<T> where T: thrust_models::Model, T::Ty: PartialEq {
250250
Box::new(x)
251251
}
252252

253253
#[thrust::extern_spec_fn]
254-
#[thrust::requires(true)]
255-
#[thrust::ensures(result == (x == y))]
256-
fn _extern_spec_box_partialeq_eq<T>(x: &Box<T>, y: &Box<T>) -> bool where T: thrust_models::Model + PartialEq {
254+
#[thrust_macros::requires(true)]
255+
#[thrust_macros::ensures(result == (x == y))]
256+
fn _extern_spec_box_partialeq_eq<T>(x: &Box<T>, y: &Box<T>) -> bool
257+
where T: thrust_models::Model + PartialEq, T::Ty: PartialEq
258+
{
257259
<Box<T> as PartialEq>::eq(x, y)
258260
}
259261

260262
#[thrust::extern_spec_fn]
261-
#[thrust::requires(true)]
262-
#[thrust::ensures(*x == ^y && *y == ^x)]
263-
fn _extern_spec_std_mem_swap<T>(x: &mut T, y: &mut T) where T: thrust_models::Model {
263+
#[thrust_macros::requires(true)]
264+
#[thrust_macros::ensures(*x == !y && *y == !x)]
265+
fn _extern_spec_std_mem_swap<T>(x: &mut T, y: &mut T) where T: thrust_models::Model, T::Ty: PartialEq {
264266
std::mem::swap(x, y)
265267
}
266268

267269
#[thrust::extern_spec_fn]
268-
#[thrust::requires(true)]
269-
#[thrust::ensures(^dest == src && result == *dest)]
270-
fn _extern_spec_std_mem_replace<T>(dest: &mut T, src: T) -> T where T: thrust_models::Model {
270+
#[thrust_macros::requires(true)]
271+
#[thrust_macros::ensures(!dest == src && result == *dest)]
272+
fn _extern_spec_std_mem_replace<T>(dest: &mut T, src: T) -> T where T: thrust_models::Model, T::Ty: PartialEq {
271273
std::mem::replace(dest, src)
272274
}
273275

274276
#[thrust::extern_spec_fn]
275-
#[thrust::requires(true)]
276-
#[thrust::ensures(result == (x == y))]
277-
fn _extern_spec_option_partialeq_eq<T>(x: &Option<T>, y: &Option<T>) -> bool where T: thrust_models::Model + PartialEq {
277+
#[thrust_macros::requires(true)]
278+
#[thrust_macros::ensures(result == (x == y))]
279+
fn _extern_spec_option_partialeq_eq<T>(x: &Option<T>, y: &Option<T>) -> bool
280+
where T: thrust_models::Model + PartialEq, T::Ty: PartialEq
281+
{
278282
<Option<T> as PartialEq>::eq(x, y)
279283
}
280284

281285
#[thrust::extern_spec_fn]
282-
#[thrust::requires(opt != std::option::Option::<T0>::None())]
283-
#[thrust::ensures(std::option::Option::<T0>::Some(result) == opt)]
284-
fn _extern_spec_option_unwrap<T>(opt: Option<T>) -> T where T: thrust_models::Model {
286+
#[thrust_macros::requires(opt != None)]
287+
#[thrust_macros::ensures(Some(result) == opt)]
288+
fn _extern_spec_option_unwrap<T>(opt: Option<T>) -> T where T: thrust_models::Model, T::Ty: PartialEq {
285289
Option::unwrap(opt)
286290
}
287291

288292
#[thrust::extern_spec_fn]
289-
#[thrust::requires(true)]
290-
#[thrust::ensures(
291-
(*opt == std::option::Option::<T0>::None() && result == true)
292-
|| (*opt != std::option::Option::<T0>::None() && result == false)
293+
#[thrust_macros::requires(true)]
294+
#[thrust_macros::ensures(
295+
(*opt == None && result == true)
296+
|| (*opt != None && result == false)
293297
)]
294-
fn _extern_spec_option_is_none<T>(opt: &Option<T>) -> bool where T: thrust_models::Model {
298+
fn _extern_spec_option_is_none<T>(opt: &Option<T>) -> bool where T: thrust_models::Model, T::Ty: PartialEq {
295299
Option::is_none(opt)
296300
}
297301

298302
#[thrust::extern_spec_fn]
299-
#[thrust::requires(true)]
300-
#[thrust::ensures(
301-
(*opt == std::option::Option::<T0>::None() && result == false)
302-
|| (*opt != std::option::Option::<T0>::None() && result == true)
303+
#[thrust_macros::requires(true)]
304+
#[thrust_macros::ensures(
305+
(*opt == None && result == false)
306+
|| (*opt != None && result == true)
303307
)]
304-
fn _extern_spec_option_is_some<T>(opt: &Option<T>) -> bool where T: thrust_models::Model {
308+
fn _extern_spec_option_is_some<T>(opt: &Option<T>) -> bool where T: thrust_models::Model, T::Ty: PartialEq {
305309
Option::is_some(opt)
306310
}
307311

308312
#[thrust::extern_spec_fn]
309-
#[thrust::requires(true)]
310-
#[thrust::ensures(
311-
(opt != std::option::Option::<T0>::None() && std::option::Option::<T0>::Some(result) == opt)
312-
|| (opt == std::option::Option::<T0>::None() && result == default)
313+
#[thrust_macros::requires(true)]
314+
#[thrust_macros::ensures(
315+
(opt != None && Some(result) == opt)
316+
|| (opt == None && result == default)
313317
)]
314-
fn _extern_spec_option_unwrap_or<T>(opt: Option<T>, default: T) -> T where T: thrust_models::Model {
318+
fn _extern_spec_option_unwrap_or<T>(opt: Option<T>, default: T) -> T where T: thrust_models::Model, T::Ty: PartialEq {
315319
Option::unwrap_or(opt, default)
316320
}
317321

318322
#[thrust::extern_spec_fn]
319-
#[thrust::requires(true)]
320-
#[thrust::ensures(
321-
(exists x:T0. opt == std::option::Option::<T0>::Some(x) && result == std::result::Result::<T0, T1>::Ok(x))
322-
|| (opt == std::option::Option::<T0>::None() && result == std::result::Result::<T0, T1>::Err(err))
323+
#[thrust_macros::requires(true)]
324+
#[thrust_macros::ensures(
325+
(thrust_models::exists(|x| opt == Some(x) && result == Ok(x)))
326+
|| (opt == None && result == Err(err))
323327
)]
324-
fn _extern_spec_option_ok_or<T, E>(opt: Option<T>, err: E) -> Result<T, E> where T: thrust_models::Model, E: thrust_models::Model {
328+
fn _extern_spec_option_ok_or<T, E>(opt: Option<T>, err: E) -> Result<T, E>
329+
where T: thrust_models::Model, T::Ty: PartialEq,
330+
E: thrust_models::Model, E::Ty: PartialEq,
331+
{
325332
Option::ok_or(opt, err)
326333
}
327334

328335
#[thrust::extern_spec_fn]
329-
#[thrust::requires(true)]
330-
#[thrust::ensures(^opt == std::option::Option::<T0>::None() && result == *opt)]
331-
fn _extern_spec_option_take<T>(opt: &mut Option<T>) -> Option<T> where T: thrust_models::Model {
336+
#[thrust_macros::requires(true)]
337+
#[thrust_macros::ensures(!opt == None && result == *opt)]
338+
fn _extern_spec_option_take<T>(opt: &mut Option<T>) -> Option<T> where T: thrust_models::Model, T::Ty: PartialEq {
332339
Option::take(opt)
333340
}
334341

335342
#[thrust::extern_spec_fn]
336-
#[thrust::requires(true)]
337-
#[thrust::ensures(^opt == std::option::Option::<T0>::Some(src) && result == *opt)]
338-
fn _extern_spec_option_replace<T>(opt: &mut Option<T>, src: T) -> Option<T> where T: thrust_models::Model {
343+
#[thrust_macros::requires(true)]
344+
#[thrust_macros::ensures(!opt == Some(src) && result == *opt)]
345+
fn _extern_spec_option_replace<T>(opt: &mut Option<T>, src: T) -> Option<T>
346+
where T: thrust_models::Model, T::Ty: PartialEq
347+
{
339348
Option::replace(opt, src)
340349
}
341350

@@ -350,63 +359,78 @@ fn _extern_spec_option_as_ref<T>(opt: &Option<T>) -> Option<&T> where T: thrust_
350359
}
351360

352361
#[thrust::extern_spec_fn]
353-
#[thrust::requires(true)]
354-
#[thrust::ensures(
355-
(exists x1:T0, x2:T0.
356-
*opt == std::option::Option::<T0>::Some(x1) &&
357-
^opt == std::option::Option::<T0>::Some(x2) &&
358-
result == std::option::Option::<&mut T0>::Some(<x1, x2>)
362+
#[thrust_macros::requires(true)]
363+
#[thrust_macros::ensures(
364+
thrust_models::exists(|x1, x2|
365+
*opt == Some(x1) &&
366+
!opt == Some(x2) &&
367+
result == Some(thrust_models::model::Mut::new(x1, x2))
359368
)
360369
|| (
361-
*opt == std::option::Option::<T0>::None() &&
362-
^opt == std::option::Option::<T0>::None() &&
363-
result == std::option::Option::<&mut T0>::None()
370+
*opt == None &&
371+
!opt == None &&
372+
result == None
364373
)
365374
)]
366-
fn _extern_spec_option_as_mut<T>(opt: &mut Option<T>) -> Option<&mut T> where T: thrust_models::Model {
375+
fn _extern_spec_option_as_mut<T>(opt: &mut Option<T>) -> Option<&mut T>
376+
where T: thrust_models::Model, T::Ty: PartialEq
377+
{
367378
Option::as_mut(opt)
368379
}
369380

370381
#[thrust::extern_spec_fn]
371-
#[thrust::requires(true)]
372-
#[thrust::ensures(result == (x == y))]
382+
#[thrust_macros::requires(true)]
383+
#[thrust_macros::ensures(result == (x == y))]
373384
fn _extern_spec_result_partialeq_eq<T, E>(x: &Result<T, E>, y: &Result<T, E>) -> bool
374-
where T: thrust_models::Model + PartialEq, E: thrust_models::Model + PartialEq
385+
where T: thrust_models::Model + PartialEq, T::Ty: PartialEq,
386+
E: thrust_models::Model + PartialEq, E::Ty: PartialEq,
375387
{
376388
<Result<T, E> as PartialEq>::eq(x, y)
377389
}
378390

379391
#[thrust::extern_spec_fn]
380-
#[thrust::requires(exists x:T0. res == std::result::Result::<T0, T1>::Ok(x))]
381-
#[thrust::ensures(std::result::Result::<T0, T1>::Ok(result) == res)]
382-
fn _extern_spec_result_unwrap<T, E: std::fmt::Debug>(res: Result<T, E>) -> T where T: thrust_models::Model {
392+
#[thrust_macros::requires(thrust_models::exists(|x| res == Ok(x)))]
393+
#[thrust_macros::ensures(Ok(result) == res)]
394+
fn _extern_spec_result_unwrap<T, E: std::fmt::Debug>(res: Result<T, E>) -> T
395+
where T: thrust_models::Model, T::Ty: PartialEq,
396+
E: thrust_models::Model, E::Ty: PartialEq,
397+
{
383398
Result::unwrap(res)
384399
}
385400

386401
#[thrust::extern_spec_fn]
387-
#[thrust::requires(exists x:T1. res == std::result::Result::<T0, T1>::Err(x))]
388-
#[thrust::ensures(std::result::Result::<T0, T1>::Err(result) == res)]
389-
fn _extern_spec_result_unwrap_err<T: std::fmt::Debug, E>(res: Result<T, E>) -> E where T: thrust_models::Model, E: thrust_models::Model {
402+
#[thrust_macros::requires(thrust_models::exists(|x| res == Err(x)))]
403+
#[thrust_macros::ensures(Err(result) == res)]
404+
fn _extern_spec_result_unwrap_err<T: std::fmt::Debug, E>(res: Result<T, E>) -> E
405+
where T: thrust_models::Model, T::Ty: PartialEq,
406+
E: thrust_models::Model, E::Ty: PartialEq,
407+
{
390408
Result::unwrap_err(res)
391409
}
392410

393411
#[thrust::extern_spec_fn]
394-
#[thrust::requires(true)]
395-
#[thrust::ensures(
396-
(exists x:T0. res == std::result::Result::<T0, T1>::Ok(x) && result == std::option::Option::<T0>::Some(x))
397-
|| (exists x:T1. res == std::result::Result::<T0, T1>::Err(x) && result == std::option::Option::<T0>::None())
412+
#[thrust_macros::requires(true)]
413+
#[thrust_macros::ensures(
414+
thrust_models::exists(|x| res == Ok(x) && result == Some(x))
415+
|| thrust_models::exists(|x| res == Err(x) && result == None)
398416
)]
399-
fn _extern_spec_result_ok<T, E>(res: Result<T, E>) -> Option<T> where T: thrust_models::Model, E: thrust_models::Model {
417+
fn _extern_spec_result_ok<T, E>(res: Result<T, E>) -> Option<T>
418+
where T: thrust_models::Model, T::Ty: PartialEq,
419+
E: thrust_models::Model, E::Ty: PartialEq,
420+
{
400421
Result::ok(res)
401422
}
402423

403424
#[thrust::extern_spec_fn]
404-
#[thrust::requires(true)]
405-
#[thrust::ensures(
406-
(exists x:T0. res == std::result::Result::<T0, T1>::Ok(x) && result == std::option::Option::<T1>::None())
407-
|| (exists x:T1. res == std::result::Result::<T0, T1>::Err(x) && result == std::option::Option::<T1>::Some(x))
425+
#[thrust_macros::requires(true)]
426+
#[thrust_macros::ensures(
427+
thrust_models::exists(|x| res == Ok(x) && result == None)
428+
|| thrust_models::exists(|x| res == Err(x) && result == Some(x))
408429
)]
409-
fn _extern_spec_result_err<T, E>(res: Result<T, E>) -> Option<E> where T: thrust_models::Model, E: thrust_models::Model {
430+
fn _extern_spec_result_err<T, E>(res: Result<T, E>) -> Option<E>
431+
where T: thrust_models::Model, T::Ty: PartialEq,
432+
E: thrust_models::Model, E::Ty: PartialEq,
433+
{
410434
Result::err(res)
411435
}
412436

@@ -431,15 +455,15 @@ fn _extern_spec_result_is_err<T, E>(res: &Result<T, E>) -> bool where T: thrust_
431455
}
432456

433457
#[thrust::extern_spec_fn]
434-
#[thrust::requires(true)] // TODO: require x != i32::MIN
435-
#[thrust::ensures(result >= 0 && (result == x || result == -x))]
458+
#[thrust_macros::requires(true)] // TODO: require x != i32::MIN
459+
#[thrust_macros::ensures(result >= 0 && (result == x || result == -x))]
436460
fn _extern_spec_i32_abs(x: i32) -> i32 {
437461
i32::abs(x)
438462
}
439463

440464
#[thrust::extern_spec_fn]
441-
#[thrust::requires(true)]
442-
#[thrust::ensures(
465+
#[thrust_macros::requires(true)]
466+
#[thrust_macros::ensures(
443467
(x >= y && result == (x - y))
444468
|| (x < y && result == (y - x))
445469
)]
@@ -448,22 +472,22 @@ fn _extern_spec_i32_abs_diff(x: i32, y: i32) -> u32 {
448472
}
449473

450474
#[thrust::extern_spec_fn]
451-
#[thrust::requires(true)]
452-
#[thrust::ensures((x == 0 && result == 0) || (x > 0 && result == 1) || (x < 0 && result == -1))]
475+
#[thrust_macros::requires(true)]
476+
#[thrust_macros::ensures((x == 0 && result == 0) || (x > 0 && result == 1) || (x < 0 && result == -1))]
453477
fn _extern_spec_i32_signum(x: i32) -> i32 {
454478
i32::signum(x)
455479
}
456480

457481
#[thrust::extern_spec_fn]
458-
#[thrust::requires(true)]
459-
#[thrust::ensures((x < 0 && result == false) || (x >= 0 && result == true))]
482+
#[thrust_macros::requires(true)]
483+
#[thrust_macros::ensures((x < 0 && result == false) || (x >= 0 && result == true))]
460484
fn _extern_spec_i32_is_positive(x: i32) -> bool {
461485
i32::is_positive(x)
462486
}
463487

464488
#[thrust::extern_spec_fn]
465-
#[thrust::requires(true)]
466-
#[thrust::ensures((x <= 0 && result == true) || (x > 0 && result == false))]
489+
#[thrust_macros::requires(true)]
490+
#[thrust_macros::ensures((x <= 0 && result == true) || (x > 0 && result == false))]
467491
fn _extern_spec_i32_is_negative(x: i32) -> bool {
468492
i32::is_negative(x)
469493
}

0 commit comments

Comments
 (0)