blob: 02e2a69769b84e86f15431d9c42b951f3e6bad32 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
------------------------------------------------------------------------
-- Agda Helium
--
-- Semantics for the Armv8-M pseudocode using Hoare triples.
------------------------------------------------------------------------
{-# OPTIONS --safe --without-K #-}
open import Helium.Data.Pseudocode.Algebra using (Pseudocode)
module Helium.Semantics.Axiomatic
{b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
(pseudocode : Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
where
open import Helium.Data.Pseudocode.Algebra.Properties pseudocode
open import Data.Nat using (ℕ)
import Data.Unit
open import Function using (_∘_)
import Helium.Semantics.Core rawPseudocode as Core′
import Helium.Semantics.Axiomatic.Term rawPseudocode as Term′
import Helium.Semantics.Axiomatic.Assertion rawPseudocode as Assertion′
private
proof-2≉0 : Core′.2≉0
proof-2≉0 = ℝ.<⇒≉ (ℝ.n≢0∧x>0⇒n×x>0 2 (ℝ.≤∧≉⇒< ℝ.0≤1 (ℝ.1≉0 ∘ ℝ.Eq.sym))) ∘ ℝ.Eq.sym
module Core where
open Core′ public hiding (shift)
shift : ℤ → ℕ → ℤ
shift = Core′.shift proof-2≉0
open Core public using (⟦_⟧ₜ; ⟦_⟧ₜ′; Κ[_]_; 2≉0)
module Term where
open Term′ public hiding (module Semantics)
module Semantics {i} {j} {k} where
open Term′.Semantics {i} {j} {k} proof-2≉0 public
open Term public using (Term; ↓_) hiding (module Term)
open Term.Term public
module Assertion where
open Assertion′ public hiding (module Semantics)
module Semantics where
open Assertion′.Semantics proof-2≉0 public
open Assertion public using (Assertion) hiding (module Assertion)
open Assertion.Assertion public
open Assertion.Construct public
open import Helium.Semantics.Axiomatic.Triple rawPseudocode proof-2≉0 public
|
