Simple demo spec (#733)

* Adding simple demo spec * Minor change * Minor change * Add files
0LNetworkCommunity · Oct 8, 2021 · 0957e6d · 0957e6d
1 parent d3275fb
commit 0957e6d
Show file tree

Hide file tree

Showing 6 changed files with 44 additions and 38 deletions.
diff --git a/language/diem-framework/modules/0L/Demos.move b/language/diem-framework/modules/0L/Demos.move
@@ -11,7 +11,7 @@ address 0x1{
         use 0x1::Signer;
         use 0x1::Errors;
         use 0x1::Testnet::is_testnet;
-    
+
         // In Move the types for data storage are `resource struct`. Here a type 
         // State is being defined. Once a type is initialized in the global state, 
         // the resource is treated as if in-memory on the heap, the diem database 
@@ -24,7 +24,7 @@ address 0x1{
         }
 
         // The operation can only be performed on testnet
-         const ETESTNET : u64 = 04001;
+        const ETESTNET : u64 = 04001;
 
         // For this demo, the `initialize` function writes a PersistenceDemo::State 
         // resource at the "sender" address. The access path will be 
@@ -38,6 +38,14 @@ address 0x1{
           move_to<State>(sender, State{ hist: Vector::empty() });
         }
 
+        // A simple example/demo spec 
+        spec initialize {
+            let addr = Signer::address_of(sender);
+            // Note: Change this to non-zero value to get move prover error
+            let init_size = 0;
+            ensures Vector::length(global<State>(addr).hist) == init_size;
+        }
+
         // To read or write to a Resource Struct an `acquires` tag is needed to 
         // permission a function. NOTE all downsteam functions will also need 
         // permission on that data struct, i.e. need the same `acquires` parameters.

diff --git a/language/diem-framework/modules/doc/Demos.md b/language/diem-framework/modules/doc/Demos.md
@@ -91,6 +91,20 @@
 
 
 
+</details>
+
+<details>
+<summary>Specification</summary>
+
+
+
+<pre><code><b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(sender);
+<b>let</b> init_size = 0;
+<b>ensures</b> <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(<b>global</b>&lt;<a href="Demos.md#0x1_PersistenceDemo_State">State</a>&gt;(addr).hist) == init_size;
+</code></pre>
+
+
+
 </details>
 
 <a name="0x1_PersistenceDemo_add_stuff"></a>

diff --git a/language/diem-framework/modules/doc/Oracle.md b/language/diem-framework/modules/doc/Oracle.md
@@ -1044,24 +1044,8 @@
 <summary>Implementation</summary>
 
 
-<<<<<<< HEAD
-<pre><code><b>public</b> <b>fun</b> <a href="Oracle.md#0x1_Oracle_test_check_upgrade">test_check_upgrade</a>(): bool <b>acquires</b> <a href="Oracle.md#0x1_Oracle_Oracles">Oracles</a> {
-  <b>assert</b>(<a href="Testnet.md#0x1_Testnet_is_testnet">Testnet::is_testnet</a>(), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(150004));
-  <b>let</b> upgrade_oracle = &borrow_global&lt;<a href="Oracle.md#0x1_Oracle_Oracles">Oracles</a>&gt;(
-    <a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()
-  ).upgrade;
-  <b>let</b> payload = *&upgrade_oracle.consensus.data;
-
-  <b>if</b> (!<a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_is_empty">Vector::is_empty</a>(&payload)) {
-    <b>true</b>
-  }
-  <b>else</b> {
-    <b>false</b>
-  }
-=======
 <pre><code><b>public</b> <b>fun</b> <a href="Oracle.md#0x1_Oracle_upgrade_vote_type">upgrade_vote_type</a>(): u8 {
   <a href="Oracle.md#0x1_Oracle_VOTE_TYPE_UPGRADE">VOTE_TYPE_UPGRADE</a>
->>>>>>> my-fork/main
 }
 </code></pre>
 
@@ -1122,8 +1106,9 @@
 
 <pre><code><b>public</b> <b>fun</b> <a href="Oracle.md#0x1_Oracle_test_helper_check_upgrade">test_helper_check_upgrade</a>(): bool <b>acquires</b> <a href="Oracle.md#0x1_Oracle_Oracles">Oracles</a> {
   <b>assert</b>(<a href="Testnet.md#0x1_Testnet_is_testnet">Testnet::is_testnet</a>(), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(150004));
-  <b>let</b> upgrade_oracle = &<b>mut</b> borrow_global_mut&lt;<a href="Oracle.md#0x1_Oracle_Oracles">Oracles</a>&gt;(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()).upgrade;
-
+  <b>let</b> upgrade_oracle = &borrow_global&lt;<a href="Oracle.md#0x1_Oracle_Oracles">Oracles</a>&gt;(
+    <a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()
+  ).upgrade;
   <b>let</b> payload = *&upgrade_oracle.consensus.data;
 
   <b>if</b> (!<a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_is_empty">Vector::is_empty</a>(&payload)) {

diff --git a/language/diem-framework/releases/artifacts/current/docs/modules/Demos.md b/language/diem-framework/releases/artifacts/current/docs/modules/Demos.md
@@ -91,6 +91,20 @@
 
 
 
+</details>
+
+<details>
+<summary>Specification</summary>
+
+
+
+<pre><code><b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(sender);
+<b>let</b> init_size = 0;
+<b>ensures</b> <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(<b>global</b>&lt;<a href="Demos.md#0x1_PersistenceDemo_State">State</a>&gt;(addr).hist) == init_size;
+</code></pre>
+
+
+
 </details>
 
 <a name="0x1_PersistenceDemo_add_stuff"></a>

diff --git a/language/diem-framework/releases/artifacts/current/docs/modules/Oracle.md b/language/diem-framework/releases/artifacts/current/docs/modules/Oracle.md
@@ -1044,24 +1044,8 @@
 <summary>Implementation</summary>
 
 
-<<<<<<< HEAD
-<pre><code><b>public</b> <b>fun</b> <a href="Oracle.md#0x1_Oracle_test_check_upgrade">test_check_upgrade</a>(): bool <b>acquires</b> <a href="Oracle.md#0x1_Oracle_Oracles">Oracles</a> {
-  <b>assert</b>(<a href="Testnet.md#0x1_Testnet_is_testnet">Testnet::is_testnet</a>(), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(150004));
-  <b>let</b> upgrade_oracle = &borrow_global&lt;<a href="Oracle.md#0x1_Oracle_Oracles">Oracles</a>&gt;(
-    <a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()
-  ).upgrade;
-  <b>let</b> payload = *&upgrade_oracle.consensus.data;
-
-  <b>if</b> (!<a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_is_empty">Vector::is_empty</a>(&payload)) {
-    <b>true</b>
-  }
-  <b>else</b> {
-    <b>false</b>
-  }
-=======
 <pre><code><b>public</b> <b>fun</b> <a href="Oracle.md#0x1_Oracle_upgrade_vote_type">upgrade_vote_type</a>(): u8 {
   <a href="Oracle.md#0x1_Oracle_VOTE_TYPE_UPGRADE">VOTE_TYPE_UPGRADE</a>
->>>>>>> my-fork/main
 }
 </code></pre>
 
@@ -1122,8 +1106,9 @@
 
 <pre><code><b>public</b> <b>fun</b> <a href="Oracle.md#0x1_Oracle_test_helper_check_upgrade">test_helper_check_upgrade</a>(): bool <b>acquires</b> <a href="Oracle.md#0x1_Oracle_Oracles">Oracles</a> {
   <b>assert</b>(<a href="Testnet.md#0x1_Testnet_is_testnet">Testnet::is_testnet</a>(), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(150004));
-  <b>let</b> upgrade_oracle = &<b>mut</b> borrow_global_mut&lt;<a href="Oracle.md#0x1_Oracle_Oracles">Oracles</a>&gt;(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()).upgrade;
-
+  <b>let</b> upgrade_oracle = &borrow_global&lt;<a href="Oracle.md#0x1_Oracle_Oracles">Oracles</a>&gt;(
+    <a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()
+  ).upgrade;
   <b>let</b> payload = *&upgrade_oracle.consensus.data;
 
   <b>if</b> (!<a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_is_empty">Vector::is_empty</a>(&payload)) {

diff --git a/language/diem-framework/releases/artifacts/current/modules/067_Oracle.mv b/language/diem-framework/releases/artifacts/current/modules/067_Oracle.mv