Document function specs some more

2 files changed, 57 insertions, 59 deletions

diff --git a/src/cobs.c b/src/cobs.c
index d3889c3..19dcad2 100644
--- a/src/cobs.c
+++ b/src/cobs.c
@@ -73,7 +73,6 @@ ssize_t cobs_encode(char *dst, size_t dstlen, char *src, size_t srclen) {
 }
 
 /*@ requires \valid_read(src + (0..srclen-1));
-  @ requires srclen < 1000000-2;
   @*/
 #ifndef VERIFICATION
 int cobs_encode_incremental(void *f, int (*output)(void *f, unsigned char c), unsigned char *src, size_t srclen) {
diff --git a/src/noise.c b/src/noise.c
index 949a68d..1d545f4 100644
--- a/src/noise.c
+++ b/src/noise.c
@@ -51,12 +51,13 @@ volatile int host_packet_length = 0;
 
 
 /*@
-    requires \valid(st);
+    requires validity: \valid(st);
+
+    ensures equal: st->remote_key_reference == remote_key_reference && st->local_key == local_key;
+    ensures equal: st->handshake_state == HANDSHAKE_UNINITIALIZED;
+    ensures equal: st->failed_handshakes == 0;
+    ensures equal: st->tx_cipher == NULL && st->rx_cipher == NULL && st->handshake == NULL;
 
-    ensures st->remote_key_reference == remote_key_reference && st->local_key == local_key;
-    ensures st->handshake_state == HANDSHAKE_UNINITIALIZED;
-    ensures st->failed_handshakes == 0;
-    ensures st->tx_cipher == NULL && st->rx_cipher == NULL && st->handshake == NULL;
     assigns *st;
  */
 void noise_state_init(struct NoiseState *st, uint8_t *remote_key_reference, uint8_t *local_key) {
@@ -71,21 +72,18 @@ void noise_state_init(struct NoiseState *st, uint8_t *remote_key_reference, uint
 }
 
 /*@
-    requires \valid(st);
-    requires \valid(st->handshake_hash + (0..31));
-    requires \separated(st, st->rx_cipher, st->tx_cipher, st->handshake);
+    requires validity: \valid(st) && \valid(st->handshake_hash + (0..31)) && \valid_read(st->local_key + (0..31));
+    requires separation: \separated(st, st->rx_cipher, st->tx_cipher, st->handshake);
 
-    ensures \result == 0 ==> (
+    ensures result: \result \in {0, -1};
+    ensures success: \result == 0 ==> (
         \valid(st->handshake) &&
         (st->handshake_state == HANDSHAKE_IN_PROGRESS));
-
-    ensures \result != 0 ==> (
+    ensures failure: \result != 0 ==> (
         (st->handshake == NULL) &&
         (st->handshake_state == HANDSHAKE_UNINITIALIZED));
 
-    ensures \result \in {0, -1};
-
-    assigns st->handshake, st->handshake_state, st->rx_cipher, st->tx_cipher;
+    assigns *st, *st->rx_cipher, *st->tx_cipher;
  */
 int reset_protocol_handshake(struct NoiseState *st) {
     uninit_handshake(st, HANDSHAKE_UNINITIALIZED);
@@ -95,21 +93,19 @@ int reset_protocol_handshake(struct NoiseState *st) {
     st->tx_cipher = NULL;
     st->rx_cipher = NULL;
     st->handshake = NULL;
-    memset(st->handshake_hash, 0, sizeof(st->handshake_hash));
+    fc_memset_uint8(st->handshake_hash, 0, sizeof(st->handshake_hash));
     return start_protocol_handshake(st);
 }
 
-/*@ requires \valid(st) && \valid_read(st->local_key + (0..31));
+/*@ requires validity: \valid(st) && \valid_read(st->local_key + (0..31));
   
-    ensures \result == 0 ==> (
+    ensures result: \result \in {0, -1};
+    ensures success: \result == 0 ==> (
         \valid(st->handshake) &&
-        (st->handshake_state == HANDSHAKE_IN_PROGRESS));
-
-    ensures \result != 0 ==> (
-        (st->handshake == \old(st->handshake)) &&
-        (st->handshake_state == \old(st->handshake_state)));
-
-    ensures \result \in {0, -1};
+        st->handshake_state == HANDSHAKE_IN_PROGRESS);
+    ensures failure: \result != 0 ==> (
+        st->handshake == \old(st->handshake) &&
+        st->handshake_state == \old(st->handshake_state));
 
     assigns st->handshake, st->handshake_state;
  */
@@ -143,9 +139,9 @@ errout:
     return -1;
 }
 
-/*@ requires \valid(st);
-    requires \valid(st->local_key + (0..31));
-    requires \separated(st, st->local_key + (0..31));
+/*@ requires validity: \valid(st) && \valid(st->local_key + (0..31));
+    requires separation: \separated(st, st->local_key + (0..31));
+
     assigns st->local_key[0..31];
  */
 int generate_identity_key(struct NoiseState *st) {
@@ -168,14 +164,13 @@ errout:
     return -1;
 }
 
-/*@requires \valid(st);
-   requires new_state == HANDSHAKE_UNINITIALIZED ||
-            new_state == HANDSHAKE_NOT_STARTED ||
-            new_state == HANDSHAKE_IN_PROGRESS ||
-            new_state == HANDSHAKE_DONE_UNKNOWN_HOST ||
-            new_state == HANDSHAKE_DONE_KNOWN_HOST;
-   ensures st->handshake_state == new_state;
-   ensures st->handshake == NULL;
+/*@requires validity: \valid(st);
+   requires state_valid: new_state \in
+           {HANDSHAKE_UNINITIALIZED, HANDSHAKE_NOT_STARTED, HANDSHAKE_IN_PROGRESS,
+           HANDSHAKE_DONE_UNKNOWN_HOST, HANDSHAKE_DONE_KNOWN_HOST};
+
+   ensures state: st->handshake_state == new_state;
+   ensures handshake: st->handshake == NULL;
 
    assigns st->handshake, st->handshake_state;
  @*/
@@ -190,18 +185,25 @@ void uninit_handshake(struct NoiseState *st, enum handshake_state new_state) {
 //@ ghost int key_checked_trace;
 //@ ghost int key_match_trace;
 /*@ 
-    requires \valid(st);
-    requires \valid(usart2_out);
-    requires \valid(st->handshake);
+    requires validity: \valid(st) && \valid(usart2_out) && \valid(st->handshake);
+
+    requires validity: \valid(st->remote_key + (0..sizeof(st->remote_key)-1));
+    requires validity: \valid(st->handshake_hash + (0..sizeof(st->handshake_hash)-1));
+
+    requires separation: \separated(&usart2_out, st, buf, st->handshake, &st->handshake_hash);
 
-    requires \valid(st->remote_key + (0..sizeof(st->remote_key)-1));
-    requires \valid(st->handshake_hash + (0..sizeof(st->handshake_hash)-1));
+    ensures result: \result \in {0, -1};
 
-    requires \separated(&usart2_out, st, buf, st->handshake, &st->handshake_hash);
+    ensures state_legal: st->handshake_state \in
+            {HANDSHAKE_UNINITIALIZED, HANDSHAKE_IN_PROGRESS, HANDSHAKE_DONE_KNOWN_HOST, HANDSHAKE_DONE_UNKNOWN_HOST};
+    ensures transition_legal_advance: (\old(st->handshake_state) != HANDSHAKE_IN_PROGRESS)
+            ==> st->handshake_state == HANDSHAKE_UNINITIALIZED;
+    ensures transition_legal_failure: st->handshake_state == HANDSHAKE_UNINITIALIZED <==> \result == -1;
 
-    ensures (st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST) ==> key_checked_trace == 1;
-    ensures (st->handshake_state != HANDSHAKE_IN_PROGRESS) ==>
+    ensures permission_valid: (st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST) ==> key_checked_trace == 1;
+    ensures state_advance_condition: (st->handshake_state != HANDSHAKE_IN_PROGRESS) ==>
         key_match_trace == 1 || (st->failed_handshakes > \old(st->failed_handshakes));
+
   @*/
 int try_continue_noise_handshake(struct NoiseState * const st, uint8_t *buf, size_t len) {
     //@ ghost key_checked_trace = 0;
@@ -303,11 +305,11 @@ errout:
 }
 
 /*@
-    requires \valid(st);
-    requires \valid_read(st->remote_key + (0..sizeof(st->remote_key)-1));
-    requires \valid(st->remote_key_reference + (0..31));
+    requires validity: \valid(st);
+    requires validity: \valid_read(st->remote_key + (0..sizeof(st->remote_key)-1));
+    requires validity: \valid(st->remote_key_reference + (0..31));
 
-    ensures st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST;
+    ensures state: st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST;
     assigns st->remote_key_reference[0..31], st->handshake_state;
  */
 void persist_remote_key(struct NoiseState *st) {
@@ -319,14 +321,11 @@ void persist_remote_key(struct NoiseState *st) {
 }
 
 /*@
-  requires \valid(st);
-  requires \valid(usart2_out);
-  requires \valid(st->tx_cipher);
-  requires \valid_read(msg + (0..len-1));
-  requires 0 <= len <= 65536;
+  requires validity: \valid(st) && \valid(usart2_out) && \valid(st->tx_cipher) && \valid_read(msg + (0..len-1));
 
+  ensures length: !(0 <= len <= MAX_HOST_PACKET_SIZE) <==> \result == -3;
   ensures \result \in {0, -1, -2, -3};
-  assigns *st->tx_cipher;
+  assigns *st->tx_cipher, *usart2_out;
  */
 int send_encrypted_message(struct NoiseState *st, const uint8_t *msg, size_t len) {
     int err;
@@ -336,16 +335,16 @@ int send_encrypted_message(struct NoiseState *st, const uint8_t *msg, size_t len
         uint8_t payload[MAX_HOST_PACKET_SIZE];
     } pkt;
 
-    if (!st->tx_cipher) {
-        LOG_PRINTF("Cannot send encrypted packet: Data ciphers not yet initialized\n");
-        return -1;
-    }
-
     if (len > sizeof(pkt.payload)) {
         LOG_PRINTF("Packet too long\n");
         return -3;
     }
 
+    if (!st->tx_cipher) {
+        LOG_PRINTF("Cannot send encrypted packet: Data ciphers not yet initialized\n");
+        return -1;
+    }
+
     pkt.header.type = HOST_DATA;
     fc_memcpy_uint8(pkt.payload, msg, len); /* This is necessary because noises API doesn't support separate in and out buffers. D'oh! */
     noise_buffer_set_inout(noise_buf, pkt.payload, len, sizeof(pkt.payload));