…reg_mem, chain to_amode, add model for GprMem

…er returning unmatched types (concrete type error between types: bv 16 int)

…ix MInst.MovzxRmR to have a structure similar to MInst.ULoad8; fix spec for synthetic_amode_to_reg_mem & reg_mem_to_gpr_mem corresponding to GprMem definition; fix type issue for ext_mode; 2) identify 4 new rules - 2.1 left_shift_small: wrote vacuous spec for raw_operand_size_of_type; 2.2 store_narror; 2.3 Xor_mem_reg; 2.4 stack_add_guard

2. store_narrow: added spec for raw_operand_size_of_type; MInst.MovRM TODO
3. stack_add: got stuck on 'providing a model for StackSlot’
4. Xor_mem_reg: added model for SinkableLoad; spec for sinkable_load & MInst.AluRM TODO
5. left_shift_small: added model for Imm8Gpr; added chain for put_masked_in_imm8_gpr; spec for const_to_type_masked_imm8 TODO; x64_shl if chained, program stucks

…to be analyzed); fix type_inference.rs to print conflicts;

2. store_narrow, xor_mem_reg: not updated;
3. stack_add_guard: deleted;
4. left_shift_small: defined model for Imm8Gpr as a struct; chained put_masked_in_imm8_gpr; wrote specs for const_to_type_masked_imm8, x64_shl (*no extern, but if chained, the script cannot run), gpr_to_imm8_gpr, shift_mask; working on specs for RegMemImm.Imm.

1. load_narrow: fix MInstr.MovzxRmR; fix reg_mem_to_gpr_mem to have  to be ;
2. left_shift_small: added spec for RegMemImm.Imm; fixed put_masked_in_imm8_gpr by removing the chain and providing a spec; fixed spec for x64_shl to type-check # of bits.

…_load, RegMemImm.Mem.

README file to the CS340 final project.

…into arrival-runner

add Compound::ExtEnum to type.rs
Implemented Display and resolve for ExtEnum and unwrap as_enum() in type.rs
Extended alloc_value to allocate ExtEnum values in veri.rs
Add Symbolic::ExtEnum and Value::ExtEnum variants in veri.rs
Implemented eval and Display for ExtEnum in veri.rs
Verified compilation succeeds after these changes.

In ast.rs: added ModelType::ExtEnum and ModelValue::ExtEnumValue, and introduced ModelVariant
In types.rs: extended Compound::from_ast to lower ModelType::ExtEnum into Compound::ExtEnum
In specs.rs: added two helpers to extend collect_models to handle ExtEnum (clone base enum, lower extra fields, and insert new Compound::ExtEnum into type_model

1. in parser.rs: extend parse_model to recognize (type-ext-enum)
2. in specs.rs (minor change)

in parser.rs - extend 'parse_model' to recognize (type-ext-enum)

… problem - still facing duplicate model problem

…e has been seen

…d fix specs.rs by specifying that if a spec already exists, do not generate one for it

…d specs, still got underconstrained error

…pplicable conditions

…tions: 323 || 476 and 1643 || 1781

…if only one of z3 or cvc5 is present