From 215dd8cd7a72ae52cefcdcd2e1b72ad9f31799ac Mon Sep 17 00:00:00 2001 From: Nat Karmios Date: Sun, 12 Mar 2023 19:49:23 +0000 Subject: [PATCH] WIP --- Gillian-JS/Examples/Amazon/EncryptionHeaderLogic.gil | 3 ++- Gillian-JS/Examples/Amazon/deserialize_factory.js | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/Gillian-JS/Examples/Amazon/EncryptionHeaderLogic.gil b/Gillian-JS/Examples/Amazon/EncryptionHeaderLogic.gil index e57db7270..ecf415c40 100644 --- 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 index 489b478f1..f079bf5b6 100644 --- 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)] } */