Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Start transitioning annotated core numbers #1143

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

Start transitioning annotated core numbers #1143

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
168 changes: 168 additions & 0 deletions proof-libs/fstar/generated_core/Core.Base.Binary.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,168 @@
module Core.Base.Binary
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

let rec positive_cmp__cmp_binary_cont
(x y: Core.Base.Spec.Binary.Positive.t_Positive)
(r: Core.Cmp.t_Ordering)
: Core.Cmp.t_Ordering =
match Core.Base.Spec.Binary.Positive.match_positive x with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH ->
(match Core.Base.Spec.Binary.Positive.match_positive y with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH -> r
| Core.Base.Spec.Binary.Positive.POSITIVE_XO q
| Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
Core.Cmp.Ordering_Less <: Core.Cmp.t_Ordering)
| Core.Base.Spec.Binary.Positive.POSITIVE_XO p ->
(match Core.Base.Spec.Binary.Positive.match_positive y with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH ->
Core.Cmp.Ordering_Greater <: Core.Cmp.t_Ordering
| Core.Base.Spec.Binary.Positive.POSITIVE_XO q -> positive_cmp__cmp_binary_cont p q r
| Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
positive_cmp__cmp_binary_cont p q (Core.Cmp.Ordering_Less <: Core.Cmp.t_Ordering))
| Core.Base.Spec.Binary.Positive.POSITIVE_XI p ->
match Core.Base.Spec.Binary.Positive.match_positive y with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH ->
Core.Cmp.Ordering_Greater <: Core.Cmp.t_Ordering
| Core.Base.Spec.Binary.Positive.POSITIVE_XO q ->
positive_cmp__cmp_binary_cont p q (Core.Cmp.Ordering_Greater <: Core.Cmp.t_Ordering)
| Core.Base.Spec.Binary.Positive.POSITIVE_XI q -> positive_cmp__cmp_binary_cont p q r

let positive_cmp (lhs rhs: Core.Base.Spec.Binary.Positive.t_Positive) : Core.Cmp.t_Ordering =
positive_cmp__cmp_binary_cont lhs rhs (Core.Cmp.Ordering_Equal <: Core.Cmp.t_Ordering)

let positive_le (lhs rhs: Core.Base.Spec.Binary.Positive.t_Positive) : bool =
match
Core.Option.Option_Some (positive_cmp lhs rhs) <: Core.Option.t_Option Core.Cmp.t_Ordering
with
| Core.Option.Option_Some (Core.Cmp.Ordering_Less )
| Core.Option.Option_Some (Core.Cmp.Ordering_Equal ) -> true
| _ -> false

let rec positive_pred_double (s: Core.Base.Spec.Binary.Positive.t_Positive)
: Core.Base.Spec.Binary.Positive.t_Positive =
match Core.Base.Spec.Binary.Positive.match_positive s with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH -> Core.Base.Spec.Binary.Positive.xH
| Core.Base.Spec.Binary.Positive.POSITIVE_XO p ->
Core.Base.Spec.Binary.Positive.xI (positive_pred_double p
<:
Core.Base.Spec.Binary.Positive.t_Positive)
| Core.Base.Spec.Binary.Positive.POSITIVE_XI p ->
Core.Base.Spec.Binary.Positive.xI (Core.Base.Spec.Binary.Positive.xO p
<:
Core.Base.Spec.Binary.Positive.t_Positive)

let rec positive_succ (s: Core.Base.Spec.Binary.Positive.t_Positive)
: Core.Base.Spec.Binary.Positive.t_Positive =
match Core.Base.Spec.Binary.Positive.match_positive s with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH ->
Core.Base.Spec.Binary.Positive.xO Core.Base.Spec.Binary.Positive.xH
| Core.Base.Spec.Binary.Positive.POSITIVE_XO q -> Core.Base.Spec.Binary.Positive.xI q
| Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
Core.Base.Spec.Binary.Positive.xO (positive_succ q <: Core.Base.Spec.Binary.Positive.t_Positive)

let positive_add (lhs rhs: Core.Base.Spec.Binary.Positive.t_Positive)
: Core.Base.Spec.Binary.Positive.t_Positive = positive_add__add lhs rhs

