Skip to content
Proof PR

arch-split Refine up to InvariantUpdates_H #3168

Sign in to view logs

arch-split Refine up to InvariantUpdates_H

arch-split Refine up to InvariantUpdates_H #3168

Triggered via pull request February 16, 2025 21:59
@XaphiosisXaphiosis
synchronize #853
Status Cancelled
Total duration 3m 9s
Artifacts –

proof.yml

on: pull_request_target
Matrix: All
Fit to window
Zoom out
Zoom in

Annotations

12 errors
Axioms: proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy#L19
Locales or definitions should usually be preferred to axioms, because axioms may make the logic inconsistent. Merely introducing a new constant (without new laws) is fine, though.
Axioms: proof/invariant-abstract/RISCV64/ArchInvariants_AI.thy#L19
Locales or definitions should usually be preferred to axioms, because axioms may make the logic inconsistent. Merely introducing a new constant (without new laws) is fine, though.
All (ARM)
Canceling since a higher priority waiting request for 'l4v-Proof PR-853-idx-0' exists
All (ARM)
The operation was canceled.
All (AARCH64)
Canceling since a higher priority waiting request for 'l4v-Proof PR-853-idx-2' exists
All (AARCH64)
The operation was canceled.
All (RISCV64)
Canceling since a higher priority waiting request for 'l4v-Proof PR-853-idx-3' exists
All (RISCV64)
The operation was canceled.
All (ARM_HYP)
Canceling since a higher priority waiting request for 'l4v-Proof PR-853-idx-1' exists
All (ARM_HYP)
The operation was canceled.
All (X64)
Canceling since a higher priority waiting request for 'l4v-Proof PR-853-idx-4' exists
All (X64)
The operation was canceled.