diff options
author | Son HO | 2023-08-07 10:42:15 +0200 |
---|---|---|
committer | GitHub | 2023-08-07 10:42:15 +0200 |
commit | 1cbc7ce007cf3433a6df9bdeb12c4e27511fad9c (patch) | |
tree | c15a16b591cf25df3ccff87ad4cd7c46ddecc489 /tests/coq/misc | |
parent | 887d0ef1efc8912c6273b5ebcf979384e9d7fa97 (diff) | |
parent | 9e14cdeaf429e9faff2d1efdcf297c1ac7dc7f1f (diff) |
Merge pull request #32 from AeneasVerif/son_arrays
Add support for arrays/slices and const generics
Diffstat (limited to 'tests/coq/misc')
-rw-r--r-- | tests/coq/misc/Constants.v | 2 | ||||
-rw-r--r-- | tests/coq/misc/External_Funs.v | 2 | ||||
-rw-r--r-- | tests/coq/misc/External_Opaque.v | 2 | ||||
-rw-r--r-- | tests/coq/misc/External_Types.v | 2 | ||||
-rw-r--r-- | tests/coq/misc/Loops.v | 2 | ||||
-rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 2 | ||||
-rw-r--r-- | tests/coq/misc/Paper.v | 2 | ||||
-rw-r--r-- | tests/coq/misc/PoloniusList.v | 2 | ||||
-rw-r--r-- | tests/coq/misc/Primitives.v | 55 |
9 files changed, 65 insertions, 6 deletions
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v index 14c05c61..710ae1d9 100644 --- a/tests/coq/misc/Constants.v +++ b/tests/coq/misc/Constants.v @@ -3,6 +3,8 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. Local Open Scope Primitives_scope. Module Constants. diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v index f18bbd1f..28370b2b 100644 --- a/tests/coq/misc/External_Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -3,6 +3,8 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. Local Open Scope Primitives_scope. Require Export External_Types. Import External_Types. diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_Opaque.v index 1224f426..d2ee42d4 100644 --- a/tests/coq/misc/External_Opaque.v +++ b/tests/coq/misc/External_Opaque.v @@ -3,6 +3,8 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. Local Open Scope Primitives_scope. Require Export External_Types. Import External_Types. diff --git a/tests/coq/misc/External_Types.v b/tests/coq/misc/External_Types.v index cec5b88e..1883fa6c 100644 --- a/tests/coq/misc/External_Types.v +++ b/tests/coq/misc/External_Types.v @@ -3,6 +3,8 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. Local Open Scope Primitives_scope. Module External_Types. diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index f17eb986..82e57576 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -3,6 +3,8 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. Local Open Scope Primitives_scope. Module Loops. diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 470a2cde..f93254e1 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -3,6 +3,8 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. Local Open Scope Primitives_scope. Module NoNestedBorrows. diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index 0f854f31..175a523d 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -3,6 +3,8 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. Local Open Scope Primitives_scope. Module Paper. diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v index e94b6dcb..54021bdf 100644 --- a/tests/coq/misc/PoloniusList.v +++ b/tests/coq/misc/PoloniusList.v @@ -3,6 +3,8 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. Local Open Scope Primitives_scope. Module PoloniusList. diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v index ae961ac2..71a2d9c3 100644 --- a/tests/coq/misc/Primitives.v +++ b/tests/coq/misc/Primitives.v @@ -394,13 +394,15 @@ Notation "x s< y" := (scalar_ltb x y) (at level 80) : Primitives_scope. Notation "x s>= y" := (scalar_geb x y) (at level 80) : Primitives_scope. Notation "x s> y" := (scalar_gtb x y) (at level 80) : Primitives_scope. -(*** Vectors *) - -Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }. +(*** Range *) +Record range (T : Type) := mk_range { + start: T; + end_: T; +}. +Arguments mk_range {_}. -Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v. - -Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)). +(*** Arrays *) +Definition array T (n : usize) := { l: list T | Z.of_nat (length l) = to_Z n}. Lemma le_0_usize_max : 0 <= usize_max. Proof. @@ -409,6 +411,47 @@ Proof. lia. Qed. +Lemma eqb_imp_eq (x y : Z) : Z.eqb x y = true -> x = y. +Proof. + lia. +Qed. + +(* TODO: finish the definitions *) +Axiom mk_array : forall (T : Type) (n : usize) (l : list T), array T n. + +Axiom array_index_shared : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T. +Axiom array_index_mut_fwd : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T. +Axiom array_index_mut_back : forall (T : Type) (n : usize) (x : array T n) (i : usize) (nx : T), result (array T n). + +(*** Slice *) +Definition slice T := { l: list T | Z.of_nat (length l) <= usize_max}. + +Axiom slice_len : forall (T : Type) (s : slice T), usize. +Axiom slice_index_shared : forall (T : Type) (x : slice T) (i : usize), result T. +Axiom slice_index_mut_fwd : forall (T : Type) (x : slice T) (i : usize), result T. +Axiom slice_index_mut_back : forall (T : Type) (x : slice T) (i : usize) (nx : T), result (slice T). + +(*** Subslices *) + +Axiom array_to_slice_shared : forall (T : Type) (n : usize) (x : array T n), result (slice T). +Axiom array_to_slice_mut_fwd : forall (T : Type) (n : usize) (x : array T n), result (slice T). +Axiom array_to_slice_mut_back : forall (T : Type) (n : usize) (x : array T n) (s : slice T), result (array T n). + +Axiom array_subslice_shared: forall (T : Type) (n : usize) (x : array T n) (r : range usize), result (slice T). +Axiom array_subslice_mut_fwd: forall (T : Type) (n : usize) (x : array T n) (r : range usize), result (slice T). +Axiom array_subslice_mut_back: forall (T : Type) (n : usize) (x : array T n) (r : range usize) (ns : slice T), result (array T n). +Axiom slice_subslice_shared: forall (T : Type) (x : slice T) (r : range usize), result (slice T). +Axiom slice_subslice_mut_fwd: forall (T : Type) (x : slice T) (r : range usize), result (slice T). +Axiom slice_subslice_mut_back: forall (T : Type) (x : slice T) (r : range usize) (ns : slice T), result (slice T). + +(*** Vectors *) + +Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }. + +Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v. + +Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)). + Definition vec_new (T: Type) : vec T := (exist _ [] le_0_usize_max). Lemma vec_len_in_usize {T} (v: vec T) : usize_min <= vec_length v <= usize_max. |