testing

test-harness/src/snapshots/toolchain__reordering into-ssprove.snap

@@ -0,0 +1,103 @@
+---
+source: test-harness/src/harness.rs
+expression: snapshot
+info:
+  kind:
+    Translate:
+      backend: ssprove
+  info:
+    name: reordering
+    manifest: reordering/Cargo.toml
+    description: ~
+  spec:
+    optional: false
+    broken: false
+    issue_id: ~
+    positive: true
+    snapshot:
+      stderr: false
+      stdout: true
+    include_flag: ~
+---
+exit = 0
+
+[stdout]
+diagnostics = []
+
+[stdout.files]
+"Reordering.v" = '''
+(* File automatically generated by Hacspec *)
+Set Warnings "-notation-overridden,-ambiguous-paths".
+From Crypt Require Import choice_type Package Prelude.
+Import PackageNotation.
+From extructures Require Import ord fset.
+From mathcomp Require Import word_ssrZ word.
+From Jasmin Require Import word.
+
+From Coq Require Import ZArith.
+From Coq Require Import Strings.String.
+Import List.ListNotations.
+Open Scope list_scope.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+From Hacspec Require Import ChoiceEquality.
+From Hacspec Require Import LocationUtility.
+From Hacspec Require Import Hacspec_Lib_Comparable.
+From Hacspec Require Import Hacspec_Lib_Pre.
+From Hacspec Require Import Hacspec_Lib.
+
+Open Scope hacspec_scope.
+Import choice.Choice.Exports.
+
+Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
+
+Definition t_Foo : choice_type :=
+  ('unit ∐ 'unit).
+Notation "'Foo_A_case'" := (inl tt) (at level 100).
+Equations Foo_A {L : {fset Location}} {I : Interface} : both L I t_Foo :=
+  Foo_A  :=
+    solve_lift (ret_both (inl (tt : 'unit) : t_Foo)) : both L I t_Foo.
+Fail Next Obligation.
+Notation "'Foo_B_case'" := (inr tt) (at level 100).
+Equations Foo_B {L : {fset Location}} {I : Interface} : both L I t_Foo :=
+  Foo_B  :=
+    solve_lift (ret_both (inr (tt : 'unit) : t_Foo)) : both L I t_Foo.
+Fail Next Obligation.
+
+(*Not implemented yet? todo(item)*)
+
+Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 int32) : both L1 I1 t_Foo :=
+  f _  :=
+    Foo_A : both L1 I1 t_Foo.
+Fail Next Obligation.
+
+Equations no_dependency_1_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  no_dependency_1_ _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations no_dependency_2_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  no_dependency_2_ _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Definition t_Bar : choice_type :=
+  (t_Foo).
+Equations 0 {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I t_Foo :=
+  0 s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (x : t_Foo))) : both L I t_Foo.
+Fail Next Obligation.
+Equations Build_t_Bar {L0 : {fset Location}} {I0 : Interface} {0 : both L0 I0 t_Foo} : both L0 I0 (t_Bar) :=
+  Build_t_Bar  :=
+    bind_both 0 (fun 0 =>
+      solve_lift (ret_both ((0) : (t_Bar)))) : both L0 I0 (t_Bar).
+Fail Next Obligation.
+Notation "'Build_t_Bar' '[' x ']' '(' '0' ':=' y ')'" := (Build_t_Bar (0 := y)).
+
+Equations g {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 t_Bar :=
+  g _  :=
+    Bar (solve_lift (f (ret_both (32 : int32)))) : both L1 I1 t_Bar.
+Fail Next Obligation.
+'''

test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap

