Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 23 additions & 0 deletions dag/test/claim/eval_cast_identity_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
module test.claim.eval_cast_identity

import std.logic { Bool }
import std.types { List }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

fn list_identity(xs: List<Int>) -> List<Int> {
xs as List<Int>
}

fn int_identity(x: Int) -> Int {
x as Int
}

test fn list_identity_cast_holds() -> Bool {
list_identity([1, 2, 3]) == [1, 2, 3]
}

test fn int_identity_cast_holds() -> Bool {
int_identity(42) == 42
}
76 changes: 55 additions & 21 deletions src/v1/stage0/src/v1_interpreter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5433,40 +5433,74 @@ fn cast_target_underlying_kernel(ctx: &InterpContext, target: Rc<Node>) -> Strin
current
}

fn str_identity_cast_if_string_family(
fn cast_expr_inferred_type_name(ctx: &InterpContext, expr: Rc<Node>) -> String {
match expr.inferred.as_deref() {
Some(InferredNode::Resolved { node }) => authored_name_at(ctx.si(), node.clone()),
_ => String::new(),
}
}

/// Runtime identity casts mirror `validate_cast`'s `source_name == target_name` arm,
/// plus String-valued casts to types whose alias chain grounds on `String`.
fn cast_identity_result(
val: &Value,
ctx: &InterpContext,
target: Rc<Node>,
source_name: &str,
target_node: Rc<Node>,
target_name: &str,
) -> Option<Value> {
let Value::Str(s) = val else {
return None;
};
let kernel = cast_target_underlying_kernel(ctx, target);
if kernel.is_empty() || kernel == "String" {
Some(Value::Str(s.clone()))
} else {
None
if !source_name.is_empty() && source_name == target_name {
return Some(val.clone());
}
if let Value::Str(s) = val {
let kernel = cast_target_underlying_kernel(ctx, target_node);
if kernel.is_empty() || kernel == "String" {
return Some(Value::Str(s.clone()));
}
}
None
}

fn eval_cast(node: &Rc<Node>, env: &Rc<Env>, ctx: &InterpContext) -> InterpResult<Value> {
let val = eval_expr(&cast_expr(node.clone()), env, ctx)?;
let inner = cast_expr(node.clone());
let source_name = cast_expr_inferred_type_name(ctx, inner.clone());
let val = eval_expr(&inner, env, ctx)?;
let target_node = cast_target(node.clone());
let target_name = cast_target_seed_name(ctx, target_node.clone());

if let Some(v) = str_identity_cast_if_string_family(&val, ctx, target_node) {
if let Some(v) =
cast_identity_result(&val, ctx, &source_name, target_node.clone(), &target_name)
{
return Ok(v);
}

match (val, target_name.as_str()) {
(Value::Int(n), "Float") => Ok(Value::Float(n as f64)),
(Value::Float(n), "Int") => Ok(Value::Int(n as i64)),
(Value::Int(n), "String") => Ok(Value::Str(n.to_string())),
(Value::Float(n), "String") => Ok(Value::Str(n.to_string())),
(Value::Bool(b), "String") => Ok(Value::Str(b.to_string())),
(v, "String") => Ok(Value::Str(format!("{}", v))),
(v, t) => Err(InterpError::TypeError {
msg: format!("cannot cast {} to {}", v.type_label(), t),
match target_name.as_str() {
"Float" => match val {
Value::Int(n) => Ok(Value::Float(n as f64)),
v => Err(InterpError::TypeError {
msg: format!("cannot cast {} to Float", v.type_label()),
}),
},
"Int" => match val {
Value::Float(n) => Ok(Value::Int(n as i64)),
v => Err(InterpError::TypeError {
msg: format!("cannot cast {} to Int", v.type_label()),
}),
},
"String" => match val {
Value::Int(n) => Ok(Value::Str(n.to_string())),
Value::Float(n) => Ok(Value::Str(n.to_string())),
Value::Bool(b) => Ok(Value::Str(b.to_string())),
Value::Str(s) => Ok(Value::Str(s)),
// Corpus wire/debug casts for structured values — not the blanket Display
// fallback that silently stringified List/Map (§5 fabricated plausible output).
Value::Variant { .. } | Value::Record { .. } => Ok(Value::Str(format!("{}", val))),
v => Err(InterpError::TypeError {
msg: format!("cannot cast {} to String", v.type_label()),
}),
},
t => Err(InterpError::TypeError {
msg: format!("cannot cast {} to {}", val.type_label(), t),
}),
}
}
Expand Down
59 changes: 58 additions & 1 deletion src/v1/tests/src/interp_string_family_cast_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,11 @@ fn assert_resolved_no_hard_errors(result: &ResolvedPipelineResult) {
.diagnostics
.iter()
.map(|d| v1_compiler::v1_std_core::diagnostic_to_message(d.diagnostic.clone()))
.filter(|m| !m.starts_with("complexity: ") && !m.starts_with("unlisted import use "))
.filter(|m| {
!m.starts_with("complexity: ")
&& !m.starts_with("unlisted import use ")
&& !m.starts_with("where-refinement unenforced:")
})
.collect();
assert!(
msgs.is_empty() && result.graph.is_some(),
Expand Down Expand Up @@ -56,6 +60,59 @@ test fn string_family_cast_holds() -> Bool {
}
}

#[test]
fn list_identity_cast_is_identity_at_runtime() {
let src = r#"module test.list_identity_cast

fn list_identity(xs: List<Int>) -> List<Int> {
xs as List<Int>
}

test fn list_identity_cast_holds() -> Bool {
list_identity([1, 2, 3]) == [1, 2, 3]
}
"#;
match run_witness(src, "list_identity_cast_holds") {
Value::Bool(true) => {}
other => panic!("expected true witness, got {other:?}"),
}
}

#[test]
fn list_to_string_cast_stays_fail_closed() {
let src = r#"module test.list_string_cast

fn bad(xs: List<Int>) -> String {
xs as String
}

test fn list_string_cast_holds() -> Bool {
bad([1]) == ""
}
"#;
let sources = resolve_imports_transitively("test/list_string_cast.dag", src);
let resolved = compile_to_resolved(Rc::new(sources.into()));
assert_resolved_no_hard_errors(&resolved);
let graph = resolved
.graph
.as_ref()
.expect("graph after successful resolve");
match v1_interpreter::run(
graph,
resolved.source_indices.clone(),
"list_string_cast_holds",
) {
Err(v1_interpreter::InterpError::TypeError { msg }) => {
assert!(
msg.contains("cannot cast List to String"),
"expected List→String type error, got: {msg}"
);
}
Ok(other) => panic!("expected List→String cast to fail closed, got {other:?}"),
Err(other) => panic!("expected TypeError for List→String, got {other:?}"),
}
}

#[test]
fn int_to_secret_cast_stays_fail_closed() {
let src = r#"module test.int_secret_cast
Expand Down
Loading