Verified reification

.gitignore

@@ -6,3 +6,6 @@ src/clib/*
 *.aux
 .lia.cache
 **Makefile*coq*
+src/verified_lowering/stringify/test/
+src/verified_lowering/stringify/lib/
+src/verified_lowering/count_reshape/out.csv

src/examples/Matmul.v

@@ -19,23 +19,23 @@ Definition matmul A B C (m1 m2 : (list (list R))) :=
       SUM [ k < B ]
       (m1 _[i;k] * m2 _[k;j])%R.
 
-Hint Unfold matmul : examples.  
+Hint Unfold matmul : examples.
 
 Section Tile.
-  Variables (A B C : nat) (m1 m2 : (list (list R))) (k : Z).
+  Variables (A B C : Z) (m1 m2 : (list (list R))) (k : Z).
   Derive matmul_tiled SuchThat
-         ((0 < k)%Z ->
+         (0 < k ->
           0 < A ->
           0 < B ->
           0 < C ->
-          consistent m1 (A,(B,tt)) ->
-          consistent m2 (B,(C,tt)) ->
-          matmul (Z.of_nat A) (Z.of_nat B) (Z.of_nat C) m1 m2 =
-            matmul_tiled) As matmultiled.
+          consistent m1 (Z.to_nat A,(Z.to_nat B,tt)) ->
+          consistent m2 (Z.to_nat B,(Z.to_nat C,tt)) ->
+          matmul A B C m1 m2 =
+            matmul_tiled)%Z As matmultiled.
   Proof.
     reschedule.
 
-    wrapid^ @flatten_truncr_tile_id' around (GEN [ _ < (Z.of_nat A) ] _)
+    wrapid^ @flatten_truncr_tile_id' around (GEN [ _ < A ] _)
       with (Z.to_nat k).
 
     inline tile.
@@ -47,47 +47,57 @@ Section Tile.
     rw @consistent_length.
     rw @consistent_length.
     rw @get_gen_some.
-    rw^ @gp_gen_iverson.    
+    rw^ @gp_gen_iverson.
     rw @get_gen_some.
-    rewrite Z2Nat.id by lia.
-
-    wrapid^ @flatten_truncr_tile_id' around (GEN [ _ < (Z.of_nat C) ] _)
+
+    wrapid^ @flatten_truncr_tile_id' around (GEN [ _ < C ] _)
       with (Z.to_nat k).
 
     inline tile.
     rw @get_gen_some.
-    rw^ @gp_gen_iverson.    
+    rw^ @gp_gen_iverson.
 
     rw @gp_double_iverson.
+
+    rw truncr_Truncr.
+    Fail progress rw truncr_Truncr. rewrite truncr_Truncr. (*??*)
+    rewrite Nat2Z.inj_sub.
+    2: { apply div_ceil_n_lower_bound. lia. }
+    rewrite Nat2Z.inj_sub.
+    2: { apply div_ceil_n_lower_bound. lia. }
+    do 2 rewrite Nat2Z.inj_mul.
+    do 2 rewrite <- of_nat_div_distr.
+    do 3 rewrite Z2Nat.id by lia.
+
     done.
   Defined.
 End Tile.
 
-Hint Unfold matmul matmul_tiled : examples.  
+Hint Unfold matmul matmul_tiled : examples.
 
 Hint Resolve floor_lt_ceil Z.div_pos : crunch.
 
 Section Tile.
-  Variables (A B C : nat) (m1 m2 : (list (list R))) (k : Z).
+  Variables (A B C : Z) (m1 m2 : (list (list R))) (k : Z).
   Derive matmul_tiled_split SuchThat
-         ((0 < k)%Z ->
+         (0 < k ->
           0 < A ->
           0 < B ->
           0 < C ->
-          consistent m1 (A,(B,tt)) ->
-          consistent m2 (B,(C,tt)) ->
-          matmul (Z.of_nat A) (Z.of_nat B) (Z.of_nat C) m1 m2 =
-            matmul_tiled_split) As matmultiledsplit.
+          consistent m1 (Z.to_nat A,(Z.to_nat B,tt)) ->
+          consistent m2 (Z.to_nat B,(Z.to_nat C,tt)) ->
+          matmul A B C m1 m2 =
+            matmul_tiled_split)%Z As matmultiledsplit.
   Proof.
     reschedule.
 
-    wrapid^ @flatten_truncr_tile_id' around (GEN [ _ < (Z.of_nat A) ] _)
+    wrapid^ @flatten_truncr_tile_id' around (GEN [ _ < A ] _)
       with (Z.to_nat k).
 
     inline tile.
     rw @get_gen_some.
 
-    rw^ @split_gen at (Z.of_nat A / k )%Z.
+    rw^ @split_gen at (A / k )%Z.
 
     simpl_guard.
     wrapid^ @transpose_transpose_id around (GEN [ _ < k ] _).
@@ -96,23 +106,31 @@ Section Tile.
     rw @consistent_length.
     rw @consistent_length.
     rw @get_gen_some.
-    rw^ @gp_gen_iverson.    
+    rw^ @gp_gen_iverson.
     rw @get_gen_some.
-    rewrite Z2Nat.id by lia.
 
-    wrapid^ @flatten_truncr_tile_id' around (GEN [ _ < (Z.of_nat C) ] _)
+    wrapid^ @flatten_truncr_tile_id' around (GEN [ _ < C ] _)
       with (Z.to_nat k).
 
     inline tile.
     rw @get_gen_some.
-    rw^ @gp_gen_iverson.    
+    rw^ @gp_gen_iverson.
 
-    rw^ @split_gen upto (Z.of_nat C // k)%Z at (Z.of_nat C / k )%Z.
+    rw^ @split_gen upto (C // k)%Z at (C / k )%Z.
     simpl_guard.
 
+    rw truncr_Truncr.
+    Fail progress rw truncr_Truncr. rewrite truncr_Truncr. (*??*)
+    rewrite Nat2Z.inj_sub.
+    2: { apply div_ceil_n_lower_bound. lia. }
+    rewrite Nat2Z.inj_sub.
+    2: { apply div_ceil_n_lower_bound. lia. }
+    do 2 rewrite Nat2Z.inj_mul.
+    do 2 rewrite <- of_nat_div_distr.
+    do 3 rewrite Z2Nat.id by lia.
+
     done.
   Defined.
 End Tile.
 
-Hint Unfold matmul_tiled_split : examples.  
-
+Hint Unfold matmul_tiled_split : examples.

src/examples/TensorAdd.v

@@ -20,7 +20,7 @@ Definition add A B C D (m1 m2 : (list (list (list (list R))))) :=
       GEN [ l < D ]
       (m1 _[i;j;k;l] * m2 _[i;j;k;l])%R.
 
-Hint Unfold add : examples.  
+Hint Unfold add : examples.
 Hint Resolve Z.div_lt_upper_bound mul_add_lt : crunch.
 
 Lemma mul_add_lt : forall i j k A C,
@@ -35,23 +35,22 @@ Proof.
     rewrite Z.mod_small by lia. reflexivity.
   - inversion H2. subst.
     rewrite div_mod_eq by lia. reflexivity.
-Qed.      
+Qed.
 
 Section Add.
-  Variables (A B C D : nat) (m1 m2 : (list (list (list (list R))))).
+  Variables (A B C D : Z) (m1 m2 : (list (list (list (list R))))).
   Derive add_split SuchThat
          (0 < A ->
           0 < B ->
           0 < C ->
           0 < D ->
-          consistent m1 (A,(B,(C,(D,tt)))) ->
-          consistent m2 (A,(B,(C,(D,tt)))) ->
-          add (Z.of_nat A) (Z.of_nat B) (Z.of_nat C) (Z.of_nat D) m1 m2 =
-            add_split) As matmultiled.
+          consistent m1 (Z.to_nat A,(Z.to_nat B,(Z.to_nat C,(Z.to_nat D,tt)))) ->
+          consistent m2 (Z.to_nat A,(Z.to_nat B,(Z.to_nat C,(Z.to_nat D,tt)))) ->
+          add A B C D m1 m2 = add_split)%Z As matmultiled.
   Proof.
     reschedule.
 
-    wrapid^ @tile_flatten_id around (GEN [ _ < (Z.of_nat A) ] _).
+    wrapid^ @tile_flatten_id around (GEN [ _ < A ] _).
 
     inline flatten.
     rw @consistent_length.
@@ -92,8 +91,14 @@ Section Add.
     rw @sum_bound_indic_no_f_guard.
 
     repeat rw Z.div_div.
+
+    rw tile_Tile.
+    Fail progress rw tile_Tile. rewrite tile_Tile.
+    Fail progress rw tile_Tile. rewrite tile_Tile.
+    do 3 rewrite Z2Nat.id by lia.
+
     done.
   Defined.
  End Add.
 
-Hint Unfold add add_split : examples.  
+Hint Unfold add add_split : examples.