From f1f1e42bc0222ac9c396d740b968f1aaaae88fb0 Mon Sep 17 00:00:00 2001
From: Tobias Eidelpes <tobias@eidelpes.info>
Date: Thu, 3 Jun 2021 10:35:09 +0200
Subject: [PATCH] Add Termination

---
 Project2.fst | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/Project2.fst b/Project2.fst
index a4a2ed0..64d315b 100644
--- a/Project2.fst
+++ b/Project2.fst
@@ -174,9 +174,23 @@ let rec nsteps n te cs =
 (* Our goal is to prove the termination of this function *)
 (* To this end, define a function the following function on callstacks that assigns a measure (in terms of a list of naturals that gets lexicographically interpreted) to each call stack *)
 
+val gas: plaincallstack -> Tot nat
+let gas cs =
+    match cs with
+        | (((gas, _, _, _), _, _)::_) -> gas
+        | _ -> 0
+
 val getDecArgList: (cs: callstack {wellformed cs}) -> Tot (list nat)
 let getDecArgList (cs: callstack {wellformed cs}) =
-  magic ()
+  [ (match cs with
+        | Exec ps -> gas ps
+        | Ter (HaltState _ _ g) _ -> g
+        | Ter ExcState _ -> 0)
+  ; size cs
+  ; match cs with
+    | Exec _ -> 1
+    | Ter _ _ -> 0
+  ]
 
 (* A simple helper function that converts a list to a lexicgraphical ordering *)
 val getLexFromList: (list nat) -> Tot (lex_t)