Skip to content

Adapt to [big_sepL2_range_Z_l] change. #183

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

Merged
rlepigre-skylabs-ai merged 1 commit into from
Sep 18, 2026
+28 −8
Merged

Adapt to [big_sepL2_range_Z_l] change. #183

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
17 changes: 17 additions & 0 deletions rocq-brick-libstdcpp/proof/compare/spec.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,7 @@ Section with_cpp.
\prepost{q v} this |-> weak_orderingR q v
\post{result}[Vptr result] result |-> partial_orderingR 1$m (Some v)).

#[ignore_missing]
cpp.spec "std::__cmp_cat::__unspec::__unspec(std::__cmp_cat::__unspec*)" as unspec_ctor from source with (
\this this
\arg{p} "" (Vptr p)
Expand All @@ -109,111 +110,127 @@ Section with_cpp.
\pre this |-> unspecR 1$m
\post emp).

#[ignore_missing]
cpp.spec "std::operator==(std::partial_ordering, std::__cmp_cat::__unspec)" as partial_ordering_eq_unspec from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\prepost{q_lhs lhs_v} lhs |-> partial_orderingR q_lhs lhs_v
\pre{q_rhs} rhs |-> unspecR q_rhs
\post[Vbool (bool_decide (lhs_v = Some Eq))] rhs |-> unspecR q_rhs).

#[ignore_missing]
cpp.spec "std::operator<(std::partial_ordering, std::__cmp_cat::__unspec)" as partial_ordering_lt_unspec from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\prepost{q_lhs lhs_v} lhs |-> partial_orderingR q_lhs lhs_v
\pre{q_rhs} rhs |-> unspecR q_rhs
\post[Vbool (bool_decide (lhs_v = Some Lt))] rhs |-> unspecR q_rhs).

#[ignore_missing]
cpp.spec "std::operator>(std::partial_ordering, std::__cmp_cat::__unspec)" as partial_ordering_gt_unspec from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\prepost{q_lhs lhs_v} lhs |-> partial_orderingR q_lhs lhs_v
\pre{q_rhs} rhs |-> unspecR q_rhs
\post[Vbool (bool_decide (lhs_v = Some Gt))] rhs |-> unspecR q_rhs).

#[ignore_missing]
cpp.spec "std::operator<=>(std::partial_ordering, std::__cmp_cat::__unspec)" as partial_ordering_cmp_unspec from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\prepost{q_lhs lhs_v} lhs |-> partial_orderingR q_lhs lhs_v
\pre{q_rhs} rhs |-> unspecR q_rhs
\post{result}[Vptr result] result |-> partial_orderingR 1$m lhs_v ** rhs |-> unspecR q_rhs).

#[ignore_missing]
cpp.spec "std::operator<(std::strong_ordering, std::__cmp_cat::__unspec)" as strong_ordering_lt_unspec from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\prepost{q_lhs lhs_v} lhs |-> strong_orderingR q_lhs lhs_v
\pre{q_rhs} rhs |-> unspecR q_rhs
\post[Vbool (bool_decide (lhs_v = Lt))] rhs |-> unspecR q_rhs).

#[ignore_missing]
cpp.spec "std::operator==(std::strong_ordering, std::__cmp_cat::__unspec)" as strong_ordering_eq_unspec from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\prepost{q_lhs lhs_v} lhs |-> strong_orderingR q_lhs lhs_v
\pre{q_rhs} rhs |-> unspecR q_rhs
\post[Vbool (bool_decide (lhs_v = Eq))] rhs |-> unspecR q_rhs).

#[ignore_missing]
cpp.spec "std::operator>(std::strong_ordering, std::__cmp_cat::__unspec)" as strong_ordering_gt_unspec from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\prepost{q_lhs lhs_v} lhs |-> strong_orderingR q_lhs lhs_v
\pre{q_rhs} rhs |-> unspecR q_rhs
\post[Vbool (bool_decide (lhs_v = Gt))] rhs |-> unspecR q_rhs).

#[ignore_missing]
cpp.spec "std::operator<=>(std::strong_ordering, std::__cmp_cat::__unspec)" as strong_ordering_cmp_unspec from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\prepost{q_lhs lhs_v} lhs |-> strong_orderingR q_lhs lhs_v
\pre{q_rhs} rhs |-> unspecR q_rhs
\post{result}[Vptr result] result |-> strong_orderingR 1$m lhs_v ** rhs |-> unspecR q_rhs).

#[ignore_missing]
cpp.spec "std::operator==(std::weak_ordering, std::__cmp_cat::__unspec)" as weak_ordering_eq_unspec from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\prepost{q_lhs lhs_v} lhs |-> weak_orderingR q_lhs lhs_v
\pre{q_rhs} rhs |-> unspecR q_rhs
\post[Vbool (bool_decide (lhs_v = Eq))] rhs |-> unspecR q_rhs).

#[ignore_missing]
cpp.spec "std::operator>(std::weak_ordering, std::__cmp_cat::__unspec)" as weak_ordering_gt_unspec from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\prepost{q_lhs lhs_v} lhs |-> weak_orderingR q_lhs lhs_v
\pre{q_rhs} rhs |-> unspecR q_rhs
\post[Vbool (bool_decide (lhs_v = Gt))] rhs |-> unspecR q_rhs).

