Merge pull request #565 from hacspec/type-ascription

feat(engine/import): support `ValueTypeAscription`

engine/lib/import_thir.ml

@@ -646,8 +646,7 @@ end) : EXPR = struct
       | StaticRef { def_id = id; _ } -> GlobalVar (def_id Value id)
       | PlaceTypeAscription _ ->
           unimplemented [ e.span ] "expression PlaceTypeAscription"
-      | ValueTypeAscription _ ->
-          unimplemented [ e.span ] "expression ValueTypeAscription"
+      | ValueTypeAscription { source; _ } -> (c_expr source).e
       | ZstLiteral _ -> unimplemented [ e.span ] "expression ZstLiteral"
       | Yield _ -> unimplemented [ e.span ] "expression Yield"
       | Todo payload -> unimplemented [ e.span ] ("expression Todo\n" ^ payload)

test-harness/src/snapshots/toolchain__slices into-coq.snap

@@ -0,0 +1,54 @@
+---
+source: test-harness/src/harness.rs
+expression: snapshot
+info:
+  kind:
+    Translate:
+      backend: coq
+  info:
+    name: slices
+    manifest: slices/Cargo.toml
+    description: ~
+  spec:
+    optional: false
+    broken: false
+    issue_id: ~
+    positive: true
+    snapshot:
+      stderr: true
+      stdout: true
+    include_flag: ~
+    backend_options: ~
+---
+exit = 0
+stderr = '''
+Compiling slices v0.1.0 (WORKSPACE_ROOT/slices)
+    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+
+[stdout]
+diagnostics = []
+
+[stdout.files]
+"Slices.v" = '''
+(* File automatically generated by Hacspec *)
+From Hacspec Require Import Hacspec_Lib MachineIntegers.
+From Coq Require Import ZArith.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+(*Not implemented yet? todo(item)*)
+
+Definition v_VERSION : seq int8 :=
+  unsize (array_from_list [(@repr WORDSIZE8 118);
+    (@repr WORDSIZE8 49)]).
+
+Definition do_something (_ : seq int8) : unit :=
+  tt.
+
+Definition r#unsized (_ : nseq (seq int8) TODO: Int.to_string length) : unit :=
+  tt.
+
+Definition sized (x : nseq (nseq int8 TODO: Int.to_string length) TODO: Int.to_string length) : unit :=
+  r#unsized (array_from_list [unsize (x.[(@repr WORDSIZE32 0)])]).
+'''

test-harness/src/snapshots/toolchain__slices into-fstar.snap

@@ -0,0 +1,51 @@
+---
+source: test-harness/src/harness.rs
+expression: snapshot
+info:
+  kind:
+    Translate:
+      backend: fstar
+  info:
+    name: slices
+    manifest: slices/Cargo.toml
+    description: ~
+  spec:
+    optional: false
+    broken: false
+    issue_id: ~
+    positive: true
+    snapshot:
+      stderr: true
+      stdout: true
+    include_flag: ~
+    backend_options: ~
+---
+exit = 0
+stderr = '''
+Compiling slices v0.1.0 (WORKSPACE_ROOT/slices)
+    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+
+[stdout]
+diagnostics = []
+
+[stdout.files]
+"Slices.fst" = '''
+module Slices
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let v_VERSION: t_Slice u8 =
+  Rust_primitives.unsize (let list = [118uy; 49uy] in
+      FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
+      Rust_primitives.Hax.array_of_list 2 list)
+
+let do_something (_: t_Slice u8) : Prims.unit = ()
+
+let r#unsized (_: t_Array (t_Slice u8) (sz 1)) : Prims.unit = ()
+
+let sized (x: t_Array (t_Array u8 (sz 4)) (sz 1)) : Prims.unit =
+  r#unsized (let list = [Rust_primitives.unsize (x.[ sz 0 ] <: t_Array u8 (sz 4)) <: t_Slice u8] in
+      FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+      Rust_primitives.Hax.array_of_list 1 list)
+'''

tests/slices/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" = { broken = false, issue_id = "85" }

tests/slices/src/lib.rs

@@ -6,3 +6,9 @@ const VERSION: &[u8] = b"v1";
 // This panics
 // thread 'rustc' panicked at 'hax-engine exited with non-zero code', cli/driver/src/exporter.rs:217:2
 pub fn do_something(_: &[u8]) {}
+
+pub fn sized(x: &[&[u8; 4]; 1]) {
+    r#unsized(&[(x[0] as &[u8])])
+}
+
+pub fn r#unsized(_: &[&[u8]; 1]) {}