Annotate the soundness statement

coq/ErrorValidationAA.v

@@ -236,6 +236,11 @@ Fixpoint validErrorboundAACmd (f: cmd Q) (* analyzed cmd with let's *)
   | Ret e => validErrorboundAA e typeMap A dVars currNoise errMap
   end.
 
+(* Notation for the universal case of the soundness statement, to help reason
+   about memoization cases. This allows us to show several monotonicity lemmas
+   that simplify the soundness proofs. This definition is just an extract from
+   the full soundness statement, for elaboration on the used assumptions and the
+   goal, find that statement below *)
 Definition checked_error_expressions (e: expr Q) E1 E2 A Gamma DeltaMap
            noise_map noise expr_map :=
   forall v__R v__FP m__FP (iv__A: intv) (err__A: error),
@@ -777,6 +782,11 @@ Proof.
       * apply flover_map_in_add.
 Qed.
 
+(* The soundness statements starts off with assumption that the checking
+   function succeeds and then also maintains several invariants. We require
+   these invariants because of the checker function dependency on the current
+   noise index and its memoization of the previosly computed polynomials. We
+   explain these invariants in-line below. *)
 Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVars :=
   forall (expr_map1 expr_map2 : FloverMap.t (affine_form Q))
     (noise_map1 : nat -> option noise_type) (noise1 noise2 : nat) (v__R : R)
@@ -790,39 +800,74 @@ Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVar
     NatSet.Subset (usedVars e -- dVars) fVars ->
     validTypes e Gamma ->
     FloverMap.find e A = Some (iv__A, err__A) ->
+    (* Starting noise index is greater than 0 and the noise mapping doesn't
+       map it and anything above to a noise value *)
     (0 < noise1)%nat ->
     (forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) ->
+    (* If a var is a dVar, we know it's in expr_map and invoke the corresponding
+     preconditions (described below) *)
     dVars_contained dVars expr_map1 ->
+    (* Precondition:
+       Memoization for the existential case of the goal: if we checked the expression
+       already, we know that there is an execution and certificate results for it *)
     (forall e' : FloverMap.key,
         FloverMap.In e' expr_map1 ->
+        (* Assumption needed for Cmd_sound proof *)
         NatSet.Subset (usedVars e') (NatSet.union fVars dVars) /\
         (exists iv__A' err__A', FloverMap.find e' A = Some (iv__A', err__A')) /\
         exists (v__FP' : R) (m__FP' : mType),
           eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP') ->
+    (* Precondition:
+       Memoization for the universal case of the goal -- note that
+       `checked_error_expressions` track only that case: if we checked
+       the expression already, then, if we provide the execution in
+       finite precision and the certificate results, we will know that
+       the execution's error is bounded *)
     (forall e' : FloverMap.key,
         FloverMap.In e' expr_map1 ->
         checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map1 noise1 expr_map1) ->
+    (* THE EXESTENTIAL CASE OF THE GOAL *)
     ((exists (v__FP : R) (m__FP : mType),
          eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
+     (* Invariant of the existential case:
+        our given expr_map1 is updated only with the expressions for which
+        the existential part holds *)
      (forall e' : FloverMap.key,
          ~ FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map2 ->
          NatSet.Subset (usedVars e') (NatSet.union fVars dVars) /\
          (exists iv__A' err__A', FloverMap.find e' A = Some (iv__A', err__A')) /\
          exists (v__FP' : R) (m__FP' : mType),
            eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP')) /\
+    (* UNIVERSAL CASE OF THE GOAL *)
     (forall (v__FP : R) (m__FP : mType),
         eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
+        (* For the given evaluation we can find a polynomial and an
+           error bound with a monotonic extension of noise_map1 to
+           noise_map2 *)
         exists (af : affine_form Q) (err__af : R) (noise_map2 : noise_mapping),
+          (* Invariant: the checker function only adds new polynomials
+             to the expr_map, never removes something from it *)
           contained_flover_map expr_map1 expr_map2 /\
+          (* Noise index invariants: the checker function returns new
+             noise that is not used in already produced polynomials *)
           (noise1 <= noise2)%nat /\
           fresh noise2 (afQ2R af) /\
+          (* Invariant: noise_map is incrementally updated *)
           contained_map noise_map1 noise_map2 /\
           (forall n0 : nat, (n0 >= noise2)%nat -> noise_map2 n0 = None) /\
           FloverMap.find (elt:=affine_form Q) e expr_map2 = Some af /\
+          (* To show that the error is bounded by the polynomial, we say that
+             the polynomial's range is bounded by err__af, which has a value
+             less or equal to the certificate error, and that the polynomial
+             captures any difference between real and finite-precision
+             evaluations *)
           (0 <= err__af)%R /\
           toInterval (afQ2R af) = ((- err__af)%R, err__af) /\
           (err__af <= Q2R err__A)%R /\
           af_evals (afQ2R af) (v__R - v__FP) noise_map2 /\
+          (* Invariant of the universal case:
+             our given expr_map1 is updated only with the expressions for which
+             the universal part (the conclusion directly above) holds *)
           (forall e' : FloverMap.key,
               ~ FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map2 ->
               checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map2 noise2 expr_map2)).