Update specification of light client algorithm to align with the code

spec/consensus/light-client.md

@@ -193,33 +193,43 @@ We consider the following set-up:
 we will write ```totalVotingPower(V)``` for ```votingpower_in(V,V)```, which returns the total voting power in V.
 We further use the function ```signers(Commit)``` that returns the set of validators that signed the Commit.
 
-**CheckSupport.** The following function checks whether we can trust the header h2 based on header h1 following the trusting period method.
+**CheckSupport.** The following function checks whether we can trust the header h2 based on header h1 following the trusting period method. Time constraint is
+captured by the `hasExpired` function that depends on trusted period (`tp`) and a parameter `Delta` that denotes minimum duration of header so it is
+not considered expired.
 
 ```go
-  func CheckSupport(h1,h2,trustlevel) bool {
-    if h1.Header.bfttime + tp < now { // Observation 1
-      return false // old header was once trusted but it is expired
-    }  
-    vp_all := totalVotingPower(h1.Header.NextV)
-      // total sum of voting power of validators in h2
-
-    if h2.Header.height == h1.Header.height + 1 {
-      // specific check for adjacent headers; everything must be
-      // properly signed.
-      // also check that h2.Header.V == h1.Header.NextV
-      // Plus the following check that 2/3 of the voting power
-      // in h1 signed h2
-      return (votingpower_in(signers(h2.Commit),h1.Header.NextV) >
-              2/3 * vp_all)
-        // signing validators are more than two third in h1.
-    }
+  // return true if header has expired, i.e., it is outside its trusted period; otherwise it returns false
+  func hasExpired(h) bool {
+    if h.Header.bfttime + tp - Delta < now { // Observation 1
+      return true
+  }
+
+  // return true if header is correctly signed by 2/3+ voting power in the corresponding validator set; otherwise false. Additional checks should be done in the implementation
+  // to ensure header is well formed.
+  func verify(h) bool {
+    vp_all := totalVotingPower(h.Header.V) // total sum of voting power of validators in h
+    return votingpower_in(signers(h.Commit),h.Header.V) > 2/3 * vp_all
+  }
 
-    return (votingpower_in(signers(h2.Commit),h1.Header.NextV) >
-            max(1/3,trustlevel) * vp_all)
-      // get validators in h1 that signed h2
-      // sum of voting powers in h1 of
-      // validators that signed h2
-      // is more than a third in h1
+  // Captures skipping condition. h1 and h2 has already passed basic validation (function `verify`).
+  // returns (true, nil) in case h2 can be trusted based on h1, (false, nil) in case it cannot be trusted but no errors are observed during check and (false, error) in case
+  // an error is detected (for example adjacent headers are not consistent).
+  func CheckSupport(h1,h2,trustlevel) (bool, error) {
+      assume h1.Header.Height < h2.header.Height
+
+      if hasExpired(h1) return (false, ErrHeaderExpired(h1))
+
+      // total sum of voting power of validators in h1.NextV
+      vp_all := totalVotingPower(h1.Header.NextV)
+
+      // check for adjacent headers
+      if (h2.Header.height == h1.Header.height + 1) {
+            if h1.Header.NextV == h2.Header.V return (true, nil)
+            else return (false, ErrInvalidAdjacentHeaders)
+      } else {
+      // check for non-adjacent headers
+            return (votingpower_in(signers(h2.Commit),h1.Header.NextV) > max(1/3,trustlevel) * vp_all, nil)
+      }
   }
 ```
 
@@ -257,28 +267,49 @@ Towards Lite Client Completeness:
 
 
 ```go
-func Bisection(h1,h2,trustlevel) bool{
-  if CheckSupport(h1,h2,trustlevel) {
-    return true
-  }
-  if h2.Header.height == h1.Header.height + 1 {
-    // we have adjacent headers that are not matching (failed
-    // the CheckSupport)
-    // we could submit evidence here
-    return false
-  }
-  pivot := (h1.Header.height + h2.Header.height) / 2
-  hp := Commit(pivot)
-    // ask a full node for header of height pivot
-  Store(hp)  
-    // store header hp locally
-  if Bisection(h1,hp,trustlevel) {
-    // only check right branch if hp is trusted
-    // (otherwise a lot of unnecessary computation may be done)
-    return Bisection(hp,h2,trustlevel)
-  }
-  else {
-    return false
+// return (true, nil) in case we can trust header h2 based on header h1; otherwise return (false, error) where error captures the nature of the error.
+func Bisection(h1,h2,trustlevel) (bool, error) {
+  assume h1.Header.Height < h2.header.Height
+
+  ok, err = CheckSupport(h1,h2,trustlevel)
+  if (ok or err != nil) return (ok, err)
+
+  // we cannot verify h2 based on h1, so we try to move trusted header closer to h2 so we can verify h2
+  th := h1 // th is trusted header
+  while th.Header.Height <= h2.Header.height - 1 do {
+       // try to move trusted header forward with stored headers
+       ih := th
+       for all stored headers h s.t ih.Header.Height < h.Header.height < h2.Header.height do {  // try to move trusted header forward
+            // we assume here that iteration is done in the order of header heights
+            ok, err = CheckSupport(th,h,trustlevel)
+            if err != nil { return (ok, err) }
+            if ok {
+                th = h
+            }
+        }
+
+        // at this point we have potentially updated th based on stored headers so we try to verify h2 based on new trusted header
+        ok, err = CheckSupport(th,h2,trustlevel)
+        if (ok or err != nil) return (ok, err)
+
+        // we cannot verify h2 based on th, so we try to move trusted header closer to h2 by downloading header(s) between th and h2
+        endHeight = h2.Header.height
+        foundPivot = false
+        while(!foundPivot) {
+            pivot := (th.Header.height + endHeight) / 2
+            hp := Commit(pivot)
+            if !verify(hp) return (false, ErrInvalidHeader(hp))
+            Store(hp)
+
+            // try to move trusted header forward to hp
+            ok, err = CheckSupport(th,hp,trustlevel)
+            if err != nil { return (ok, err) }
+            if ok {
+                th = hp
+                foundPivot = true
+            }
+            endHeight = pivot
+        }
   }
 }
 ```