1use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
6
7use super::functions::*;
8use std::collections::{HashMap, VecDeque};
9
10#[allow(dead_code)]
14pub struct RecordWriter {
15 inner: BufferedWriter,
16 record_count: usize,
17}
18impl RecordWriter {
19 #[allow(dead_code)]
21 pub fn new(flush_threshold: usize) -> Self {
22 Self {
23 inner: BufferedWriter::new(flush_threshold),
24 record_count: 0,
25 }
26 }
27 #[allow(dead_code)]
29 pub fn write_record(&mut self, record: &str) {
30 self.inner.writeln(record);
31 self.record_count += 1;
32 }
33 #[allow(dead_code)]
35 pub fn record_count(&self) -> usize {
36 self.record_count
37 }
38 #[allow(dead_code)]
40 pub fn total_written(&self) -> usize {
41 self.inner.total_written()
42 }
43 #[allow(dead_code)]
45 pub fn flush(&mut self) {
46 self.inner.flush();
47 }
48}
49#[allow(dead_code)]
51#[derive(Debug, Clone, PartialEq, Eq)]
52pub struct Capability {
53 pub level: u32,
55 pub description: String,
57}
58#[allow(dead_code)]
59impl Capability {
60 pub fn new(level: u32, description: impl Into<String>) -> Self {
62 Self {
63 level,
64 description: description.into(),
65 }
66 }
67 pub fn null() -> Self {
69 Self::new(0, "null")
70 }
71 pub fn read_only() -> Self {
73 Self::new(1, "read-only")
74 }
75 pub fn read_write() -> Self {
77 Self::new(2, "read-write")
78 }
79 pub fn full() -> Self {
81 Self::new(u32::MAX, "full")
82 }
83 pub fn is_sufficient_for(&self, required: u32) -> bool {
85 self.level >= required
86 }
87 pub fn attenuate(&self, max_level: u32) -> Capability {
89 Capability::new(
90 self.level.min(max_level),
91 format!("attenuated({})", max_level),
92 )
93 }
94}
95#[allow(dead_code)]
99pub struct DelimiterSplitter {
100 buffer: Vec<u8>,
101 delimiter: u8,
102}
103impl DelimiterSplitter {
104 #[allow(dead_code)]
106 pub fn new(delimiter: u8) -> Self {
107 Self {
108 buffer: Vec::new(),
109 delimiter,
110 }
111 }
112 #[allow(dead_code)]
114 pub fn feed(&mut self, data: &[u8]) {
115 self.buffer.extend_from_slice(data);
116 }
117 #[allow(dead_code)]
121 pub fn drain(&mut self) -> Vec<Vec<u8>> {
122 let mut records = Vec::new();
123 while let Some(pos) = self.buffer.iter().position(|&b| b == self.delimiter) {
124 let record = self.buffer.drain(..pos).collect();
125 self.buffer.drain(..1);
126 records.push(record);
127 }
128 records
129 }
130 #[allow(dead_code)]
132 pub fn buffered_len(&self) -> usize {
133 self.buffer.len()
134 }
135}
136#[derive(Debug, Clone)]
138pub struct FileMetadata {
139 pub path: String,
141 pub size: u64,
143 pub is_dir: bool,
145 pub is_file: bool,
147 pub read_only: bool,
149}
150impl FileMetadata {
151 pub fn regular_file(path: impl Into<String>, size: u64) -> Self {
153 Self {
154 path: path.into(),
155 size,
156 is_dir: false,
157 is_file: true,
158 read_only: false,
159 }
160 }
161 pub fn directory(path: impl Into<String>) -> Self {
163 Self {
164 path: path.into(),
165 size: 0,
166 is_dir: true,
167 is_file: false,
168 read_only: false,
169 }
170 }
171 pub fn with_read_only(mut self) -> Self {
173 self.read_only = true;
174 self
175 }
176}
177#[allow(dead_code)]
181#[derive(Debug, Default, Clone)]
182pub struct MockFs {
183 files: std::collections::HashMap<String, Vec<u8>>,
184}
185impl MockFs {
186 #[allow(dead_code)]
188 pub fn new() -> Self {
189 Self::default()
190 }
191 #[allow(dead_code)]
193 pub fn write(&mut self, path: &str, data: Vec<u8>) {
194 self.files.insert(path.to_string(), data);
195 }
196 #[allow(dead_code)]
198 pub fn write_str(&mut self, path: &str, content: &str) {
199 self.write(path, content.as_bytes().to_vec());
200 }
201 #[allow(dead_code)]
203 pub fn read(&self, path: &str) -> Result<Vec<u8>, IoError> {
204 self.files
205 .get(path)
206 .cloned()
207 .ok_or_else(|| IoError::not_found(path))
208 }
209 #[allow(dead_code)]
211 pub fn read_str(&self, path: &str) -> Result<String, IoError> {
212 let bytes = self.read(path)?;
213 String::from_utf8(bytes).map_err(|_| IoError::invalid_data("invalid UTF-8"))
214 }
215 #[allow(dead_code)]
217 pub fn exists(&self, path: &str) -> bool {
218 self.files.contains_key(path)
219 }
220 #[allow(dead_code)]
222 pub fn remove(&mut self, path: &str) -> bool {
223 self.files.remove(path).is_some()
224 }
225 #[allow(dead_code)]
227 pub fn list_paths(&self) -> Vec<&str> {
228 self.files.keys().map(String::as_str).collect()
229 }
230 #[allow(dead_code)]
232 pub fn file_size(&self, path: &str) -> Result<u64, IoError> {
233 self.files
234 .get(path)
235 .map(|v| v.len() as u64)
236 .ok_or_else(|| IoError::not_found(path))
237 }
238}
239#[allow(dead_code)]
243pub struct HoareVerifier {
244 triples: Vec<(String, String, String)>,
246}
247#[allow(dead_code)]
248impl HoareVerifier {
249 pub fn new() -> Self {
251 Self {
252 triples: Vec::new(),
253 }
254 }
255 pub fn add_triple(
257 &mut self,
258 op: impl Into<String>,
259 pre: impl Into<String>,
260 post: impl Into<String>,
261 ) {
262 self.triples.push((op.into(), pre.into(), post.into()));
263 }
264 pub fn triple_count(&self) -> usize {
266 self.triples.len()
267 }
268 pub fn postcondition_of(&self, op: &str) -> Option<&str> {
270 self.triples
271 .iter()
272 .find(|(o, _, _)| o == op)
273 .map(|(_, _, post)| post.as_str())
274 }
275 pub fn has_triple(&self, op: &str) -> bool {
277 self.triples.iter().any(|(o, _, _)| o == op)
278 }
279 pub fn operations(&self) -> Vec<&str> {
281 self.triples.iter().map(|(o, _, _)| o.as_str()).collect()
282 }
283}
284#[derive(Debug, Clone, PartialEq, Eq)]
286pub enum IoErrorKind {
287 NotFound,
289 PermissionDenied,
291 ConnectionRefused,
293 TimedOut,
295 UnexpectedEof,
297 WriteZero,
299 InvalidData,
301 Other,
303}
304#[allow(dead_code)]
306pub struct SessionChannel {
307 protocol: Vec<SessionAction>,
308 cursor: usize,
309 messages: Vec<String>,
310}
311#[allow(dead_code)]
312impl SessionChannel {
313 pub fn new(protocol: Vec<SessionAction>) -> Self {
315 Self {
316 protocol,
317 cursor: 0,
318 messages: Vec::new(),
319 }
320 }
321 pub fn send(&mut self, msg: impl Into<String>) -> Result<(), String> {
325 if self.cursor >= self.protocol.len() {
326 return Err("protocol exhausted".to_string());
327 }
328 if self.protocol[self.cursor] != SessionAction::Send {
329 return Err(format!(
330 "protocol violation: expected {:?}, got Send",
331 self.protocol[self.cursor]
332 ));
333 }
334 self.messages.push(msg.into());
335 self.cursor += 1;
336 Ok(())
337 }
338 pub fn recv(&mut self) -> Result<Option<String>, String> {
342 if self.cursor >= self.protocol.len() {
343 return Err("protocol exhausted".to_string());
344 }
345 if self.protocol[self.cursor] != SessionAction::Recv {
346 return Err(format!(
347 "protocol violation: expected {:?}, got Recv",
348 self.protocol[self.cursor]
349 ));
350 }
351 self.cursor += 1;
352 Ok(self.messages.pop())
353 }
354 pub fn is_complete(&self) -> bool {
356 self.cursor >= self.protocol.len()
357 }
358 pub fn remaining_steps(&self) -> usize {
360 self.protocol.len().saturating_sub(self.cursor)
361 }
362}
363#[allow(dead_code)]
367pub struct AsyncTaskQueue {
368 pending: std::collections::VecDeque<(usize, String)>,
369 completed: std::collections::HashMap<usize, String>,
370 next_id: usize,
371}
372#[allow(dead_code)]
373impl AsyncTaskQueue {
374 pub fn new() -> Self {
376 Self {
377 pending: std::collections::VecDeque::new(),
378 completed: std::collections::HashMap::new(),
379 next_id: 0,
380 }
381 }
382 pub fn enqueue(&mut self, description: impl Into<String>) -> usize {
384 let id = self.next_id;
385 self.next_id += 1;
386 self.pending.push_back((id, description.into()));
387 id
388 }
389 pub fn complete_next(&mut self, result: impl Into<String>) -> Option<usize> {
391 if let Some((id, _)) = self.pending.pop_front() {
392 self.completed.insert(id, result.into());
393 Some(id)
394 } else {
395 None
396 }
397 }
398 pub fn result_of(&self, id: usize) -> Option<&str> {
400 self.completed.get(&id).map(String::as_str)
401 }
402 pub fn pending_count(&self) -> usize {
404 self.pending.len()
405 }
406 pub fn completed_count(&self) -> usize {
408 self.completed.len()
409 }
410 pub fn is_complete(&self, id: usize) -> bool {
412 self.completed.contains_key(&id)
413 }
414}
415#[derive(Debug, Clone)]
417pub struct IoAction {
418 pub kind: IoActionKind,
420 pub result_type: Expr,
422}
423impl IoAction {
424 pub fn new(kind: IoActionKind, result_type: Expr) -> Self {
426 Self { kind, result_type }
427 }
428 pub fn println() -> Self {
430 Self::new(
431 IoActionKind::Println,
432 Expr::Const(Name::str("Unit"), vec![]),
433 )
434 }
435 pub fn read_line() -> Self {
437 Self::new(
438 IoActionKind::ReadStdin,
439 Expr::Const(Name::str("String"), vec![]),
440 )
441 }
442 pub fn exit(code: i32) -> Self {
444 Self::new(
445 IoActionKind::Exit(code),
446 Expr::Const(Name::str("Empty"), vec![]),
447 )
448 }
449}
450#[derive(Debug, Clone)]
452pub struct IoError {
453 pub kind: IoErrorKind,
455 pub message: String,
457}
458impl IoError {
459 pub fn new(kind: IoErrorKind, message: impl Into<String>) -> Self {
461 Self {
462 kind,
463 message: message.into(),
464 }
465 }
466 pub fn not_found(path: &str) -> Self {
468 Self::new(IoErrorKind::NotFound, format!("file not found: {}", path))
469 }
470 pub fn permission_denied(path: &str) -> Self {
472 Self::new(
473 IoErrorKind::PermissionDenied,
474 format!("permission denied: {}", path),
475 )
476 }
477 pub fn unexpected_eof() -> Self {
479 Self::new(IoErrorKind::UnexpectedEof, "unexpected end of file")
480 }
481 pub fn invalid_data(msg: impl Into<String>) -> Self {
483 Self::new(IoErrorKind::InvalidData, msg)
484 }
485}
486#[allow(dead_code)]
490pub struct StmLog {
491 reads: Vec<(usize, i64)>,
493 writes: Vec<(usize, i64)>,
495 aborted: bool,
497}
498#[allow(dead_code)]
499impl StmLog {
500 pub fn new() -> Self {
502 Self {
503 reads: Vec::new(),
504 writes: Vec::new(),
505 aborted: false,
506 }
507 }
508 pub fn record_read(&mut self, cell_id: usize, value: i64) {
510 self.reads.push((cell_id, value));
511 }
512 pub fn record_write(&mut self, cell_id: usize, value: i64) {
514 self.writes.push((cell_id, value));
515 }
516 pub fn abort(&mut self) {
518 self.aborted = true;
519 }
520 pub fn is_aborted(&self) -> bool {
522 self.aborted
523 }
524 pub fn conflicts_with(&self, other: &StmLog) -> bool {
526 for (wid, _) in &self.writes {
527 for (owid, _) in &other.writes {
528 if wid == owid {
529 return true;
530 }
531 }
532 }
533 false
534 }
535 pub fn read_count(&self) -> usize {
537 self.reads.len()
538 }
539 pub fn write_count(&self) -> usize {
541 self.writes.len()
542 }
543}
544#[derive(Debug, Clone, PartialEq)]
548pub enum IoActionKind {
549 ReadStdin,
551 WriteStdout,
553 WriteStderr,
555 OpenRead(String),
557 OpenWrite(String),
559 Close,
561 Println,
563 Flush,
565 Sleep(u64),
567 Exit(i32),
569}
570pub struct BufferedReader {
574 data: Vec<u8>,
576 pos: usize,
578 capacity: usize,
580}
581impl BufferedReader {
582 pub fn new(data: Vec<u8>) -> Self {
584 Self {
585 capacity: data.len(),
586 data,
587 pos: 0,
588 }
589 }
590 #[allow(clippy::should_implement_trait)]
592 pub fn from_str(s: &str) -> Self {
593 Self::new(s.as_bytes().to_vec())
594 }
595 pub fn read_byte(&mut self) -> Option<u8> {
597 if self.pos < self.data.len() {
598 let b = self.data[self.pos];
599 self.pos += 1;
600 Some(b)
601 } else {
602 None
603 }
604 }
605 pub fn read_line(&mut self) -> Option<String> {
609 if self.pos >= self.data.len() {
610 return None;
611 }
612 let start = self.pos;
613 while self.pos < self.data.len() && self.data[self.pos] != b'\n' {
614 self.pos += 1;
615 }
616 if self.pos < self.data.len() {
617 self.pos += 1;
618 }
619 String::from_utf8(self.data[start..self.pos].to_vec()).ok()
620 }
621 pub fn read_to_string(&mut self) -> Result<String, IoError> {
623 let remaining = &self.data[self.pos..];
624 self.pos = self.data.len();
625 String::from_utf8(remaining.to_vec())
626 .map_err(|_| IoError::invalid_data("invalid UTF-8 sequence"))
627 }
628 pub fn read_exact(&mut self, n: usize) -> Result<Vec<u8>, IoError> {
632 if self.pos + n > self.data.len() {
633 return Err(IoError::unexpected_eof());
634 }
635 let slice = self.data[self.pos..self.pos + n].to_vec();
636 self.pos += n;
637 Ok(slice)
638 }
639 pub fn peek(&self) -> Option<u8> {
641 self.data.get(self.pos).copied()
642 }
643 pub fn is_eof(&self) -> bool {
645 self.pos >= self.data.len()
646 }
647 pub fn remaining(&self) -> usize {
649 self.data.len().saturating_sub(self.pos)
650 }
651 pub fn reset(&mut self) {
653 self.pos = 0;
654 }
655 pub fn skip(&mut self, n: usize) {
657 self.pos = (self.pos + n).min(self.data.len());
658 }
659 pub fn capacity(&self) -> usize {
661 self.capacity
662 }
663 pub fn lines(&mut self) -> Vec<String> {
665 let mut result = Vec::new();
666 while let Some(line) = self.read_line() {
667 result.push(line);
668 }
669 result
670 }
671}
672#[allow(dead_code)]
676#[derive(Debug, Default, Clone)]
677pub struct EnvRegistry {
678 vars: std::collections::HashMap<String, String>,
679}
680impl EnvRegistry {
681 #[allow(dead_code)]
683 pub fn new() -> Self {
684 Self::default()
685 }
686 #[allow(dead_code)]
688 pub fn set(&mut self, key: &str, val: &str) {
689 self.vars.insert(key.to_string(), val.to_string());
690 }
691 #[allow(dead_code)]
693 pub fn get(&self, key: &str) -> Option<&str> {
694 self.vars.get(key).map(String::as_str)
695 }
696 #[allow(dead_code)]
698 pub fn remove(&mut self, key: &str) {
699 self.vars.remove(key);
700 }
701 #[allow(dead_code)]
703 pub fn keys(&self) -> Vec<&str> {
704 self.vars.keys().map(String::as_str).collect()
705 }
706}
707#[allow(dead_code)]
712#[derive(Debug, Clone, PartialEq)]
713pub enum SessionAction {
714 Send,
716 Recv,
718}
719pub struct BufferedWriter {
723 buffer: Vec<u8>,
725 flush_threshold: usize,
727 total_written: usize,
729}
730impl BufferedWriter {
731 pub fn new(flush_threshold: usize) -> Self {
733 Self {
734 buffer: Vec::new(),
735 flush_threshold,
736 total_written: 0,
737 }
738 }
739 pub fn default_threshold() -> Self {
741 Self::new(4096)
742 }
743 pub fn write_bytes(&mut self, data: &[u8]) {
747 self.buffer.extend_from_slice(data);
748 self.total_written += data.len();
749 if self.buffer.len() >= self.flush_threshold {
750 self.flush();
751 }
752 }
753 pub fn write_str(&mut self, s: &str) {
755 self.write_bytes(s.as_bytes());
756 }
757 pub fn writeln(&mut self, s: &str) {
759 self.write_str(s);
760 self.write_bytes(b"\n");
761 }
762 pub fn flush(&mut self) {
764 self.buffer.clear();
765 }
766 pub fn as_str(&self) -> Result<&str, IoError> {
768 std::str::from_utf8(&self.buffer)
769 .map_err(|_| IoError::invalid_data("buffer contains invalid UTF-8"))
770 }
771 pub fn buffered_len(&self) -> usize {
773 self.buffer.len()
774 }
775 pub fn total_written(&self) -> usize {
777 self.total_written
778 }
779 pub fn is_empty(&self) -> bool {
781 self.buffer.is_empty()
782 }
783}
784#[derive(Debug, Default)]
789pub struct IoActionPipeline {
790 actions: Vec<IoAction>,
792}
793impl IoActionPipeline {
794 pub fn new() -> Self {
796 Self::default()
797 }
798 pub fn push(&mut self, action: IoAction) {
800 self.actions.push(action);
801 }
802 pub fn len(&self) -> usize {
804 self.actions.len()
805 }
806 pub fn is_empty(&self) -> bool {
808 self.actions.is_empty()
809 }
810 pub fn actions(&self) -> &[IoAction] {
812 &self.actions
813 }
814 pub fn has_exit(&self) -> bool {
816 self.actions
817 .iter()
818 .any(|a| matches!(a.kind, IoActionKind::Exit(_)))
819 }
820 pub fn result_type(&self) -> Option<&Expr> {
822 self.actions.last().map(|a| &a.result_type)
823 }
824 pub fn clear(&mut self) {
826 self.actions.clear();
827 }
828}