Skip to content

Commit

Permalink
mkm: clean up proof
Browse files Browse the repository at this point in the history
  • Loading branch information
@septract
septract committed Dec 27, 2024
1 parent b7c4a19 commit faaa2ef
Show file tree
Hide file tree
Showing 2 changed files with 35 additions and 106 deletions.
40 changes: 15 additions & 25 deletions components/mission_key_management/client.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -264,6 +264,7 @@ enum client_event_result client_read(struct client* c)
/*$
requires
take Client_in = ClientPred(c);
let pos = (u64) Client_in.pos;
ensures
take Client_out = ClientPred(c);
// TODO: more compact notation?
Expand All @@ -286,20 +287,14 @@ ensures
return RES_DONE;
}

// TODO: unclear why this works???
// TODO: Mysterious why this particular case split is needed
/*$ split_case(Client_in.state == (u32) CS_RECV_KEY_ID); $*/

#ifdef CN_ENV
uint64_t pos = c->pos; // TODO: ghost code, shouldn't be necessary
#endif

/*$ apply SplitAt_Owned_u8(buf, (u64) buf_size, (u64) pos, (u64) (buf_size - pos) ); $*/
/*$ apply ViewShift_Owned_u8(buf, buf + pos, (u64) pos, (u64) (buf_size - pos) ); $*/

/*$ apply SplitAt_Owned_u8(buf, buf_size, pos, buf_size - pos ); $*/
/*$ apply ViewShift_Owned_u8(buf, buf + pos, pos, buf_size - pos ); $*/
int ret = read(c->fd, buf + c->pos, buf_size - (uint64_t) c->pos);

/*$ apply UnViewShift_Owned_u8(buf, buf + pos, (u64) pos, (u64) (buf_size - pos) ); $*/
/*$ apply UnSplitAt_Owned_u8(buf, (u64) buf_size, (u64) pos, (u64) (buf_size - pos) ); $*/
/*$ apply UnViewShift_Owned_u8(buf, buf + pos, pos, buf_size - pos ); $*/
/*$ apply UnSplitAt_Owned_u8(buf, buf_size, pos, buf_size - pos ); $*/

if (ret < 0) {
perror("read (client_read)");
Expand All @@ -317,6 +312,7 @@ enum client_event_result client_write(struct client* c)
requires
take Client_in = ClientPred(c);
! is_null(Client_in.key);
let pos = (u64) Client_in.pos;
ensures
take Client_out = ClientPred(c);
Client_out.state == Client_in.state;
Expand All @@ -334,23 +330,17 @@ ensures
return RES_DONE;
}

// TODO: unclear why this works???
// TODO: Mysterious why this particular case split is needed
/*$ split_case(Client_in.state == (u32) CS_SEND_CHALLENGE); $*/

#ifdef CN_ENV
uint64_t pos = c->pos; // TODO: ghost code, shouldn't be necessary
#endif

// TODO: why is this needed for client_write, but not client_read???
/*$ extract Owned<uint8_t>, (u64)pos; $*/

/*$ apply SplitAt_Owned_u8(buf, (u64) buf_size, (u64) pos, (u64) (buf_size - pos) ); $*/
/*$ apply ViewShift_Owned_u8(buf, buf + pos, (u64) pos, (u64) (buf_size - pos) ); $*/
// TODO: Why is this is needed for write() but not read() ?
/*$ extract Owned<uint8_t>, pos; $*/

/*$ apply SplitAt_Owned_u8(buf, buf_size, pos, buf_size - pos ); $*/
/*$ apply ViewShift_Owned_u8(buf, buf + pos, pos, buf_size - pos ); $*/
int ret = write(c->fd, buf + c->pos, buf_size - (uint64_t) c->pos);

/*$ apply UnViewShift_Owned_u8(buf, buf + pos, (u64) pos, (u64) (buf_size - pos) ); $*/
/*$ apply UnSplitAt_Owned_u8(buf, (u64) buf_size, (u64) pos, (u64) (buf_size - pos) ); $*/
/*$ apply UnViewShift_Owned_u8(buf, buf + pos, pos, buf_size - pos ); $*/
/*$ apply UnSplitAt_Owned_u8(buf, buf_size, pos, buf_size - pos ); $*/