let rec positive_mul (lhs rhs: Core.Base.Spec.Binary.Positive.t_Positive)
: Core.Base.Spec.Binary.Positive.t_Positive =
match Core.Base.Spec.Binary.Positive.match_positive lhs with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH -> rhs
| Core.Base.Spec.Binary.Positive.POSITIVE_XO p ->
Core.Base.Spec.Binary.Positive.xO (positive_mul p rhs
<:
Core.Base.Spec.Binary.Positive.t_Positive)
| Core.Base.Spec.Binary.Positive.POSITIVE_XI p ->
positive_add (Core.Clone.f_clone #Core.Base.Spec.Binary.Positive.t_Positive
#FStar.Tactics.Typeclasses.solve
rhs
<:
Core.Base.Spec.Binary.Positive.t_Positive)
(Core.Base.Spec.Binary.Positive.xO (positive_mul p rhs
<:
Core.Base.Spec.Binary.Positive.t_Positive)
<:
Core.Base.Spec.Binary.Positive.t_Positive)

let rec positive_add__add (lhs rhs: Core.Base.Spec.Binary.Positive.t_Positive)
: Core.Base.Spec.Binary.Positive.t_Positive =
match Core.Base.Spec.Binary.Positive.match_positive lhs with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH ->
(match Core.Base.Spec.Binary.Positive.match_positive rhs with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH ->
Core.Base.Spec.Binary.Positive.xO Core.Base.Spec.Binary.Positive.xH
| Core.Base.Spec.Binary.Positive.POSITIVE_XO q -> Core.Base.Spec.Binary.Positive.xI q
| Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
Core.Base.Spec.Binary.Positive.xO (positive_succ q
<:
Core.Base.Spec.Binary.Positive.t_Positive))
| Core.Base.Spec.Binary.Positive.POSITIVE_XO p ->
(match Core.Base.Spec.Binary.Positive.match_positive rhs with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH -> Core.Base.Spec.Binary.Positive.xI p
| Core.Base.Spec.Binary.Positive.POSITIVE_XO q ->
Core.Base.Spec.Binary.Positive.xO (positive_add__add p q
<:
Core.Base.Spec.Binary.Positive.t_Positive)
| Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
Core.Base.Spec.Binary.Positive.xI (positive_add__add p q
<:
Core.Base.Spec.Binary.Positive.t_Positive))
| Core.Base.Spec.Binary.Positive.POSITIVE_XI p ->
match Core.Base.Spec.Binary.Positive.match_positive rhs with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH ->
Core.Base.Spec.Binary.Positive.xO (positive_succ p
<:
Core.Base.Spec.Binary.Positive.t_Positive)
| Core.Base.Spec.Binary.Positive.POSITIVE_XO q ->
Core.Base.Spec.Binary.Positive.xI (positive_add__add p q
<:
Core.Base.Spec.Binary.Positive.t_Positive)
| Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
Core.Base.Spec.Binary.Positive.xO (positive_add__add_carry p q
<:
Core.Base.Spec.Binary.Positive.t_Positive)

and positive_add__add_carry (lhs rhs: Core.Base.Spec.Binary.Positive.t_Positive)
: Core.Base.Spec.Binary.Positive.t_Positive =
match Core.Base.Spec.Binary.Positive.match_positive lhs with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH ->
(match Core.Base.Spec.Binary.Positive.match_positive rhs with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH ->
Core.Base.Spec.Binary.Positive.xI Core.Base.Spec.Binary.Positive.xH
| Core.Base.Spec.Binary.Positive.POSITIVE_XO q ->
Core.Base.Spec.Binary.Positive.xO (positive_succ q
<:
Core.Base.Spec.Binary.Positive.t_Positive)
| Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
Core.Base.Spec.Binary.Positive.xI (positive_succ q
<:
Core.Base.Spec.Binary.Positive.t_Positive))
| Core.Base.Spec.Binary.Positive.POSITIVE_XO p ->
(match Core.Base.Spec.Binary.Positive.match_positive rhs with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH ->
Core.Base.Spec.Binary.Positive.xO (positive_succ p
<:
Core.Base.Spec.Binary.Positive.t_Positive)
| Core.Base.Spec.Binary.Positive.POSITIVE_XO q ->
Core.Base.Spec.Binary.Positive.xI (positive_add__add p q
<:
Core.Base.Spec.Binary.Positive.t_Positive)
| Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
Core.Base.Spec.Binary.Positive.xO (positive_add__add_carry p q
<:
Core.Base.Spec.Binary.Positive.t_Positive))
| Core.Base.Spec.Binary.Positive.POSITIVE_XI p ->
match Core.Base.Spec.Binary.Positive.match_positive rhs with
| Core.Base.Spec.Binary.Positive.POSITIVE_XH ->
Core.Base.Spec.Binary.Positive.xI (positive_succ p
<:
Core.Base.Spec.Binary.Positive.t_Positive)
| Core.Base.Spec.Binary.Positive.POSITIVE_XO q ->
Core.Base.Spec.Binary.Positive.xO (positive_add__add_carry p q
<:
Core.Base.Spec.Binary.Positive.t_Positive)
| Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
Core.Base.Spec.Binary.Positive.xI (positive_add__add_carry p q
<:
Core.Base.Spec.Binary.Positive.t_Positive)
76 changes: 76 additions & 0 deletions proof-libs/fstar/generated_core/Core.Base.Number_conversion.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
module Core.Base.Number_conversion
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

