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

Make compatible with current mathcomp #1039

Merged
merged 1 commit into from
Feb 3, 2025
Merged

Make compatible with current mathcomp #1039

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
3 changes: 1 addition & 2 deletions proofs/arch/asm_gen.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
Require Import
oseq
compiler_util
expr
fexpr
Expand All @@ -12,7 +11,7 @@ Require Import
arch_decl
arch_extra.
Import Utf8 String.
Import compiler_util.
Import compiler_util oseq.

Module E.

Expand Down
2 changes: 1 addition & 1 deletion proofs/arch/asm_gen_proof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
From mathcomp Require Import fintype finfun ssralg.
From Coq Require Import Relation_Operators.
Require Import
oseq
compiler_util
psem
psem_facts
Expand All @@ -20,6 +19,7 @@ Require Import
sem_params_of_arch_extra.
Require Export asm_gen.
Import Utf8.
Import oseq.

Section ASM_EXTRA.

Expand Down
2 changes: 1 addition & 1 deletion proofs/compiler/arm_stack_zeroization_proof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
From mathcomp Require Import word_ssrZ.
From Coq Require Import Lia.

Require Import seq_extra.
Require Import
expr
fexpr
Expand All @@ -24,6 +23,7 @@ Require Import
arm_instr_decl
arm_params_common_proof.
Require Export arm_stack_zeroization.
Import seq_extra.

(* FIXME: We should use the higher-level [eval_lsem] lemmas. *)
Section FIXME.
Expand Down
2 changes: 1 addition & 1 deletion proofs/compiler/riscv_stack_zeroization_proof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
From mathcomp Require Import word_ssrZ.
Require Import Lia.

Require Import seq_extra.
Require Import
expr
fexpr
Expand All @@ -24,6 +23,7 @@ Require Import
riscv_instr_decl
riscv_params_common_proof.
Require Export riscv_stack_zeroization.
Import seq_extra.

(* FIXME: We should use the higher-level [eval_lsem] lemmas. *)
Section FIXME.
Expand Down
4 changes: 2 additions & 2 deletions proofs/compiler/tunneling_proof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,13 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
From Coq Require Import ZArith.
From Coq Require Import Utf8.

Require Import oseq expr_facts compiler_util label linear linear_sem.
Require Import expr_facts compiler_util label linear linear_sem.
Require Import sem_params.
Import word_ssrZ.

Local Open Scope seq_scope.

Require Import seq_extra unionfind tunneling unionfind_proof.
Require Import oseq seq_extra unionfind tunneling unionfind_proof.
Require Import linear_sem.


Expand Down
2 changes: 1 addition & 1 deletion proofs/compiler/x86_stack_zeroization_proof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
From mathcomp Require Import word_ssrZ.
From Coq Require Import Lia.

Require Import seq_extra.
Require Import
expr
fexpr
Expand All @@ -23,6 +22,7 @@ Require Import
x86_extra
x86_instr_decl.
Require Export x86_stack_zeroization.
Import seq_extra.

(* FIXME: We should use the higher-level [eval_lsem] lemmas. *)
Section FIXME.
Expand Down