Merge pull request #369 from hacspec/monomorphize-update-at

Monomorphize update at

engine/lib/concrete_ident/names.rs

@@ -24,6 +24,9 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mu
 
     let _ = [()].into_iter();
     let _ = 1..2;
+    let _ = 1..;
+    let _ = ..;
+    let _ = ..1;
 
     const _: () = {
         use core::{cmp::*, ops::*};
@@ -116,9 +119,15 @@ mod hax {
 
     fn repeat() {}
     fn update_at() {}
+    mod monomorphized_update_at {
+        fn update_at_usize() {}
+        fn update_at_range() {}
+        fn update_at_range_from() {}
+        fn update_at_range_to() {}
+        fn update_at_range_full() {}
+    }
     // TODO: Should that live here? (this is F* specific)
     fn array_of_list() {}
-
     fn never_to_any() {}
 
     mod control_flow_monad {

engine/lib/phases/phase_trivialize_assign_lhs.ml

@@ -52,11 +52,28 @@ module%inlined_contents Make (F : Features.T) = struct
           | _ -> Error.raise { kind = ArbitraryLHS; span })
       | LhsArrayAccessor { e; typ = _; index; _ } ->
           let lhs = UA.expr_of_lhs span e |> dexpr in
-          let rhs =
-            UB.call Rust_primitives__hax__update_at
-              [ lhs; dexpr index; rhs ]
-              span lhs.typ
+          let update_at : Concrete_ident.name =
+            let index_typ =
+              match index.typ with TRef { typ; _ } -> typ | _ -> index.typ
+            in
+            match index_typ with
+            | TInt { size = SSize; signedness = Unsigned } ->
+                Rust_primitives__hax__monomorphized_update_at__update_at_usize
+            | TApp { ident; _ }
+              when Global_ident.eq_name Core__ops__range__Range ident ->
+                Rust_primitives__hax__monomorphized_update_at__update_at_range
+            | TApp { ident; _ }
+              when Global_ident.eq_name Core__ops__range__RangeFrom ident ->
+                Rust_primitives__hax__monomorphized_update_at__update_at_range_from
+            | TApp { ident; _ }
+              when Global_ident.eq_name Core__ops__range__RangeTo ident ->
+                Rust_primitives__hax__monomorphized_update_at__update_at_range_to
+            | TApp { ident; _ }
+              when Global_ident.eq_name Core__ops__range__RangeFull ident ->
+                Rust_primitives__hax__monomorphized_update_at__update_at_range_full
+            | _ -> Rust_primitives__hax__update_at
           in
+          let rhs = UB.call update_at [ lhs; dexpr index; rhs ] span lhs.typ in
           updater_of_lhs e rhs span
       | LhsArbitraryExpr _ -> Error.raise { kind = ArbitraryLHS; span }
 

proof-libs/fstar/core/Core.Ops.Range.fsti

@@ -4,6 +4,7 @@ open Rust_primitives
 type t_RangeTo   (t: Type) = {f_end: t}
 type t_RangeFrom (t: Type) = {f_start: t}
 type t_Range     (t: Type) = {f_start: t; f_end: t}
+type t_RangeFull           = | RangeFull
 
 open Core.Iter.Traits.Iterator
 
@@ -57,6 +58,11 @@ instance impl_index_range_from_slice t n : t_Index (t_Slice t) (t_RangeFrom (int
     ; f_index = (fun s {f_start} -> 
          let len = Rust_primitives.length s in
          if v f_start = v len then Seq.empty else Seq.slice s (v f_start) (v len))}
+
+instance impl_index_range_full_slice t : t_Index (t_Slice t) t_RangeFull
+  = { f_Output = t_Slice t
+    ; in_range = (fun (s: t_Slice t) _ -> True)
+    ; f_index = (fun s _ -> s)}
 
 instance impl_range_index_array t len n : t_Index (t_Array t len) (t_Range (int_t n)) = 
   let i = impl_index_range_slice t n in
@@ -76,6 +82,12 @@ instance impl_range_from_index_array t len n : t_Index (t_Array t len) (t_RangeF
   ; in_range = (fun (s: t_Array t len) r -> i.in_range s r)
   ; f_index = (fun s r -> i.f_index s r) }
 
+instance impl_range_full_index_array t len : t_Index (t_Array t len) t_RangeFull = 
+  let i = impl_index_range_full_slice t in
+  { f_Output = i.f_Output
+  ; in_range = (fun (s: t_Array t len) r -> i.in_range s r)
+  ; f_index = (fun s r -> i.f_index s r) }
+
 open Rust_primitives.Hax
 
 let update_at_tc_array_range_super t l n: t_Index (t_Array t l) (t_Range (int_t n))
@@ -84,6 +96,8 @@ let update_at_tc_array_range_to_super t l n: t_Index (t_Array t l) (t_RangeTo (i
   = FStar.Tactics.Typeclasses.solve
 let update_at_tc_array_range_from_super t l n: t_Index (t_Array t l) (t_RangeFrom (int_t n))
   = FStar.Tactics.Typeclasses.solve
+let update_at_tc_array_range_full_super t l n: t_Index (t_Array t l) t_RangeFull
+  = FStar.Tactics.Typeclasses.solve
 
 val update_at_array_range t l n
   (s: t_Array t l) (i: t_Range (int_t n) {(update_at_tc_array_range_super t l n).in_range s i})
@@ -94,6 +108,9 @@ val update_at_array_range_to t l n
 val update_at_array_range_from t l n
   (s: t_Array t l) (i: t_RangeFrom (int_t n) {(update_at_tc_array_range_from_super t l n).in_range s i})
   : (update_at_tc_array_range_from_super t l n).f_Output -> t_Array t l
+val update_at_array_range_full t l n
+  (s: t_Array t l) (i: t_RangeFull)
+  : (update_at_tc_array_range_full_super t l n).f_Output -> t_Array t l
 
 instance update_at_tc_array_range t l n: update_at_tc (t_Array t l) (t_Range (int_t n)) = {
   super_index = update_at_tc_array_range_super t l n;
@@ -107,3 +124,7 @@ instance update_at_tc_array_range_from t l n: update_at_tc (t_Array t l) (t_Rang
   super_index = update_at_tc_array_range_from_super t l n;
   update_at = update_at_array_range_from t l n
 }
+instance update_at_tc_array_range_full t l n: update_at_tc (t_Array t l) t_RangeFull = {
+  super_index = update_at_tc_array_range_full_super t l n;
+  update_at = update_at_array_range_full t l n
+}

proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Monomorphized_update_at.fst

@@ -0,0 +1,42 @@
+module Rust_primitives.Hax.Monomorphized_update_at
+
+open Rust_primitives
+open Rust_primitives.Hax
+open Core.Ops.Range
+
+let update_at_usize
+  (s: t_Slice 't)
+  (i: usize {i <. length s}) 
+  (v: 't)
+  : t_Array 't (length s)
+  = update_at s i v
+
+let update_at_range #n
+  (s: t_Slice 't)
+  (i: t_Range (int_t n) {(impl_index_range_slice 't n).in_range s i}) 
+  (v: t_Slice 't)
+  : t_Array 't (length s)
+  = update_at s i v
+
+let update_at_range_to #n
+  (s: t_Slice 't)
+  (i: t_RangeTo (int_t n) {(impl_index_range_to_slice 't n).in_range s i}) 
+  (v: t_Slice 't)
+  : t_Array 't (length s)
+  = update_at s i v
+
+let update_at_range_from #n
+  (s: t_Slice 't)
+  (i: t_RangeFrom (int_t n) {(impl_index_range_from_slice 't n).in_range s i}) 
+  (v: t_Slice 't)
+  : t_Array 't (length s)
+  = update_at s i v
+
+let update_at_range_full
+  (s: t_Slice 't)
+  (i: t_RangeFull {(impl_index_range_full_slice 't).in_range s i}) 
+  (v: t_Slice 't)
+  : t_Array 't (length s)
+  = update_at s i v
+
+

test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap

@@ -41,7 +41,9 @@ open FStar.Mul
 class t_FooTrait (v_Self: Type) = { f_z:v_Self -> v_Self }
 
 let array (x: t_Array u8 (sz 10)) : t_Array u8 (sz 10) =
-  let x:t_Array u8 (sz 10) = Rust_primitives.Hax.update_at x (sz 1) (x.[ sz 2 ] <: u8) in
+  let x:t_Array u8 (sz 10) =
+    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize x (sz 1) (x.[ sz 2 ] <: u8)
+  in
   x
 
 let f: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
@@ -80,16 +82,18 @@ let index_mutation (x: Core.Ops.Range.t_Range usize) (a: t_Slice u8) : Prims.uni
         Alloc.Boxed.t_Box (t_Slice u8) Alloc.Alloc.t_Global)
   in
   let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Rust_primitives.Hax.update_at v
+    Rust_primitives.Hax.Monomorphized_update_at.update_at_range v
       x
       (Core.Slice.impl__copy_from_slice (v.[ x ] <: t_Slice u8) a <: t_Slice u8)
   in
-  let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Rust_primitives.Hax.update_at v (sz 1) 3uy in
+  let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v (sz 1) 3uy
+  in
   ()
 
 let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 =
   let x:t_Array u8 (sz 12) =
-    Rust_primitives.Hax.update_at x
+    Rust_primitives.Hax.Monomorphized_update_at.update_at_range x
       ({ Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = sz 5 }
         <:
         Core.Ops.Range.t_Range usize)
@@ -149,7 +153,14 @@ let impl_FooTrait_for_Foo: t_FooTrait t_Foo = { f_z = fun (self: t_Foo) -> self
 type t_S = { f_b:t_Array u8 (sz 5) }
 
 let impl__S__update (self: t_S) (x: u8) : t_S =
-  let self:t_S = { self with f_b = Rust_primitives.Hax.update_at self.f_b (sz 0) x } <: t_S in
+  let self:t_S =
+    {
+      self with
+      f_b = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize self.f_b (sz 0) x
+    }
+    <:
+    t_S
+  in
   self
 
 let foo (lhs rhs: t_S) : t_S =
@@ -170,7 +181,7 @@ let foo (lhs rhs: t_S) : t_S =
             lhs with
             f_b
             =
-            Rust_primitives.Hax.update_at lhs.f_b
+            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize lhs.f_b
               i
               ((lhs.f_b.[ i ] <: u8) +! (rhs.f_b.[ i ] <: u8) <: u8)
             <: