Revive the JS verification

Gillian-JS/Examples/Amazon/AmazonLogic.jsil

@@ -37,7 +37,6 @@ lemma ObjectTableAbsentProperty(l, PVPairs, prop)
     ((#l, #prop) -> none) *
     empty_fields(#l : -u- (#pSet, -{ #prop }-))
 ]]
-[*  *]
 
 (* Removing a property from a list of prop-value pairs *)
 pred RemoveProp(+PVPairs : List, +prop : Str, found : Bool, value : Str, newPairs : List) :

Gillian-JS/Examples/Amazon/ListLogic.gil

@@ -179,7 +179,7 @@ lemma ListToSetAddElement(lst, set, element)
     ListToSet(l+ (#lst, {{ #element }}), -u- (#set, -{ #element }-))
 ]]
 [*
-    unfold ListToSet(#lst, #element);
+    unfold ListToSet(#lst, #set);
     if (!(#lst == {{ }})) then {
         sep_assert ((#lst == l+ ({{ #fProp }}, #restLst))) [bind: #fProp, #restLst];
         sep_assert (ListToSet(#restLst, #restSet)) [bind: #restSet];

Gillian-JS/Examples/Amazon/deserialize_factory.js

@@ -128,7 +128,6 @@ function readElements(elementCount, fieldsPerElement, buffer, readPos) {
         [bind: #doneEl, #innerLoopReadPos, #fLeft, #remElList, #remElLength, #doneElList, #doneElLength] */
     while (fieldCount--) {
       /* @tactic
-          unfold innerLoopInvariantFacts(#definition, #remElsList, #view, #innerLoopReadPos, #fLeft, #remElList, #eLength, #remElsLength, #doneElLength, #remElLength);
           if (#definition = "Complete") then {
               unfold CElement(#view, #innerLoopReadPos, #fLeft, #remElList, #remElLength)
           } else {
@@ -809,19 +808,7 @@ function deserializeMessageHeader(messageBuffer) {
 
   var suiteId = dataView.getUint16(2, false)  // big endian
   /* Precondition: suiteId must match supported algorithm suite */
-  /*
-    @tactic
-        if (#definition = "Complete") then {
-            unfold CAlgorithmSuite(#suiteId, #stringId, #headerIvLength, #tagLength)
-        }
-  */
   needs(AlgorithmSuiteIdentifier[suiteId], 'Malformed Header: Unsupported algorithm suite.')
-  /*
-    @tactic
-        if (#definition = "Complete") then {
-            fold CAlgorithmSuite(#suiteId, #stringId, #headerIvLength, #tagLength)
-        }
-  */
   var messageId = messageBuffer.slice(4, 20)
   var contextLength = dataView.getUint16(20, false) // big endian
 

Gillian-JS/runtime/JSLogic/ArrayBuffer.jsil

@@ -15,7 +15,7 @@ nounfold pred ArrayBuffer (+ab:Obj, data:List) :
   ((#md, "@extensible")            -> true) *          (* Array buffers are extensible                   *)
   ((#md, "@ArrayBufferData")       -> data) *          (* Array buffer contents                          *)
   ((#md, "@ArrayBufferByteLength") -> #len_data) *     (* Array buffer length                            *)
-  (#len_data == l-len data) *
+  ((as_int #len_data) == l-len data) *
 
   (* No other internal properties *)
   empty_fields (#md : -{ "@class", "@extensible", "@proto", "@ArrayBufferData", "@ArrayBufferByteLength" }-);
@@ -44,7 +44,7 @@ nounfold pred ArrayBufferPrototype (proto) :
 
 axiomatic spec ABP_byteLength (xsc, vthis)
     [[ (vthis == #vthis) * ArrayBuffer(#vthis, #data) ]]
-    [[ ArrayBuffer(#vthis, #data) * (ret == l-len #data) ]]
+    [[ ArrayBuffer(#vthis, #data) * (ret == (l-len #data)) ]]
     normal
 
 axiomatic spec ABP_slice (xsc, vthis, start, end)

Gillian-JS/runtime/JSLogic/ByteLogic.gil

@@ -7,47 +7,53 @@
  ****************************************)
 
 (* Interpretation: one byte as an unsigned 8-bit integer *)
-pure pred rawToUInt8(+bytes:List, x:Int) :
+pure pred rawToUInt8(+bytes:List, x:Num) :
     (bytes == {{ #b0 }}) * (x == #b0) *
-    (0i i<=# #b0) * (#b0 i<# 256i);
-
-pure pred rawToUInt8JS(+bytes:List, n:Num) :
-    rawToUInt8(bytes, #x) * (n == (as_num #x));
+    (0 <=# #b0) * (#b0 <# 256.) *
+    (is_int #b0);
 
 (* Interpretation: two bytes as an unsigned 16-bit integer *)
 @nopath
-pure pred rawToUInt16(+bytes:List, +littleEndian:Bool, x:Int) :
+pure pred rawToUInt16(+bytes:List, +littleEndian:Bool, x:Num) :
     (littleEndian == false) *
       (bytes == {{ #b0, #b1 }}) *
-      (0i i<=# #b0) * (#b0 i<# 256i) *
-      (0i i<=# #b1) * (#b1 i<# 256i) *
-      (x == (#b0 i* 256i) i+ #b1),
+      (0. <=# #b0) * (#b0 <# 256.) *
+      (0. <=# #b1) * (#b1 <# 256.) *
+      (x == (#b0 * 256.) + #b1) *
+      (is_int #b0) *
+      (is_int #b1),
     (littleEndian == true) *
       (bytes == {{ #b0, #b1 }}) *
-      (0i i<=# #b0) * (#b0 i<# 256i) *
-      (0i i<=# #b1) * (#b1 i<# 256i) *
-      (x == (#b1 i* 256i) i+ #b0);
-
-pure pred rawToUInt16JS(+bytes:List, +littleEndian:Bool, n:Num) :
-    rawToUInt16(bytes, littleEndian, #x) * (n == (as_num #x));
+      (0. <=# #b0) * (#b0 <# 256.) *
+      (0. <=# #b1) * (#b1 <# 256.) *
+      (x == (#b1 * 256.) + #b0) *
+      (is_int #b0) *
+      (is_int #b1);
+  facts: (is_int x);
 
 (* Interpretation: four bytes as an unsigned 32-bit integer *)
 @nopath
-pure pred rawToUInt32(+bytes:List, +littleEndian:Bool, x:Int) :
+pure pred rawToUInt32(+bytes:List, +littleEndian:Bool, x:Num) :
     (littleEndian == false) *
       (bytes == {{ #b0, #b1, #b2, #b3 }}) *
-      (0i i<=# #b0) * (#b0 i<# 256i) *
-      (0i i<=# #b1) * (#b1 i<# 256i) *
-      (0i i<=# #b2) * (#b2 i<# 256i) *
-      (0i i<=# #b3) * (#b3 i<# 256i) *
-      (x == (#b0 i* 16777216i) i+ (#b1 i* 65536i) i+ (#b2 i* 256i) i+ #b3),
+      (0. <=# #b0) * (#b0 <# 256.) *
+      (0. <=# #b1) * (#b1 <# 256.) *
+      (0. <=# #b2) * (#b2 <# 256.) *
+      (0. <=# #b3) * (#b3 <# 256.) *
+      (x == (#b0 * 16777216.) + (#b1 * 65536.) + (#b2 * 256.) + #b3) *
+      (is_int #b0) *
+      (is_int #b1) *
+      (is_int #b2) *
+      (is_int #b3),
     (littleEndian == true) *
       (bytes == {{ #b0, #b1, #b2, #b3 }}) *
-      (0i i<=# #b0) * (#b0 i<# 256i) *
-      (0i i<=# #b1) * (#b1 i<# 256i) *
-      (0i i<=# #b2) * (#b2 i<# 256i) *
-      (0i i<=# #b3) * (#b3 i<# 256i) *
-      (x == (#b3 i* 16777216i) i+ (#b2 i* 65536i) i+ (#b1 i* 256i) i+ #b0);
-
-pure pred rawToUInt32JS(+bytes:List, +littleEndian:Bool, n:Num) :
-    rawToUInt32(bytes, littleEndian, #x) * (n == (as_num #x));
+      (0. <=# #b0) * (#b0 <# 256.) *
+      (0. <=# #b1) * (#b1 <# 256.) *
+      (0. <=# #b2) * (#b2 <# 256.) *
+      (0. <=# #b3) * (#b3 <# 256.) *
+      (x == (#b3 * 16777216.) + (#b2 * 65536.) + (#b1 * 256.) + #b0) *
+      (is_int #b0) *
+      (is_int #b1) *
+      (is_int #b2) *
+      (is_int #b3);
+    facts: (is_int x);

Gillian-JS/runtime/JSLogic/DataView.jsil

@@ -116,47 +116,47 @@ axiomatic spec DVP_byteOffset (xsc, vthis)
 axiomatic spec DVP_getUint8 (xsc, vthis, byteOffset)
     [[ (vthis == #vthis) * (byteOffset == #byteOffset) *
        DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
-       (0 <=# byteOffset) * (#elementSize == 1) * (#byteOffset + #elementSize <=# #viewSize) *
+       (0 <=# byteOffset) * (#elementSize == 1.) * (#byteOffset + #elementSize <=# #viewSize) *
        (#view == l-sub(#data, #viewOffset, #viewSize)) ]]
     [[ DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
        (#raw == l-sub (#view, #byteOffset, #elementSize)) *
-       rawToUInt8JS(#raw, ret) ]]
+       rawToUInt8(#raw, ret) ]]
     normal
 
 axiomatic spec DVP_getUint16 (xsc, vthis, byteOffset, littleEndian)
     [[ (vthis == #vthis) * (byteOffset == #byteOffset) * (littleEndian == undefined) *
        DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
-       (0 <=# byteOffset) * (#elementSize == 2) * (#byteOffset + #elementSize <=# #viewSize) *
+       (0 <=# byteOffset) * (#elementSize == 2.) * (#byteOffset + #elementSize <=# #viewSize) *
        (#view == l-sub(#data, #viewOffset, #viewSize)) ]]
     [[ DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
        (#raw == l-sub (#view, #byteOffset, #elementSize)) *
-       rawToUInt16JS(#raw, false, ret) ]]
+       rawToUInt16(#raw, false, ret) ]]
     normal;
 
     [[ (vthis == #vthis) * (byteOffset == #byteOffset) * (littleEndian == #littleEndian) *
        DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
-       (0 <=# byteOffset) * (#elementSize == 2) * (#byteOffset + #elementSize <=# #viewSize) *
+       (0 <=# byteOffset) * (#elementSize == 2.) * (#byteOffset + #elementSize <=# #viewSize) *
        (#view == l-sub(#data, #viewOffset, #viewSize)) ]]
     [[ DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
-       (#raw== l-sub (#view, #byteOffset, #elementSize)) *
-       rawToUInt16JS(#raw, #littleEndian, ret) ]]
+       (#raw == l-sub (#view, #byteOffset, #elementSize)) *
+       rawToUInt16(#raw, #littleEndian, ret) ]]
     normal
 
 axiomatic spec DVP_getUint32 (xsc, vthis, byteOffset, littleEndian)
     [[ (vthis == #vthis) * (byteOffset == #byteOffset) * (littleEndian == undefined) *
        DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
-       (0 <=# byteOffset) * (#elementSize == 4) * (#byteOffset + #elementSize <=# #viewSize) *
+       (0 <=# byteOffset) * (#elementSize == 4.) * (#byteOffset + #elementSize <=# #viewSize) *
        (#view == l-sub(#data, #viewOffset, #viewSize)) ]]
     [[ DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
        (#raw == l-sub (#view, #byteOffset, #elementSize)) *
-       rawToUInt32JS(#raw, false, ret) ]]
+       rawToUInt32(#raw, false, ret) ]]
     normal;
 
     [[ (vthis == #vthis) * (byteOffset == #byteOffset) * (littleEndian == #littleEndian) *
        DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
-       (0 <=# byteOffset) * (#elementSize == 4) * (#byteOffset + #elementSize <=# #viewSize) *
+       (0 <=# byteOffset) * (#elementSize == 4.) * (#byteOffset + #elementSize <=# #viewSize) *
        (#view == l-sub(#data, #viewOffset, #viewSize)) ]]
     [[ DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
        (#raw == l-sub (#view, #byteOffset, #elementSize)) *
-       rawToUInt32JS(#raw, #littleEndian, ret) ]]
+       rawToUInt32(#raw, #littleEndian, ret) ]]
     normal

GillianCore/engine/Abstraction/PState.ml

@@ -587,22 +587,24 @@ module Make (State : SState.S) :
     (* This will not do anything in the original pass,
        but will do precisely what is needed in the re-establishment *)
     let vars_to_forget = SS.inter state_lvars (SS.of_list lvar_binders) in
-    if vars_to_forget <> SS.empty then (
-      let oblivion_subst = fresh_subst vars_to_forget in
-      L.verbose (fun m ->
-          m "Forget @[%a@] with subst: %a"
-            Fmt.(iter ~sep:comma SS.iter string)
-            vars_to_forget SVal.SESubst.pp oblivion_subst);
-
-      (* TODO: THIS SUBST IN PLACE MUST NOT BRANCH *)
-      let subst_in_place =
-        substitution_in_place ~subst_all:true oblivion_subst astate
-      in
-      assert (List.length subst_in_place = 1);
-      let astate = List.hd subst_in_place in
+    let astate =
+      if vars_to_forget <> SS.empty then (
+        let oblivion_subst = fresh_subst vars_to_forget in
+        L.verbose (fun m ->
+            m "Forget @[%a@] with subst: %a"
+              Fmt.(iter ~sep:comma SS.iter string)
+              vars_to_forget SVal.SESubst.pp oblivion_subst);
+
+        (* TODO: THIS SUBST IN PLACE MUST NOT BRANCH *)
+        let subst_in_place =
+          substitution_in_place ~subst_all:true oblivion_subst astate
+        in
+        assert (List.length subst_in_place = 1);
+        let astate = List.hd subst_in_place in
 
-      L.verbose (fun m -> m "State after substitution:@\n@[%a@]\n" pp astate))
-    else ();
+        L.verbose (fun m -> m "State after substitution:@\n@[%a@]\n" pp astate);
+        astate)
+      else astate in
     let mp =
       match mp with
       | Error asrts ->
@@ -628,6 +630,7 @@ module Make (State : SState.S) :
     let open Res_list.Syntax in
     let open Syntaxes.List in
     let** new_state, subst', _ =
+      L.verbose (fun m -> m "State before matching:@\n@[%a@]\n" pp astate);
       let+ result = SMatcher.match_ astate subst mp Invariant in
       match result with
       | Ok state -> Ok state

GillianCore/engine/Abstraction/Verifier.ml

@@ -623,7 +623,7 @@ struct
     match test.flag with
     | Some _ ->
         let msg = "Verifying one spec of procedure " ^ test.name ^ "... " in
-        L.tmi (fun fmt -> fmt "%s" msg);
+        L.normal (fun fmt -> fmt "%s" msg);
         Fmt.pr "%s@?" msg;
         (* Reset coverage for every procedure in verification *)
         { prog with coverage = Hashtbl.create 1 }
@@ -656,7 +656,7 @@ struct
             else Ok () (* It's already correct *)
         | Some proof -> (
             let msg = "Verifying lemma " ^ test.name ^ "... " in
-            L.tmi (fun fmt -> fmt "%s" msg);
+            L.normal (fun fmt -> fmt "%s" msg);
             Fmt.pr "%s@?" msg;
             let lemma_evaluation_results =
               SAInterpreter.evaluate_lcmds prog proof state