zero.zok

struct State {
	field pc;
	field A;
}

struct Witness {
	field X;
	field reg_write_X_A;
	field instr_ASSERT_IS_ZERO_A;
	field X_const;
	field X_read_free;
	field read_X_A;
	field read_X_pc;
	field X_free_value;
	field first_step;
	field first_step_next;
}

def main(State s, private Witness w) -> State {
	assert((w.first_step * s.A) == 0);
	assert((w.instr_ASSERT_IS_ZERO_A * (s.A - 0)) == 0);
	assert(w.X == ((((w.read_X_A * s.A) + (w.read_X_pc * s.pc)) + w.X_const) + (w.X_read_free * w.X_free_value)));

	field A_next = (((w.first_step_next * 0) + (w.reg_write_X_A * w.X)) + ((1 - (w.first_step_next + w.reg_write_X_A)) * s.A));
	field pc_next = ((1 - w.first_step_next) * (s.pc + 1));

	return State {
		pc: pc_next,
		A: A_next,
	};
}