4 goals (ID 1561) Malloc_id : @eq CheriMemoryWithPNVI.storage_instance_id (CheriMemoryWithPNVI.next_alloc_id mem_state1) (CheriMemoryWithoutPNVI.next_alloc_id mem_state2) Mnextiota : @eq CheriMemoryWithPNVI.symbolic_storage_instance_id (CheriMemoryWithPNVI.next_iota mem_state1) (CheriMemoryWithoutPNVI.next_iota mem_state2) Mlastaddr : @eq AddressValue.t (CheriMemoryWithPNVI.last_address mem_state1) (CheriMemoryWithoutPNVI.last_address mem_state2) Mallocs : @ZMap.Equal allocation (CheriMemoryWithPNVI.allocations mem_state1) (CheriMemoryWithoutPNVI.allocations mem_state2) Miotas : @ZMap.Equal (sum CheriMemoryWithPNVI.storage_instance_id (prod CheriMemoryWithPNVI.storage_instance_id CheriMemoryWithPNVI.storage_instance_id)) (CheriMemoryWithPNVI.iota_map mem_state1) (CheriMemoryWithoutPNVI.iota_map mem_state2) Mfuncs : @ZMap.Equal (prod (prod digest string) Capability_GS.t) (CheriMemoryWithPNVI.funptrmap mem_state1) (CheriMemoryWithoutPNVI.funptrmap mem_state2) Mvarargs : @ZMap.Equiv (prod Z (list (prod CoqCtype.ctype pointer_value_ind))) varargs_eq (CheriMemoryWithPNVI.varargs mem_state1) (CheriMemoryWithoutPNVI.varargs mem_state2) Mnextvararg : @eq Z (CheriMemoryWithPNVI.next_varargs_id mem_state1) (CheriMemoryWithoutPNVI.next_varargs_id mem_state2) Mbytes : @ZMap.Equal AbsByte (CheriMemoryWithPNVI.bytemap mem_state1) (CheriMemoryWithoutPNVI.bytemap mem_state2) Mcapmeta : @ZMap.Equal (prod bool CapGhostState) (CheriMemoryWithPNVI.capmeta mem_state1) (CheriMemoryWithoutPNVI.capmeta mem_state2) m : CheriMemoryWithPNVI.mem_state m1 : memMError Heqp : @eq (prod CheriMemoryWithPNVI.mem_state (sum memMError CheriMemoryWithPNVI.pointer_value)) match CheriMemoryWithPNVI.allocator (Capability_GS.representable_length (CheriMemoryWithPNVI.num_of_int size_int)) (Z.max (CheriMemoryWithPNVI.num_of_int align_int) (Z.succ (AddressValue.to_Z (AddressValue.bitwise_complement (AddressValue.of_Z (Z.of_N (@MachineWord.MachineWord.word_to_N (Z.to_nat (Z.add (Z.sub (Zpos (xI (xI (xI (xI (xI xH)))))) Z0) (Zpos xH))) (@Values.get_word (Z.add (Z.sub (Zpos (xI (xI (xI (xI (xI xH)))))) Z0) (Zpos xH)) (CapFns.CapGetRepresentableMask (MachineWord.MachineWord.Z_to_word (Pos.to_nat (xO (xO (xO (xO (xO (xO xH))))))) (CheriMemoryWithPNVI.num_of_int size_int))))))))))) mem_state1 return (prod CheriMemoryWithPNVI.mem_state (sum memMError pointer_value_ind)) with | pair s' s0 => match s0 return (prod CheriMemoryWithPNVI.mem_state (sum memMError pointer_value_ind)) with | inl v => @pair CheriMemoryWithPNVI.mem_state (sum memMError pointer_value_ind) s' (@inl memMError pointer_value_ind v) | inr x => match x return (CheriMemoryWithPNVI.memM pointer_value_ind) with | pair alloc_id addr => fun s : CheriMemoryWithPNVI.mem_state => @pair CheriMemoryWithPNVI.mem_state (sum memMError pointer_value_ind) (CheriMemoryWithPNVI.Build_mem_state_r (CheriMemoryWithPNVI.next_alloc_id s) (CheriMemoryWithPNVI.next_iota s) (CheriMemoryWithPNVI.last_address s) (@ZMap.add allocation alloc_id (Build_allocation PrefMalloc addr (Capability_GS.representable_length (CheriMemoryWithPNVI.num_of_int size_int)) (@None CoqCtype.ctype) IsWritable true false Unexposed) (CheriMemoryWithPNVI.allocations s)) (CheriMemoryWithPNVI.iota_map s) (CheriMemoryWithPNVI.funptrmap s) (CheriMemoryWithPNVI.varargs s) (CheriMemoryWithPNVI.next_varargs_id s) (CheriMemoryWithPNVI.bytemap s) (CheriMemoryWithPNVI.capmeta s)) (@inr memMError pointer_value_ind (PV match is_PNVI (WithPNVISwitches.get_switches tt) return provenance with | true => Prov_some alloc_id | false => Prov_disabled end (PVconcrete (Capability_GS.alloc_cap addr (AddressValue.of_Z (Capability_GS.representable_length (CheriMemoryWithPNVI.num_of_int size_int))))))) end s' end end (@pair CheriMemoryWithPNVI.mem_state (sum memMError CheriMemoryWithPNVI.pointer_value) m (@inl memMError CheriMemoryWithPNVI.pointer_value m1)) m0 : CheriMemoryWithoutPNVI.mem_state m2 : memMError m3 : CheriMemoryWithoutPNVI.mem_state s : sum memMError (prod CheriMemoryWithoutPNVI.storage_instance_id AddressValue.t) Heqp1 : @eq (prod CheriMemoryWithoutPNVI.mem_state (sum memMError (prod CheriMemoryWithoutPNVI.storage_instance_id AddressValue.t))) (CheriMemoryWithoutPNVI.allocator (Capability_GS.representable_length (CheriMemoryWithoutPNVI.num_of_int size_int)) (Z.max (CheriMemoryWithoutPNVI.num_of_int align_int) (Z.succ (AddressValue.to_Z (AddressValue.bitwise_complement (AddressValue.of_Z (Z.of_N (@MachineWord.MachineWord.word_to_N (Z.to_nat (Z.add (Z.sub (Zpos (xI (xI (xI (xI (xI xH)))))) Z0) (Zpos xH))) (@Values.get_word (Z.add (Z.sub (Zpos (xI (xI (xI (xI (xI xH)))))) Z0) (Zpos xH)) (CapFns.CapGetRepresentableMask (MachineWord.MachineWord.Z_to_word (Pos.to_nat (xO (xO (xO (xO (xO (xO xH))))))) (CheriMemoryWithoutPNVI.num_of_int size_int))))))))))) mem_state2) (@pair CheriMemoryWithoutPNVI.mem_state (sum memMError (prod CheriMemoryWithoutPNVI.storage_instance_id AddressValue.t)) m3 s) Heqp0 : @eq (prod CheriMemoryWithoutPNVI.mem_state (sum memMError CheriMemoryWithoutPNVI.pointer_value)) match s return (prod CheriMemoryWithoutPNVI.mem_state (sum memMError pointer_value_ind)) with | inl v => @pair CheriMemoryWithoutPNVI.mem_state (sum memMError pointer_value_ind) m3 (@inl memMError pointer_value_ind v) | inr x => match x return (CheriMemoryWithoutPNVI.memM pointer_value_ind) with | pair alloc_id addr => fun s : CheriMemoryWithoutPNVI.mem_state => @pair CheriMemoryWithoutPNVI.mem_state (sum memMError pointer_value_ind) (CheriMemoryWithoutPNVI.Build_mem_state_r (CheriMemoryWithoutPNVI.next_alloc_id s) (CheriMemoryWithoutPNVI.next_iota s) (CheriMemoryWithoutPNVI.last_address s) (@ZMap.add allocation alloc_id (Build_allocation PrefMalloc addr (Capability_GS.representable_length (CheriMemoryWithoutPNVI.num_of_int size_int)) (@None CoqCtype.ctype) IsWritable true false Unexposed) (CheriMemoryWithoutPNVI.allocations s)) (CheriMemoryWithoutPNVI.iota_map s) (CheriMemoryWithoutPNVI.funptrmap s) (CheriMemoryWithoutPNVI.varargs s) (CheriMemoryWithoutPNVI.next_varargs_id s) (CheriMemoryWithoutPNVI.bytemap s) (CheriMemoryWithoutPNVI.capmeta s)) (@inr memMError pointer_value_ind (PV match is_PNVI (WithoutPNVISwitches.get_switches tt) return provenance with | true => Prov_some alloc_id | false => Prov_disabled end (PVconcrete (Capability_GS.alloc_cap addr (AddressValue.of_Z (Capability_GS.representable_length (CheriMemoryWithoutPNVI.num_of_int size_int))))))) end m3 end (@pair CheriMemoryWithoutPNVI.mem_state (sum memMError CheriMemoryWithoutPNVI.pointer_value) m0 (@inl memMError CheriMemoryWithoutPNVI.pointer_value m2)) ============================ @eq memMError m1 m2 goal 2 (ID 1547) is: False goal 3 (ID 1548) is: False goal 4 (ID 1549) is: pointer_value_eq p p0