refactor(control_tree): modularize normalized_shadow dev pipeline
This commit is contained in:
@ -42,6 +42,20 @@ pub(crate) use control_flow::{detect_parse_number_pattern, ParseNumberInfo};
|
||||
pub(crate) use control_flow::{detect_parse_string_pattern, ParseStringInfo};
|
||||
// Phase 91 P5b: Re-export escape skip pattern detection for loop_canonicalizer
|
||||
pub(crate) use control_flow::{detect_escape_skip_pattern, EscapeSkipPatternInfo};
|
||||
|
||||
/// Phase 129: Public (crate) wrapper for StepTree capability guard.
|
||||
///
|
||||
/// `control_flow` is intentionally private to keep control-flow entrypoints centralized.
|
||||
/// Shadow pipelines outside `mir::builder` must call this wrapper instead of reaching into
|
||||
/// `control_flow::*` directly.
|
||||
pub(crate) fn check_step_tree_capabilities(
|
||||
tree: &crate::mir::control_tree::StepTree,
|
||||
func_name: &str,
|
||||
strict: bool,
|
||||
dev: bool,
|
||||
) -> Result<(), String> {
|
||||
control_flow::joinir::control_tree_capability_guard::check(tree, func_name, strict, dev)
|
||||
}
|
||||
mod exprs_lambda; // lambda lowering
|
||||
mod exprs_peek; // peek expression
|
||||
mod exprs_qmark; // ?-propagate
|
||||
|
||||
@ -176,91 +176,36 @@ impl MirBuilder {
|
||||
fn lower_function_body(&mut self, body: Vec<ASTNode>) -> Result<(), String> {
|
||||
let trace = crate::mir::builder::control_flow::joinir::trace::trace();
|
||||
|
||||
// Phase 112: StepTree capability guard (strict-only)
|
||||
// Phase 112: StepTree capability guard (strict-only) + dev shadow lowering
|
||||
let strict = crate::config::env::joinir_dev::strict_enabled();
|
||||
let dev = crate::config::env::joinir_dev_enabled();
|
||||
let func_name = self
|
||||
.scope_ctx
|
||||
.current_function
|
||||
.as_ref()
|
||||
.map(|f| f.signature.name.clone())
|
||||
.unwrap_or_else(|| "<unknown>".to_string());
|
||||
|
||||
if strict || dev {
|
||||
let tree = crate::mir::control_tree::StepTreeBuilderBox::build_from_block(&body);
|
||||
|
||||
if dev {
|
||||
trace.dev("control_tree/step_tree", &tree.to_compact_string());
|
||||
}
|
||||
|
||||
// Phase 112: Guard check (strict mode only)
|
||||
let func_name = self
|
||||
.scope_ctx
|
||||
.current_function
|
||||
.as_ref()
|
||||
.map(|f| f.signature.name.clone())
|
||||
.unwrap_or_else(|| "<unknown>".to_string());
|
||||
|
||||
crate::mir::builder::control_flow::joinir::control_tree_capability_guard::check(
|
||||
&tree, &func_name, strict, dev,
|
||||
)?;
|
||||
|
||||
// Phase 121/122: StepTree→Normalized shadow lowering (dev-only)
|
||||
if dev {
|
||||
use crate::mir::control_tree::normalized_shadow::StepTreeNormalizedShadowLowererBox;
|
||||
use crate::mir::control_tree::normalized_shadow::parity;
|
||||
use crate::mir::control_tree::normalized_shadow::available_inputs_collector::AvailableInputsCollectorBox;
|
||||
|
||||
// Phase 126: Collect available_inputs from SSOT sources
|
||||
// Note: CapturedEnv is None for now (if-only patterns don't use CapturedEnv yet)
|
||||
let available_inputs = AvailableInputsCollectorBox::collect(self, None);
|
||||
|
||||
// Try shadow lowering (if-only scope)
|
||||
let shadow_result = StepTreeNormalizedShadowLowererBox::try_lower_if_only(&tree, &available_inputs);
|
||||
|
||||
match shadow_result {
|
||||
Ok(Some((module, _meta))) => {
|
||||
// Phase 122: Verify Normalized JoinModule structure
|
||||
let expected_env_fields =
|
||||
StepTreeNormalizedShadowLowererBox::expected_env_field_count(
|
||||
&tree,
|
||||
&available_inputs,
|
||||
);
|
||||
|
||||
if let Err(err) =
|
||||
parity::verify_normalized_structure(&module, expected_env_fields)
|
||||
{
|
||||
if strict {
|
||||
return Err(err);
|
||||
}
|
||||
trace.dev("phase122/emit/error", &err);
|
||||
} else {
|
||||
// Shadow lowering succeeded + structure verified
|
||||
let status = format!(
|
||||
"module_emitted=true funcs={} env_fields={} step_tree_sig={}",
|
||||
module.functions.len(),
|
||||
expected_env_fields,
|
||||
tree.signature_basis_string()
|
||||
);
|
||||
trace.dev("phase122/emit", &status);
|
||||
}
|
||||
}
|
||||
Ok(None) => {
|
||||
// Out of scope (e.g., contains loops)
|
||||
let status = StepTreeNormalizedShadowLowererBox::get_status_string(&tree);
|
||||
trace.dev("phase121/shadow", &status);
|
||||
}
|
||||
Err(err) => {
|
||||
// Should be supported but failed (internal error)
|
||||
let msg = format!(
|
||||
"phase121/shadow: internal error for {}: {}",
|
||||
func_name, err
|
||||
);
|
||||
if strict {
|
||||
return Err(format!(
|
||||
"Phase121 shadow lowering failed (strict mode): {}\nHint: if-only pattern should be supported but conversion failed",
|
||||
err
|
||||
));
|
||||
}
|
||||
trace.dev("phase121/shadow/error", &msg);
|
||||
}
|
||||
}
|
||||
struct JoinLoopTraceDevAdapter<'a> {
|
||||
trace: &'a crate::mir::builder::control_flow::joinir::trace::JoinLoopTrace,
|
||||
}
|
||||
impl crate::mir::control_tree::normalized_shadow::dev_pipeline::DevTrace
|
||||
for JoinLoopTraceDevAdapter<'_>
|
||||
{
|
||||
fn dev(&self, tag: &str, msg: &str) {
|
||||
self.trace.dev(tag, msg)
|
||||
}
|
||||
}
|
||||
let trace_adapter = JoinLoopTraceDevAdapter { trace: &trace };
|
||||
|
||||
crate::mir::control_tree::normalized_shadow::dev_pipeline::StepTreeDevPipelineBox::run(
|
||||
self,
|
||||
&body,
|
||||
&func_name,
|
||||
strict,
|
||||
dev,
|
||||
&trace_adapter,
|
||||
)?;
|
||||
|
||||
trace.emit_if(
|
||||
"debug",
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
98
src/mir/control_tree/normalized_shadow/dev_pipeline.rs
Normal file
98
src/mir/control_tree/normalized_shadow/dev_pipeline.rs
Normal file
@ -0,0 +1,98 @@
|
||||
//! Dev/strict StepTree pipeline (capability guard + shadow lowering)
|
||||
|
||||
use crate::ast::ASTNode;
|
||||
use crate::mir::control_tree::normalized_shadow::available_inputs_collector::AvailableInputsCollectorBox;
|
||||
use crate::mir::control_tree::normalized_shadow::normalized_verifier;
|
||||
use crate::mir::control_tree::normalized_shadow::StepTreeNormalizedShadowLowererBox;
|
||||
use crate::mir::control_tree::StepTreeBuilderBox;
|
||||
|
||||
pub trait DevTrace {
|
||||
fn dev(&self, tag: &str, msg: &str);
|
||||
}
|
||||
|
||||
pub struct StepTreeDevPipelineBox;
|
||||
|
||||
impl StepTreeDevPipelineBox {
|
||||
pub fn run(
|
||||
builder: &mut crate::mir::builder::MirBuilder,
|
||||
body: &[ASTNode],
|
||||
func_name: &str,
|
||||
strict: bool,
|
||||
dev: bool,
|
||||
trace: &dyn DevTrace,
|
||||
) -> Result<(), String> {
|
||||
if !strict && !dev {
|
||||
return Ok(());
|
||||
}
|
||||
|
||||
let tree = StepTreeBuilderBox::build_from_block(body);
|
||||
|
||||
if dev {
|
||||
trace.dev("control_tree/step_tree", &tree.to_compact_string());
|
||||
}
|
||||
|
||||
crate::mir::builder::check_step_tree_capabilities(&tree, func_name, strict, dev)?;
|
||||
|
||||
if !dev {
|
||||
return Ok(());
|
||||
}
|
||||
|
||||
// Phase 126: Collect available_inputs from SSOT sources
|
||||
// Note: CapturedEnv is None for now (if-only patterns don't use CapturedEnv yet)
|
||||
let available_inputs = AvailableInputsCollectorBox::collect(builder, None);
|
||||
|
||||
// Try shadow lowering (if-only scope)
|
||||
let shadow_result =
|
||||
StepTreeNormalizedShadowLowererBox::try_lower_if_only(&tree, &available_inputs);
|
||||
|
||||
match shadow_result {
|
||||
Ok(Some((module, _meta))) => {
|
||||
// Phase 122: Verify Normalized JoinModule structure
|
||||
let expected_env_fields =
|
||||
StepTreeNormalizedShadowLowererBox::expected_env_field_count(
|
||||
&tree,
|
||||
&available_inputs,
|
||||
);
|
||||
|
||||
if let Err(err) =
|
||||
normalized_verifier::verify_normalized_structure(&module, expected_env_fields)
|
||||
{
|
||||
if strict {
|
||||
return Err(err);
|
||||
}
|
||||
trace.dev("phase122/emit/error", &err);
|
||||
} else {
|
||||
// Shadow lowering succeeded + structure verified
|
||||
let status = format!(
|
||||
"module_emitted=true funcs={} env_fields={} step_tree_sig={}",
|
||||
module.functions.len(),
|
||||
expected_env_fields,
|
||||
tree.signature_basis_string()
|
||||
);
|
||||
trace.dev("phase122/emit", &status);
|
||||
}
|
||||
}
|
||||
Ok(None) => {
|
||||
// Out of scope (e.g., contains loops)
|
||||
let status = StepTreeNormalizedShadowLowererBox::get_status_string(&tree);
|
||||
trace.dev("phase121/shadow", &status);
|
||||
}
|
||||
Err(err) => {
|
||||
// Should be supported but failed (internal error)
|
||||
let msg = format!(
|
||||
"phase121/shadow: internal error for {}: {}",
|
||||
func_name, err
|
||||
);
|
||||
if strict {
|
||||
return Err(format!(
|
||||
"Phase121 shadow lowering failed (strict mode): {}\nHint: if-only pattern should be supported but conversion failed",
|
||||
err
|
||||
));
|
||||
}
|
||||
trace.dev("phase121/shadow/error", &msg);
|
||||
}
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
59
src/mir/control_tree/normalized_shadow/env_layout.rs
Normal file
59
src/mir/control_tree/normalized_shadow/env_layout.rs
Normal file
@ -0,0 +1,59 @@
|
||||
//! Env layout helper (writes + inputs) for normalized shadow lowering
|
||||
|
||||
use crate::mir::control_tree::step_tree::StepTree;
|
||||
use crate::mir::control_tree::step_tree_contract_box::StepTreeContract;
|
||||
use crate::mir::ValueId;
|
||||
use std::collections::BTreeMap;
|
||||
|
||||
/// Phase 125: Normalized env layout (writes + inputs)
|
||||
///
|
||||
/// ## SSOT
|
||||
///
|
||||
/// - writes: From `StepTreeContract.writes`
|
||||
/// - inputs: From `(StepTreeContract.reads ∩ available_inputs)`
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct EnvLayout {
|
||||
/// Variables written (generate ValueId for these)
|
||||
pub writes: Vec<String>,
|
||||
/// Variables read from outer scope (reference ValueId from available_inputs)
|
||||
pub inputs: Vec<String>,
|
||||
}
|
||||
|
||||
impl EnvLayout {
|
||||
/// Create env layout from contract and available_inputs (Phase 125)
|
||||
pub fn from_contract(
|
||||
contract: &StepTreeContract,
|
||||
available_inputs: &BTreeMap<String, ValueId>,
|
||||
) -> Self {
|
||||
// Phase 125 P2: writes from contract
|
||||
let writes: Vec<String> = contract.writes.iter().cloned().collect();
|
||||
|
||||
// Phase 125 P2: inputs = reads ∩ available_inputs (deterministic order)
|
||||
let inputs: Vec<String> = contract
|
||||
.reads
|
||||
.iter()
|
||||
.filter(|name| available_inputs.contains_key(*name))
|
||||
.cloned()
|
||||
.collect();
|
||||
|
||||
EnvLayout { writes, inputs }
|
||||
}
|
||||
|
||||
/// Flatten writes+inputs to a single field list (deterministic)
|
||||
pub fn env_fields(&self) -> Vec<String> {
|
||||
self.writes
|
||||
.iter()
|
||||
.chain(self.inputs.iter())
|
||||
.cloned()
|
||||
.collect()
|
||||
}
|
||||
}
|
||||
|
||||
/// Phase 129-B: Expected env field count (writes + inputs)
|
||||
pub fn expected_env_field_count(
|
||||
step_tree: &StepTree,
|
||||
available_inputs: &BTreeMap<String, ValueId>,
|
||||
) -> usize {
|
||||
let env_layout = EnvLayout::from_contract(&step_tree.contract, available_inputs);
|
||||
env_layout.writes.len() + env_layout.inputs.len()
|
||||
}
|
||||
385
src/mir/control_tree/normalized_shadow/if_as_last_join_k.rs
Normal file
385
src/mir/control_tree/normalized_shadow/if_as_last_join_k.rs
Normal file
@ -0,0 +1,385 @@
|
||||
//! Phase 129-B: if-as-last lowering with join_k (dev-only)
|
||||
|
||||
use super::env_layout::EnvLayout;
|
||||
use super::legacy::LegacyLowerer;
|
||||
use crate::mir::control_tree::step_tree::{StepNode, StepStmtKind, StepTree};
|
||||
use crate::mir::join_ir::lowering::carrier_info::JoinFragmentMeta;
|
||||
use crate::mir::join_ir::lowering::error_tags;
|
||||
use crate::mir::join_ir::{ConstValue, JoinFunction, JoinFuncId, JoinInst, JoinModule, MirLikeInst};
|
||||
use crate::mir::ValueId;
|
||||
use std::collections::BTreeMap;
|
||||
|
||||
pub struct IfAsLastJoinKLowererBox;
|
||||
|
||||
impl IfAsLastJoinKLowererBox {
|
||||
/// Phase 129-B: If-as-last shape detection (no post-if)
|
||||
pub fn expects_join_k_as_last(step_tree: &StepTree) -> bool {
|
||||
match &step_tree.root {
|
||||
StepNode::If { .. } => true,
|
||||
StepNode::Block(nodes) => matches!(nodes.last(), Some(StepNode::If { .. })),
|
||||
_ => false,
|
||||
}
|
||||
}
|
||||
|
||||
/// Lower if-only StepTree to Normalized JoinModule using join_k tailcalls.
|
||||
///
|
||||
/// Scope: "if-as-last" only (no post-if). If it doesn't match, return Ok(None).
|
||||
pub fn lower(
|
||||
step_tree: &StepTree,
|
||||
env_layout: &EnvLayout,
|
||||
) -> Result<Option<(JoinModule, JoinFragmentMeta)>, String> {
|
||||
let (prefix_nodes, if_node) = match &step_tree.root {
|
||||
StepNode::If { .. } => (&[][..], &step_tree.root),
|
||||
StepNode::Block(nodes) => {
|
||||
let last = nodes.last();
|
||||
if matches!(last, Some(StepNode::If { .. })) {
|
||||
(&nodes[..nodes.len() - 1], nodes.last().unwrap())
|
||||
} else {
|
||||
return Ok(None);
|
||||
}
|
||||
}
|
||||
_ => return Ok(None),
|
||||
};
|
||||
|
||||
let if_node = match if_node {
|
||||
StepNode::If { .. } => if_node,
|
||||
_ => return Ok(None),
|
||||
};
|
||||
|
||||
let env_fields = env_layout.env_fields();
|
||||
|
||||
fn alloc_value_id(next_value_id: &mut u32) -> ValueId {
|
||||
let vid = ValueId(*next_value_id);
|
||||
*next_value_id += 1;
|
||||
vid
|
||||
}
|
||||
|
||||
let mut next_value_id: u32 = 1;
|
||||
|
||||
let alloc_env_params =
|
||||
|fields: &[String], next_value_id: &mut u32| -> Vec<ValueId> {
|
||||
fields
|
||||
.iter()
|
||||
.map(|_| alloc_value_id(next_value_id))
|
||||
.collect()
|
||||
};
|
||||
|
||||
let build_env_map = |fields: &[String], params: &[ValueId]| -> BTreeMap<String, ValueId> {
|
||||
let mut env = BTreeMap::new();
|
||||
for (name, vid) in fields.iter().zip(params.iter()) {
|
||||
env.insert(name.clone(), *vid);
|
||||
}
|
||||
env
|
||||
};
|
||||
|
||||
let collect_env_args = |fields: &[String], env: &BTreeMap<String, ValueId>| -> Result<Vec<ValueId>, String> {
|
||||
let mut args = Vec::with_capacity(fields.len());
|
||||
for name in fields {
|
||||
let vid = env.get(name).copied().ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/env_missing",
|
||||
&format!("env missing required field '{name}'"),
|
||||
"ensure env layout and env map are built from the same SSOT field list",
|
||||
)
|
||||
})?;
|
||||
args.push(vid);
|
||||
}
|
||||
Ok(args)
|
||||
};
|
||||
|
||||
// IDs (stable, dev-only)
|
||||
let main_id = JoinFuncId::new(0);
|
||||
let k_then_id = JoinFuncId::new(1);
|
||||
let k_else_id = JoinFuncId::new(2);
|
||||
let join_k_id = JoinFuncId::new(3);
|
||||
|
||||
// main(env)
|
||||
let main_params = alloc_env_params(&env_fields, &mut next_value_id);
|
||||
let mut env_main = build_env_map(&env_fields, &main_params);
|
||||
let mut main_func = JoinFunction::new(main_id, "main".to_string(), main_params);
|
||||
|
||||
// Lower prefix (pre-if) statements into main
|
||||
for n in prefix_nodes {
|
||||
match n {
|
||||
StepNode::Stmt { kind, .. } => match kind {
|
||||
StepStmtKind::Assign { target, value_ast } => {
|
||||
if LegacyLowerer::lower_assign_stmt(
|
||||
target,
|
||||
value_ast,
|
||||
&mut main_func.body,
|
||||
&mut next_value_id,
|
||||
&mut env_main,
|
||||
)
|
||||
.is_err()
|
||||
{
|
||||
return Ok(None);
|
||||
}
|
||||
}
|
||||
StepStmtKind::LocalDecl { .. } => {}
|
||||
_ => {
|
||||
return Ok(None);
|
||||
}
|
||||
},
|
||||
_ => {
|
||||
return Ok(None);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Extract return variable and branch bodies.
|
||||
fn split_branch_for_as_last(
|
||||
branch: &StepNode,
|
||||
) -> Result<(&[StepNode], &crate::mir::control_tree::step_tree::AstNodeHandle), String> {
|
||||
use crate::mir::control_tree::step_tree::StepNode;
|
||||
use crate::mir::control_tree::step_tree::StepStmtKind;
|
||||
use crate::mir::join_ir::lowering::error_tags;
|
||||
|
||||
match branch {
|
||||
StepNode::Stmt { kind, .. } => match kind {
|
||||
StepStmtKind::Return { value_ast } => {
|
||||
let ast_handle = value_ast.as_ref().ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/branch_return_void",
|
||||
"branch return must return a variable (not void)",
|
||||
"use `return x` in both then/else branches",
|
||||
)
|
||||
})?;
|
||||
Ok((&[][..], ast_handle))
|
||||
}
|
||||
_ => Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/branch_not_return",
|
||||
"branch must end with return",
|
||||
"use `return x` in both then/else branches",
|
||||
)),
|
||||
},
|
||||
StepNode::Block(nodes) => {
|
||||
let last = nodes.last().ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/branch_empty",
|
||||
"branch is empty",
|
||||
"add `return x` as the last statement of the branch",
|
||||
)
|
||||
})?;
|
||||
match last {
|
||||
StepNode::Stmt { kind, .. } => match kind {
|
||||
StepStmtKind::Return { value_ast } => {
|
||||
let ast_handle = value_ast.as_ref().ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/branch_return_void",
|
||||
"branch return must return a variable (not void)",
|
||||
"use `return x` in both then/else branches",
|
||||
)
|
||||
})?;
|
||||
Ok((&nodes[..nodes.len() - 1], ast_handle))
|
||||
}
|
||||
_ => Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/branch_not_return",
|
||||
"branch must end with return",
|
||||
"add `return x` as the last statement of the branch",
|
||||
)),
|
||||
},
|
||||
_ => Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/branch_last_not_stmt",
|
||||
"branch last node must be a statement return",
|
||||
"ensure the branch ends with `return x`",
|
||||
)),
|
||||
}
|
||||
}
|
||||
_ => Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/branch_node_unsupported",
|
||||
"unsupported branch node",
|
||||
"Phase 129-B supports only Block/Return branches",
|
||||
)),
|
||||
}
|
||||
}
|
||||
|
||||
fn extract_return_var_name(ast_handle: &crate::mir::control_tree::step_tree::AstNodeHandle) -> Result<String, String> {
|
||||
use crate::ast::ASTNode;
|
||||
use crate::mir::join_ir::lowering::error_tags;
|
||||
match ast_handle.0.as_ref() {
|
||||
ASTNode::Variable { name, .. } => Ok(name.clone()),
|
||||
_ => Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/return_expr_unsupported",
|
||||
"branch return expression must be a variable",
|
||||
"use `return x` (variable) in both then/else branches",
|
||||
)),
|
||||
}
|
||||
}
|
||||
|
||||
let (cond_ast, then_branch, else_branch) = match if_node {
|
||||
StepNode::If {
|
||||
cond_ast,
|
||||
then_branch,
|
||||
else_branch,
|
||||
..
|
||||
} => (cond_ast, then_branch.as_ref(), else_branch.as_deref()),
|
||||
_ => unreachable!(),
|
||||
};
|
||||
|
||||
let else_branch = match else_branch {
|
||||
Some(b) => b,
|
||||
None => return Ok(None),
|
||||
};
|
||||
|
||||
let (then_prefix, then_ret_ast) = match split_branch_for_as_last(then_branch) {
|
||||
Ok(v) => v,
|
||||
Err(_msg) => return Ok(None),
|
||||
};
|
||||
let (else_prefix, else_ret_ast) = match split_branch_for_as_last(else_branch) {
|
||||
Ok(v) => v,
|
||||
Err(_msg) => return Ok(None),
|
||||
};
|
||||
|
||||
let then_ret_var = match extract_return_var_name(then_ret_ast) {
|
||||
Ok(v) => v,
|
||||
Err(_msg) => return Ok(None),
|
||||
};
|
||||
let else_ret_var = match extract_return_var_name(else_ret_ast) {
|
||||
Ok(v) => v,
|
||||
Err(_msg) => return Ok(None),
|
||||
};
|
||||
|
||||
if then_ret_var != else_ret_var {
|
||||
return Ok(None);
|
||||
}
|
||||
|
||||
let ret_var = then_ret_var;
|
||||
if !env_layout.writes.iter().any(|w| w == &ret_var) {
|
||||
return Ok(None);
|
||||
}
|
||||
|
||||
// join_k(env_phi): return env_phi[ret_var]
|
||||
let join_k_params = alloc_env_params(&env_fields, &mut next_value_id);
|
||||
let env_join_k = build_env_map(&env_fields, &join_k_params);
|
||||
let ret_vid = env_join_k.get(&ret_var).copied().ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/ret_vid_missing",
|
||||
"return variable not found in join_k env",
|
||||
"ensure env layout includes the return variable in writes",
|
||||
)
|
||||
})?;
|
||||
let mut join_k_func = JoinFunction::new(join_k_id, "join_k".to_string(), join_k_params);
|
||||
join_k_func.body.push(JoinInst::Ret { value: Some(ret_vid) });
|
||||
|
||||
// k_then(env_in): <prefix> ; tailcall join_k(env_out)
|
||||
let then_params = alloc_env_params(&env_fields, &mut next_value_id);
|
||||
let mut env_then = build_env_map(&env_fields, &then_params);
|
||||
let mut then_func = JoinFunction::new(k_then_id, "k_then".to_string(), then_params);
|
||||
for n in then_prefix {
|
||||
match n {
|
||||
StepNode::Stmt { kind, .. } => match kind {
|
||||
StepStmtKind::Assign { target, value_ast } => {
|
||||
if LegacyLowerer::lower_assign_stmt(
|
||||
target,
|
||||
value_ast,
|
||||
&mut then_func.body,
|
||||
&mut next_value_id,
|
||||
&mut env_then,
|
||||
)
|
||||
.is_err()
|
||||
{
|
||||
return Ok(None);
|
||||
}
|
||||
}
|
||||
StepStmtKind::LocalDecl { .. } => {}
|
||||
_ => {
|
||||
return Ok(None);
|
||||
}
|
||||
},
|
||||
_ => {
|
||||
return Ok(None);
|
||||
}
|
||||
}
|
||||
}
|
||||
let then_args = collect_env_args(&env_fields, &env_then)?;
|
||||
then_func.body.push(JoinInst::Call {
|
||||
func: join_k_id,
|
||||
args: then_args,
|
||||
k_next: None,
|
||||
dst: None,
|
||||
});
|
||||
|
||||
// k_else(env_in): <prefix> ; tailcall join_k(env_out)
|
||||
let else_params = alloc_env_params(&env_fields, &mut next_value_id);
|
||||
let mut env_else = build_env_map(&env_fields, &else_params);
|
||||
let mut else_func = JoinFunction::new(k_else_id, "k_else".to_string(), else_params);
|
||||
for n in else_prefix {
|
||||
match n {
|
||||
StepNode::Stmt { kind, .. } => match kind {
|
||||
StepStmtKind::Assign { target, value_ast } => {
|
||||
if LegacyLowerer::lower_assign_stmt(
|
||||
target,
|
||||
value_ast,
|
||||
&mut else_func.body,
|
||||
&mut next_value_id,
|
||||
&mut env_else,
|
||||
)
|
||||
.is_err()
|
||||
{
|
||||
return Ok(None);
|
||||
}
|
||||
}
|
||||
StepStmtKind::LocalDecl { .. } => {}
|
||||
_ => {
|
||||
return Ok(None);
|
||||
}
|
||||
},
|
||||
_ => {
|
||||
return Ok(None);
|
||||
}
|
||||
}
|
||||
}
|
||||
let else_args = collect_env_args(&env_fields, &env_else)?;
|
||||
else_func.body.push(JoinInst::Call {
|
||||
func: join_k_id,
|
||||
args: else_args,
|
||||
k_next: None,
|
||||
dst: None,
|
||||
});
|
||||
|
||||
// main: cond compare + conditional jump to k_then, else to k_else
|
||||
let (lhs_var, op, rhs_literal) = LegacyLowerer::parse_minimal_compare(&cond_ast.0)?;
|
||||
let lhs_vid = env_main.get(&lhs_var).copied().ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/cond_lhs_missing",
|
||||
&format!("condition lhs var '{lhs_var}' not found in env"),
|
||||
"ensure the if condition uses a variable from writes or captured inputs",
|
||||
)
|
||||
})?;
|
||||
let rhs_vid = alloc_value_id(&mut next_value_id);
|
||||
main_func.body.push(JoinInst::Compute(MirLikeInst::Const {
|
||||
dst: rhs_vid,
|
||||
value: ConstValue::Integer(rhs_literal),
|
||||
}));
|
||||
let cond_vid = alloc_value_id(&mut next_value_id);
|
||||
main_func.body.push(JoinInst::Compute(MirLikeInst::Compare {
|
||||
dst: cond_vid,
|
||||
op,
|
||||
lhs: lhs_vid,
|
||||
rhs: rhs_vid,
|
||||
}));
|
||||
|
||||
let main_args = collect_env_args(&env_fields, &env_main)?;
|
||||
main_func.body.push(JoinInst::Jump {
|
||||
cont: k_then_id.as_cont(),
|
||||
args: main_args.clone(),
|
||||
cond: Some(cond_vid),
|
||||
});
|
||||
main_func.body.push(JoinInst::Jump {
|
||||
cont: k_else_id.as_cont(),
|
||||
args: main_args,
|
||||
cond: None,
|
||||
});
|
||||
|
||||
// Build module
|
||||
let mut module = JoinModule::new();
|
||||
module.add_function(main_func);
|
||||
module.add_function(then_func);
|
||||
module.add_function(else_func);
|
||||
module.add_function(join_k_func);
|
||||
module.entry = Some(main_id);
|
||||
module.mark_normalized();
|
||||
|
||||
Ok(Some((module, JoinFragmentMeta::empty())))
|
||||
}
|
||||
}
|
||||
488
src/mir/control_tree/normalized_shadow/legacy/mod.rs
Normal file
488
src/mir/control_tree/normalized_shadow/legacy/mod.rs
Normal file
@ -0,0 +1,488 @@
|
||||
//! Phase 123-128 legacy lowering path (kept for compatibility)
|
||||
|
||||
use crate::mir::control_tree::normalized_shadow::env_layout::EnvLayout;
|
||||
use crate::mir::control_tree::step_tree::StepTree;
|
||||
use crate::mir::control_tree::step_tree_contract_box::StepTreeContract;
|
||||
use crate::mir::join_ir::lowering::carrier_info::JoinFragmentMeta;
|
||||
use crate::mir::join_ir::{CompareOp, JoinFunction, JoinFuncId, JoinInst, JoinModule, MirLikeInst};
|
||||
use crate::mir::ValueId;
|
||||
use std::collections::BTreeMap;
|
||||
|
||||
pub struct LegacyLowerer;
|
||||
|
||||
impl LegacyLowerer {
|
||||
/// Lower if-only StepTree to Normalized JoinModule (Phase 123-128 legacy path)
|
||||
///
|
||||
/// Returns Ok(None) when unsupported patterns are encountered.
|
||||
pub fn lower_if_only_to_normalized(
|
||||
step_tree: &StepTree,
|
||||
env_layout: &EnvLayout,
|
||||
) -> Result<Option<(JoinModule, JoinFragmentMeta)>, String> {
|
||||
let main_func_id = JoinFuncId::new(0);
|
||||
|
||||
// Phase 125 P2: writes 用の ValueId 生成
|
||||
let mut next_value_id = 1;
|
||||
let writes_params: Vec<ValueId> = env_layout
|
||||
.writes
|
||||
.iter()
|
||||
.map(|_| {
|
||||
let vid = ValueId(next_value_id);
|
||||
next_value_id += 1;
|
||||
vid
|
||||
})
|
||||
.collect();
|
||||
|
||||
// Phase 129-B: inputs 用の ValueId 生成(writes + inputs が env params のSSOT)
|
||||
let inputs_params: Vec<ValueId> = env_layout
|
||||
.inputs
|
||||
.iter()
|
||||
.map(|_| {
|
||||
let vid = ValueId(next_value_id);
|
||||
next_value_id += 1;
|
||||
vid
|
||||
})
|
||||
.collect();
|
||||
|
||||
// Phase 125 P2: env マッピング(writes + inputs)
|
||||
let mut env: BTreeMap<String, ValueId> = BTreeMap::new();
|
||||
for (name, vid) in env_layout.writes.iter().zip(writes_params.iter()) {
|
||||
env.insert(name.clone(), *vid);
|
||||
}
|
||||
for (name, vid) in env_layout.inputs.iter().zip(inputs_params.iter()) {
|
||||
env.insert(name.clone(), *vid);
|
||||
}
|
||||
|
||||
// Phase 129-B: 関数パラメータは writes + inputs(env params SSOT)
|
||||
let mut env_params = writes_params;
|
||||
env_params.extend(inputs_params);
|
||||
|
||||
// main 関数生成
|
||||
let mut main_func = JoinFunction::new(
|
||||
main_func_id,
|
||||
"main".to_string(),
|
||||
env_params.clone(),
|
||||
);
|
||||
|
||||
// Phase 123-128: Return node lowering
|
||||
// If Phase 123-128 patterns are not supported, return Ok(None)
|
||||
match Self::lower_return_from_tree(
|
||||
&step_tree.root,
|
||||
&mut main_func.body,
|
||||
&mut next_value_id,
|
||||
&mut env,
|
||||
&step_tree.contract,
|
||||
) {
|
||||
Ok(()) => {
|
||||
// Success - continue
|
||||
}
|
||||
Err(msg)
|
||||
if msg.starts_with("[phase123/")
|
||||
|| msg.starts_with("[phase124/")
|
||||
|| msg.starts_with("[phase125/")
|
||||
|| msg.starts_with("[phase128/") =>
|
||||
{
|
||||
// Phase 123-128 limitation - out of scope
|
||||
return Ok(None);
|
||||
}
|
||||
Err(msg) => {
|
||||
// Real error - propagate
|
||||
return Err(msg);
|
||||
}
|
||||
}
|
||||
|
||||
// JoinModule 構築
|
||||
let mut module = JoinModule::new();
|
||||
module.add_function(main_func);
|
||||
module.entry = Some(main_func_id);
|
||||
module.mark_normalized();
|
||||
|
||||
// JoinFragmentMeta 生成(最小)
|
||||
let meta = JoinFragmentMeta::empty();
|
||||
|
||||
Ok(Some((module, meta)))
|
||||
}
|
||||
|
||||
/// Phase 123-128 P1-P3: Lower node from StepTree
|
||||
pub fn lower_return_from_tree(
|
||||
node: &crate::mir::control_tree::step_tree::StepNode,
|
||||
body: &mut Vec<crate::mir::join_ir::JoinInst>,
|
||||
next_value_id: &mut u32,
|
||||
env: &mut BTreeMap<String, ValueId>,
|
||||
contract: &StepTreeContract,
|
||||
) -> Result<(), String> {
|
||||
use crate::mir::control_tree::step_tree::{StepNode, StepStmtKind};
|
||||
use crate::mir::join_ir::JoinInst;
|
||||
|
||||
match node {
|
||||
StepNode::Block(nodes) => {
|
||||
// Process nodes in order
|
||||
for n in nodes {
|
||||
match n {
|
||||
StepNode::Stmt {
|
||||
kind: StepStmtKind::Assign { target, value_ast },
|
||||
..
|
||||
} => {
|
||||
// Phase 128: Process assign statement
|
||||
Self::lower_assign_stmt(target, value_ast, body, next_value_id, env)?;
|
||||
// Continue to next node
|
||||
}
|
||||
StepNode::Stmt {
|
||||
kind: StepStmtKind::Return { value_ast },
|
||||
..
|
||||
} => {
|
||||
return Self::lower_return_value(value_ast, body, next_value_id, env, contract);
|
||||
}
|
||||
StepNode::If { .. } => {
|
||||
// Phase 123 P3: Lower If node
|
||||
return Self::lower_if_node(n, body, next_value_id, env, contract);
|
||||
}
|
||||
_ => {
|
||||
// Other nodes not yet supported
|
||||
}
|
||||
}
|
||||
}
|
||||
// No return found - default to void
|
||||
body.push(JoinInst::Ret { value: None });
|
||||
Ok(())
|
||||
}
|
||||
StepNode::Stmt {
|
||||
kind: StepStmtKind::Return { value_ast },
|
||||
..
|
||||
} => Self::lower_return_value(value_ast, body, next_value_id, env, contract),
|
||||
StepNode::If { .. } => {
|
||||
// Phase 123 P3: Lower If node
|
||||
Self::lower_if_node(node, body, next_value_id, env, contract)
|
||||
}
|
||||
_ => {
|
||||
// No return in tree - default to void
|
||||
body.push(JoinInst::Ret { value: None });
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Phase 128: Lower assign statement (int literal only)
|
||||
pub fn lower_assign_stmt(
|
||||
target: &Option<String>,
|
||||
value_ast: &Option<crate::mir::control_tree::step_tree::AstNodeHandle>,
|
||||
body: &mut Vec<crate::mir::join_ir::JoinInst>,
|
||||
next_value_id: &mut u32,
|
||||
env: &mut BTreeMap<String, ValueId>,
|
||||
) -> Result<(), String> {
|
||||
use crate::ast::{ASTNode, LiteralValue};
|
||||
use crate::mir::join_ir::{ConstValue, JoinInst, MirLikeInst};
|
||||
|
||||
// Check target
|
||||
let target_name = target
|
||||
.as_ref()
|
||||
.ok_or_else(|| "[phase128/assign/target] Assign target must be a variable".to_string())?;
|
||||
|
||||
// Check value_ast
|
||||
let value_ast = value_ast.as_ref().ok_or_else(|| {
|
||||
"[phase128/assign/value] Assign value AST is missing".to_string()
|
||||
})?;
|
||||
|
||||
// Parse value - Phase 128: int literal only
|
||||
match value_ast.0.as_ref() {
|
||||
ASTNode::Literal {
|
||||
value: LiteralValue::Integer(i),
|
||||
..
|
||||
} => {
|
||||
// Generate Const instruction
|
||||
let dst_vid = ValueId(*next_value_id);
|
||||
*next_value_id += 1;
|
||||
|
||||
body.push(JoinInst::Compute(MirLikeInst::Const {
|
||||
dst: dst_vid,
|
||||
value: ConstValue::Integer(*i),
|
||||
}));
|
||||
|
||||
// Update env
|
||||
env.insert(target_name.clone(), dst_vid);
|
||||
|
||||
Ok(())
|
||||
}
|
||||
_ => {
|
||||
// Phase 128 limitation: only int literal supported
|
||||
Err(format!(
|
||||
"[phase128/assign/unsupported] Phase128 supports int literal only Hint: Assign RHS must be an integer literal (e.g., x = 42)"
|
||||
))
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Phase 123-128 P3: Lower If node with minimal compare
|
||||
pub fn lower_if_node(
|
||||
node: &crate::mir::control_tree::step_tree::StepNode,
|
||||
body: &mut Vec<crate::mir::join_ir::JoinInst>,
|
||||
next_value_id: &mut u32,
|
||||
env: &mut BTreeMap<String, ValueId>,
|
||||
contract: &StepTreeContract,
|
||||
) -> Result<(), String> {
|
||||
use crate::mir::control_tree::step_tree::StepNode;
|
||||
use crate::mir::join_ir::{ConstValue, JoinInst, MirLikeInst};
|
||||
|
||||
if let StepNode::If {
|
||||
cond_ast,
|
||||
then_branch,
|
||||
else_branch,
|
||||
..
|
||||
} = node
|
||||
{
|
||||
let ast = &cond_ast.0;
|
||||
|
||||
// Phase 123 P3: Parse minimal binary comparison only
|
||||
let (_lhs_var, op, rhs_literal) = Self::parse_minimal_compare(ast)?;
|
||||
|
||||
// Generate Compare instruction
|
||||
// 1. Load/create lhs variable (for now, assume it's a parameter)
|
||||
// For Phase 123 minimal: we'll just create a load instruction placeholder
|
||||
// This is a simplification - real implementation would need variable resolution
|
||||
let lhs_vid = ValueId(*next_value_id);
|
||||
*next_value_id += 1;
|
||||
|
||||
// For now, emit a const for the variable (placeholder)
|
||||
// Real implementation in Phase 124 will use reads facts
|
||||
body.push(JoinInst::Compute(MirLikeInst::Const {
|
||||
dst: lhs_vid,
|
||||
value: ConstValue::Integer(0), // Placeholder
|
||||
}));
|
||||
|
||||
// 2. Create constant for rhs literal
|
||||
let rhs_vid = ValueId(*next_value_id);
|
||||
*next_value_id += 1;
|
||||
body.push(JoinInst::Compute(MirLikeInst::Const {
|
||||
dst: rhs_vid,
|
||||
value: ConstValue::Integer(rhs_literal),
|
||||
}));
|
||||
|
||||
// 3. Generate Compare instruction
|
||||
let cond_vid = ValueId(*next_value_id);
|
||||
*next_value_id += 1;
|
||||
body.push(JoinInst::Compute(MirLikeInst::Compare {
|
||||
dst: cond_vid,
|
||||
op,
|
||||
lhs: lhs_vid,
|
||||
rhs: rhs_vid,
|
||||
}));
|
||||
|
||||
// Phase 123 P3: Verify then/else branches contain only Return(Integer literal)
|
||||
Self::verify_branch_is_return_literal(then_branch)?;
|
||||
if let Some(else_br) = else_branch {
|
||||
Self::verify_branch_is_return_literal(else_br)?;
|
||||
}
|
||||
|
||||
// For Phase 123-124, we generate a simplified structure:
|
||||
// The actual branching logic will be added in future phases
|
||||
// For now, just emit the then branch return
|
||||
Self::lower_return_from_tree(then_branch, body, next_value_id, env, contract)?;
|
||||
|
||||
Ok(())
|
||||
} else {
|
||||
Err("[phase123/if/internal] Expected If node".to_string())
|
||||
}
|
||||
}
|
||||
|
||||
/// Parse minimal binary comparison: Variable op Integer
|
||||
///
|
||||
/// Returns: (variable_name, compare_op, integer_value)
|
||||
pub fn parse_minimal_compare(
|
||||
ast: &crate::ast::ASTNode,
|
||||
) -> Result<(String, CompareOp, i64), String> {
|
||||
use crate::ast::{ASTNode, BinaryOperator, LiteralValue};
|
||||
|
||||
match ast {
|
||||
ASTNode::BinaryOp {
|
||||
operator,
|
||||
left,
|
||||
right,
|
||||
..
|
||||
} => {
|
||||
// Phase 123: Only support Variable on left, Integer literal on right
|
||||
let var_name = match &**left {
|
||||
ASTNode::Variable { name, .. } => name.clone(),
|
||||
_ => {
|
||||
return Err(format!(
|
||||
"[phase123/if/compare_lhs_unsupported] Phase 123 only supports Variable on left side of comparison. Hint: Use simple variable comparison or wait for Phase 124"
|
||||
));
|
||||
}
|
||||
};
|
||||
|
||||
let int_value = match &**right {
|
||||
ASTNode::Literal {
|
||||
value: LiteralValue::Integer(i),
|
||||
..
|
||||
} => *i,
|
||||
_ => {
|
||||
return Err(format!(
|
||||
"[phase123/if/compare_rhs_unsupported] Phase 123 only supports Integer literal on right side of comparison. Hint: Use integer literal or wait for Phase 124"
|
||||
));
|
||||
}
|
||||
};
|
||||
|
||||
let compare_op = match operator {
|
||||
BinaryOperator::Equal => CompareOp::Eq,
|
||||
BinaryOperator::NotEqual => CompareOp::Ne,
|
||||
BinaryOperator::Less => CompareOp::Lt,
|
||||
BinaryOperator::LessEqual => CompareOp::Le,
|
||||
BinaryOperator::Greater => CompareOp::Gt,
|
||||
BinaryOperator::GreaterEqual => CompareOp::Ge,
|
||||
_ => {
|
||||
return Err(format!(
|
||||
"[phase123/if/compare_op_unsupported] Phase 123 only supports comparison operators (==, !=, <, <=, >, >=). Hint: Use comparison operator or wait for Phase 124"
|
||||
));
|
||||
}
|
||||
};
|
||||
|
||||
Ok((var_name, compare_op, int_value))
|
||||
}
|
||||
_ => Err(format!(
|
||||
"[phase123/if/cond_unsupported] Phase 123 only supports binary comparisons. Hint: Use simple comparison (var == literal) or wait for Phase 124"
|
||||
)),
|
||||
}
|
||||
}
|
||||
|
||||
/// Verify branch contains only Return(Integer literal)
|
||||
pub fn verify_branch_is_return_literal(
|
||||
branch: &crate::mir::control_tree::step_tree::StepNode,
|
||||
) -> Result<(), String> {
|
||||
use crate::ast::{ASTNode, LiteralValue};
|
||||
use crate::mir::control_tree::step_tree::{StepNode, StepStmtKind};
|
||||
|
||||
match branch {
|
||||
StepNode::Stmt {
|
||||
kind: StepStmtKind::Return { value_ast },
|
||||
..
|
||||
} => {
|
||||
if let Some(ast_handle) = value_ast {
|
||||
let ast = &ast_handle.0;
|
||||
if let ASTNode::Literal {
|
||||
value: LiteralValue::Integer(_),
|
||||
..
|
||||
} = &**ast
|
||||
{
|
||||
Ok(())
|
||||
} else {
|
||||
Err(format!(
|
||||
"[phase123/if/branch_return_not_int_literal] Phase 123 only supports Return(Integer literal) in then/else branches. Hint: Return integer literal only or wait for Phase 124"
|
||||
))
|
||||
}
|
||||
} else {
|
||||
Err(format!(
|
||||
"[phase123/if/branch_return_void] Phase 123 requires Return(Integer literal) in branches, not void return. Hint: Return integer literal or wait for Phase 124"
|
||||
))
|
||||
}
|
||||
}
|
||||
StepNode::Block(nodes) => {
|
||||
// Check first node only
|
||||
if nodes.is_empty() {
|
||||
return Err(format!(
|
||||
"[phase123/if/branch_empty] Phase 123 requires Return(Integer literal) in branches. Hint: Add return statement"
|
||||
));
|
||||
}
|
||||
Self::verify_branch_is_return_literal(&nodes[0])
|
||||
}
|
||||
_ => Err(format!(
|
||||
"[phase123/if/branch_not_return] Phase 123 only supports Return(Integer literal) in then/else branches. Hint: Use return statement with integer literal"
|
||||
)),
|
||||
}
|
||||
}
|
||||
|
||||
/// Phase 123-125 P1-P2-P3-P4: Lower return value
|
||||
pub fn lower_return_value(
|
||||
value_ast: &Option<crate::mir::control_tree::step_tree::AstNodeHandle>,
|
||||
body: &mut Vec<crate::mir::join_ir::JoinInst>,
|
||||
next_value_id: &mut u32,
|
||||
env: &BTreeMap<String, ValueId>,
|
||||
contract: &StepTreeContract,
|
||||
) -> Result<(), String> {
|
||||
use crate::ast::{ASTNode, LiteralValue};
|
||||
use crate::mir::join_ir::{ConstValue, JoinInst, MirLikeInst};
|
||||
|
||||
match value_ast {
|
||||
None => {
|
||||
body.push(JoinInst::Ret { value: None });
|
||||
Ok(())
|
||||
}
|
||||
Some(ast_handle) => {
|
||||
let ast = &ast_handle.0;
|
||||
match &**ast {
|
||||
ASTNode::Literal { value, .. } => match value {
|
||||
LiteralValue::Integer(i) => {
|
||||
// Phase 123 P1: Integer literal → Const + Ret(Some(vid))
|
||||
let const_vid = ValueId(*next_value_id);
|
||||
*next_value_id += 1;
|
||||
|
||||
// Generate Const instruction (wrapped in Compute)
|
||||
body.push(JoinInst::Compute(MirLikeInst::Const {
|
||||
dst: const_vid,
|
||||
value: ConstValue::Integer(*i),
|
||||
}));
|
||||
|
||||
// Generate Ret instruction
|
||||
body.push(JoinInst::Ret {
|
||||
value: Some(const_vid),
|
||||
});
|
||||
|
||||
Ok(())
|
||||
}
|
||||
_ => {
|
||||
// Phase 123: Other literals not supported
|
||||
Err(format!(
|
||||
"[phase123/return/literal_unsupported] Phase 123 only supports integer literals. Hint: Use integer literal or wait for Phase 124"
|
||||
))
|
||||
}
|
||||
},
|
||||
ASTNode::Variable { name, .. } => {
|
||||
// Phase 124-125 P3-P4: Variable return support (dev-only)
|
||||
// Check if variable is in env (writes + inputs)
|
||||
if let Some(&vid) = env.get(name) {
|
||||
// Phase 125 P4: Variable found in env (writes or inputs) - return it
|
||||
body.push(JoinInst::Ret { value: Some(vid) });
|
||||
Ok(())
|
||||
} else {
|
||||
// Phase 125 P4: Variable not in env - Fail-Fast with hint
|
||||
// Check if variable is in reads (potential input)
|
||||
let in_reads = contract.reads.contains(name);
|
||||
let in_writes = contract.writes.contains(name);
|
||||
|
||||
let hint = if in_reads && !in_writes {
|
||||
// Variable is read but not available as input
|
||||
format!(
|
||||
"Variable '{}' is read but not available from outer scope. \
|
||||
Hint: Pass as function parameter, add to pinned capture, or define before if",
|
||||
name
|
||||
)
|
||||
} else if in_writes {
|
||||
// Variable is written but not captured in env
|
||||
format!(
|
||||
"Variable '{}' is written but not captured in env. \
|
||||
Hint: Ensure writes are captured in env layout (Phase 125)",
|
||||
name
|
||||
)
|
||||
} else {
|
||||
// Not in reads or writes
|
||||
format!(
|
||||
"Variable '{}' not found in env. \
|
||||
Hint: Add to reads/writes contract or define before return",
|
||||
name
|
||||
)
|
||||
};
|
||||
|
||||
Err(format!(
|
||||
"[phase125/return/variable_missing] Variable '{}' not found in env. {}",
|
||||
name, hint
|
||||
))
|
||||
}
|
||||
}
|
||||
_ => {
|
||||
// Phase 123: Other expressions not supported
|
||||
Err(format!(
|
||||
"[phase123/return/expr_unsupported] Phase 123 only supports integer literals or variables. Hint: Use simple return or wait for future phases"
|
||||
))
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -31,9 +31,15 @@
|
||||
|
||||
pub mod builder;
|
||||
pub mod contracts;
|
||||
pub mod parity;
|
||||
pub mod normalized_verifier;
|
||||
pub mod env_layout;
|
||||
pub mod if_as_last_join_k;
|
||||
pub mod legacy;
|
||||
pub mod dev_pipeline;
|
||||
pub mod parity_contract;
|
||||
pub mod available_inputs_collector; // Phase 126: available_inputs SSOT
|
||||
|
||||
pub use builder::StepTreeNormalizedShadowLowererBox;
|
||||
pub use contracts::{CapabilityCheckResult, UnsupportedCapability};
|
||||
pub use parity::{MismatchKind, ShadowParityResult};
|
||||
pub use parity_contract::{MismatchKind, ShadowParityResult};
|
||||
pub use env_layout::EnvLayout;
|
||||
|
||||
170
src/mir/control_tree/normalized_shadow/normalized_verifier.rs
Normal file
170
src/mir/control_tree/normalized_shadow/normalized_verifier.rs
Normal file
@ -0,0 +1,170 @@
|
||||
//! Structural validation for Normalized shadow JoinModule (dev/strict)
|
||||
//!
|
||||
//! - Fail-Fast in strict mode with `freeze_with_hint`
|
||||
//! - No value parity; structure only
|
||||
|
||||
use crate::mir::join_ir::{JoinFuncId, JoinInst, JoinModule};
|
||||
use crate::mir::join_ir::lowering::error_tags;
|
||||
|
||||
/// Verify Normalized JoinModule structure emitted by the shadow lowerer.
|
||||
///
|
||||
/// ## Contract
|
||||
/// - Module phase must be Normalized
|
||||
/// - Entry exists and all functions share the same env arity
|
||||
/// - No IfMerge/NestedIfMerge (PHI is forbidden in Phase 129-B scope)
|
||||
/// - join_k tailcalls must target one function that ends with `Ret(Some)`
|
||||
pub fn verify_normalized_structure(
|
||||
module: &JoinModule,
|
||||
expected_env_fields: usize,
|
||||
) -> Result<(), String> {
|
||||
// Check phase
|
||||
if !module.is_normalized() {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/not_normalized",
|
||||
&format!("module phase is not Normalized: {:?}", module.phase),
|
||||
"ensure the shadow lowering marks module as Normalized",
|
||||
));
|
||||
}
|
||||
|
||||
if module.functions.is_empty() {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/no_functions",
|
||||
"no functions in module",
|
||||
"ensure the shadow lowering emits at least the entry function",
|
||||
));
|
||||
}
|
||||
|
||||
// Check entry point
|
||||
let entry_id = module.entry.ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/no_entry",
|
||||
"no entry point in module",
|
||||
"ensure the shadow lowering sets JoinModule.entry",
|
||||
)
|
||||
})?;
|
||||
|
||||
// Check entry function exists
|
||||
let entry_func = module.functions.get(&entry_id).ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/entry_missing",
|
||||
&format!("entry function {:?} not found", entry_id),
|
||||
"ensure the emitted module includes the entry function id",
|
||||
)
|
||||
})?;
|
||||
|
||||
// Env layout: writes + inputs (SSOT)
|
||||
if entry_func.params.len() != expected_env_fields {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/env_arity_mismatch",
|
||||
&format!(
|
||||
"env args mismatch: expected {}, got {}",
|
||||
expected_env_fields,
|
||||
entry_func.params.len()
|
||||
),
|
||||
"ensure env params are built from (writes + inputs) SSOT",
|
||||
));
|
||||
}
|
||||
|
||||
// All functions in this shadow module must share the same env param arity.
|
||||
for (fid, func) in &module.functions {
|
||||
if func.params.len() != expected_env_fields {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/env_arity_mismatch",
|
||||
&format!(
|
||||
"env args mismatch in {:?}: expected {}, got {}",
|
||||
fid,
|
||||
expected_env_fields,
|
||||
func.params.len()
|
||||
),
|
||||
"ensure all continuations share the same env layout (writes + inputs)",
|
||||
));
|
||||
}
|
||||
}
|
||||
|
||||
// PHI prohibition (Phase 129-B scope): no IfMerge/NestedIfMerge in shadow output.
|
||||
for (fid, func) in &module.functions {
|
||||
for inst in &func.body {
|
||||
if matches!(inst, JoinInst::IfMerge { .. } | JoinInst::NestedIfMerge { .. }) {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/phi_forbidden",
|
||||
&format!("PHI-like merge instruction found in {:?}", fid),
|
||||
"Phase 129-B join_k path forbids IfMerge/NestedIfMerge; use join_k tailcall merge instead",
|
||||
));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Detect join_k tailcall form (if present) and validate it.
|
||||
fn tailcall_target(func: &crate::mir::join_ir::JoinFunction) -> Option<(JoinFuncId, usize)> {
|
||||
match func.body.last()? {
|
||||
JoinInst::Call {
|
||||
func,
|
||||
args,
|
||||
k_next: None,
|
||||
dst: None,
|
||||
} => Some((*func, args.len())),
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
|
||||
let mut tailcall_targets: Vec<(JoinFuncId, usize)> = Vec::new();
|
||||
for func in module.functions.values() {
|
||||
if let Some((target, argc)) = tailcall_target(func) {
|
||||
tailcall_targets.push((target, argc));
|
||||
}
|
||||
}
|
||||
|
||||
if tailcall_targets.is_empty() {
|
||||
return Ok(());
|
||||
}
|
||||
|
||||
// join_k merge should have at least two branch continuations tailcalling the same target.
|
||||
if tailcall_targets.len() < 2 {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/tailcall_count",
|
||||
&format!(
|
||||
"join_k tailcall form requires >=2 tailcalls, got {}",
|
||||
tailcall_targets.len()
|
||||
),
|
||||
"ensure both then/else branches tailcall join_k as the last instruction",
|
||||
));
|
||||
}
|
||||
|
||||
let first_target = tailcall_targets[0].0;
|
||||
for (target, argc) in &tailcall_targets {
|
||||
if *target != first_target {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/tailcall_target_mismatch",
|
||||
"tailcalls do not target a single join_k function",
|
||||
"ensure then/else both tailcall the same join_k function id",
|
||||
));
|
||||
}
|
||||
if *argc != expected_env_fields {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/tailcall_arg_arity_mismatch",
|
||||
&format!(
|
||||
"tailcall env arg count mismatch: expected {}, got {}",
|
||||
expected_env_fields, argc
|
||||
),
|
||||
"ensure join_k is called with the full env fields list (writes + inputs)",
|
||||
));
|
||||
}
|
||||
}
|
||||
|
||||
let join_k_func = module.functions.get(&first_target).ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/join_k_missing",
|
||||
"tailcall target join_k function not found in module",
|
||||
"ensure join_k is registered in JoinModule.functions",
|
||||
)
|
||||
})?;
|
||||
|
||||
match join_k_func.body.last() {
|
||||
Some(JoinInst::Ret { value: Some(_) }) => Ok(()),
|
||||
_ => Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/join_k_not_ret",
|
||||
"join_k must end with Ret(Some(value))",
|
||||
"ensure join_k returns the merged env variable and has no post-if continuation in Phase 129-B",
|
||||
)),
|
||||
}
|
||||
}
|
||||
@ -1,380 +0,0 @@
|
||||
//! Phase 121: Parity verification between shadow and existing router
|
||||
//!
|
||||
//! ## Responsibility
|
||||
//!
|
||||
//! - Compare exit contracts and writes between shadow and existing paths
|
||||
//! - Log mismatches in dev mode
|
||||
//! - Fail-fast in strict mode with `freeze_with_hint`
|
||||
//!
|
||||
//! ## Comparison Strategy (Minimal & Robust)
|
||||
//!
|
||||
//! - Compare structural contracts (exits, writes)
|
||||
//! - Do NOT compare actual values (too fragile)
|
||||
//! - Focus on "did we extract the same information?"
|
||||
|
||||
use crate::mir::control_tree::step_tree_contract_box::StepTreeContract;
|
||||
/// Mismatch classification
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
||||
pub enum MismatchKind {
|
||||
/// Exit contract mismatch
|
||||
ExitMismatch,
|
||||
/// Writes contract mismatch
|
||||
WritesMismatch,
|
||||
/// Unsupported kind (should not happen for if-only)
|
||||
UnsupportedKind,
|
||||
}
|
||||
|
||||
impl MismatchKind {
|
||||
/// Get human-readable description
|
||||
pub fn description(&self) -> &'static str {
|
||||
match self {
|
||||
MismatchKind::ExitMismatch => "exit contract mismatch",
|
||||
MismatchKind::WritesMismatch => "writes contract mismatch",
|
||||
MismatchKind::UnsupportedKind => "unsupported pattern for parity check",
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Result of parity check
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct ShadowParityResult {
|
||||
/// Whether parity check passed
|
||||
pub ok: bool,
|
||||
/// Mismatch kind if not ok
|
||||
pub mismatch_kind: Option<MismatchKind>,
|
||||
/// Hint for debugging (must be non-empty if not ok)
|
||||
pub hint: Option<String>,
|
||||
}
|
||||
|
||||
impl ShadowParityResult {
|
||||
/// Create successful parity result
|
||||
pub fn ok() -> Self {
|
||||
Self {
|
||||
ok: true,
|
||||
mismatch_kind: None,
|
||||
hint: None,
|
||||
}
|
||||
}
|
||||
|
||||
/// Create failed parity result with hint
|
||||
pub fn mismatch(kind: MismatchKind, hint: String) -> Self {
|
||||
assert!(!hint.is_empty(), "hint must not be empty for mismatch");
|
||||
Self {
|
||||
ok: false,
|
||||
mismatch_kind: Some(kind),
|
||||
hint: Some(hint),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Compare exit contracts between shadow and existing path
|
||||
///
|
||||
/// ## Contract
|
||||
///
|
||||
/// - Input: Two `StepTreeContract` instances (shadow vs existing)
|
||||
/// - Compares `exits` field (BTreeSet for deterministic ordering)
|
||||
/// - Returns mismatch with specific hint if different
|
||||
pub fn compare_exit_contracts(
|
||||
shadow: &StepTreeContract,
|
||||
existing: &StepTreeContract,
|
||||
) -> ShadowParityResult {
|
||||
if shadow.exits != existing.exits {
|
||||
let hint = format!(
|
||||
"exit mismatch: shadow={:?}, existing={:?}",
|
||||
shadow.exits, existing.exits
|
||||
);
|
||||
return ShadowParityResult::mismatch(MismatchKind::ExitMismatch, hint);
|
||||
}
|
||||
ShadowParityResult::ok()
|
||||
}
|
||||
|
||||
/// Compare writes contracts between shadow and existing path
|
||||
///
|
||||
/// ## Contract
|
||||
///
|
||||
/// - Input: Two `StepTreeContract` instances (shadow vs existing)
|
||||
/// - Compares `writes` field (BTreeSet for deterministic ordering)
|
||||
/// - Returns mismatch with specific hint if different
|
||||
pub fn compare_writes_contracts(
|
||||
shadow: &StepTreeContract,
|
||||
existing: &StepTreeContract,
|
||||
) -> ShadowParityResult {
|
||||
if shadow.writes != existing.writes {
|
||||
let hint = format!(
|
||||
"writes mismatch: shadow={:?}, existing={:?}",
|
||||
shadow.writes, existing.writes
|
||||
);
|
||||
return ShadowParityResult::mismatch(MismatchKind::WritesMismatch, hint);
|
||||
}
|
||||
ShadowParityResult::ok()
|
||||
}
|
||||
|
||||
/// Full parity check (exits + writes)
|
||||
///
|
||||
/// ## Contract
|
||||
///
|
||||
/// - Combines exit and writes checks
|
||||
/// - Returns first mismatch found
|
||||
/// - Returns ok only if all checks pass
|
||||
pub fn check_full_parity(
|
||||
shadow: &StepTreeContract,
|
||||
existing: &StepTreeContract,
|
||||
) -> ShadowParityResult {
|
||||
// Check exits first
|
||||
let exit_result = compare_exit_contracts(shadow, existing);
|
||||
if !exit_result.ok {
|
||||
return exit_result;
|
||||
}
|
||||
|
||||
// Check writes second
|
||||
let writes_result = compare_writes_contracts(shadow, existing);
|
||||
if !writes_result.ok {
|
||||
return writes_result;
|
||||
}
|
||||
|
||||
ShadowParityResult::ok()
|
||||
}
|
||||
|
||||
/// Phase 122: Verify Normalized JoinModule structure
|
||||
///
|
||||
/// ## Contract
|
||||
///
|
||||
/// - Checks function count, continuation count, tail-call form, env args
|
||||
/// - Does NOT check actual execution (RC comparison is optional)
|
||||
/// - Returns Err(freeze_with_hint) if structure is invalid
|
||||
pub fn verify_normalized_structure(
|
||||
module: &crate::mir::join_ir::JoinModule,
|
||||
expected_env_fields: usize,
|
||||
) -> Result<(), String> {
|
||||
use crate::mir::join_ir::{JoinFuncId, JoinInst};
|
||||
use crate::mir::join_ir::lowering::error_tags;
|
||||
|
||||
// Check phase
|
||||
if !module.is_normalized() {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/not_normalized",
|
||||
&format!("module phase is not Normalized: {:?}", module.phase),
|
||||
"ensure the shadow lowering marks module as Normalized",
|
||||
));
|
||||
}
|
||||
|
||||
if module.functions.is_empty() {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/no_functions",
|
||||
"no functions in module",
|
||||
"ensure the shadow lowering emits at least the entry function",
|
||||
));
|
||||
}
|
||||
|
||||
// Check entry point
|
||||
let entry_id = module.entry.ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/no_entry",
|
||||
"no entry point in module",
|
||||
"ensure the shadow lowering sets JoinModule.entry",
|
||||
)
|
||||
})?;
|
||||
|
||||
// Check entry function exists
|
||||
let entry_func = module.functions.get(&entry_id).ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/entry_missing",
|
||||
&format!("entry function {:?} not found", entry_id),
|
||||
"ensure the emitted module includes the entry function id",
|
||||
)
|
||||
})?;
|
||||
|
||||
// Env layout: writes + inputs (SSOT)
|
||||
if entry_func.params.len() != expected_env_fields {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/env_arity_mismatch",
|
||||
&format!(
|
||||
"env args mismatch: expected {}, got {}",
|
||||
expected_env_fields,
|
||||
entry_func.params.len()
|
||||
),
|
||||
"ensure env params are built from (writes + inputs) SSOT",
|
||||
));
|
||||
}
|
||||
|
||||
// All functions in this shadow module must share the same env param arity.
|
||||
for (fid, func) in &module.functions {
|
||||
if func.params.len() != expected_env_fields {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/env_arity_mismatch",
|
||||
&format!(
|
||||
"env args mismatch in {:?}: expected {}, got {}",
|
||||
fid,
|
||||
expected_env_fields,
|
||||
func.params.len()
|
||||
),
|
||||
"ensure all continuations share the same env layout (writes + inputs)",
|
||||
));
|
||||
}
|
||||
}
|
||||
|
||||
// PHI prohibition (Phase 129-B scope): no IfMerge/NestedIfMerge in shadow output.
|
||||
for (fid, func) in &module.functions {
|
||||
for inst in &func.body {
|
||||
if matches!(inst, JoinInst::IfMerge { .. } | JoinInst::NestedIfMerge { .. }) {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/phi_forbidden",
|
||||
&format!("PHI-like merge instruction found in {:?}", fid),
|
||||
"Phase 129-B join_k path forbids IfMerge/NestedIfMerge; use join_k tailcall merge instead",
|
||||
));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Detect join_k tailcall form (if present) and validate it.
|
||||
fn tailcall_target(func: &crate::mir::join_ir::JoinFunction) -> Option<(JoinFuncId, usize)> {
|
||||
match func.body.last()? {
|
||||
JoinInst::Call {
|
||||
func,
|
||||
args,
|
||||
k_next: None,
|
||||
dst: None,
|
||||
} => Some((*func, args.len())),
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
|
||||
let mut tailcall_targets: Vec<(JoinFuncId, usize)> = Vec::new();
|
||||
for func in module.functions.values() {
|
||||
if let Some((target, argc)) = tailcall_target(func) {
|
||||
tailcall_targets.push((target, argc));
|
||||
}
|
||||
}
|
||||
|
||||
if tailcall_targets.is_empty() {
|
||||
return Ok(());
|
||||
}
|
||||
|
||||
// join_k merge should have at least two branch continuations tailcalling the same target.
|
||||
if tailcall_targets.len() < 2 {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/tailcall_count",
|
||||
&format!(
|
||||
"join_k tailcall form requires >=2 tailcalls, got {}",
|
||||
tailcall_targets.len()
|
||||
),
|
||||
"ensure both then/else branches tailcall join_k as the last instruction",
|
||||
));
|
||||
}
|
||||
|
||||
let first_target = tailcall_targets[0].0;
|
||||
for (target, argc) in &tailcall_targets {
|
||||
if *target != first_target {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/tailcall_target_mismatch",
|
||||
"tailcalls do not target a single join_k function",
|
||||
"ensure then/else both tailcall the same join_k function id",
|
||||
));
|
||||
}
|
||||
if *argc != expected_env_fields {
|
||||
return Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/tailcall_arg_arity_mismatch",
|
||||
&format!(
|
||||
"tailcall env arg count mismatch: expected {}, got {}",
|
||||
expected_env_fields, argc
|
||||
),
|
||||
"ensure join_k is called with the full env fields list (writes + inputs)",
|
||||
));
|
||||
}
|
||||
}
|
||||
|
||||
let join_k_func = module.functions.get(&first_target).ok_or_else(|| {
|
||||
error_tags::freeze_with_hint(
|
||||
"phase129/join_k/join_k_missing",
|
||||
"tailcall target join_k function not found in module",
|
||||
"ensure join_k is registered in JoinModule.functions",
|
||||
)
|
||||
})?;
|
||||
|
||||
match join_k_func.body.last() {
|
||||
Some(JoinInst::Ret { value: Some(_) }) => Ok(()),
|
||||
_ => Err(error_tags::freeze_with_hint(
|
||||
"phase129/join_k/join_k_not_ret",
|
||||
"join_k must end with Ret(Some(value))",
|
||||
"ensure join_k returns the merged env variable and has no post-if continuation in Phase 129-B",
|
||||
)),
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::*;
|
||||
use crate::mir::control_tree::step_tree::ExitKind;
|
||||
|
||||
fn make_contract(exits: Vec<ExitKind>, writes: Vec<&str>) -> StepTreeContract {
|
||||
StepTreeContract {
|
||||
exits: exits.into_iter().collect(),
|
||||
writes: writes.into_iter().map(String::from).collect(),
|
||||
reads: Default::default(), // Phase 124
|
||||
required_caps: Default::default(),
|
||||
cond_sig: Default::default(),
|
||||
}
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_exit_parity_match() {
|
||||
let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let c2 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let result = compare_exit_contracts(&c1, &c2);
|
||||
assert!(result.ok);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_exit_parity_mismatch() {
|
||||
let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let c2 = make_contract(vec![ExitKind::Break], vec!["x"]);
|
||||
let result = compare_exit_contracts(&c1, &c2);
|
||||
assert!(!result.ok);
|
||||
assert_eq!(result.mismatch_kind, Some(MismatchKind::ExitMismatch));
|
||||
assert!(result.hint.is_some());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_writes_parity_match() {
|
||||
let c1 = make_contract(vec![ExitKind::Return], vec!["x", "y"]);
|
||||
let c2 = make_contract(vec![ExitKind::Return], vec!["x", "y"]);
|
||||
let result = compare_writes_contracts(&c1, &c2);
|
||||
assert!(result.ok);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_writes_parity_mismatch() {
|
||||
let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let c2 = make_contract(vec![ExitKind::Return], vec!["x", "y"]);
|
||||
let result = compare_writes_contracts(&c1, &c2);
|
||||
assert!(!result.ok);
|
||||
assert_eq!(result.mismatch_kind, Some(MismatchKind::WritesMismatch));
|
||||
assert!(result.hint.is_some());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_full_parity_ok() {
|
||||
let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let c2 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let result = check_full_parity(&c1, &c2);
|
||||
assert!(result.ok);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_full_parity_exit_mismatch() {
|
||||
let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let c2 = make_contract(vec![ExitKind::Break], vec!["x"]);
|
||||
let result = check_full_parity(&c1, &c2);
|
||||
assert!(!result.ok);
|
||||
assert_eq!(result.mismatch_kind, Some(MismatchKind::ExitMismatch));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_full_parity_writes_mismatch() {
|
||||
let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let c2 = make_contract(vec![ExitKind::Return], vec!["x", "y"]);
|
||||
let result = check_full_parity(&c1, &c2);
|
||||
assert!(!result.ok);
|
||||
assert_eq!(result.mismatch_kind, Some(MismatchKind::WritesMismatch));
|
||||
}
|
||||
}
|
||||
188
src/mir/control_tree/normalized_shadow/parity_contract.rs
Normal file
188
src/mir/control_tree/normalized_shadow/parity_contract.rs
Normal file
@ -0,0 +1,188 @@
|
||||
//! Parity verification between shadow and existing router (contracts only)
|
||||
//!
|
||||
//! ## Responsibility
|
||||
//!
|
||||
//! - Compare exit/writes contracts extracted from StepTree
|
||||
//! - Do not inspect generated JoinIR; purely contract parity
|
||||
|
||||
use crate::mir::control_tree::step_tree_contract_box::StepTreeContract;
|
||||
|
||||
/// Mismatch classification
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
||||
pub enum MismatchKind {
|
||||
/// Exit contract mismatch
|
||||
ExitMismatch,
|
||||
/// Writes contract mismatch
|
||||
WritesMismatch,
|
||||
/// Unsupported kind (should not happen for if-only)
|
||||
UnsupportedKind,
|
||||
}
|
||||
|
||||
impl MismatchKind {
|
||||
/// Get human-readable description
|
||||
pub fn description(&self) -> &'static str {
|
||||
match self {
|
||||
MismatchKind::ExitMismatch => "exit contract mismatch",
|
||||
MismatchKind::WritesMismatch => "writes contract mismatch",
|
||||
MismatchKind::UnsupportedKind => "unsupported pattern for parity check",
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Result of parity check
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct ShadowParityResult {
|
||||
/// Whether parity check passed
|
||||
pub ok: bool,
|
||||
/// Mismatch kind if not ok
|
||||
pub mismatch_kind: Option<MismatchKind>,
|
||||
/// Hint for debugging (must be non-empty if not ok)
|
||||
pub hint: Option<String>,
|
||||
}
|
||||
|
||||
impl ShadowParityResult {
|
||||
/// Create successful parity result
|
||||
pub fn ok() -> Self {
|
||||
Self {
|
||||
ok: true,
|
||||
mismatch_kind: None,
|
||||
hint: None,
|
||||
}
|
||||
}
|
||||
|
||||
/// Create failed parity result with hint
|
||||
pub fn mismatch(kind: MismatchKind, hint: String) -> Self {
|
||||
assert!(!hint.is_empty(), "hint must not be empty for mismatch");
|
||||
Self {
|
||||
ok: false,
|
||||
mismatch_kind: Some(kind),
|
||||
hint: Some(hint),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Compare exit contracts between shadow and existing path
|
||||
pub fn compare_exit_contracts(
|
||||
shadow: &StepTreeContract,
|
||||
existing: &StepTreeContract,
|
||||
) -> ShadowParityResult {
|
||||
if shadow.exits != existing.exits {
|
||||
let hint = format!(
|
||||
"exit mismatch: shadow={:?}, existing={:?}",
|
||||
shadow.exits, existing.exits
|
||||
);
|
||||
return ShadowParityResult::mismatch(MismatchKind::ExitMismatch, hint);
|
||||
}
|
||||
ShadowParityResult::ok()
|
||||
}
|
||||
|
||||
/// Compare writes contracts between shadow and existing path
|
||||
pub fn compare_writes_contracts(
|
||||
shadow: &StepTreeContract,
|
||||
existing: &StepTreeContract,
|
||||
) -> ShadowParityResult {
|
||||
if shadow.writes != existing.writes {
|
||||
let hint = format!(
|
||||
"writes mismatch: shadow={:?}, existing={:?}",
|
||||
shadow.writes, existing.writes
|
||||
);
|
||||
return ShadowParityResult::mismatch(MismatchKind::WritesMismatch, hint);
|
||||
}
|
||||
ShadowParityResult::ok()
|
||||
}
|
||||
|
||||
/// Full parity check (exits + writes)
|
||||
pub fn check_full_parity(
|
||||
shadow: &StepTreeContract,
|
||||
existing: &StepTreeContract,
|
||||
) -> ShadowParityResult {
|
||||
let exit_result = compare_exit_contracts(shadow, existing);
|
||||
if !exit_result.ok {
|
||||
return exit_result;
|
||||
}
|
||||
|
||||
let writes_result = compare_writes_contracts(shadow, existing);
|
||||
if !writes_result.ok {
|
||||
return writes_result;
|
||||
}
|
||||
|
||||
ShadowParityResult::ok()
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::*;
|
||||
use crate::mir::control_tree::step_tree::ExitKind;
|
||||
|
||||
fn make_contract(exits: Vec<ExitKind>, writes: Vec<&str>) -> StepTreeContract {
|
||||
StepTreeContract {
|
||||
exits: exits.into_iter().collect(),
|
||||
writes: writes.into_iter().map(String::from).collect(),
|
||||
reads: Default::default(), // Phase 124
|
||||
required_caps: Default::default(),
|
||||
cond_sig: Default::default(),
|
||||
}
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_exit_parity_match() {
|
||||
let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let c2 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let result = compare_exit_contracts(&c1, &c2);
|
||||
assert!(result.ok);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_exit_parity_mismatch() {
|
||||
let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let c2 = make_contract(vec![ExitKind::Break], vec!["x"]);
|
||||
let result = compare_exit_contracts(&c1, &c2);
|
||||
assert!(!result.ok);
|
||||
assert_eq!(result.mismatch_kind, Some(MismatchKind::ExitMismatch));
|
||||
assert!(result.hint.is_some());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_writes_parity_match() {
|
||||
let c1 = make_contract(vec![ExitKind::Return], vec!["x", "y"]);
|
||||
let c2 = make_contract(vec![ExitKind::Return], vec!["x", "y"]);
|
||||
let result = compare_writes_contracts(&c1, &c2);
|
||||
assert!(result.ok);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_writes_parity_mismatch() {
|
||||
let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let c2 = make_contract(vec![ExitKind::Return], vec!["x", "y"]);
|
||||
let result = compare_writes_contracts(&c1, &c2);
|
||||
assert!(!result.ok);
|
||||
assert_eq!(result.mismatch_kind, Some(MismatchKind::WritesMismatch));
|
||||
assert!(result.hint.is_some());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_full_parity_ok() {
|
||||
let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let c2 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let result = check_full_parity(&c1, &c2);
|
||||
assert!(result.ok);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_full_parity_exit_mismatch() {
|
||||
let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let c2 = make_contract(vec![ExitKind::Break], vec!["x"]);
|
||||
let result = check_full_parity(&c1, &c2);
|
||||
assert!(!result.ok);
|
||||
assert_eq!(result.mismatch_kind, Some(MismatchKind::ExitMismatch));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_full_parity_writes_mismatch() {
|
||||
let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
|
||||
let c2 = make_contract(vec![ExitKind::Return], vec!["x", "y"]);
|
||||
let result = check_full_parity(&c1, &c2);
|
||||
assert!(!result.ok);
|
||||
assert_eq!(result.mismatch_kind, Some(MismatchKind::WritesMismatch));
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user