if (ret < 0) {
perror("write (client_write)");
Expand All @@ -374,7 +364,7 @@ ensures
// TODO: more compact notation?
Client_out.fd == Client_in.fd;
Client_out.challenge == Client_in.challenge;
ptr_eq(Client_out.key, Client_in.key); // <-- unnecessary
// ptr_eq(Client_out.key, Client_in.key); // <-- unnecessary
Client_out.key_id == Client_in.key_id;
Client_out.pos == 0u8;
Client_out.state == new_state;
Expand Down
101 changes: 20 additions & 81 deletions components/mission_key_management/cn_stubs.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,24 +77,9 @@ void perror(const char *msg);
ensures true;
$*/

// #define fprintf(...) 0
// #define snprintf(...) 0


// From `unistd.h`

ssize_t _read_uint8_t(int fildes, void *buf, size_t n);
/*$
spec _read_uint8_t(i32 fildes, pointer buf, u64 n);
requires
take buf_in = each (u64 i; i < n) { Owned<uint8_t>(array_shift<uint8_t>(buf, i))};
ensures
return >= -1i64 && return <= (i64)n;
take buf_out = each (u64 i; i < n) { Owned<uint8_t>(array_shift<uint8_t>(buf, i))};
buf_out == buf_in;
$*/
#define read(f,b,s) _read_uint8_t(f,b,s)

int _close(int fildes);
/*$
spec _close(i32 fildes);
Expand All @@ -103,18 +88,29 @@ ensures true;
$*/
#define close(x) _close(x)

ssize_t _write_uint8_t(int fildes, const void *buf, size_t nbyte);
ssize_t _read_uint8_t(int fd, void *buf, size_t count);
/*$
spec _write_uint8_t(i32 fildes, pointer buf, u64 nbyte);
spec _read_uint8_t(i32 fd, pointer buf, u64 count);
requires
((i32)nbyte) >= 0i32;
take bufi = each(u64 i; i < nbyte) {Owned<uint8_t>(array_shift<uint8_t>(buf,i))};
take buf_in = each (u64 i; i < count) { Owned<uint8_t>(array_shift<uint8_t>(buf, i))};
ensures
take bufo = each(u64 i; i < nbyte) {Owned<uint8_t>(array_shift<uint8_t>(buf,i))};
bufi == bufo;
return >= -1i64 && return < (i64)nbyte;
take buf_out = each (u64 i; i < count) { Owned<uint8_t>(array_shift<uint8_t>(buf, i))};
buf_out == buf_in;
return >= -1i64 && return <= (i64)count;
$*/
#define write(f,b,s) _write_uint8_t(f,b,s)
#define read(f,b,c) _read_uint8_t(f,b,c)

ssize_t _write_uint8_t(int fd, const void *buf, size_t count);
/*$
spec _write_uint8_t(i32 fd, pointer buf, u64 count);
requires
take buf_in = each(u64 i; i < count) {Owned<uint8_t>(array_shift<uint8_t>(buf,i))};
ensures
take buf_out = each(u64 i; i < count) {Owned<uint8_t>(array_shift<uint8_t>(buf,i))};
buf_in == buf_out;
return >= -1i64 && return < (i64)count;
$*/
#define write(f,b,c) _write_uint8_t(f,b,c)

int _shutdown(int fildes, int how);
/*$ spec _shutdown(i32 fildes, i32 how);
Expand All @@ -123,65 +119,8 @@ int _shutdown(int fildes, int how);
$*/
#define shutdown(x,h) _shutdown(x,h)

// Defined in ../../components/include/cn_memory.h
#define memcpy(d,s,n) _memcpy(d,s,n)
#define memcmp(s1,s2,n) _memcmp(s1,s2,n)
#define malloc(x) _malloc(x)
#define free(x) _free(x)


// void *_memcpy_uint8_t(void *dest, const void *src, size_t nbyte);
// /*$
// spec _memcpy_uint8_t(pointer dest, pointer src, u64 nbyte);
// requires
// ((i32)nbyte) >= 0i32;
// take src_in = each (u64 i; i < nbyte) { Owned<uint8_t>(array_shift<uint8_t>(src,i)) };
// take dest_in = each (u64 i; i < nbyte) { Owned<uint8_t>(array_shift<uint8_t>(dest,i)) };
// ensures
// take src_out = each (u64 i; i < nbyte) { Owned<uint8_t>(array_shift<uint8_t>(src,i)) };
// take dest_out = each (u64 i; i < nbyte) { Owned<uint8_t>(array_shift<uint8_t>(dest,i)) };
// src_in == src_out;
// // TODO: is this the right behavior?
// if (is_null(return)) {
// dest_out == dest_in
// } else {
// ptr_eq(return, dest)
// &&
// dest_out == src_out
// };
// $*/
// #define memcpy(d,s,n) _memcpy_uint8_t(d,s,n)

// int _memcmp_uint8_t(const void *s1, const void *s2, size_t nbyte);
// /*$
// spec _memcmp_uint8_t(pointer s1, pointer s2, u64 nbyte);
// requires
// ((i32)nbyte) >= 0i32;
// take S1_in = each (u64 i; i < nbyte) { Owned<uint8_t>(array_shift<uint8_t>(s1,i)) };
// take S2_in = each (u64 i; i < nbyte) { Owned<uint8_t>(array_shift<uint8_t>(s2,i)) };
// ensures
// take S1_out = each (u64 i; i < nbyte) { Owned<uint8_t>(array_shift<uint8_t>(s1,i)) };
// take S2_out = each (u64 i; i < nbyte) { Owned<uint8_t>(array_shift<uint8_t>(s2,i)) };
// S1_out == S1_in; S2_out == S2_in;
// if (S1_in == S2_in) { return > 0i32 } else { return == 0i32 };
// $*/
// #define memcmp(s1,s2,n) _memcmp_uint8_t(s1,s2,n)

// struct client *_malloc_struct_client(size_t nbyte);
// /*$
// spec _malloc_struct_client(u64 nbyte);
// requires
// ((i32)nbyte) >= 0i32;
// ensures
// take Client_out = Owned<struct client>(return);
// $*/
// #define malloc(n) _malloc_struct_client(n)

// void _free_struct_client(struct client *target);
// /*$
// spec _free_struct_client(pointer target);
// requires
// take Client_out = Owned<struct client>(target);
// ensures
// true;
// $*/
// #define free(t) _free_struct_client(t)

0 comments on commit faaa2ef

Please sign in to comment.