Commit 94223ac7 authored by Martin Clochard's avatar Martin Clochard
Browse files

verifythis_2016_matrix_multiplication:

- Define set with create (and constrained a benign mistake on axioms)
- s/FloatMatrix/Matrix
parent 1dbdd078
......@@ -29,8 +29,9 @@ theory MatrixGen
axiom set_def4:
forall m: mat 'a, i j: int, v: 'a. 0 <= i < rows m -> 0 <= j < cols m ->
forall i' j': int. (i <> i' \/ j <> j') ->
get (set m i j v) i' j' = get m i' j'
forall i' j': int. 0 <= i' < rows m /\ 0 <= j' < cols m /\
(i <> i' \/ j <> j') ->
get (set m i j v) i' j' = get m i' j'
predicate (==) (m1 m2: mat 'a) =
rows m1 = rows m2 && cols m1 = cols m2 &&
......@@ -46,12 +47,18 @@ theory MatrixGen
end
theory FloatMatrix
theory Matrix
clone export MatrixGen
use import int.Int
use HighOrd
use import int.Int
type mat 'a
function rows (mat 'a) : int
function cols (mat 'a) : int
function get (mat 'a) int int : 'a
function create (r c: int) (f: int -> int -> 'a) : mat 'a
......@@ -67,6 +74,21 @@ theory FloatMatrix
forall r c: int, f: int -> int -> 'a, i j: int.
0 <= i < r -> 0 <= j < c -> get (create r c f) i j = f i j
function set (m:mat 'a) (x y:int) (z:'a) : mat 'a =
create m.rows m.cols (\x1 y1. if x1 = x && y1 = y then z else get m x1 y1)
clone export MatrixGen with type mat 'a = mat 'a,
function rows = rows,
function cols = cols,
function get = get,
function set = set,
lemma set_def1,
lemma set_def2,
lemma set_def3,
lemma set_def4
use import int.Int
end
theory FixedMatrix
......@@ -125,7 +147,7 @@ module MatrixArithmetic
use import int.Int
use import int.Sum
use import sum_extended.Sum_extended
use import FloatMatrix
use import Matrix
(* Zero matrix *)
constant zerof : int -> int -> int = \_ _. 0
......@@ -267,7 +289,7 @@ module BlockMul
use import int.Int
use import int.Sum
use import sum_extended.Sum_extended
use import FloatMatrix
use import Matrix
use import MatrixArithmetic
function ofs2 (a: mat int) (ai aj: int) : int -> int -> int
......
......@@ -4,10 +4,22 @@
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../matrices.mlw" expanded="true">
<theory name="MatrixGen" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<file name="../matrices.mlw">
<theory name="MatrixGen" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="FloatMatrix" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="Matrix" sum="862099dd531bba3a8ce8aca77f580ae7">
<goal name="set_def1">
<proof prover="1"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="set_def2">
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="set_def3">
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="set_def4">
<proof prover="1"><result status="valid" time="0.00" steps="22"/></proof>
</goal>
</theory>
<theory name="FixedMatrix" sum="81d1f6ecddc981db1f906002ad2c6515">
<goal name="rows_and_cols_nonnegative">
......@@ -19,7 +31,7 @@
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
</theory>
<theory name="MatrixArithmetic" sum="95c5ea5a8476dec9b6807e6463fa7c50">
<theory name="MatrixArithmetic" sum="179a17c543d2ee8c5d1128db6e7ac5b9">
<goal name="zero_neutral">
<transf name="split_goal_wp">
<goal name="zero_neutral.1" expl="1.">
......@@ -64,7 +76,7 @@
<proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="opposite_add">
<proof prover="0"><result status="valid" time="0.25"/></proof>
<proof prover="0"><result status="valid" time="0.49"/></proof>
</goal>
<goal name="WP_parameter mul_assoc_get" expl="VC for mul_assoc_get">
<transf name="split_goal_wp">
......@@ -72,7 +84,7 @@
<proof prover="1"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter mul_assoc_get.2" expl="2. precondition">
<proof prover="1"><result status="valid" time="2.40" steps="94"/></proof>
<proof prover="1"><result status="valid" time="3.14" steps="94"/></proof>
</goal>
<goal name="WP_parameter mul_assoc_get.3" expl="3. assertion">
<proof prover="1"><result status="valid" time="0.06" steps="37"/></proof>
......@@ -145,10 +157,10 @@
</transf>
</goal>
<goal name="mul_zero_right">
<proof prover="1"><result status="valid" time="1.91" steps="404"/></proof>
<proof prover="1"><result status="valid" time="1.91" steps="394"/></proof>
</goal>
<goal name="mul_zero_left">
<proof prover="1"><result status="valid" time="1.65" steps="396"/></proof>
<proof prover="1"><result status="valid" time="1.65" steps="387"/></proof>
</goal>
<goal name="mul_opp">
<transf name="split_goal_wp">
......@@ -162,14 +174,14 @@
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="mul_opp.4" expl="4.">
<proof prover="1"><result status="valid" time="3.92" steps="2401"/></proof>
<proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="BlockMul" sum="08ae5cbffa4e68e45d31bc65f734c776">
<theory name="BlockMul" sum="a0d8b3f3a9391a77a23d88b4d4a63f23">
<goal name="WP_parameter block_mul_ij" expl="VC for block_mul_ij">
<proof prover="1"><result status="valid" time="2.31" steps="880"/></proof>
<proof prover="1"><result status="valid" time="1.25" steps="880"/></proof>
</goal>
<goal name="WP_parameter mul_split" expl="VC for mul_split">
<proof prover="1"><result status="valid" time="0.29" steps="218"/></proof>
......
......@@ -3,7 +3,7 @@ module Symb
use import int.Int
use import list.List
use import matrices.FloatMatrix
use import matrices.Matrix
use import matrices.MatrixArithmetic
namespace LOCAL
......
......@@ -5,9 +5,9 @@
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../matrices_ring_simp.mlw">
<theory name="Symb" sum="16040e7e8e08a9182d0ed1e9cad734f1">
<theory name="Symb" sum="aa56815b148e133d02ca363f67192b13">
<goal name="LOCAL.WP_parameter l_mdl_ok" expl="VC for l_mdl_ok">
<proof prover="1"><result status="valid" time="0.03" steps="84"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="100"/></proof>
</goal>
<goal name="LOCAL.WP_parameter m_mdl_ok" expl="VC for m_mdl_ok">
<proof prover="1"><result status="valid" time="0.03" steps="33"/></proof>
......@@ -16,7 +16,7 @@
<proof prover="1"><result status="valid" time="0.04" steps="88"/></proof>
</goal>
<goal name="LOCAL.WP_parameter lm_mdl_same" expl="VC for lm_mdl_same">
<proof prover="1"><result status="valid" time="0.08" steps="148"/></proof>
<proof prover="1"><result status="valid" time="0.08" steps="152"/></proof>
</goal>
<goal name="LOCAL.WP_parameter l_compare_zero" expl="VC for l_compare_zero">
<proof prover="1"><result status="valid" time="0.03" steps="44"/></proof>
......@@ -56,7 +56,7 @@
<proof prover="1"><result status="valid" time="0.09" steps="192"/></proof>
</goal>
<goal name="LOCAL.WP_parameter lm_dump_ok" expl="VC for lm_dump_ok">
<proof prover="1"><result status="valid" time="0.16" steps="248"/></proof>
<proof prover="1"><result status="valid" time="0.16" steps="247"/></proof>
</goal>
<goal name="LOCAL.WP_parameter lm_merge_ok" expl="VC for lm_merge_ok">
<transf name="split_goal_wp">
......@@ -103,7 +103,7 @@
<proof prover="1"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter lm_merge_ok.15" expl="15. postcondition">
<proof prover="0"><result status="valid" time="1.87"/></proof>
<proof prover="0"><result status="valid" time="3.07"/></proof>
</goal>
</transf>
</goal>
......@@ -117,7 +117,7 @@
<proof prover="1"><result status="valid" time="0.08" steps="211"/></proof>
</goal>
<goal name="LOCAL.WP_parameter lm_distribute_ok" expl="VC for lm_distribute_ok">
<proof prover="1"><result status="valid" time="0.19" steps="363"/></proof>
<proof prover="1"><result status="valid" time="0.19" steps="356"/></proof>
</goal>
<goal name="LOCAL.WP_parameter lm_opp_ok" expl="VC for lm_opp_ok">
<transf name="split_goal_wp">
......@@ -148,25 +148,25 @@
</transf>
</goal>
<goal name="extends_rw">
<proof prover="1"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter symb_env" expl="VC for symb_env">
<proof prover="1"><result status="valid" time="0.02" steps="2"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="3"/></proof>
</goal>
<goal name="WP_parameter symb_reg" expl="VC for symb_reg">
<proof prover="1"><result status="valid" time="0.07" steps="59"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="60"/></proof>
</goal>
<goal name="WP_parameter symb_opp" expl="VC for symb_opp">
<proof prover="1"><result status="valid" time="0.03" steps="15"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="16"/></proof>
</goal>
<goal name="WP_parameter symb_add" expl="VC for symb_add">
<proof prover="1"><result status="valid" time="0.10" steps="145"/></proof>
<proof prover="1"><result status="valid" time="0.10" steps="148"/></proof>
</goal>
<goal name="WP_parameter symb_sub" expl="VC for symb_sub">
<proof prover="1"><result status="valid" time="0.04" steps="40"/></proof>
<proof prover="1"><result status="valid" time="0.04" steps="41"/></proof>
</goal>
<goal name="WP_parameter symb_mul" expl="VC for symb_mul">
<proof prover="1"><result status="valid" time="0.03" steps="24"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="25"/></proof>
</goal>
<goal name="WP_parameter harness" expl="VC for harness">
<transf name="split_goal_wp">
......@@ -179,7 +179,7 @@
<goal name="WP_parameter harness.1.1.1.1" expl="1. precondition">
<transf name="introduce_premises">
<goal name="WP_parameter harness.1.1.1.1.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.03" steps="30"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="31"/></proof>
</goal>
</transf>
</goal>
......@@ -190,7 +190,7 @@
</transf>
</goal>
<goal name="WP_parameter harness.2" expl="2. precondition">
<proof prover="1"><result status="valid" time="0.06" steps="76"/></proof>
<proof prover="1"><result status="valid" time="0.06" steps="77"/></proof>
</goal>
<goal name="WP_parameter harness.3" expl="3. precondition">
<transf name="compute_specified">
......@@ -201,7 +201,7 @@
<goal name="WP_parameter harness.3.1.1.1" expl="1. precondition">
<transf name="introduce_premises">
<goal name="WP_parameter harness.3.1.1.1.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="33"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
</transf>
</goal>
......@@ -212,13 +212,13 @@
</transf>
</goal>
<goal name="WP_parameter harness.4" expl="4. precondition">
<proof prover="1"><result status="valid" time="0.07" steps="88"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="89"/></proof>
</goal>
<goal name="WP_parameter harness.5" expl="5. precondition">
<proof prover="1"><result status="valid" time="0.04" steps="62"/></proof>
<proof prover="1"><result status="valid" time="0.04" steps="63"/></proof>
</goal>
<goal name="WP_parameter harness.6" expl="6. precondition">
<proof prover="1"><result status="valid" time="0.06" steps="100"/></proof>
<proof prover="1"><result status="valid" time="0.06" steps="101"/></proof>
</goal>
<goal name="WP_parameter harness.7" expl="7. precondition">
<transf name="compute_specified">
......@@ -229,7 +229,7 @@
<goal name="WP_parameter harness.7.1.1.1" expl="1. precondition">
<transf name="introduce_premises">
<goal name="WP_parameter harness.7.1.1.1.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="41"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
</transf>
</goal>
......@@ -240,13 +240,13 @@
</transf>
</goal>
<goal name="WP_parameter harness.8" expl="8. precondition">
<proof prover="1"><result status="valid" time="0.07" steps="111"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="112"/></proof>
</goal>
<goal name="WP_parameter harness.9" expl="9. precondition">
<proof prover="1"><result status="valid" time="0.06" steps="76"/></proof>
<proof prover="1"><result status="valid" time="0.06" steps="77"/></proof>
</goal>
<goal name="WP_parameter harness.10" expl="10. precondition">
<proof prover="1"><result status="valid" time="0.05" steps="76"/></proof>
<proof prover="1"><result status="valid" time="0.05" steps="77"/></proof>
</goal>
<goal name="WP_parameter harness.11" expl="11. precondition">
<transf name="compute_specified">
......@@ -257,7 +257,7 @@
<goal name="WP_parameter harness.11.1.1.1" expl="1. precondition">
<transf name="introduce_premises">
<goal name="WP_parameter harness.11.1.1.1.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="44"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="45"/></proof>
</goal>
</transf>
</goal>
......@@ -268,67 +268,67 @@
</transf>
</goal>
<goal name="WP_parameter harness.12" expl="12. precondition">
<proof prover="1"><result status="valid" time="0.10" steps="132"/></proof>
<proof prover="1"><result status="valid" time="0.10" steps="133"/></proof>
</goal>
<goal name="WP_parameter harness.13" expl="13. precondition">
<proof prover="1"><result status="valid" time="0.05" steps="90"/></proof>
<proof prover="1"><result status="valid" time="0.05" steps="91"/></proof>
</goal>
<goal name="WP_parameter harness.14" expl="14. precondition">
<proof prover="1"><result status="valid" time="0.05" steps="90"/></proof>
<proof prover="1"><result status="valid" time="0.05" steps="91"/></proof>
</goal>
<goal name="WP_parameter harness.15" expl="15. precondition">
<proof prover="1"><result status="valid" time="0.06" steps="96"/></proof>
<proof prover="1"><result status="valid" time="0.06" steps="97"/></proof>
</goal>
<goal name="WP_parameter harness.16" expl="16. precondition">
<proof prover="1"><result status="valid" time="0.06" steps="96"/></proof>
<proof prover="1"><result status="valid" time="0.06" steps="97"/></proof>
</goal>
<goal name="WP_parameter harness.17" expl="17. precondition">
<proof prover="1"><result status="valid" time="0.06" steps="103"/></proof>
<proof prover="1"><result status="valid" time="0.06" steps="104"/></proof>
</goal>
<goal name="WP_parameter harness.18" expl="18. precondition">
<proof prover="1"><result status="valid" time="0.07" steps="103"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="104"/></proof>
</goal>
<goal name="WP_parameter harness.19" expl="19. precondition">
<proof prover="1"><result status="valid" time="0.07" steps="110"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="111"/></proof>
</goal>
<goal name="WP_parameter harness.20" expl="20. precondition">
<proof prover="1"><result status="valid" time="0.06" steps="110"/></proof>
<proof prover="1"><result status="valid" time="0.06" steps="111"/></proof>
</goal>
<goal name="WP_parameter harness.21" expl="21. precondition">
<proof prover="1"><result status="valid" time="0.07" steps="116"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="117"/></proof>
</goal>
<goal name="WP_parameter harness.22" expl="22. precondition">
<proof prover="1"><result status="valid" time="0.07" steps="116"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="117"/></proof>
</goal>
<goal name="WP_parameter harness.23" expl="23. precondition">
<proof prover="1"><result status="valid" time="0.07" steps="123"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="124"/></proof>
</goal>
<goal name="WP_parameter harness.24" expl="24. precondition">
<proof prover="1"><result status="valid" time="0.07" steps="123"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="124"/></proof>
</goal>
<goal name="WP_parameter harness.25" expl="25. precondition">
<proof prover="1"><result status="valid" time="0.08" steps="130"/></proof>
<proof prover="1"><result status="valid" time="0.08" steps="131"/></proof>
</goal>
<goal name="WP_parameter harness.26" expl="26. precondition">
<proof prover="1"><result status="valid" time="0.07" steps="130"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="131"/></proof>
</goal>
<goal name="WP_parameter harness.27" expl="27. precondition">
<proof prover="1"><result status="valid" time="0.07" steps="137"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="138"/></proof>
</goal>
<goal name="WP_parameter harness.28" expl="28. precondition">
<proof prover="1"><result status="valid" time="0.08" steps="137"/></proof>
<proof prover="1"><result status="valid" time="0.08" steps="138"/></proof>
</goal>
<goal name="WP_parameter harness.29" expl="29. precondition">
<proof prover="1"><result status="valid" time="0.08" steps="143"/></proof>
<proof prover="1"><result status="valid" time="0.08" steps="144"/></proof>
</goal>
<goal name="WP_parameter harness.30" expl="30. precondition">
<proof prover="1"><result status="valid" time="0.08" steps="143"/></proof>
<proof prover="1"><result status="valid" time="0.08" steps="144"/></proof>
</goal>
<goal name="WP_parameter harness.31" expl="31. precondition">
<proof prover="1"><result status="valid" time="0.09" steps="149"/></proof>
<proof prover="1"><result status="valid" time="0.09" steps="150"/></proof>
</goal>
<goal name="WP_parameter harness.32" expl="32. precondition">
<proof prover="1"><result status="valid" time="0.07" steps="149"/></proof>
<proof prover="1"><result status="valid" time="0.07" steps="150"/></proof>
</goal>
<goal name="WP_parameter harness.33" expl="33. assertion">
<transf name="compute_specified">
......
......@@ -4,7 +4,7 @@ module MatrixMultiplication
use import int.Sum
use import ref.Ref
use import map.Map
use import matrices.FloatMatrix as F
use import matrices.Matrix as F
use import matrices.MatrixArithmetic
use import matrices.BlockMul
use import matrices_ring_simp.Symb
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment