Cargo.toml

[package]
name = "gale"
version = "0.1.0"
edition = "2024"
rust-version = "1.85"
description = "Gale — formally verified Zephyr kernel primitives for ASIL-D safety-critical systems"
publish = false

[lib]
path = "plain/src/lib.rs"

# Standard tests use the plain (non-Verus) code.
# Verus verification is done via Bazel (BUILD.bazel).

[dependencies]

[dev-dependencies]
# Property-based testing
proptest = "1"
# Benchmarking
criterion = { version = "0.5", features = ["html_reports"] }
# Concurrency permutation testing — tokio-rs/loom (NOT pulseengine/loom WASM optimizer).
# Only pulled in when the `--cfg loom` compile flag is set so that default
# `cargo test` builds do not fetch or link it.
[target.'cfg(loom)'.dev-dependencies]
loom = "0.7"

[features]
default = []

[[bench]]
name = "sem_bench"
harness = false

[profile.release]
# Safety-critical: overflow checks always on
overflow-checks = true
# LTO for production
lto = true

[profile.bench]
overflow-checks = true

[profile.dev]
overflow-checks = true

[profile.test]
overflow-checks = true

[lints.rust]
# Core safety lints
unsafe_code = "deny"
# TODO: enable missing_docs = "warn" once all items are documented
unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)', 'cfg(verus_keep_ghost)', 'cfg(loom)'] }
# plain/src/ is auto-generated by verus-strip — ghost variables used in
# requires/ensures become unused after stripping. Suppress here since the
# source of truth (src/*.rs) is verified by Verus.
unused_variables = "allow"
unused_assignments = "allow"
# self.flags = self.flags; is a Verus workaround for old(self) tracking
dead_code = "allow"

[lints.clippy]
# === DENY: Correctness & safety-critical ===
# Integer overflow / wrapping
arithmetic_side_effects = "deny"
cast_possible_truncation = "deny"
cast_possible_wrap = "deny"
cast_sign_loss = "deny"
checked_conversions = "deny"
# Panicking paths — forbidden in safety-critical code
unwrap_used = "deny"
expect_used = "deny"
panic = "deny"
unreachable = "deny"
todo = "deny"
unimplemented = "deny"
indexing_slicing = "deny"
# Memory / resource
large_stack_arrays = "deny"
mem_forget = "deny"
# Logic errors
bool_comparison = "deny"
erasing_op = "deny"
misrefactored_assign_op = "deny"
# Fallibility
fallible_impl_from = "deny"
# Shadowing (can hide bugs in safety-critical code)
shadow_unrelated = "deny"
# Float issues (not used, but deny preemptively)
float_arithmetic = "deny"
float_cmp_const = "deny"
# Verbose/explicitness (catches subtle bugs)
implicit_clone = "deny"
# Exhaustive matching
wildcard_enum_match_arm = "deny"

# === WARN: Style & maintainability ===
pedantic = { level = "warn", priority = -1 }
nursery = { level = "warn", priority = -1 }
# Allow some pedantic lints that conflict with our style
must_use_candidate = "allow"
module_name_repetitions = "allow"
missing_errors_doc = "allow"
missing_panics_doc = "allow"
doc_markdown = "allow"
missing_const_for_fn = "allow"
use_self = "allow"
# plain/src/ is auto-generated by verus-strip — these patterns are
# inherent to the stripping process and cannot be avoided:
wildcard_imports = "allow"        # use crate::error::*
assign_op_pattern = "allow"      # i = i + 1 (Verus while-loop style)
if_not_else = "allow"            # if x != y {} else {} (Verus spec style)
single_match = "allow"           # match thread { Some(t) => ..., None => {} }
single_match_else = "allow"      # match with else arm
option_if_let_else = "allow"     # match Option for map_or
new_without_default = "allow"    # WaitQueue::new() without Default
return_self_not_must_use = "allow" # methods returning Self
self_assignment = "allow"        # self.flags = self.flags (Verus old() workaround)
cast_lossless = "allow"          # u32 as u64 (explicit in verified code)
len_zero = "allow"               # .len() > 0 vs !is_empty()
clone_on_copy = "allow"          # .clone() on Copy types (Verus style)
match_same_arms = "allow"        # identical match arms (Verus exhaustive style)
too_long_first_doc_paragraph = "allow" # doc comment style
manual_div_ceil = "allow"        # explicit div_ceil arithmetic
let_and_return = "allow"         # let x = ...; x (Verus binding style)
manual_is_power_of_two = "allow" # (m & (m-1)) == 0 pattern
len_without_is_empty = "allow"   # len() without is_empty()
needless_bool = "allow"          # if x { false } else { true }
match_like_matches_macro = "allow" # match => matches!
question_mark = "allow"          # match Some/None => ?
collapsible_if = "allow"         # nested if (Verus loop style)
manual_map = "allow"             # match None/Some => .map()
uninlined_format_args = "allow"  # format!("{}", x) vs format!("{x}")
bool_to_int_with_if = "allow"   # if x { 1 } else { 0 } (C FFI convention)
unreadable_literal = "allow"    # 0xFFFFFFFF in tests
no_effect_underscore_binding = "allow" # _x = Enum::Variant in layout tests
if_same_then_else = "allow"  # verus-strip: identical branches from spec guards