hax-lib 0.4.0

Hax-specific helpers for Rust programs
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81

module Core_models.Mem.Transmutability
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core_models
open FStar.Mul


val f_transmute__panic_cold_explicit: Prims.unit
  -> Prims.Pure Rust_primitives.Hax.t_Never Prims.l_True (fun _ -> Prims.l_True)

type t_Assume = {
  f_alignment:bool;
  f_lifetimes:bool;
  f_safety:bool;
  f_validity:bool
}

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl_5:Core_models.Marker.t_StructuralPartialEq t_Assume

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl_6:Core_models.Cmp.t_PartialEq t_Assume t_Assume

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl_7:Core_models.Cmp.t_Eq t_Assume

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl_8:Core_models.Clone.t_Clone t_Assume

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl_9:Core_models.Marker.t_Copy t_Assume

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl_10:Core_models.Fmt.t_Debug t_Assume

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl_1:Core_models.Marker.t_UnsizedConstParamTy t_Assume

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl:Core_models.Marker.t_ConstParamTy_ t_Assume

let impl_Assume__NOTHING: t_Assume = () <: t_Assume

let impl_Assume__ALIGNMENT: t_Assume = () <: t_Assume

let impl_Assume__LIFETIMES: t_Assume = () <: t_Assume

let impl_Assume__SAFETY: t_Assume = () <: t_Assume

let impl_Assume__VALIDITY: t_Assume = () <: t_Assume

val impl_Assume__and (self other_assumptions: t_Assume)
    : Prims.Pure t_Assume Prims.l_True (fun _ -> Prims.l_True)

val impl_Assume__but_not (self other_assumptions: t_Assume)
    : Prims.Pure t_Assume Prims.l_True (fun _ -> Prims.l_True)

val f_add__impl_3__panic_cold_explicit: Prims.unit
  -> Prims.Pure Rust_primitives.Hax.t_Never Prims.l_True (fun _ -> Prims.l_True)

val f_sub__impl_4__panic_cold_explicit: Prims.unit
  -> Prims.Pure Rust_primitives.Hax.t_Never Prims.l_True (fun _ -> Prims.l_True)

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_3: Core_models.Ops.Arith.t_Add t_Assume t_Assume =
  {
    f_Output = t_Assume;
    f_Output_11695847888444666345 = FStar.Tactics.Typeclasses.solve;
    f_add_pre = (fun (self: t_Assume) (other_assumptions: t_Assume) -> true);
    f_add_post = (fun (self: t_Assume) (other_assumptions: t_Assume) (out: t_Assume) -> true);
    f_add = fun (self: t_Assume) (other_assumptions: t_Assume) -> () <: t_Assume
  }

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_4: Core_models.Ops.Arith.t_Sub t_Assume t_Assume =
  {
    f_Output = t_Assume;
    f_Output_9381071510542709353 = FStar.Tactics.Typeclasses.solve;
    f_sub_pre = (fun (self: t_Assume) (other_assumptions: t_Assume) -> true);
    f_sub_post = (fun (self: t_Assume) (other_assumptions: t_Assume) (out: t_Assume) -> true);
    f_sub = fun (self: t_Assume) (other_assumptions: t_Assume) -> () <: t_Assume
  }