Add CN specs to MKM

components/include/cn_memory.h

@@ -69,4 +69,31 @@ ensures
     take i = each(u64 j; j >= 0u64 && j < n) {Block<uint8_t>(array_shift<uint8_t>(return, j))};
 $*/
 
+/*$
+datatype OptionMemory {
+    SomeMemory {{u64 base, u64 size} al, map<u64, u8> bu}, 
+    NothingMemory {}
+}
+predicate (datatype OptionMemory) MallocResult(pointer p, u64 n)
+{
+  if (is_null(p)) {
+    return NothingMemory {}; 
+  } else {
+    take log = Alloc(p);
+    assert(allocs[(alloc_id)p] == log);
+    assert(log.base == (u64) p);
+    assert(log.size == n);
+    take i = each(u64 j; j >= 0u64 && j < n) {Block<uint8_t>(array_shift<uint8_t>(p, j))};
+    return SomeMemory { al : log, bu : i};
+  }
+}
+$*/
+
+void *_malloc_canfail(size_t n);
+/*$
+spec _malloc_canfail(u64 n);
+requires true;
+ensures  take Out = MallocResult(return, n);
+$*/
+
 #endif // CN_MEMCPY_H_

components/mission_key_management/Makefile

@@ -1,5 +1,8 @@
 ROOT_DIR:=$(shell dirname $(realpath $(firstword $(MAKEFILE_LIST))))
 
+$(opam env)
+CN=cn verify --magic-comment-char-dollar --include=$(ROOT_DIR)/../include/wars.h -I $(ROOT_DIR)/../include -I $(OPAM_SWITCH_PREFIX)/lib/cerberus/runtime/libc/include/posix
+
 ifeq ($(TARGET),x86_64)
 CC = x86_64-linux-gnu-gcc
 CXX = x86_64-linux-gnu-g++
@@ -34,3 +37,7 @@ $(BUILD_DIR)/%.o: $(ROOT_DIR)/%.c
 .PHONY: clean
 clean:
 	rm -rf build/ build.*/
+
+.PHONY: cn_proof
+cn_proof:
+	$(CN) client.c