diff options
Diffstat (limited to '')
28 files changed, 637 insertions, 63 deletions
@@ -125,15 +125,13 @@ thol4-paper: SUBDIR := misc-paper trans-array: OPTIONS += -no-state trans-array: SUBDIR := array -tfstar-array: OPTIONS += -tcoq-array: OPTIONS += +tfstar-array: OPTIONS += -decreases-clauses -template-clauses +tcoq-array: OPTIONS += -use-fuel tlean-array: SUBDIR := tlean-array: OPTIONS += thol4-array: OPTIONS += # TODO: activate the arrays for all the backends -tcoq-array: - echo "Ignoring the array test for Coq" thol4-array: echo "Ignoring the array test for HOL4" @@ -144,7 +142,7 @@ tcoq-loops: OPTIONS += -use-fuel -no-split-files tlean-loops: SUBDIR := thol4-loops: SUBDIR := misc-loops -trans-hashmap: OPTIONS += -no-state +trans-hashmap: OPTIONS += -no-state -test-trans-units trans-hashmap: SUBDIR := hashmap tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap: OPTIONS += -use-fuel @@ -152,7 +150,7 @@ tlean-hashmap: SUBDIR := tlean-hashmap: OPTIONS += thol4-hashmap: OPTIONS += -trans-hashmap_main: OPTIONS += +trans-hashmap_main: OPTIONS += -test-trans-units trans-hashmap_main: SUBDIR := hashmap_on_disk tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap_main: OPTIONS += -use-fuel @@ -177,7 +175,7 @@ tlean-constants: OPTIONS += thol4-constants: SUBDIR := misc-constants thol4-constants: OPTIONS += -trans-external: OPTIONS += +trans-external: OPTIONS += -test-trans-units trans-external: SUBDIR := misc tfstar-external: OPTIONS += tcoq-external: OPTIONS += @@ -187,7 +185,7 @@ thol4-external: SUBDIR := misc-external thol4-external: OPTIONS += BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses -transp-betree_main: OPTIONS += -backward-no-state-update +transp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units transp-betree_main: SUBDIR:=betree tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) tcoqp-betree_main: OPTIONS += -use-fuel @@ -239,20 +237,20 @@ transp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-% echo "# Test $* done" .PHONY: tfstar-% -tfstar-%: OPTIONS += -backend fstar -test-trans-units +tfstar-%: OPTIONS += -backend fstar tfstar-%: BACKEND_SUBDIR := fstar tfstar-%: $(AENEAS_CMD) # "p" stands for "Polonius" .PHONY: tfstarp-% -tfstarp-%: OPTIONS += -backend fstar -test-trans-units +tfstarp-%: OPTIONS += -backend fstar tfstarp-%: BACKEND_SUBDIR := fstar tfstarp-%: $(AENEAS_CMD) .PHONY: tcoq-% -tcoq-%: OPTIONS += -backend coq -test-trans-units +tcoq-%: OPTIONS += -backend coq tcoq-%: BACKEND_SUBDIR := coq tcoq-%: $(AENEAS_CMD) @@ -265,7 +263,7 @@ tcoqp-%: $(AENEAS_CMD) .PHONY: tlean-% -tlean-%: OPTIONS += -backend lean -test-trans-units +tlean-%: OPTIONS += -backend lean tlean-%: BACKEND_SUBDIR := lean tlean-%: $(AENEAS_CMD) @@ -273,19 +271,19 @@ tlean-%: # "p" stands for "Polonius" .PHONY: tleanp-% -tleanp-%: OPTIONS += -backend lean -test-trans-units +tleanp-%: OPTIONS += -backend lean tleanp-%: BACKEND_SUBDIR := lean tleanp-%: $(AENEAS_CMD) .PHONY: thol4-% -thol4-%: OPTIONS += -backend hol4 -test-trans-units +thol4-%: OPTIONS += -backend hol4 thol4-%: BACKEND_SUBDIR := hol4 thol4-%: $(AENEAS_CMD) .PHONY: thol4p-% -thol4p-%: OPTIONS += -backend hol4 -test-trans-units +thol4p-%: OPTIONS += -backend hol4 thol4p-%: BACKEND_SUBDIR := hol4 thol4p-%: $(AENEAS_CMD) diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v index d462715f..71a2d9c3 100644 --- a/backends/coq/Primitives.v +++ b/backends/coq/Primitives.v @@ -213,7 +213,6 @@ Proof. pose (scalar_max_cons_valid ty). lia. Qed. -Print scalar_le_max_valid. Definition scalar_in_bounds (ty: scalar_ty) (x: Z) : bool := scalar_ge_min ty x && scalar_le_max ty x . diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index 86a9d5f2..85aecfc8 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_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 BetreeMain_Types. Import BetreeMain_Types. @@ -1190,4 +1192,7 @@ Definition betree_be_tree_lookup_back Definition main_fwd : result unit := Return tt. +(** Unit test for [betree_main::main] *) +Check (main_fwd )%return. + End BetreeMain_Funs . diff --git a/tests/coq/betree/BetreeMain_Opaque.v b/tests/coq/betree/BetreeMain_Opaque.v index bd49500b..ecd81b9d 100644 --- a/tests/coq/betree/BetreeMain_Opaque.v +++ b/tests/coq/betree/BetreeMain_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 BetreeMain_Types. Import BetreeMain_Types. diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v index 25f280dd..c8af54cd 100644 --- a/tests/coq/betree/BetreeMain_Types.v +++ b/tests/coq/betree/BetreeMain_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 BetreeMain_Types. diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v index ae961ac2..71a2d9c3 100644 --- a/tests/coq/betree/Primitives.v +++ b/tests/coq/betree/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. diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index c8630eb6..c412abcd 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_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 Hashmap_Types. Import Hashmap_Types. diff --git a/tests/coq/hashmap/Hashmap_Types.v b/tests/coq/hashmap/Hashmap_Types.v index ce6e7dab..dbde6be9 100644 --- a/tests/coq/hashmap/Hashmap_Types.v +++ b/tests/coq/hashmap/Hashmap_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 Hashmap_Types. diff --git a/tests/coq/hashmap/Primitives.v b/tests/coq/hashmap/Primitives.v index ae961ac2..71a2d9c3 100644 --- a/tests/coq/hashmap/Primitives.v +++ b/tests/coq/hashmap/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. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 1b7304cc..e6095fe1 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_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 HashmapMain_Types. Import HashmapMain_Types. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v index 1ad9c697..2d17cc29 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_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 HashmapMain_Types. Import HashmapMain_Types. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Types.v b/tests/coq/hashmap_on_disk/HashmapMain_Types.v index b92cbf3a..36aaaf25 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Types.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_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 HashmapMain_Types. diff --git a/tests/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_on_disk/Primitives.v index ae961ac2..71a2d9c3 100644 --- a/tests/coq/hashmap_on_disk/Primitives.v +++ b/tests/coq/hashmap_on_disk/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. 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. diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst index 98a696b6..9db82069 100644 --- a/tests/fstar/betree/Primitives.fst +++ b/tests/fstar/betree/Primitives.fst @@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +(*** Range *) +type range (a : Type0) = { + start : a; + end_ : a; +} + +(*** Array *) +type array (a : Type0) (n : usize) = s:list a{length s = n} + +// We tried putting the normalize_term condition as a refinement on the list +// but it didn't work. It works with the requires clause. +let mk_array (a : Type0) (n : usize) + (l : list a) : + Pure (array a n) + (requires (normalize_term(FStar.List.Tot.length l) = n)) + (ensures (fun _ -> True)) = + normalize_term_spec (FStar.List.Tot.length l); + l + +let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Slice *) +type slice (a : Type0) = s:list a{length s <= usize_max} + +let slice_len (a : Type0) (s : slice a) : usize = length s + +let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Subslices *) + +let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = + if length s = n then Return s + else Fail Failure + +// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) +let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) = + admit() + +let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) = + admit() + (*** Vector *) type vec (a : Type0) = v:list a{length v <= usize_max} diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst index 98a696b6..9db82069 100644 --- a/tests/fstar/betree_back_stateful/Primitives.fst +++ b/tests/fstar/betree_back_stateful/Primitives.fst @@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +(*** Range *) +type range (a : Type0) = { + start : a; + end_ : a; +} + +(*** Array *) +type array (a : Type0) (n : usize) = s:list a{length s = n} + +// We tried putting the normalize_term condition as a refinement on the list +// but it didn't work. It works with the requires clause. +let mk_array (a : Type0) (n : usize) + (l : list a) : + Pure (array a n) + (requires (normalize_term(FStar.List.Tot.length l) = n)) + (ensures (fun _ -> True)) = + normalize_term_spec (FStar.List.Tot.length l); + l + +let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Slice *) +type slice (a : Type0) = s:list a{length s <= usize_max} + +let slice_len (a : Type0) (s : slice a) : usize = length s + +let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Subslices *) + +let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = + if length s = n then Return s + else Fail Failure + +// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) +let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) = + admit() + +let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) = + admit() + (*** Vector *) type vec (a : Type0) = v:list a{length v <= usize_max} diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst index 98a696b6..9db82069 100644 --- a/tests/fstar/hashmap/Primitives.fst +++ b/tests/fstar/hashmap/Primitives.fst @@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +(*** Range *) +type range (a : Type0) = { + start : a; + end_ : a; +} + +(*** Array *) +type array (a : Type0) (n : usize) = s:list a{length s = n} + +// We tried putting the normalize_term condition as a refinement on the list +// but it didn't work. It works with the requires clause. +let mk_array (a : Type0) (n : usize) + (l : list a) : + Pure (array a n) + (requires (normalize_term(FStar.List.Tot.length l) = n)) + (ensures (fun _ -> True)) = + normalize_term_spec (FStar.List.Tot.length l); + l + +let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Slice *) +type slice (a : Type0) = s:list a{length s <= usize_max} + +let slice_len (a : Type0) (s : slice a) : usize = length s + +let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Subslices *) + +let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = + if length s = n then Return s + else Fail Failure + +// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) +let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) = + admit() + +let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) = + admit() + (*** Vector *) type vec (a : Type0) = v:list a{length v <= usize_max} diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst index 98a696b6..9db82069 100644 --- a/tests/fstar/hashmap_on_disk/Primitives.fst +++ b/tests/fstar/hashmap_on_disk/Primitives.fst @@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +(*** Range *) +type range (a : Type0) = { + start : a; + end_ : a; +} + +(*** Array *) +type array (a : Type0) (n : usize) = s:list a{length s = n} + +// We tried putting the normalize_term condition as a refinement on the list +// but it didn't work. It works with the requires clause. +let mk_array (a : Type0) (n : usize) + (l : list a) : + Pure (array a n) + (requires (normalize_term(FStar.List.Tot.length l) = n)) + (ensures (fun _ -> True)) = + normalize_term_spec (FStar.List.Tot.length l); + l + +let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Slice *) +type slice (a : Type0) = s:list a{length s <= usize_max} + +let slice_len (a : Type0) (s : slice a) : usize = length s + +let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Subslices *) + +let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = + if length s = n then Return s + else Fail Failure + +// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) +let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) = + admit() + +let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) = + admit() + (*** Vector *) type vec (a : Type0) = v:list a{length v <= usize_max} diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst index 98a696b6..9db82069 100644 --- a/tests/fstar/misc/Primitives.fst +++ b/tests/fstar/misc/Primitives.fst @@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +(*** Range *) +type range (a : Type0) = { + start : a; + end_ : a; +} + +(*** Array *) +type array (a : Type0) (n : usize) = s:list a{length s = n} + +// We tried putting the normalize_term condition as a refinement on the list +// but it didn't work. It works with the requires clause. +let mk_array (a : Type0) (n : usize) + (l : list a) : + Pure (array a n) + (requires (normalize_term(FStar.List.Tot.length l) = n)) + (ensures (fun _ -> True)) = + normalize_term_spec (FStar.List.Tot.length l); + l + +let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Slice *) +type slice (a : Type0) = s:list a{length s <= usize_max} + +let slice_len (a : Type0) (s : slice a) : usize = length s + +let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Subslices *) + +let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = + if length s = n then Return s + else Fail Failure + +// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) +let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) = + admit() + +let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) = + admit() + (*** Vector *) type vec (a : Type0) = v:list a{length v <= usize_max} diff --git a/tests/lean/Array/Funs.lean b/tests/lean/Array/Funs.lean index b1365143..8a2c1045 100644 --- a/tests/lean/Array/Funs.lean +++ b/tests/lean/Array/Funs.lean @@ -9,24 +9,24 @@ namespace array /- [array::array_to_shared_slice_]: forward function -/ def array_to_shared_slice_ (T : Type) (s : Array T (Usize.ofInt 32)) : Result (Slice T) := - Array.to_slice T (Usize.ofInt 32) s + Array.to_slice_shared T (Usize.ofInt 32) s /- [array::array_to_mut_slice_]: forward function -/ def array_to_mut_slice_ (T : Type) (s : Array T (Usize.ofInt 32)) : Result (Slice T) := - Array.to_mut_slice T (Usize.ofInt 32) s + Array.to_slice_mut T (Usize.ofInt 32) s /- [array::array_to_mut_slice_]: backward function 0 -/ def array_to_mut_slice__back (T : Type) (s : Array T (Usize.ofInt 32)) (ret0 : Slice T) : Result (Array T (Usize.ofInt 32)) := - Array.to_mut_slice_back T (Usize.ofInt 32) s ret0 + Array.to_slice_mut_back T (Usize.ofInt 32) s ret0 /- [array::array_len]: forward function -/ def array_len (T : Type) (s : Array T (Usize.ofInt 32)) : Result Usize := do - let s0 ← Array.to_slice T (Usize.ofInt 32) s + let s0 ← Array.to_slice_shared T (Usize.ofInt 32) s let i := Slice.len T s0 Result.ret i @@ -34,7 +34,7 @@ def array_len (T : Type) (s : Array T (Usize.ofInt 32)) : Result Usize := def shared_array_len (T : Type) (s : Array T (Usize.ofInt 32)) : Result Usize := do - let s0 ← Array.to_slice T (Usize.ofInt 32) s + let s0 ← Array.to_slice_shared T (Usize.ofInt 32) s let i := Slice.len T s0 Result.ret i @@ -109,21 +109,22 @@ def slice_subslice_mut__back := Slice.subslice_mut_back U32 x (Range.mk y z) ret0 -/- [array::array_to_slice_shared]: forward function -/ -def array_to_slice_shared +/- [array::array_to_slice_shared_]: forward function -/ +def array_to_slice_shared_ (x : Array U32 (Usize.ofInt 32)) : Result (Slice U32) := - Array.to_slice U32 (Usize.ofInt 32) x + Array.to_slice_shared U32 (Usize.ofInt 32) x -/- [array::array_to_slice_mut]: forward function -/ -def array_to_slice_mut (x : Array U32 (Usize.ofInt 32)) : Result (Slice U32) := - Array.to_mut_slice U32 (Usize.ofInt 32) x +/- [array::array_to_slice_mut_]: forward function -/ +def array_to_slice_mut_ + (x : Array U32 (Usize.ofInt 32)) : Result (Slice U32) := + Array.to_slice_mut U32 (Usize.ofInt 32) x -/- [array::array_to_slice_mut]: backward function 0 -/ -def array_to_slice_mut_back +/- [array::array_to_slice_mut_]: backward function 0 -/ +def array_to_slice_mut__back (x : Array U32 (Usize.ofInt 32)) (ret0 : Slice U32) : Result (Array U32 (Usize.ofInt 32)) := - Array.to_mut_slice_back U32 (Usize.ofInt 32) x ret0 + Array.to_slice_mut_back U32 (Usize.ofInt 32) x ret0 /- [array::array_subslice_shared_]: forward function -/ def array_subslice_shared_ @@ -186,17 +187,14 @@ def array_local_deep_copy (x : Array U32 (Usize.ofInt 32)) : Result Unit := def f0 : Result Unit := do let s ← - Array.to_mut_slice U32 (Usize.ofInt 2) + Array.to_slice_mut U32 (Usize.ofInt 2) (Array.make U32 (Usize.ofInt 2) [ (U32.ofInt 1), (U32.ofInt 2) ]) let s0 ← Slice.index_mut_back U32 s (Usize.ofInt 0) (U32.ofInt 1) let _ ← - Array.to_mut_slice_back U32 (Usize.ofInt 2) + Array.to_slice_mut_back U32 (Usize.ofInt 2) (Array.make U32 (Usize.ofInt 2) [ (U32.ofInt 1), (U32.ofInt 2) ]) s0 Result.ret () -/- Unit test for [array::f0] -/ -#assert (f0 == .ret ()) - /- [array::f1]: forward function -/ def f1 : Result Unit := do @@ -206,9 +204,6 @@ def f1 : Result Unit := (Usize.ofInt 0) (U32.ofInt 1) Result.ret () -/- Unit test for [array::f1] -/ -#assert (f1 == .ret ()) - /- [array::sum]: loop 0: forward function -/ divergent def sum_loop (s : Slice U32) (sum0 : U32) (i : Usize) : Result U32 := let i0 := Slice.len U32 s @@ -268,7 +263,7 @@ def f3 : Result U32 := (Usize.ofInt 0) let _ ← f2 i let s ← - Array.to_slice U32 (Usize.ofInt 2) + Array.to_slice_shared U32 (Usize.ofInt 2) (Array.make U32 (Usize.ofInt 2) [ (U32.ofInt 1), (U32.ofInt 2) ]) let s0 ← f4 |