|
| 1 | +// Merge into debug/mod.rs in v1: |
| 2 | +// - debug_constraints |
| 3 | +// - debug_constraints_and_interactions |
| 4 | +use std::sync::Arc; |
| 5 | + |
| 6 | +use itertools::{izip, Itertools}; |
| 7 | +use openvm_stark_backend::{ |
| 8 | + air_builders::{ |
| 9 | + debug::{check_constraints, check_logup, USE_DEBUG_BUILDER}, |
| 10 | + symbolic::SymbolicConstraints, |
| 11 | + }, |
| 12 | + prover::types::AirProofRawInput, |
| 13 | + AirRef, |
| 14 | +}; |
| 15 | + |
| 16 | +use crate::{ |
| 17 | + keygen::{types::StarkProvingKeyV2, MultiStarkKeygenBuilderV2}, |
| 18 | + prover::{ |
| 19 | + ColMajorMatrix, DeviceDataTransporterV2, ProverBackendV2, ProvingContextV2, |
| 20 | + StridedColMajorMatrixView, |
| 21 | + }, |
| 22 | + SystemParams, SC, |
| 23 | +}; |
| 24 | + |
| 25 | +// TODO[jpw]: move into StarkEngineV2::debug default implementation after `SC` is made generic. |
| 26 | +/// `airs` should be the full list of all AIRs, not just used AIRs. |
| 27 | +pub fn debug_impl<PB: ProverBackendV2<Val = crate::F>, PD: DeviceDataTransporterV2<PB>>( |
| 28 | + config: SystemParams, |
| 29 | + device: &PD, |
| 30 | + airs: &[AirRef<SC>], |
| 31 | + ctx: &ProvingContextV2<PB>, |
| 32 | +) { |
| 33 | + let mut keygen_builder = MultiStarkKeygenBuilderV2::new(config); |
| 34 | + for air in airs { |
| 35 | + keygen_builder.add_air(air.clone()); |
| 36 | + } |
| 37 | + let pk = keygen_builder.generate_pk().unwrap(); |
| 38 | + |
| 39 | + let transpose = |mat: ColMajorMatrix<crate::F>| { |
| 40 | + let row_major = StridedColMajorMatrixView::from(mat.as_view()).to_row_major_matrix(); |
| 41 | + Arc::new(row_major) |
| 42 | + }; |
| 43 | + let (inputs, used_airs, used_pks): (Vec<_>, Vec<_>, Vec<_>) = ctx |
| 44 | + .per_trace |
| 45 | + .iter() |
| 46 | + .map(|(air_id, air_ctx)| { |
| 47 | + // Transfer from device **back** to host so the debugger can read the data. |
| 48 | + let common_main = device.transport_matrix_from_device_to_host(&air_ctx.common_main); |
| 49 | + let cached_mains = air_ctx |
| 50 | + .cached_mains |
| 51 | + .iter() |
| 52 | + .map(|cd| transpose(device.transport_matrix_from_device_to_host(&cd.trace))) |
| 53 | + .collect_vec(); |
| 54 | + let common_main = Some(transpose(common_main)); |
| 55 | + let public_values = air_ctx.public_values.clone(); |
| 56 | + ( |
| 57 | + AirProofRawInput { |
| 58 | + cached_mains, |
| 59 | + common_main, |
| 60 | + public_values, |
| 61 | + }, |
| 62 | + airs[*air_id].clone(), |
| 63 | + &pk.per_air[*air_id], |
| 64 | + ) |
| 65 | + }) |
| 66 | + .multiunzip(); |
| 67 | + |
| 68 | + debug_constraints_and_interactions(&used_airs, &used_pks, &inputs); |
| 69 | +} |
| 70 | + |
| 71 | +/// The debugging will check the main AIR constraints and then separately check LogUp constraints by |
| 72 | +/// checking the actual multiset equalities. Currently it will not debug check any after challenge |
| 73 | +/// phase constraints for implementation simplicity. |
| 74 | +#[allow(dead_code)] |
| 75 | +#[allow(clippy::too_many_arguments)] |
| 76 | +pub fn debug_constraints_and_interactions( |
| 77 | + airs: &[AirRef<SC>], |
| 78 | + pk: &[&StarkProvingKeyV2], |
| 79 | + inputs: &[AirProofRawInput<crate::F>], |
| 80 | +) { |
| 81 | + USE_DEBUG_BUILDER.with(|debug| { |
| 82 | + if *debug.lock().unwrap() { |
| 83 | + let (main_parts_per_air, pvs_per_air): (Vec<_>, Vec<_>) = inputs |
| 84 | + .iter() |
| 85 | + .map(|input| { |
| 86 | + let mut main_parts = input |
| 87 | + .cached_mains |
| 88 | + .iter() |
| 89 | + .map(|trace| trace.as_view()) |
| 90 | + .collect_vec(); |
| 91 | + if let Some(trace) = input.common_main.as_ref() { |
| 92 | + main_parts.push(trace.as_view()); |
| 93 | + } |
| 94 | + (main_parts, input.public_values.clone()) |
| 95 | + }) |
| 96 | + .unzip(); |
| 97 | + let preprocessed = izip!(airs, pk, &main_parts_per_air, &pvs_per_air) |
| 98 | + .map(|(air, pk, main_parts, pvs)| { |
| 99 | + let preprocessed_trace = pk |
| 100 | + .preprocessed_data |
| 101 | + .as_ref() |
| 102 | + .map(|data| data.mat_view(0).to_row_major_matrix()); |
| 103 | + tracing::debug!("Checking constraints for {}", air.name()); |
| 104 | + check_constraints( |
| 105 | + air.as_ref(), |
| 106 | + &air.name(), |
| 107 | + &preprocessed_trace.as_ref().map(|t| t.as_view()), |
| 108 | + main_parts, |
| 109 | + pvs, |
| 110 | + ); |
| 111 | + preprocessed_trace |
| 112 | + }) |
| 113 | + .collect_vec(); |
| 114 | + |
| 115 | + let (air_names, interactions): (Vec<_>, Vec<_>) = pk |
| 116 | + .iter() |
| 117 | + .map(|pk| { |
| 118 | + let sym_constraints = SymbolicConstraints::from(&pk.vk.symbolic_constraints); |
| 119 | + (pk.air_name.clone(), sym_constraints.interactions) |
| 120 | + }) |
| 121 | + .unzip(); |
| 122 | + let preprocessed_views = preprocessed |
| 123 | + .iter() |
| 124 | + .map(|t| t.as_ref().map(|t| t.as_view())) |
| 125 | + .collect_vec(); |
| 126 | + check_logup( |
| 127 | + &air_names, |
| 128 | + &interactions, |
| 129 | + &preprocessed_views, |
| 130 | + &main_parts_per_air, |
| 131 | + &pvs_per_air, |
| 132 | + ); |
| 133 | + } |
| 134 | + }); |
| 135 | +} |
0 commit comments