@@ -0,0 +1,275 @@
+---
+source: test-harness/src/harness.rs
+expression: snapshot
+info:
+  kind:
+    Translate:
+      backend: ssprove
+  info:
+    name: side-effects
+    manifest: side-effects/Cargo.toml
+    description: ~
+  spec:
+    optional: false
+    broken: false
+    issue_id: ~
+    positive: true
+    snapshot:
+      stderr: true
+      stdout: true
+    include_flag: ~
+---
+exit = 0
+stderr = '''
+Compiling side-effects v0.1.0 (WORKSPACE_ROOT/side-effects)
+    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+
+[stdout]
+diagnostics = []
+
+[stdout.files]
+"Side_effects.v" = '''
+(* File automatically generated by Hacspec *)
+Set Warnings "-notation-overridden,-ambiguous-paths".
+From Crypt Require Import choice_type Package Prelude.
+Import PackageNotation.
+From extructures Require Import ord fset.
+From mathcomp Require Import word_ssrZ word.
+From Jasmin Require Import word.
+
+From Coq Require Import ZArith.
+From Coq Require Import Strings.String.
+Import List.ListNotations.
+Open Scope list_scope.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+From Hacspec Require Import ChoiceEquality.
+From Hacspec Require Import LocationUtility.
+From Hacspec Require Import Hacspec_Lib_Comparable.
+From Hacspec Require Import Hacspec_Lib_Pre.
+From Hacspec Require Import Hacspec_Lib.
+
+Open Scope hacspec_scope.
+Import choice.Choice.Exports.
+
+Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
+
+(*Not implemented yet? todo(item)*)
+
+Equations add3 {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) (z : both L3 I3 int32) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 :=
+  add3 x y z  :=
+    solve_lift (impl__u32__wrapping_add (impl__u32__wrapping_add x y) z) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32.
+Fail Next Obligation.
+
+Equations direct_result_question_mark {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result 'unit int32)) : both L1 I1 (t_Result int8 int32) :=
+  direct_result_question_mark y  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := impl__map_err y f_from in
+    Result_Ok (Result_Ok (ret_both (0 : int8))))) : both L1 I1 (t_Result int8 int32).
+Fail Next Obligation.
+
+Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
+  direct_result_question_mark_coercion y  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist1 := impl__map_err y f_from in
+    Result_Ok (Result_Ok hoist1))) : both L1 I1 (t_Result int8 int32).
+Fail Next Obligation.
+
+Equations early_returns {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 :=
+  early_returns x  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (3 : int32))
+    then letm[choice_typeMonad.result_bind_code int32] hoist2 := v_Break (ret_both (0 : int32)) in
+    ControlFlow_Continue (never_to_any hoist2)
+    else () in
+    letb hoist3 := x >.? (ret_both (30 : int32)) in
+    letm[choice_typeMonad.result_bind_code int32] hoist5 := ifb hoist3
+    then matchb ret_both (true : 'bool) with
+    | true =>
+      letm[choice_typeMonad.result_bind_code int32] hoist4 := v_Break (ret_both (34 : int32)) in
+      ControlFlow_Continue (solve_lift (never_to_any hoist4))
+    | _ =>
+      ControlFlow_Continue (solve_lift (ret_both (3 : int32)))
+    end
+    else ControlFlow_Continue (letb _ := assign todo(term) in
+    x .+ (ret_both (1 : int32))) in
+    letb hoist6 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist5 in
+    letb hoist7 := impl__u32__wrapping_add hoist6 x in
+    letm[choice_typeMonad.result_bind_code int32] hoist8 := v_Break hoist7 in
+    ControlFlow_Continue (never_to_any hoist8))) : both L1 I1 int32.
+Fail Next Obligation.
+
+Definition y_loc : Location :=
+  (int32;0%nat).
+Definition y_loc : Location :=
+  (int32;1%nat).
+Equations local_mutation {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc;y_loc]) I1 int32 :=
+  local_mutation x  :=
+    letb y loc(y_loc) := ret_both (0 : int32) in
+    letb _ := assign todo(term) in
+    letb hoist9 := x >.? (ret_both (3 : int32)) in
+    solve_lift (ifb hoist9
+    then letb _ := assign todo(term) in
+    letb y loc(y_loc) := x ./ (ret_both (2 : int32)) in
+    letb _ := assign todo(term) in
+    letb hoist10 := ret_both (0 : int32) in
+    letb hoist11 := Build_t_Range (f_start := hoist10) (f_end := ret_both (10 : int32)) in
+    letb hoist12 := f_into_iter hoist11 in
+    letb _ := foldi_both_list hoist12 (fun i =>
+      ssp (fun _ =>
+        assign todo(term) : (both (*1*)(L1:|:fset [y_loc]) (I1) 'unit))) (ret_both (tt : 'unit)) in
+    impl__u32__wrapping_add x y
+    else letb hoist15 := matchb x with
+    | 12 =>
+      letb _ := assign todo(term) in
+      solve_lift (ret_both (3 : int32))
+    | 13 =>
+      letb hoist14 := x in
+      letb _ := assign todo(term) in
+      letb hoist13 := impl__u32__wrapping_add (ret_both (123 : int32)) x in
+      solve_lift (add3 hoist14 hoist13 x)
+    | _ =>
+      solve_lift (ret_both (0 : int32))
+    end in
+    letb _ := assign todo(term) in
+    impl__u32__wrapping_add x y) : both (L1 :|: fset [y_loc;y_loc]) I1 int32.
+Fail Next Obligation.
+
+Equations options {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 (t_Option int8)) (y : both L2 I2 (t_Option int8)) (z : both L3 I3 (t_Option int64)) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8) :=
+  options x y z  :=
+    solve_lift (run (letm[choice_typeMonad.option_bind_code] hoist19 := x in
+    letb hoist20 := hoist19 >.? (ret_both (10 : int8)) in
+    letm[choice_typeMonad.option_bind_code] hoist26 := ifb hoist20
+    then letm[choice_typeMonad.option_bind_code] hoist21 := x in
+    Option_Some (letb hoist22 := impl__u8__wrapping_add hoist21 (ret_both (3 : int8)) in
+    Option_Some hoist22)
+    else letm[choice_typeMonad.option_bind_code] hoist24 := x in
+    letm[choice_typeMonad.option_bind_code] hoist23 := y in
+    Option_Some (letb hoist25 := impl__u8__wrapping_add hoist24 hoist23 in
+    Option_Some hoist25) in
+    letm[choice_typeMonad.option_bind_code] hoist27 := hoist26 in
+    letm[choice_typeMonad.option_bind_code] v := matchb hoist27 with
+    | 3 =>
+      Option_None
+    | 4 =>
+      letm[choice_typeMonad.option_bind_code] hoist16 := z in
+      Option_Some (letb hoist17 := hoist16 >.? (ret_both (4 : int64)) in
+      letb hoist18 := ifb hoist17
+      then ret_both (0 : int8)
+      else ret_both (3 : int8) in
+      solve_lift ((ret_both (4 : int8)) .+ hoist18))
+    | _ =>
+      Option_Some (solve_lift (ret_both (12 : int8)))
+    end in
+    letm[choice_typeMonad.option_bind_code] hoist28 := x in
+    letb hoist30 := impl__u8__wrapping_add v hoist28 in
+    letm[choice_typeMonad.option_bind_code] hoist29 := y in
+    Option_Some (letb hoist31 := impl__u8__wrapping_add hoist30 hoist29 in
+    Option_Some hoist31))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8).
+Fail Next Obligation.
+
+Definition y_loc : Location :=
+  (int32;2%nat).
+Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32) :=
+  question_mark x  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
+    then letb y loc(y_loc) := ret_both (0 : int32) in
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    letb hoist32 := x >.? (ret_both (90 : int32)) in
+    ifb hoist32
+    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
+    else ()
+    else () in
+    Result_Ok (Result_Ok (impl__u32__wrapping_add (ret_both (3 : int32)) x)))) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32).
+Fail Next Obligation.
+
+Definition t_A : choice_type :=
+  'unit.
+Equations Build_t_A : both (fset []) (fset []) (t_A) :=
+  Build_t_A  :=
+    solve_lift (ret_both (tt (* Empty tuple *) : (t_A))) : both (fset []) (fset []) (t_A).
+Fail Next Obligation.
+
+Definition t_B : choice_type :=
+  'unit.
+Equations Build_t_B : both (fset []) (fset []) (t_B) :=
+  Build_t_B  :=
+    solve_lift (ret_both (tt (* Empty tuple *) : (t_B))) : both (fset []) (fset []) (t_B).
+Fail Next Obligation.
+
+Definition t_Bar : choice_type :=
+  ('bool × nseq ('bool × 'bool) 6 × 'bool).
+Equations f_a {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I 'bool :=
+  f_a s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (fst x : 'bool))) : both L I 'bool.
+Fail Next Obligation.
+Equations f_b {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I (nseq ('bool × 'bool) 6 × 'bool) :=
+  f_b s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (snd x : (nseq ('bool × 'bool) 6 × 'bool)))) : both L I (nseq ('bool × 'bool) 6 × 'bool).
+Fail Next Obligation.
+Equations Build_t_Bar {L0 : {fset Location}} {L1 : {fset Location}} {I0 : Interface} {I1 : Interface} {f_a : both L0 I0 'bool} {f_b : both L1 I1 (nseq ('bool × 'bool) 6 × 'bool)} : both (L0:|:L1) (I0:|:I1) (t_Bar) :=
+  Build_t_Bar  :=
+    bind_both f_b (fun f_b =>
+      bind_both f_a (fun f_a =>
+        solve_lift (ret_both ((f_a,f_b) : (t_Bar))))) : both (L0:|:L1) (I0:|:I1) (t_Bar).
+Fail Next Obligation.
+Notation "'Build_t_Bar' '[' x ']' '(' 'f_a' ':=' y ')'" := (Build_t_Bar (f_a := y) (f_b := f_b x)).
+Notation "'Build_t_Bar' '[' x ']' '(' 'f_b' ':=' y ')'" := (Build_t_Bar (f_a := f_a x) (f_b := y)).
+
+Equations monad_lifting {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result t_A t_B) :=
+  monad_lifting x  :=
+    solve_lift (run (ifb x >.? (ret_both (123 : int8))
+    then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist33 := ControlFlow_Continue (impl__map_err (Result_Err B) f_from) in
+    letb hoist34 := Result_Ok hoist33 in
+    letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist35 := v_Break hoist34 in
+    ControlFlow_Continue (never_to_any hoist35)
+    else ControlFlow_Continue (Result_Ok A))) : both L1 I1 (t_Result t_A t_B).
+Fail Next Obligation.
+
+Definition t_Foo : choice_type :=
+  ('bool × 'bool × t_Vec t_Bar t_Global × nseq t_Bar 6 × t_Bar).
+Equations f_x {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I 'bool :=
+  f_x s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (fst (fst (fst x)) : 'bool))) : both L I 'bool.
+Fail Next Obligation.
+Equations f_y {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I ('bool × t_Vec t_Bar t_Global) :=
+  f_y s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (snd (fst (fst x)) : ('bool × t_Vec t_Bar t_Global)))) : both L I ('bool × t_Vec t_Bar t_Global).
+Fail Next Obligation.
+Equations f_z {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I (nseq t_Bar 6) :=
+  f_z s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (snd (fst x) : (nseq t_Bar 6)))) : both L I (nseq t_Bar 6).
+Fail Next Obligation.
+Equations f_bar {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I t_Bar :=
+  f_bar s  :=
+    bind_both s (fun x =>
+      solve_lift (ret_both (snd x : t_Bar))) : both L I t_Bar.
+Fail Next Obligation.
+Equations Build_t_Foo {L0 : {fset Location}} {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I0 : Interface} {I1 : Interface} {I2 : Interface} {I3 : Interface} {f_x : both L0 I0 'bool} {f_y : both L1 I1 ('bool × t_Vec t_Bar t_Global)} {f_z : both L2 I2 (nseq t_Bar 6)} {f_bar : both L3 I3 t_Bar} : both (L0:|:L1:|:L2:|:L3) (I0:|:I1:|:I2:|:I3) (t_Foo) :=
+  Build_t_Foo  :=
+    bind_both f_bar (fun f_bar =>
+      bind_both f_z (fun f_z =>
+        bind_both f_y (fun f_y =>
+          bind_both f_x (fun f_x =>
+            solve_lift (ret_both ((f_x,f_y,f_z,f_bar) : (t_Foo))))))) : both (L0:|:L1:|:L2:|:L3) (I0:|:I1:|:I2:|:I3) (t_Foo).
+Fail Next Obligation.
+Notation "'Build_t_Foo' '[' x ']' '(' 'f_x' ':=' y ')'" := (Build_t_Foo (f_x := y) (f_y := f_y x) (f_z := f_z x) (f_bar := f_bar x)).
+Notation "'Build_t_Foo' '[' x ']' '(' 'f_y' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := y) (f_z := f_z x) (f_bar := f_bar x)).
+Notation "'Build_t_Foo' '[' x ']' '(' 'f_z' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := y) (f_bar := f_bar x)).
+Notation "'Build_t_Foo' '[' x ']' '(' 'f_bar' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := f_z x) (f_bar := y)).
+
+Equations assign_non_trivial_lhs {L1 : {fset Location}} {I1 : Interface} (foo : both L1 I1 t_Foo) : both L1 I1 t_Foo :=
+  assign_non_trivial_lhs foo  :=
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    solve_lift foo : both L1 I1 t_Foo.
+Fail Next Obligation.
+'''

tests/enum-repr/Cargo.toml

@@ -6,4 +6,4 @@ edition = "2021"
 [dependencies]
 
 [package.metadata.hax-tests]
-into."fstar+coq" = { broken = false, snapshot = "none", issue_id = "162" }
+into."fstar+coq+ssprove" = { broken = false, snapshot = "none", issue_id = "162" }

tests/enum-struct-variant/Cargo.toml

@@ -9,3 +9,4 @@ edition = "2021"
 
 [package.metadata.hax-tests]
 into."fstar+coq" = {broken = false, snapshot = "none"}
+into."ssprove" = {broken = true, snapshot = "none"}

tests/if-let/Cargo.toml

@@ -6,4 +6,4 @@ edition = "2021"
 [dependencies]
 
 [package.metadata.hax-tests]
-into."fstar+coq" = { broken = false, snapshot = "none", issue_id = "85" }
+into."fstar+coq+ssprove" = { broken = false, snapshot = "none", issue_id = "85" }