From 0957e6de956ec30899588f82b4efb2e9202e7057 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?G=C3=B6khan=20=C5=9Eim=C5=9Fek?= Date: Sat, 9 Oct 2021 02:23:24 +0300 Subject: [PATCH] Simple demo spec (#733) * Adding simple demo spec * Minor change * Minor change * Add files --- language/diem-framework/modules/0L/Demos.move | 12 ++++++++-- language/diem-framework/modules/doc/Demos.md | 14 ++++++++++++ language/diem-framework/modules/doc/Oracle.md | 21 +++--------------- .../artifacts/current/docs/modules/Demos.md | 14 ++++++++++++ .../artifacts/current/docs/modules/Oracle.md | 21 +++--------------- .../artifacts/current/modules/067_Oracle.mv | Bin 3958 -> 3965 bytes 6 files changed, 44 insertions(+), 38 deletions(-) diff --git a/language/diem-framework/modules/0L/Demos.move b/language/diem-framework/modules/0L/Demos.move index 6b5c9954c4..24a5ace07b 100644 --- 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(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(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 index d2faf04a0b..529e2c1d77 100644 --- a/language/diem-framework/modules/doc/Demos.md +++ b/language/diem-framework/modules/doc/Demos.md @@ -91,6 +91,20 @@ + + +
+Specification + + + +
let addr = Signer::address_of(sender);
+let init_size = 0;
+ensures Vector::length(global<State>(addr).hist) == init_size;
+
+ + +
diff --git a/language/diem-framework/modules/doc/Oracle.md b/language/diem-framework/modules/doc/Oracle.md index 859e3e3cee..bd39bdf140 100644 --- a/language/diem-framework/modules/doc/Oracle.md +++ b/language/diem-framework/modules/doc/Oracle.md @@ -1044,24 +1044,8 @@ Implementation -<<<<<<< HEAD -
public fun test_check_upgrade(): bool acquires Oracles {
-  assert(Testnet::is_testnet(), Errors::invalid_state(150004));
-  let upgrade_oracle = &borrow_global<Oracles>(
-    CoreAddresses::DIEM_ROOT_ADDRESS()
-  ).upgrade;
-  let payload = *&upgrade_oracle.consensus.data;
-
-  if (!Vector::is_empty(&payload)) {
-    true
-  }
-  else {
-    false
-  }
-=======
 
public fun upgrade_vote_type(): u8 {
   VOTE_TYPE_UPGRADE
->>>>>>> my-fork/main
 }
 

 
@@ -1122,8 +1106,9 @@
 
 
public fun test_helper_check_upgrade(): bool acquires Oracles {
   assert(Testnet::is_testnet(), Errors::invalid_state(150004));
-  let upgrade_oracle = &mut borrow_global_mut<Oracles>(CoreAddresses::DIEM_ROOT_ADDRESS()).upgrade;
-
+  let upgrade_oracle = &borrow_global<Oracles>(
+    CoreAddresses::DIEM_ROOT_ADDRESS()
+  ).upgrade;
   let payload = *&upgrade_oracle.consensus.data;
 
   if (!Vector::is_empty(&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
index d2faf04a0b..529e2c1d77 100644
--- 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 @@
 
 
 
+
+
+

+Specification
+
+
+
+
let addr = Signer::address_of(sender);
+let init_size = 0;
+ensures Vector::length(global<State>(addr).hist) == init_size;
+

+
+
+
 

 
 
diff --git a/language/diem-framework/releases/artifacts/current/docs/modules/Oracle.md b/language/diem-framework/releases/artifacts/current/docs/modules/Oracle.md
index 859e3e3cee..bd39bdf140 100644
--- 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 @@
 Implementation
 
 
-<<<<<<< HEAD
-
public fun test_check_upgrade(): bool acquires Oracles {
-  assert(Testnet::is_testnet(), Errors::invalid_state(150004));
-  let upgrade_oracle = &borrow_global<Oracles>(
-    CoreAddresses::DIEM_ROOT_ADDRESS()
-  ).upgrade;
-  let payload = *&upgrade_oracle.consensus.data;
-
-  if (!Vector::is_empty(&payload)) {
-    true
-  }
-  else {
-    false
-  }
-=======
 
public fun upgrade_vote_type(): u8 {
   VOTE_TYPE_UPGRADE
->>>>>>> my-fork/main
 }
 

 
@@ -1122,8 +1106,9 @@
 
 
public fun test_helper_check_upgrade(): bool acquires Oracles {
   assert(Testnet::is_testnet(), Errors::invalid_state(150004));
-  let upgrade_oracle = &mut borrow_global_mut<Oracles>(CoreAddresses::DIEM_ROOT_ADDRESS()).upgrade;
-
+  let upgrade_oracle = &borrow_global<Oracles>(
+    CoreAddresses::DIEM_ROOT_ADDRESS()
+  ).upgrade;
   let payload = *&upgrade_oracle.consensus.data;
 
   if (!Vector::is_empty(&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
index 7d49387da0f2818483458025cafac55eaa13035f..9b04d8a6bf54f2c4efbb968019217c54c1b00908 100644
GIT binary patch
delta 50
zcmew+_g8L$yy#pGjt#s5YzKIqxtjSLd5-Ws;pbhk(Ikw8N3tZfxFkL!HK!o8XmdZy
Gb1nd-2oWFv

delta 43
zcmew>_f2ksyy!Fzj+MLuY&&_Kx&H7v^6ce%!q2;Kqe&PGt58X5amnUsEYG