Skip to content

Adapt to rocq-prover/rocq#21987 (secvar status) #533

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
samuelgruetter merged 1 commit into from
May 26, 2026
Merged

Adapt to rocq-prover/rocq#21987 (secvar status) #533

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
32 changes: 28 additions & 4 deletions bedrock2/src/bedrock2/LeakageWeakestPreconditionProperties.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,9 +21,9 @@ Section WeakestPrecondition.
when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
we'd get a typechecking failure at Qed time. *)
repeat match goal with x : ?T |- _ => first
[ constr_eq T X; move x before pick_sp
| constr_eq T X; move x before ext_spec
| constr_eq T X; move x before locals
[ constr_eq x pick_sp
| constr_eq x ext_spec
| constr_eq x locals

@SkySkimmer SkySkimmer May 22, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this is basically emulating a "is_section_variable" tactic, I could have added one in rocq-prover/rocq#21987 but we would need this code for backwards compat anyway so I think it will wait for another PR

| constr_eq T X; move x at top
| revert x ] end;
match goal with x : X |- _ => induction x end;
Expand Down Expand Up @@ -83,6 +83,30 @@ Section WeakestPrecondition.
Context {locals_ok : map.ok locals}.
Context {ext_spec_ok : LeakageSemantics.ext_spec.ok ext_spec}.

Ltac ind_on X ::=
intros;
(* Note: Comment below dates from when we were using a parameter record p *)
(* Note: "before p" means actually "after p" when reading from top to bottom, because,
as the manual points out, "before" and "after" are with respect to the direction of
the move, and we're moving hypotheses upwards here.
We need to make sure not to revert/clear p, because the other lemmas depend on it.
If we still reverted/cleared p, we'd get errors like
"Error: Proper_load depends on the variable p which is not declared in the context."
when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
we'd get a typechecking failure at Qed time. *)
repeat match goal with x : ?T |- _ => first
[ constr_eq x ext_spec_ok
| constr_eq x locals_ok
| constr_eq x mem_ok
| constr_eq x word_ok
| constr_eq x pick_sp
| constr_eq x ext_spec
| constr_eq x locals
| constr_eq T X; move x at top
| revert x ] end;
match goal with x : X |- _ => induction x end;
intros.

Global Instance Proper_cmd :
Proper (
(pointwise_relation _ (
Expand Down Expand Up @@ -112,7 +136,7 @@ Section WeakestPrecondition.
{ destruct H1 as (?&?&?&?). eexists. eexists. split.
{ eapply Proper_expr; eauto; cbv [pointwise_relation Basics.impl]; eauto. }
{ intuition eauto 6. } }
{ eapply H4; eauto. simpl. intros. eauto. }
{ match goal with h : _ |- _ => solve [eapply h; eauto; simpl; intros; eauto] end. }
{ eapply LeakageSemantics.exec.weaken; eassumption. }
{ destruct H1 as (?&?&?&?). eexists. eexists. split.
{ eapply Proper_list_map'; eauto; try exact H4; cbv [respectful pointwise_relation Basics.impl]; intuition eauto 2.
Expand Down
27 changes: 25 additions & 2 deletions bedrock2/src/bedrock2/MetricWeakestPreconditionProperties.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@ Section MetricWeakestPrecondition.
when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
we'd get a typechecking failure at Qed time. *)
repeat match goal with x : ?T |- _ => first
[ constr_eq T X; move x before ext_spec
| constr_eq T X; move x before locals
[ constr_eq x ext_spec
| constr_eq x locals
| constr_eq T X; move x at top
| revert x ] end;
match goal with x : X |- _ => induction x end;
Expand Down Expand Up @@ -72,6 +72,29 @@ Section MetricWeakestPrecondition.
Context {locals_ok : map.ok locals}.
Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.

Ltac ind_on X ::=
intros;
(* Note: Comment below dates from when we were using a parameter record p *)
(* Note: "before p" means actually "after p" when reading from top to bottom, because,
as the manual points out, "before" and "after" are with respect to the direction of
the move, and we're moving hypotheses upwards here.
We need to make sure not to revert/clear p, because the other lemmas depend on it.
If we still reverted/cleared p, we'd get errors like
"Error: Proper_load depends on the variable p which is not declared in the context."
when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
we'd get a typechecking failure at Qed time. *)
repeat match goal with x : ?T |- _ => first
[ constr_eq x ext_spec
| constr_eq x locals
| constr_eq x word_ok
| constr_eq x mem_ok
| constr_eq x locals_ok
| constr_eq x ext_spec_ok
| constr_eq T X; move x at top
| revert x ] end;
match goal with x : X |- _ => induction x end;
intros.

Global Instance Proper_cmd :
Proper
(pointwise_relation _ (
Expand Down
26 changes: 24 additions & 2 deletions bedrock2/src/bedrock2/WeakestPreconditionProperties.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,8 @@ Section WeakestPrecondition.
when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
we'd get a typechecking failure at Qed time. *)
repeat match goal with x : ?T |- _ => first
[ constr_eq T X; move x before ext_spec
| constr_eq T X; move x before locals
[ constr_eq x ext_spec
| constr_eq x locals
| constr_eq T X; move x at top
| revert x ] end;
match goal with x : X |- _ => induction x end;
Expand Down Expand Up @@ -69,6 +69,28 @@ Section WeakestPrecondition.
Context {locals_ok : map.ok locals}.
Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.

Ltac ind_on X ::=
intros;
(* Note: Comment below dates from when we were using a parameter record p *)
(* Note: "before p" means actually "after p" when reading from top to bottom, because,
as the manual points out, "before" and "after" are with respect to the direction of
the move, and we're moving hypotheses upwards here.
We need to make sure not to revert/clear p, because the other lemmas depend on it.
If we still reverted/cleared p, we'd get errors like
"Error: Proper_load depends on the variable p which is not declared in the context."
when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
we'd get a typechecking failure at Qed time. *)
repeat match goal with x : ?T |- _ => first
[ constr_eq x ext_spec
| constr_eq x locals
| constr_eq x word_ok
| constr_eq x locals_ok
| constr_eq x ext_spec_ok
| constr_eq T X; move x at top
| revert x ] end;
match goal with x : X |- _ => induction x end;
intros.

Global Instance Proper_cmd :
Proper (
(pointwise_relation _ (
Expand Down
7 changes: 5 additions & 2 deletions compiler/src/compiler/ForeverSafe.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,10 @@ Section ForeverSafe.
runsTo (mcomp_sat (run1 iset)) st safe1 ->
mcomp_sat (run1 iset) st (fun st' => runsTo (mcomp_sat (run1 iset)) st' safe1).
Proof.
induction 1; rename P into safe1.
(* avoid induction generalizing safe1 which prevents using run_pong
alternative: pose proof run_pong before induction then use the resulting hyp *)
remember safe1 as safe1' eqn:E in |-*. apply eq_sym in E.
induction 1; rename P into safe1'; subst safe1'.
- pose proof (run_1_2 _ H) as P. inversion P.
+ exfalso. eapply exclusive; eauto.
+ eapply mcomp_sat_weaken. 2: eassumption.
Expand All @@ -98,7 +101,7 @@ Section ForeverSafe.
- eapply mcomp_sat_weaken. 2: eassumption.
intros.
eapply H0. assumption.
Fail Qed. Abort. (* TODO report *)

@SkySkimmer SkySkimmer May 22, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess this TODO report was about some section variable bug fixed by rocq-prover/rocq#21987

Succeed Qed. Abort.

(* one step of invariant preservation: *)
Lemma runsTo_safe1_inv: forall (st: RiscvMachineL),
Expand Down
Loading