include Core.Intrinsics.Rec_bundle_253787241 {from_u128_binary as impl_24__from_u128_binary}

include Core.Intrinsics.Rec_bundle_253787241 {impl_8 as impl_8}

include Core.Intrinsics.Rec_bundle_253787241 {impl_20 as impl_20}

include Core.Intrinsics.Rec_bundle_253787241 {from_u16_binary as impl_24__from_u16_binary}

include Core.Intrinsics.Rec_bundle_253787241 {impl_2 as impl_2}

include Core.Intrinsics.Rec_bundle_253787241 {impl_14 as impl_14}

include Core.Intrinsics.Rec_bundle_253787241 {from_u32_binary as impl_24__from_u32_binary}

include Core.Intrinsics.Rec_bundle_253787241 {impl_4 as impl_4}

include Core.Intrinsics.Rec_bundle_253787241 {impl_16 as impl_16}

include Core.Intrinsics.Rec_bundle_253787241 {from_u64_binary as impl_24__from_u64_binary}

include Core.Intrinsics.Rec_bundle_253787241 {impl_6 as impl_6}

include Core.Intrinsics.Rec_bundle_253787241 {impl_18 as impl_18}

include Core.Intrinsics.Rec_bundle_253787241 {from_u8_binary as impl_24__from_u8_binary}

include Core.Intrinsics.Rec_bundle_253787241 {impl as impl}

include Core.Intrinsics.Rec_bundle_253787241 {impl_12 as impl_12}

include Core.Intrinsics.Rec_bundle_253787241 {from_usize_binary as impl_24__from_usize_binary}

include Core.Intrinsics.Rec_bundle_253787241 {impl_10 as impl_10}

include Core.Intrinsics.Rec_bundle_253787241 {impl_22 as impl_22}

include Core.Intrinsics.Rec_bundle_253787241 {to_u128_binary as impl_24__to_u128_binary}

include Core.Intrinsics.Rec_bundle_253787241 {impl_9 as impl_9}

include Core.Intrinsics.Rec_bundle_253787241 {impl_21 as impl_21}

include Core.Intrinsics.Rec_bundle_253787241 {to_u16_binary as impl_24__to_u16_binary}

include Core.Intrinsics.Rec_bundle_253787241 {impl_3 as impl_3}

include Core.Intrinsics.Rec_bundle_253787241 {impl_15 as impl_15}

include Core.Intrinsics.Rec_bundle_253787241 {to_u32_binary as impl_24__to_u32_binary}

include Core.Intrinsics.Rec_bundle_253787241 {impl_5 as impl_5}

include Core.Intrinsics.Rec_bundle_253787241 {impl_17 as impl_17}

include Core.Intrinsics.Rec_bundle_253787241 {to_u64_binary as impl_24__to_u64_binary}

include Core.Intrinsics.Rec_bundle_253787241 {impl_7 as impl_7}

include Core.Intrinsics.Rec_bundle_253787241 {impl_19 as impl_19}

include Core.Intrinsics.Rec_bundle_253787241 {to_u8_binary as impl_24__to_u8_binary}

include Core.Intrinsics.Rec_bundle_253787241 {impl_1 as impl_1}

include Core.Intrinsics.Rec_bundle_253787241 {impl_13 as impl_13}

include Core.Intrinsics.Rec_bundle_253787241 {to_usize_binary as impl_24__to_usize_binary}

include Core.Intrinsics.Rec_bundle_253787241 {impl_11 as impl_11}

include Core.Intrinsics.Rec_bundle_253787241 {impl_23 as impl_23}
Loading