#[ignore_missing]
cpp.spec "std::operator<=>(std::weak_ordering, std::__cmp_cat::__unspec)" as weak_ordering_cmp_unspec from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\prepost{q_lhs lhs_v} lhs |-> weak_orderingR q_lhs lhs_v
\pre{q_rhs} rhs |-> unspecR q_rhs
\post{result}[Vptr result] result |-> weak_orderingR 1$m lhs_v ** rhs |-> unspecR q_rhs).

#[ignore_missing]
cpp.spec "std::operator<(std::__cmp_cat::__unspec, std::partial_ordering)" as unspec_lt_partial_ordering from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\pre{q_lhs} lhs |-> unspecR q_lhs
\prepost{q_rhs rhs_v} rhs |-> partial_orderingR q_rhs rhs_v
\post[Vbool (bool_decide (rhs_v = Some Gt))] lhs |-> unspecR q_lhs).

#[ignore_missing]
cpp.spec "std::operator<=>(std::__cmp_cat::__unspec, std::partial_ordering)" as unspec_cmp_partial_ordering from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\pre{q_lhs} lhs |-> unspecR q_lhs
\prepost{q_rhs rhs_v} rhs |-> partial_orderingR q_rhs rhs_v
\post{result}[Vptr result] result |-> partial_orderingR 1$m (CompOpp <$> rhs_v) ** lhs |-> unspecR q_lhs).

#[ignore_missing]
cpp.spec "std::operator>(std::__cmp_cat::__unspec, std::strong_ordering)" as unspec_gt_strong_ordering from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\pre{q_lhs} lhs |-> unspecR q_lhs
\prepost{q_rhs rhs_v} rhs |-> strong_orderingR q_rhs rhs_v
\post[Vbool (bool_decide (rhs_v = Lt))] lhs |-> unspecR q_lhs).

#[ignore_missing]
cpp.spec "std::operator<=>(std::__cmp_cat::__unspec, std::strong_ordering)" as unspec_cmp_strong_ordering from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
\pre{q_lhs} lhs |-> unspecR q_lhs
\prepost{q_rhs rhs_v} rhs |-> strong_orderingR q_rhs rhs_v
\post{result}[Vptr result] result |-> strong_orderingR 1$m (CompOpp rhs_v) ** lhs |-> unspecR q_lhs).

#[ignore_missing]
cpp.spec "std::operator<=>(std::__cmp_cat::__unspec, std::weak_ordering)" as unspec_cmp_weak_ordering from source with (
\arg{lhs} "" (Vptr lhs)
\arg{rhs} "" (Vptr rhs)
Expand Down
19 changes: 11 additions & 8 deletions rocq-brick-libstdcpp/proof/iterator/spec.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -357,9 +357,9 @@ NES.Begin std.
iApply (observe with "A").
auto using observe_only_provable_impl, obs_Forall2_big_sepL2. }
f_equiv; rewrite !only_provable_True // !left_id; f_equiv.
rewrite big_sepL2_rangeZ_l -Hrng; last first.
{ rewrite lengthN_rangeZ. lia. }
apply big_sepL_proper => k y.
rewrite big_sepL2_rangeZ_l -Hrng only_provable_True; last first.
{ rewrite lengthN_rangeZ Z2N.id; lia. }
rewrite left_id. apply big_sepL_proper => k y.
rewrite lookup_rangeZ => - [_ ->].
by rewrite only_provable_True // left_id.
Qed.
Expand Down Expand Up @@ -531,10 +531,11 @@ NES.Begin std.
rewrite o_sub_sub Hi_len.
iFrame "#".
rewrite [ [| i ≤ j |] ] only_provable_True // left_id.
rewrite !big_sepL2_rangeZ_l //; last first.
{ rewrite lengthN_rangeZ. lia. }
rewrite 1!big_opL_fmap.
rewrite (big_opL_rangeZ vs) //.
rewrite !big_sepL2_rangeZ_l 1!big_opL_fmap.
rewrite [ [| lengthZ vs = _ |] ]only_provable_True; last lia.
rewrite left_id.
rewrite (big_opL_rangeZ vs) //. rewrite -bi.sep_assoc.
iSplit. { iPureIntro. rewrite lengthN_rangeZ. lia. }
rewrite -big_opL_op.
iApply (big_sepL_mono with "SEP") => k x Hx.
rewrite only_provable_True // left_id.
Expand All @@ -551,7 +552,9 @@ NES.Begin std.
rewrite length_fmap -lengthZ_correct o_sub_sub.
have -> : i + lengthZ vs = j by lia.
iFrame "valid".
rewrite !big_sepL2_rangeZ_l // !big_opL_fmap.
rewrite !big_sepL2_rangeZ_l.
rewrite !only_provable_True ?left_id; try lia.
rewrite !big_opL_fmap.
rewrite (big_opL_rangeZ vs) //.
iCombine "SEP B" as "A".
rewrite -big_opL_op.
Expand Down
Loading