partially implement obj_cmp for test_get_core_state

src/ksoroban/kdist/soroban-semantics/host/context.md

@@ -7,6 +7,46 @@ module HOST-CONTEXT
     imports HOST-INTEGER
 ```
 
+## obj_cmp
+
+```k
+    rule [hostfun-obj-cmp]:
+        <instrs> hostCall ( "x" , "0" , [ i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObjectFull(HostVal(OBJ_B))
+              ~> loadObjectFull(HostVal(OBJ_A))
+              ~> objCmp
+                 ...
+        </instrs>
+        <locals>
+            0 |-> <i64> OBJ_A
+            1 |-> <i64> OBJ_B
+        </locals>
+
+    // TODO This only works for addresses. Implement it properly for other cases.
+    // https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#comparison
+    syntax InternalInstr ::= "objCmp"   [symbol(objCmp)]
+ // ----------------------------------------------------
+    rule [objCmp-equal]:
+        <instrs> objCmp => i64.const compareAddress(A, B) ... </instrs>
+        <hostStack> ScAddress(A) : ScAddress(B) : S => S </hostStack>
+
+    syntax Int ::= compareAddress(Address, Address)    [function, total, symbol(compareAddress)]
+ // -------------------------------------------------------------------------------------
+    rule compareAddress(Account(_),  Contract(_)) => -1
+    rule compareAddress(Contract(_), Account(_))  => 1
+    rule compareAddress(Contract(A), Contract(B)) => compareBytes(A, B)
+    rule compareAddress(Account(A),  Account(B))  => compareBytes(A, B)
+
+    syntax Int ::= compareBytes(Bytes, Bytes)       [function, total, symbol(compareBytes)]
+                 | compareString(String, String)    [function, total, symbol(compareString)]
+ // -------------------------------------------------------------------------------------
+    rule compareBytes(A, B) => compareString(Bytes2String(A), Bytes2String(B))
+    rule compareString(A, B) => -1 requires A  <String B
+    rule compareString(A, B) =>  0 requires A ==String B
+    rule compareString(A, B) =>  1 requires A  >String B
+
+```
+
 ## get_ledger_sequence
 
 Return the current ledger sequence number as `U32`.

src/tests/integration/data/soroban/contracts/test_fxdao/src/lib.rs

@@ -48,7 +48,7 @@ impl TestFxDAOContract {
         let client = VaultsContract::Client::new(&env, &fxdao_addr);
 
         client.calculate_deposit_ratio(&currency_rate, &collateral, &debt);
-        
+
         true
     }
 
@@ -58,13 +58,12 @@ impl TestFxDAOContract {
         let client = VaultsContract::Client::new(&env, &fxdao_addr);
 
         let core_state = client.get_core_state();
-
-        // commented out lines require the obj_cmp host function 
-        // assert_eq!(&core_state.col_token, &self_addr);
-        // assert_eq!(&core_state.oracle, &self_addr);
-        // assert_eq!(&core_state.protocol_manager, &self_addr);
-        // assert_eq!(&core_state.admin, &self_addr);
-        // assert_eq!(&core_state.stable_issuer, &self_addr);
+
+        assert_eq!(&core_state.col_token, &self_addr);
+        assert_eq!(&core_state.oracle, &self_addr);
+        assert_eq!(&core_state.protocol_manager, &self_addr);
+        assert_eq!(&core_state.admin, &self_addr);
+        assert_eq!(&core_state.stable_issuer, &self_addr);
         assert_eq!(&core_state.panic_mode, &false);
         assert_eq!(&core_state.fee, &FEE);