Skip to content

Commit 7a8bb9b

Browse files
NadrierilNadrieril
committed
Update test outputs
1 parent 1a071ac commit 7a8bb9b

File tree

4 files changed

+221
-124
lines changed

4 files changed

+221
-124
lines changed

‎test-harness/src/snapshots/toolchain__attributes into-fstar.snap‎

Lines changed: 145 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -20,10 +20,27 @@ info:
2020
include_flag: ~
2121
backend_options: ~
2222
---
23-
exit = 0
24-
25-
[stdout]
26-
diagnostics = []
23+
exit = 1
24+
[[stdout.diagnostics]]
25+
message = '''
26+
(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
27+
Please upvote or comment this issue if you see this error message.
28+
Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.'''
29+
spans = ['Span { lo: Loc { line: 301, col: 17 }, hi: Loc { line: 301, col: 22 }, filename: Real(LocalPath("/home/nadrieril/wip/work/hax/hax-bounded-integers/src/lib.rs")), rust_span_data: None }']
30+
31+
[[stdout.diagnostics]]
32+
message = '''
33+
(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
34+
Please upvote or comment this issue if you see this error message.
35+
Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.'''
36+
spans = ['Span { lo: Loc { line: 301, col: 30 }, hi: Loc { line: 301, col: 32 }, filename: Real(LocalPath("/home/nadrieril/wip/work/hax/hax-bounded-integers/src/lib.rs")), rust_span_data: None }']
37+
38+
[[stdout.diagnostics]]
39+
message = '''
40+
(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
41+
Please upvote or comment this issue if you see this error message.
42+
Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.'''
43+
spans = ['Span { lo: Loc { line: 295, col: 19 }, hi: Loc { line: 295, col: 24 }, filename: Real(LocalPath("attributes/src/lib.rs")), rust_span_data: None }']
2744

