WIP

GillianPlatform · Mar 12, 2023 · 215dd8c · 215dd8c
1 parent 0a6fa28
commit 215dd8c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/Gillian-JS/Examples/Amazon/EncryptionHeaderLogic.gil b/Gillian-JS/Examples/Amazon/EncryptionHeaderLogic.gil
@@ -450,8 +450,9 @@ nounfold pred ElementsJS(definition : Str, +buffer : List, +readPos : Num,
                          +eCount : Num, +fCount : Num, eList : List,
                          esLength : Num) :
   Elements(definition, buffer, (as_int readPos), (as_int eCount), (as_int fCount), eList, #esLength) *
-    (is-int readPos) * (is-int eCount) * (is-int fCount) *
     (esLength == (as_num #esLength));
+  facts: (0 <# readPos) and (readPos <# as_int(l-len buffer)) and (0 <# eCount) and (0 <# fCount) and (0 <=# esLength)
+      and (is-int readPos) and (is-int eCount) and (is-int fCount);
 
 lemma ElementsShift(buffer, readPos, eCount, fCount, shift)
   [[  Elements(#definition, #buffer, #readPos, #eCount, #fCount, #eList, #esLength) *

diff --git a/Gillian-JS/Examples/Amazon/deserialize_factory.js b/Gillian-JS/Examples/Amazon/deserialize_factory.js
@@ -105,8 +105,9 @@ function readElements(elementCount, fieldsPerElement, buffer, readPos) {
   while (elementCount--) {
     /* @tactic
         unfold ElementsJS(#definition, #view, #outerLoopReadPos, #eLeft, #fCount, #remElsList, #remElsLength);
+        unfold Elements(#definition, #view, (as_int #outerLoopReadPos), (as_int #eLeft), (as_int #fCount), #remElsList, (as_int #remElsLength));
         if (#definition = "Complete") then {
-            unfold CElementsJS(#view, #outerLoopReadPos, #eLeft, #fCount, #remElsList, #remElsLength) [bind: (#element := #fList) and (#eLength := #eLength)]
+            unfold CElements(#view, (as_int #outerLoopReadPos), #eLeft, (as_int #fCount), #remElsList, #remElsLength) [bind: (#element := #fList) and (#eLength := #eLength)]
         } else {
             unfold IElementsJS(#view, #outerLoopReadPos, #eLeft, #fCount, #remElsList, #remElsLength) [bind: (#fList := #fList) and (#eLength := #eLength)]
         } */