Coap stack

include coap_byte_stream

action app_send_event(src:ip.endpoint, dst:ip.endpoint, data : stream_data, pos : stream_pos, close : bool)

function coap_data       : stream_data
function coap_packet_end : stream_pos
function coap_pos        : stream_pos
function coap_packet_finished : bool

after init {
    coap_pos := 0;
    coap_packet_finished := false;
}

after app_send_event {
    var send_end := pos + data.end;
    require ~(send_end > coap_packet_end & coap_packet_finished);  # [4]
    var end := coap_data.end;
    if end < send_end {
        end := send_end
    };
    coap_data := coap_data.resize(end,0);  # [1]
    var idx := data.begin;
    while idx < data.end {
        var val := coap_data.value(pos + idx);

TODO: using zero as a "null" value is not correct here. We need a data structure to capture the known intervals!

        require val ~= 0 ->  data.value(idx) = val;  # [2]
        coap_data := coap_data.set(pos+idx,data.value(idx));
        idx := idx.next
    };
    coap_packet_end := end;  # [1]
    if close {
        coap_packet_finished := true;  # [3]
    }
}