2845
[stdout.files]
2946
"Attributes.Ensures_on_arity_zero_fns.fst" = '''
@@ -57,25 +74,24 @@ open FStar.Mul
5774
type t_Dummy = | Dummy : t_Dummy
5875

5976
[@@ FStar.Tactics.Typeclasses.tcinstance]
60-
assume
61-
val impl_1': Core.Marker.t_StructuralPartialEq t_Dummy
62-
63-
unfold
64-
let impl_1 = impl_1'
77+
let impl_1: Core.Marker.t_StructuralPartialEq t_Dummy = { __marker_trait = () }
6578

6679
[@@ FStar.Tactics.Typeclasses.tcinstance]
67-
assume
68-
val impl_2': Core.Cmp.t_PartialEq t_Dummy t_Dummy
69-
70-
unfold
71-
let impl_2 = impl_2'
80+
let impl_2: Core.Cmp.t_PartialEq t_Dummy t_Dummy =
81+
{
82+
f_eq_pre = (fun (self: t_Dummy) (other: t_Dummy) -> true);
83+
f_eq_post = (fun (self: t_Dummy) (other: t_Dummy) (out: bool) -> true);
84+
f_eq = fun (self: t_Dummy) (other: t_Dummy) -> true
85+
}
7286

7387
[@@ FStar.Tactics.Typeclasses.tcinstance]
74-
assume
75-
val impl': Core.Cmp.t_Eq t_Dummy
76-
77-
unfold
78-
let impl = impl'
88+
let impl: Core.Cmp.t_Eq t_Dummy =
89+
{
90+
_super_5579681813951091494 = FStar.Tactics.Typeclasses.solve;
91+
f_assert_receiver_is_total_eq_pre = (fun (self: t_Dummy) -> true);
92+
f_assert_receiver_is_total_eq_post = (fun (self: t_Dummy) (out: Prims.unit) -> true);
93+
f_assert_receiver_is_total_eq = fun (self: t_Dummy) -> ()
94+
}
7995

8096
let impl_Dummy__f (self: t_Dummy)
8197
: Prims.Pure t_Dummy
@@ -129,14 +145,21 @@ open FStar.Mul
129145

130146
unfold type t_Int = int
131147

132-
let impl_1: Core.Clone.t_Clone t_Int = { f_clone = (fun x -> x) }
133-
134148
[@@ FStar.Tactics.Typeclasses.tcinstance]
135-
assume
136-
val impl': Core.Marker.t_Copy t_Int
149+
let impl_1: Core.Clone.t_Clone t_Int =
150+
{
151+
f_clone_pre = (fun (self: t_Int) -> true);
152+
f_clone_post = (fun (self: t_Int) (out: t_Int) -> true);
153+
f_clone
154+
=
155+
fun (self: t_Int) ->
156+
Rust_primitives.Hax.failure "(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.\nPlease upvote or comment this issue if you see this error message.\nSorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now."
157+
""
158+
}
137159

138-
unfold
139-
let impl = impl'
160+
[@@ FStar.Tactics.Typeclasses.tcinstance]
161+
let impl: Core.Marker.t_Copy t_Int =
162+
{ _super_15837849249852401974 = FStar.Tactics.Typeclasses.solve }
140163

141164
unfold let add x y = x + y
142165

@@ -471,56 +494,117 @@ let t_BoundedAbsI16 (v_B: usize) =
471494
(Rust_primitives.Hax.Int.from_machine x <: Hax_lib.Int.t_Int) <=
472495
(Rust_primitives.Hax.Int.from_machine v_B <: Hax_lib.Int.t_Int) }
473496

474-
let impl (v_B: usize) : Core.Clone.t_Clone (t_BoundedAbsI16 v_B) = { f_clone = (fun x -> x) }
475-
476497
[@@ FStar.Tactics.Typeclasses.tcinstance]
477-
assume
478-
val impl_1': v_B: usize -> Core.Marker.t_Copy (t_BoundedAbsI16 v_B)
479-
480-
unfold
481-
let impl_1 (v_B: usize) = impl_1' v_B
498+
let impl (v_B: usize) : Core.Clone.t_Clone (t_BoundedAbsI16 v_B) =
499+
{
500+
f_clone_pre = (fun (self: t_BoundedAbsI16 v_B) -> true);
501+
f_clone_post = (fun (self: t_BoundedAbsI16 v_B) (out: t_BoundedAbsI16 v_B) -> true);
502+
f_clone
503+
=
504+
fun (self: t_BoundedAbsI16 v_B) ->
505+
Rust_primitives.Hax.failure "(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.\nPlease upvote or comment this issue if you see this error message.\nSorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now."
506+
""
507+
}
482508

483509
[@@ FStar.Tactics.Typeclasses.tcinstance]
484-
assume
485-
val impl_3': v_B: usize -> Core.Marker.t_StructuralPartialEq (t_BoundedAbsI16 v_B)
486-
487-
unfold
488-
let impl_3 (v_B: usize) = impl_3' v_B
510+
let impl_1 (v_B: usize) : Core.Marker.t_Copy (t_BoundedAbsI16 v_B) =
511+
{ _super_15837849249852401974 = FStar.Tactics.Typeclasses.solve }
489512

490513
[@@ FStar.Tactics.Typeclasses.tcinstance]
491-
assume
492-
val impl_4': v_B: usize -> Core.Cmp.t_PartialEq (t_BoundedAbsI16 v_B) (t_BoundedAbsI16 v_B)
493-
494-
unfold
495-
let impl_4 (v_B: usize) = impl_4' v_B
514+
let impl_3 (v_B: usize) : Core.Marker.t_StructuralPartialEq (t_BoundedAbsI16 v_B) =
515+
{ __marker_trait = () }
496516

497517
[@@ FStar.Tactics.Typeclasses.tcinstance]
498-
assume
499-
val impl_2': v_B: usize -> Core.Cmp.t_Eq (t_BoundedAbsI16 v_B)
500-
501-
unfold
502-
let impl_2 (v_B: usize) = impl_2' v_B
518+
let impl_4 (v_B: usize) : Core.Cmp.t_PartialEq (t_BoundedAbsI16 v_B) (t_BoundedAbsI16 v_B) =
519+
{
520+
f_eq_pre = (fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) -> true);
521+
f_eq_post = (fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) (out: bool) -> true);
522+
f_eq = fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) -> self._0 =. other._0
523+
}
503524

504525
[@@ FStar.Tactics.Typeclasses.tcinstance]
505-
assume
506-
val impl_6': v_B: usize -> Core.Cmp.t_PartialOrd (t_BoundedAbsI16 v_B) (t_BoundedAbsI16 v_B)
507-
508-
unfold
509-
let impl_6 (v_B: usize) = impl_6' v_B
526+
let impl_2 (v_B: usize) : Core.Cmp.t_Eq (t_BoundedAbsI16 v_B) =
527+
{
528+
_super_5579681813951091494 = FStar.Tactics.Typeclasses.solve;
529+
f_assert_receiver_is_total_eq_pre = (fun (self: t_BoundedAbsI16 v_B) -> true);
530+
f_assert_receiver_is_total_eq_post = (fun (self: t_BoundedAbsI16 v_B) (out: Prims.unit) -> true);
531+
f_assert_receiver_is_total_eq
532+
=
533+
fun (self: t_BoundedAbsI16 v_B) ->
534+
Rust_primitives.Hax.failure "(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.\nPlease upvote or comment this issue if you see this error message.\nSorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now."
535+
""
536+
}
510537

511538
[@@ FStar.Tactics.Typeclasses.tcinstance]
512-
assume
513-
val impl_5': v_B: usize -> Core.Cmp.t_Ord (t_BoundedAbsI16 v_B)
514-
515-
unfold
516-
let impl_5 (v_B: usize) = impl_5' v_B
539+
let impl_6 (v_B: usize) : Core.Cmp.t_PartialOrd (t_BoundedAbsI16 v_B) (t_BoundedAbsI16 v_B) =
540+
{
541+
_super_17767811571638026139 = FStar.Tactics.Typeclasses.solve;
542+
f_partial_cmp_pre = (fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) -> true);
543+
f_partial_cmp_post
544+
=
545+
(fun
546+
(self: t_BoundedAbsI16 v_B)
547+
(other: t_BoundedAbsI16 v_B)
548+
(out: Core.Option.t_Option Core.Cmp.t_Ordering)
549+
->
550+
true);
551+
f_partial_cmp
552+
=
553+
fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) ->
554+
Core.Cmp.f_partial_cmp #i16 #i16 #FStar.Tactics.Typeclasses.solve self._0 other._0
555+
}
517556

518557
[@@ FStar.Tactics.Typeclasses.tcinstance]
519-
assume
520-
val impl_7': v_B: usize -> Core.Hash.t_Hash (t_BoundedAbsI16 v_B)
558+
let impl_5 (v_B: usize) : Core.Cmp.t_Ord (t_BoundedAbsI16 v_B) =
559+
{
560+
_super_8562072132021960682 = FStar.Tactics.Typeclasses.solve;
561+
_super_17650760217149814164 = FStar.Tactics.Typeclasses.solve;
562+
f_cmp_pre = (fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) -> true);
563+
f_cmp_post
564+
=
565+
(fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) (out: Core.Cmp.t_Ordering) -> true
566+
);
567+
f_cmp
568+
=
569+
fun (self: t_BoundedAbsI16 v_B) (other: t_BoundedAbsI16 v_B) ->
570+
Core.Cmp.f_cmp #i16 #FStar.Tactics.Typeclasses.solve self._0 other._0
571+
}
521572

522-
unfold
523-
let impl_7 (v_B: usize) = impl_7' v_B
573+
[@@ FStar.Tactics.Typeclasses.tcinstance]
574+
let impl_7 (v_B: usize) : Core.Hash.t_Hash (t_BoundedAbsI16 v_B) =
575+
{
576+
f_hash_pre
577+
=
578+
(fun
579+
(#e_ee_H: Type0)
580+
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Hash.t_Hasher e_ee_H)
581+
(self: t_BoundedAbsI16 v_B)
582+
(state: e_ee_H)
583+
->
584+
true);
585+
f_hash_post
586+
=
587+
(fun
588+
(#e_ee_H: Type0)
589+
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Hash.t_Hasher e_ee_H)
590+
(self: t_BoundedAbsI16 v_B)
591+
(state: e_ee_H)
592+
(out: e_ee_H)
593+
->
594+
true);
595+
f_hash
596+
=
597+
fun
598+
(#e_ee_H: Type0)
599+
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Hash.t_Hasher e_ee_H)
600+
(self: t_BoundedAbsI16 v_B)
601+
(state: e_ee_H)
602+
->
603+
let state:e_ee_H =
604+
Core.Hash.f_hash #i16 #FStar.Tactics.Typeclasses.solve #e_ee_H self._0 state
605+
in
606+
state
607+
}
524608

525609
let double_abs_i16 (v_N v_M: usize) (x: t_BoundedAbsI16 v_N)
526610
: Prims.Pure (t_BoundedAbsI16 v_M)

‎test-harness/src/snapshots/toolchain__lean-tests into-lean.snap‎

Lines changed: 9 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -20,38 +20,12 @@ info:
2020
include_flag: ~
2121
backend_options: ~
2222
---
23-
exit = 0
24-
stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
25-
26-
[stdout]
27-
diagnostics = []
28-
29-
[stdout.files]
30-
"lean_tests.lean" = '''
31-
-- Experimental lean backend for Hax
32-
-- Comment the following line to not import the prelude (requires the Lib.lean file) :
33-
import Lib
34-
35-
36-
37-
-- unimplemented yet
38-
39-
def FORTYTWO : usize := 42
40-
41-
def returns42 (_ : hax_Tuple0) : usize := FORTYTWO
42-
43-
def add_two_numbers (x : usize) (y : usize) : usize := (hax_machine_int_add x y)
44-
45-
def letBinding (x : usize) (y : usize) : usize :=
46-
let useless := (.constr_hax_Tuple0 : hax_Tuple0);
47-
let result1 := (hax_machine_int_add x y);
48-
let result2 := (hax_machine_int_add result1 2);
49-
(hax_machine_int_add result2 1)
50-
51-
def closure (_ : hax_Tuple0) : i32 :=
52-
let x := 41;
53-
let f := (fun y => (hax_machine_int_add y x));
54-
(ops_function_Fn_call f
55-
(.constr_hax_Tuple1 {hax_Tuple1_Tuple0 := 1} : (hax_Tuple1 i32)))
56-
57-
abbrev UsizeAlias := usize'''
23+
exit = 1
24+
stderr = """
25+
Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs
26+
27+
thread 'main' panicked at rust-engine/src/ocaml_engine.rs:88:14:
28+
called `Result::unwrap()` on an `Err` value: Os { code: 2, kind: NotFound, message: \"No such file or directory\" }
29+
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
30+
\u001B[1m\u001B[91merror\u001B[0m: \u001B[1mhax: hax-engine exited with non-zero code 101\u001B[0m"""
31+
stdout = ''

‎test-harness/src/snapshots/toolchain__literals into-coq.snap‎

Lines changed: 32 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -20,11 +20,23 @@ info:
2020
include_flag: ~
2121
backend_options: ~
2222
---
23-
exit = 0
24-
stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
25-
26-
[stdout]
27-
diagnostics = []
23+
exit = 1
24+
stderr = """
25+
Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs
26+
\u001B[1m\u001B[91merror\u001B[0m: \u001B[1m[HAX0001] (AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
27+
Please upvote or comment this issue if you see this error message.
28+
Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.\u001B[0m
29+
\u001B[1m\u001B[94m-->\u001B[0m literals/src/lib.rs:43:21
30+
\u001B[1m\u001B[94m |\u001B[0m
31+
\u001B[1m\u001B[94m43 |\u001B[0m #[derive(PartialEq, Eq)]
32+
\u001B[1m\u001B[94m |\u001B[0m\u001B[1m\u001B[91m ^^\u001B[0m
33+
\u001B[1m\u001B[94m |\u001B[0m"""
34+
[[stdout.diagnostics]]
35+
message = '''
36+
(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
37+
Please upvote or comment this issue if you see this error message.
38+
Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now.'''
39+
spans = ['Span { lo: Loc { line: 43, col: 20 }, hi: Loc { line: 43, col: 22 }, filename: Real(LocalPath("literals/src/lib.rs")), rust_span_data: None }']
2840

2941
[stdout.files]
3042
"Literals.v" = '''
@@ -91,11 +103,23 @@ Record Foo_record : Type :=
91103
#[export] Instance settable_Foo_record : Settable _ :=
92104
settable! (Build_Foo_record) <Foo_f_field>.
93105
106+
Instance t_StructuralPartialEq_61223753 : t_StructuralPartialEq ((t_Foo)) :=
107+
{
108+
}.
94109
110+
Instance t_PartialEq_662037409 : t_PartialEq ((t_Foo)) ((t_Foo)) :=
111+
{
112+
implaabbcc_t_PartialEq_f_eq := fun (self : t_Foo) (other : t_Foo)=>
113+
f_eq (f_field self) (f_field other);
114+
}.
95115
96-
97-
98-
116+
Instance t_Eq_795626685 : t_Eq ((t_Foo)) :=
117+
{
118+
implaabbcc_t_Eq_f_assert_receiver_is_total_eq := fun (self : t_Foo)=>
119+
failure (("(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/156.
120+
Please upvote or comment this issue if you see this error message.
121+
Sorry, Hax does not support declare-first let bindings (see https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) for now."%string : string)) ((""%string : string));
122+
}.
99123
100124
Definition v_CONSTANT : t_Foo :=
101125
Foo ((3 : t_u8)).

0 commit comments

Comments
 (0)