Skip to content

Commit 362d9ea

Browse files
samuelgruettersamuelgruetter
authored
Merge pull request #533 from SkySkimmer/context-secvar
Adapt to rocq-prover/rocq#21987 (secvar status)
2 parents 25aad83 + 8a6e344 commit 362d9ea

4 files changed

Lines changed: 82 additions & 10 deletions

File tree

‎bedrock2/src/bedrock2/LeakageWeakestPreconditionProperties.v‎

Lines changed: 28 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -21,9 +21,9 @@ Section WeakestPrecondition.
2121
when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
2222
we'd get a typechecking failure at Qed time. *)
2323
repeat match goal with x : ?T |- _ => first
24-
[ constr_eq T X; move x before pick_sp
25-
| constr_eq T X; move x before ext_spec
26-
| constr_eq T X; move x before locals
24+
[ constr_eq x pick_sp
25+
| constr_eq x ext_spec
26+
| constr_eq x locals
2727
| constr_eq T X; move x at top
2828
| revert x ] end;
2929
match goal with x : X |- _ => induction x end;
@@ -83,6 +83,30 @@ Section WeakestPrecondition.
8383
Context {locals_ok : map.ok locals}.
8484
Context {ext_spec_ok : LeakageSemantics.ext_spec.ok ext_spec}.
8585

86+
Ltac ind_on X ::=
87+
intros;
88+
(* Note: Comment below dates from when we were using a parameter record p *)
89+
(* Note: "before p" means actually "after p" when reading from top to bottom, because,
90+
as the manual points out, "before" and "after" are with respect to the direction of
91+
the move, and we're moving hypotheses upwards here.
92+
We need to make sure not to revert/clear p, because the other lemmas depend on it.
93+
If we still reverted/cleared p, we'd get errors like
94+
"Error: Proper_load depends on the variable p which is not declared in the context."
95+
when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
96+
we'd get a typechecking failure at Qed time. *)
97+
repeat match goal with x : ?T |- _ => first
98+
[ constr_eq x ext_spec_ok
99+
| constr_eq x locals_ok
100+
| constr_eq x mem_ok
101+
| constr_eq x word_ok
102+
| constr_eq x pick_sp
103+
| constr_eq x ext_spec
104+
| constr_eq x locals
105+
| constr_eq T X; move x at top
106+
| revert x ] end;
107+
match goal with x : X |- _ => induction x end;
108+
intros.
109+
86110
Global Instance Proper_cmd :
87111
Proper (
88112
(pointwise_relation _ (
@@ -112,7 +136,7 @@ Section WeakestPrecondition.
112136
{ destruct H1 as (?&?&?&?). eexists. eexists. split.
113137
{ eapply Proper_expr; eauto; cbv [pointwise_relation Basics.impl]; eauto. }
114138
{ intuition eauto 6. } }
115-
{ eapply H4; eauto. simpl. intros. eauto. }
139+
{ match goal with h : _ |- _ => solve [eapply h; eauto; simpl; intros; eauto] end. }
116140
{ eapply LeakageSemantics.exec.weaken; eassumption. }
117141
{ destruct H1 as (?&?&?&?). eexists. eexists. split.
118142
{ eapply Proper_list_map'; eauto; try exact H4; cbv [respectful pointwise_relation Basics.impl]; intuition eauto 2.

‎bedrock2/src/bedrock2/MetricWeakestPreconditionProperties.v‎

Lines changed: 25 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@ Section MetricWeakestPrecondition.
2222
when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
2323
we'd get a typechecking failure at Qed time. *)
2424
repeat match goal with x : ?T |- _ => first
25-
[ constr_eq T X; move x before ext_spec
26-
| constr_eq T X; move x before locals
25+
[ constr_eq x ext_spec
26+
| constr_eq x locals
2727
| constr_eq T X; move x at top
2828
| revert x ] end;
2929
match goal with x : X |- _ => induction x end;
@@ -72,6 +72,29 @@ Section MetricWeakestPrecondition.
7272
Context {locals_ok : map.ok locals}.
7373
Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
7474

75+
Ltac ind_on X ::=
76+
intros;
77+
(* Note: Comment below dates from when we were using a parameter record p *)
78+
(* Note: "before p" means actually "after p" when reading from top to bottom, because,
79+
as the manual points out, "before" and "after" are with respect to the direction of
80+
the move, and we're moving hypotheses upwards here.
81+
We need to make sure not to revert/clear p, because the other lemmas depend on it.
82+
If we still reverted/cleared p, we'd get errors like
83+
"Error: Proper_load depends on the variable p which is not declared in the context."
84+
when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
85+
we'd get a typechecking failure at Qed time. *)
86+
repeat match goal with x : ?T |- _ => first
87+
[ constr_eq x ext_spec
88+
| constr_eq x locals
89+
| constr_eq x word_ok
90+
| constr_eq x mem_ok
91+
| constr_eq x locals_ok
92+
| constr_eq x ext_spec_ok
93+
| constr_eq T X; move x at top
94+
| revert x ] end;
95+
match goal with x : X |- _ => induction x end;
96+
intros.
97+
7598
Global Instance Proper_cmd :
7699
Proper
77100
(pointwise_relation _ (

‎bedrock2/src/bedrock2/WeakestPreconditionProperties.v‎

Lines changed: 24 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,8 @@ Section WeakestPrecondition.
2121
when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
2222
we'd get a typechecking failure at Qed time. *)
2323
repeat match goal with x : ?T |- _ => first
24-
[ constr_eq T X; move x before ext_spec
25-
| constr_eq T X; move x before locals
24+
[ constr_eq x ext_spec
25+
| constr_eq x locals
2626
| constr_eq T X; move x at top
2727
| revert x ] end;
2828
match goal with x : X |- _ => induction x end;
@@ -69,6 +69,28 @@ Section WeakestPrecondition.
6969
Context {locals_ok : map.ok locals}.
7070
Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
7171

72+
Ltac ind_on X ::=
73+
intros;
74+
(* Note: Comment below dates from when we were using a parameter record p *)
75+
(* Note: "before p" means actually "after p" when reading from top to bottom, because,
76+
as the manual points out, "before" and "after" are with respect to the direction of
77+
the move, and we're moving hypotheses upwards here.
78+
We need to make sure not to revert/clear p, because the other lemmas depend on it.
79+
If we still reverted/cleared p, we'd get errors like
80+
"Error: Proper_load depends on the variable p which is not declared in the context."
81+
when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
82+
we'd get a typechecking failure at Qed time. *)
83+
repeat match goal with x : ?T |- _ => first
84+
[ constr_eq x ext_spec
85+
| constr_eq x locals
86+
| constr_eq x word_ok
87+
| constr_eq x locals_ok
88+
| constr_eq x ext_spec_ok
89+
| constr_eq T X; move x at top
90+
| revert x ] end;
91+
match goal with x : X |- _ => induction x end;
92+
intros.
93+
7294
Global Instance Proper_cmd :
7395
Proper (
7496
(pointwise_relation _ (

‎compiler/src/compiler/ForeverSafe.v‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,10 @@ Section ForeverSafe.
8989
runsTo (mcomp_sat (run1 iset)) st safe1 ->
9090
mcomp_sat (run1 iset) st (fun st' => runsTo (mcomp_sat (run1 iset)) st' safe1).
9191
Proof.
92-
induction 1; rename P into safe1.
92+
(* avoid induction generalizing safe1 which prevents using run_pong
93+
alternative: pose proof run_pong before induction then use the resulting hyp *)
94+
remember safe1 as safe1' eqn:E in |-*. apply eq_sym in E.
95+
induction 1; rename P into safe1'; subst safe1'.
9396
- pose proof (run_1_2 _ H) as P. inversion P.
9497
+ exfalso. eapply exclusive; eauto.
9598
+ eapply mcomp_sat_weaken. 2: eassumption.
@@ -98,7 +101,7 @@ Section ForeverSafe.
98101
- eapply mcomp_sat_weaken. 2: eassumption.
99102
intros.
100103
eapply H0. assumption.
101-
Fail Qed. Abort. (* TODO report *)
104+
Succeed Qed. Abort.
102105

103106
(* one step of invariant preservation: *)
104107
Lemma runsTo_safe1_inv: forall (st: RiscvMachineL),

0 commit comments

Comments
 (0)