[test] Update VP example

tests/positive/VP/SimpleFungibleToken.mjuvix

@@ -1,56 +1,12 @@
 module SimpleFungibleToken;
 
-axiom String : Type {
-  ghc ↦ "[Char]";
-};
-
-axiom Int : Type {
-  ghc ↦ "Int";
-};
-
-inductive OptionInt {
-  Nothing : OptionInt;
-  Just : Int -> OptionInt;
-};
-
-inductive OptionString {
-  NothingString : OptionString;
-  JustString : String -> OptionString;
-};
-
-foreign ghc { defaultinteger = 0;};
-
-axiom defaultinteger : Int {
-  ghc ↦ "defaultinteger";
-};
-
-fromOptionInt  : OptionInt -> Int;
-fromOptionInt  Nothing := defaultinteger;
-
-fromOptionInt  (Just n) := n;
-
 foreign ghc {
-foreign import ccall "read_pre" read_pre :: String -> Maybe Int
-foreign import ccall "read_post" read_post :: String -> Maybe Int
-foreign import ccall "is_balance_key"  is_balance_key :: String -> String -> Maybe String
+  import Anoma
 };
 
-axiom read-pre : String -> OptionInt {
-  ghc ↦ "read_pre";
-};
-
-axiom read-post : String -> OptionInt {
-  ghc ↦ "read_post";
-};
-
-axiom is-balance-key : String -> String -> OptionString {
-  ghc ↦ "is_balance_key";
-};
-
-inductive ListString {
-  Nil : ListString;
-  Cons : String -> ListString -> ListString;
-};
+--------------------------------------------------------------------------------
+-- Booleans
+--------------------------------------------------------------------------------
 
 inductive Bool {
   true : Bool;
@@ -60,38 +16,69 @@ inductive Bool {
 infixr 2 ||;
 || : Bool → Bool → Bool;
 || false a ≔ a;
-|| true _  ≔ true;
+|| true _ ≔ true;
 
-and : Bool → Bool → Bool;
-and false _ ≔ false;
-and true a  ≔ a;
+infixr 3 &&;
+&& : Bool → Bool → Bool;
+&& false _ ≔ false;
+&& true a ≔ a;
 
-infix 4 ==String;
-axiom ==String : String -> String -> Bool {
-  ghc ↦  "(==)";
+--------------------------------------------------------------------------------
+-- Backend Booleans
+--------------------------------------------------------------------------------
+
+axiom BackendBool : Type {
+  ghc ↦ "Bool";
+};
+
+axiom backend-true : BackendBool {
+  ghc ↦ "True";
+};
+
+axiom backend-false : BackendBool {
+  ghc ↦ "False";
+};
+
+--------------------------------------------------------------------------------
+-- Backend Bridge
+--------------------------------------------------------------------------------
+
+foreign ghc {
+  bool :: Bool -> a -> a -> a
+  bool True x _ = x
+  bool False _ y = y
+};
+
+axiom bool : BackendBool → Bool → Bool → Bool {
+  ghc ↦ "bool";
+};
+
+from-backend-bool : BackendBool → Bool;
+from-backend-bool bb ≔ bool bb true false;
+
+--------------------------------------------------------------------------------
+-- Integers
+--------------------------------------------------------------------------------
+
+axiom Int : Type {
+  ghc ↦ "Int";
+};
+
+axiom lt : Int → Int → BackendBool {
+  ghc ↦ "(<)";
+};
+
+infix 4 <;
+< : Int → Int → Bool;
+< i1 i2 ≔ from-backend-bool (lt i1 i2);
+
+axiom eqInt : Int → Int → BackendBool {
+  ghc ↦ "(==)";
 };
 
 infix 4 ==Int;
-axiom ==Int : Int -> Int -> Bool {
-  ghc ↦  "(==)";
-};
-
-elem : String -> ListString -> Bool;
-elem s Nil := false;
-elem s (Cons x xs) := (s ==String x) || elem s xs;
-
-inductive PairIntBool {
-  MakePair : Int -> Bool -> PairIntBool;
-};
-
-ifthenelse : Bool -> PairIntBool -> PairIntBool -> PairIntBool;
-ifthenelse true case1 _ := case1;
-ifthenelse false _ case2 := case2;
-
-infix 4 <;
-axiom < : Int -> Int -> Bool {
-  ghc ↦ "(<)";
-};
+==Int : Int → Int → Bool;
+==Int i1 i2 ≔ from-backend-bool (eqInt i1 i2);
 
 infixl 6 -;
 axiom - : Int -> Int -> Int {
@@ -103,46 +90,151 @@ axiom + : Int -> Int -> Int {
   ghc ↦ "(+)";
 };
 
-check-vp : ListString -> String -> String -> Int -> PairIntBool;
-check-vp verifiers key owner change :=
-  ifthenelse
-    (((fromOptionInt (read-post key)) - (fromOptionInt (read-pre key))) < 0)
-    (MakePair (change + ((fromOptionInt (read-post key)) - (fromOptionInt (read-pre key))))
-              (elem owner verifiers))
-    (MakePair
-       (change +
-        ((fromOptionInt (read-post key)) - (fromOptionInt (read-pre key))))
-         true);
+--------------------------------------------------------------------------------
+-- Strings
+--------------------------------------------------------------------------------
 
-check-vp' : ListString -> String -> Int -> String -> PairIntBool;
-check-vp' verifiers key change owner := check-vp verifiers key owner change;
-
-pairFromOptionString : (String -> PairIntBool) -> OptionString -> PairIntBool;
-pairFromOptionString _ NothingString := MakePair 0 false;
-pairFromOptionString f (JustString o) := f o;
-
-foreign ghc {
-  token = "secret";
-};
-axiom token : String {
-  ghc ↦ "token";
+axiom String : Type {
+  ghc ↦ "[Char]";
 };
 
-check-keys : ListString -> PairIntBool -> String -> PairIntBool;
-check-keys verifiers (MakePair change is-success) key :=
-  ifthenelse is-success
-    (pairFromOptionString (check-vp' verifiers key change) (is-balance-key token key))
-    (MakePair 0 false);
+axiom eqString : String → String → BackendBool {
+  ghc ↦ "(==)";
+};
 
-foldl :  (PairIntBool -> String -> PairIntBool) → PairIntBool → ListString → PairIntBool;
-foldl f z Nil ≔ z ;
+infix 4 ==String;
+==String : String → String → Bool;
+==String s1 s2 ≔ from-backend-bool (eqString s1 s2);
+
+--------------------------------------------------------------------------------
+-- Lists
+--------------------------------------------------------------------------------
+
+inductive ListString {
+  Nil : ListString;
+  Cons : String → ListString → ListString;
+};
+
+elem : String → ListString → Bool;
+elem s Nil ≔ false;
+elem s (Cons x xs) ≔ (s ==String x) || elem s xs;
+
+--------------------------------------------------------------------------------
+-- Pair
+--------------------------------------------------------------------------------
+
+inductive PairIntBool {
+  MakePair : Int → Bool → PairIntBool;
+};
+
+if-pairIntBool : Bool → PairIntBool → PairIntBool → PairIntBool;
+if-pairIntBool true x _ ≔ x;
+if-pairIntBool false _ y ≔ y;
+
+--------------------------------------------------------------------------------
+-- Optionals
+--------------------------------------------------------------------------------
+
+inductive OptionInt {
+  NothingInt : OptionInt;
+  JustInt : Int -> OptionInt;
+};
+
+if-optionInt : Bool → OptionInt → OptionInt → OptionInt;
+if-optionInt true x _ ≔ x;
+if-optionInt false _ y ≔ y;
+
+from-int : Int → OptionInt;
+from-int i ≔ if-optionInt (i < 0) NothingInt (JustInt i);
+
+maybe-int : Int → OptionInt → Int;
+maybe-int d NothingInt ≔ d;
+maybe-int _ (JustInt i) ≔ i;
+
+inductive OptionString {
+  NothingString : OptionString;
+  JustString : String -> OptionString;
+};
+
+if-optionString : Bool → OptionString → OptionString → OptionString;
+if-optionString true x _ ≔ x;
+if-optionString false _ y ≔ y;
+
+from-string : String → OptionString;
+from-string s ≔ if-optionString (s ==String "") NothingString (JustString s);
+
+pair-from-optionString : (String → PairIntBool) → OptionString → PairIntBool;
+pair-from-optionString _ NothingString ≔ MakePair 0 false;
+pair-from-optionString f (JustString o) ≔ f o;
+
+--------------------------------------------------------------------------------
+-- foldl
+--------------------------------------------------------------------------------
+
+foldl : (PairIntBool → String → PairIntBool) → PairIntBool → ListString → PairIntBool;
+foldl f z Nil ≔ z;
 foldl f z (Cons h hs) ≔ foldl f (f z h) hs;
 
-auxVP : PairIntBool -> Bool;
-auxVP (MakePair change all-checked) := and (change ==Int 0) all-checked;
+--------------------------------------------------------------------------------
+-- Anoma
+--------------------------------------------------------------------------------
 
-vp : String -> ListString -> ListString -> Bool;
-vp token keys-changed verifiers :=
-  auxVP (foldl (check-keys verifiers) (MakePair 0 false) keys-changed);
+axiom readPre : String → Int {
+  ghc ↦ "readPre";
+};
+
+axiom readPost : String → Int {
+  ghc ↦ "readPost";
+};
+
+axiom isBalanceKey : String → String → String {
+  ghc ↦ "isBalanceKey";
+};
+
+read-pre : String → OptionInt;
+read-pre s ≔ from-int (readPre s);
+
+read-post : String → OptionInt;
+read-post s ≔ from-int (readPost s);
+
+is-balance-key : String → String → OptionString;
+is-balance-key token key ≔ from-string (isBalanceKey token key);
+
+unwrap-default : OptionInt → Int;
+unwrap-default o ≔ maybe-int 0 o;
+
+--------------------------------------------------------------------------------
+-- Validity Predicate
+--------------------------------------------------------------------------------
+
+change-from-key : String → Int;
+change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pre key);
+
+check-vp : ListString → String → String → Int → PairIntBool;
+check-vp verifiers key owner change ≔
+    if-pairIntBool
+        (change-from-key key < 0)
+        (MakePair (change + (change-from-key key)) (elem owner verifiers))
+        (MakePair (change + (change-from-key key)) true);
+
+check-vp' : ListString → String → Int → String → PairIntBool;
+check-vp' verifiers key change owner ≔ check-vp verifiers key owner change;
+
+check-keys : String → ListString → PairIntBool → String → PairIntBool;
+check-keys token verifiers (MakePair change is-success) key ≔
+    if-pairIntBool
+        is-success
+        (pair-from-optionString (check-vp' verifiers key change) (is-balance-key token key))
+        (MakePair 0 false);
+
+check-result : PairIntBool → Bool;
+check-result (MakePair change all-checked) ≔ (change ==Int 0) && all-checked;
+
+vp : String → ListString → ListString → Bool;
+vp token keys-changed verifiers ≔
+    check-result
+        (foldl
+            (check-keys token verifiers)
+            (MakePair 0 false) keys-changed);
 
 end;